From 51807364378ff94fb5541ecfcb321e7aae516f64 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 19 Jun 2023 05:31:19 +0000 Subject: [PATCH] chore: cleanup a `change at` porting note (#5243) Co-authored-by: Scott Morrison --- Mathlib/Algebra/Order/AbsoluteValue.lean | 3 --- Mathlib/LinearAlgebra/Basis.lean | 4 +--- Mathlib/NumberTheory/Padics/PadicNumbers.lean | 3 ++- 3 files changed, 3 insertions(+), 7 deletions(-) diff --git a/Mathlib/Algebra/Order/AbsoluteValue.lean b/Mathlib/Algebra/Order/AbsoluteValue.lean index afe08d1e3c6e4..24b7d3189aa77 100644 --- a/Mathlib/Algebra/Order/AbsoluteValue.lean +++ b/Mathlib/Algebra/Order/AbsoluteValue.lean @@ -16,9 +16,6 @@ import Mathlib.Algebra.Ring.Regular /-! # Absolute values -> THIS FILE IS SYNCHRONIZED WITH MATHLIB4. -> Any changes to this file require a corresponding PR to mathlib4. - This file defines a bundled type of absolute values `AbsoluteValue R S`. ## Main definitions diff --git a/Mathlib/LinearAlgebra/Basis.lean b/Mathlib/LinearAlgebra/Basis.lean index 59ab1757a8882..7d7a90c006a9d 100644 --- a/Mathlib/LinearAlgebra/Basis.lean +++ b/Mathlib/LinearAlgebra/Basis.lean @@ -1103,9 +1103,7 @@ theorem maximal [Nontrivial R] (b : Basis ι R M) : b.linearIndependent.Maximal ⟨fun i => ⟨b i, h ⟨i, rfl⟩⟩, fun i i' r => b.injective (by simpa only [Subtype.mk_eq_mk] using r)⟩ simp_rw [Finsupp.total_apply] at e - -- Porting note: `change at` doesn't work - replace e : ((b.repr x).sum fun (i : ι) (a : R) ↦ a • (u i : M)) = - ((⟨x, p⟩ : w) : M) := e + change ((b.repr x).sum fun (i : ι) (a : R) ↦ a • (u i : M)) = ((⟨x, p⟩ : w) : M) at e rw [← Finsupp.sum_embDomain (f := u) (g := fun x r ↦ r • (x : M)), ← Finsupp.total_apply] at e -- Now we can contradict the linear independence of `hi` refine' hi.total_ne_of_not_mem_support _ _ e diff --git a/Mathlib/NumberTheory/Padics/PadicNumbers.lean b/Mathlib/NumberTheory/Padics/PadicNumbers.lean index 0308cb360f1ce..73c65de702781 100644 --- a/Mathlib/NumberTheory/Padics/PadicNumbers.lean +++ b/Mathlib/NumberTheory/Padics/PadicNumbers.lean @@ -663,7 +663,8 @@ theorem rat_dense' (q : ℚ_[p]) {ε : ℚ} (hε : 0 < ε) : ∃ r : ℚ, padicN let ⟨N, hN⟩ := this ⟨q' N, by dsimp [padicNormE] - -- Porting note: `change` → `convert_to` and `PadicSeq p` type annotation + -- Porting note: `change` → `convert_to` (`change` times out!) + -- and add `PadicSeq p` type annotation convert_to PadicSeq.norm (q' - const _ (q' N) : PadicSeq p) < ε cases' Decidable.em (q' - const (padicNorm p) (q' N) ≈ 0) with heq hne' · simpa only [heq, PadicSeq.norm, dif_pos]