From 90590d5e079c6831f84df45d3108d3e443b1a73f Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Tue, 31 Oct 2023 11:08:55 +0100 Subject: [PATCH 1/4] chore: clear some porting notes on rfl We remove some porting notes for `rfl`s that by now work again. --- Mathlib/Algebra/DirectLimit.lean | 3 +-- Mathlib/Algebra/Lie/Submodule.lean | 3 +-- Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean | 4 ++-- Mathlib/Data/Finsupp/AList.lean | 10 ++++------ Mathlib/Data/Polynomial/Basic.lean | 3 +-- Mathlib/RingTheory/WittVector/Isocrystal.lean | 6 +----- 6 files changed, 10 insertions(+), 19 deletions(-) diff --git a/Mathlib/Algebra/DirectLimit.lean b/Mathlib/Algebra/DirectLimit.lean index afd41080e5552..6e62ea3518c24 100644 --- a/Mathlib/Algebra/DirectLimit.lean +++ b/Mathlib/Algebra/DirectLimit.lean @@ -128,8 +128,7 @@ theorem exists_of [Nonempty ι] [IsDirected ι (· ≤ ·)] (z : DirectLimit G f let ⟨k, hik, hjk⟩ := exists_ge_ge i j ⟨k, f i k hik x + f j k hjk y, by rw [LinearMap.map_add, of_f, of_f, ihx, ihy] - -- porting note: was `rfl` - simp only [Submodule.Quotient.mk''_eq_mk, Quotient.mk_add]⟩ + rfl ⟩ #align module.direct_limit.exists_of Module.DirectLimit.exists_of @[elab_as_elim] diff --git a/Mathlib/Algebra/Lie/Submodule.lean b/Mathlib/Algebra/Lie/Submodule.lean index 2f836528f6afd..0723e225aabb4 100644 --- a/Mathlib/Algebra/Lie/Submodule.lean +++ b/Mathlib/Algebra/Lie/Submodule.lean @@ -320,8 +320,7 @@ theorem exists_lieIdeal_coe_eq_iff : (∃ I : LieIdeal R L, ↑I = K) ↔ ∀ x y : L, y ∈ K → ⁅x, y⁆ ∈ K := by simp only [← coe_to_submodule_eq_iff, LieIdeal.coe_to_lieSubalgebra_to_submodule, Submodule.exists_lieSubmodule_coe_eq_iff L] - -- Porting note: was `exact Iff.rfl` - simp only [mem_coe_submodule] + exact Iff.rfl #align lie_subalgebra.exists_lie_ideal_coe_eq_iff LieSubalgebra.exists_lieIdeal_coe_eq_iff theorem exists_nested_lieIdeal_coe_eq_iff {K' : LieSubalgebra R L} (h : K ≤ K') : diff --git a/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean b/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean index c39d379d10a77..3136f0fea5b3c 100644 --- a/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean +++ b/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean @@ -67,8 +67,8 @@ theorem incMatrix_apply [Zero R] [One R] {a : α} {e : Sym2 α} : /-- Entries of the incidence matrix can be computed given additional decidable instances. -/ theorem incMatrix_apply' [Zero R] [One R] [DecidableEq α] [DecidableRel G.Adj] {a : α} {e : Sym2 α} : G.incMatrix R a e = if e ∈ G.incidenceSet a then 1 else 0 := by - unfold incMatrix Set.indicator -- Porting note: was `convert rfl` - simp only [Pi.one_apply] + unfold incMatrix Set.indicator + convert rfl #align simple_graph.inc_matrix_apply' SimpleGraph.incMatrix_apply' section MulZeroOneClass diff --git a/Mathlib/Data/Finsupp/AList.lean b/Mathlib/Data/Finsupp/AList.lean index e82a8b6a4aa77..98ed6de508117 100644 --- a/Mathlib/Data/Finsupp/AList.lean +++ b/Mathlib/Data/Finsupp/AList.lean @@ -76,17 +76,15 @@ noncomputable def lookupFinsupp (l : AList fun _x : α => M) : α →₀ M @[simp] theorem lookupFinsupp_apply [DecidableEq α] (l : AList fun _x : α => M) (a : α) : l.lookupFinsupp a = (l.lookup a).getD 0 := by - -- porting note: was `convert rfl` - simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]; congr + convert rfl; congr #align alist.lookup_finsupp_apply AList.lookupFinsupp_apply @[simp] theorem lookupFinsupp_support [DecidableEq α] [DecidableEq M] (l : AList fun _x : α => M) : l.lookupFinsupp.support = (l.1.filter fun x => Sigma.snd x ≠ 0).keys.toFinset := by - -- porting note: was `convert rfl` - simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]; congr - · apply Subsingleton.elim - · funext; congr + convert rfl; congr + · apply Subsingleton.elim + · funext; congr #align alist.lookup_finsupp_support AList.lookupFinsupp_support theorem lookupFinsupp_eq_iff_of_ne_zero [DecidableEq α] {l : AList fun _x : α => M} {a : α} {x : M} diff --git a/Mathlib/Data/Polynomial/Basic.lean b/Mathlib/Data/Polynomial/Basic.lean index 41bd31f88f57c..f59e338279c75 100644 --- a/Mathlib/Data/Polynomial/Basic.lean +++ b/Mathlib/Data/Polynomial/Basic.lean @@ -1082,8 +1082,7 @@ theorem coeff_erase (p : R[X]) (n i : ℕ) : (p.erase n).coeff i = if i = n then 0 else p.coeff i := by rcases p with ⟨⟩ simp only [erase_def, coeff] - -- Porting note: Was `convert rfl`. - exact ite_congr rfl (fun _ => rfl) (fun _ => rfl) + convert rfl #align polynomial.coeff_erase Polynomial.coeff_erase @[simp] diff --git a/Mathlib/RingTheory/WittVector/Isocrystal.lean b/Mathlib/RingTheory/WittVector/Isocrystal.lean index a66974445c4db..06dc661aff52f 100644 --- a/Mathlib/RingTheory/WittVector/Isocrystal.lean +++ b/Mathlib/RingTheory/WittVector/Isocrystal.lean @@ -197,11 +197,7 @@ instance (m : ℤ) : Isocrystal p k (StandardOneDimIsocrystal p k m) where @[simp] theorem StandardOneDimIsocrystal.frobenius_apply (m : ℤ) (x : StandardOneDimIsocrystal p k m) : - Φ(p, k) x = (p : K(p, k)) ^ m • φ(p, k) x := by - -- Porting note: was just `rfl` - erw [smul_eq_mul] - simp only [map_zpow₀, map_natCast] - rfl + Φ(p, k) x = (p : K(p, k)) ^ m • φ(p, k) x := rfl #align witt_vector.standard_one_dim_isocrystal.frobenius_apply WittVector.StandardOneDimIsocrystal.frobenius_apply end PerfectRing From 2e9f1604b771c647135e91ad0facac1e77a4bb37 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Tue, 31 Oct 2023 14:20:34 +0100 Subject: [PATCH 2/4] fix --- Mathlib/Data/Polynomial/Basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Data/Polynomial/Basic.lean b/Mathlib/Data/Polynomial/Basic.lean index f59e338279c75..41bd31f88f57c 100644 --- a/Mathlib/Data/Polynomial/Basic.lean +++ b/Mathlib/Data/Polynomial/Basic.lean @@ -1082,7 +1082,8 @@ theorem coeff_erase (p : R[X]) (n i : ℕ) : (p.erase n).coeff i = if i = n then 0 else p.coeff i := by rcases p with ⟨⟩ simp only [erase_def, coeff] - convert rfl + -- Porting note: Was `convert rfl`. + exact ite_congr rfl (fun _ => rfl) (fun _ => rfl) #align polynomial.coeff_erase Polynomial.coeff_erase @[simp] From 40fdcf5708202dab7a2811e3c1867ba38ac69257 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Tue, 31 Oct 2023 14:40:11 +0100 Subject: [PATCH 3/4] one more --- Mathlib/Logic/Hydra.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Mathlib/Logic/Hydra.lean b/Mathlib/Logic/Hydra.lean index c0cb9ad258153..9130d740a1e83 100644 --- a/Mathlib/Logic/Hydra.lean +++ b/Mathlib/Logic/Hydra.lean @@ -110,10 +110,7 @@ theorem cutExpand_fibration (r : α → α → Prop) : Fibration (GameAdd (CutExpand r) (CutExpand r)) (CutExpand r) fun s ↦ s.1 + s.2 := by rintro ⟨s₁, s₂⟩ s ⟨t, a, hr, he⟩; dsimp at he ⊢ classical - -- Porting note: Originally `obtain ⟨ha, rfl⟩` - -- This is https://github.com/leanprover/std4/issues/62 - obtain ⟨ha, hb⟩ := add_singleton_eq_iff.1 he - rw [hb] + obtain ⟨ha, rfl⟩ := add_singleton_eq_iff.1 he rw [add_assoc, mem_add] at ha obtain h | h := ha · refine' ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, _⟩, _⟩ From aead19dd400fb94ce1dd878ec55b470e22ac23ff Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Tue, 31 Oct 2023 15:07:27 +0100 Subject: [PATCH 4/4] more std4 issue 62 removal --- Mathlib/Algebra/Order/Ring/Defs.lean | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/Mathlib/Algebra/Order/Ring/Defs.lean b/Mathlib/Algebra/Order/Ring/Defs.lean index ba1d48dbb013e..99cc43176c4fc 100644 --- a/Mathlib/Algebra/Order/Ring/Defs.lean +++ b/Mathlib/Algebra/Order/Ring/Defs.lean @@ -800,12 +800,9 @@ theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg (hab : 0 ≤ a * b) 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 := by refine' Decidable.or_iff_not_and_not.2 _ simp only [not_and, not_le]; intro ab nab; apply not_lt_of_le hab _ - -- Porting note: for the middle case, we used to have `rfl`, but it is now rejected. - -- https://github.com/leanprover/std4/issues/62 - rcases lt_trichotomy 0 a with (ha | ha | ha) + rcases lt_trichotomy 0 a with (ha | rfl | ha) · exact mul_neg_of_pos_of_neg ha (ab ha.le) - · subst ha - exact ((ab le_rfl).asymm (nab le_rfl)).elim + · exact ((ab le_rfl).asymm (nab le_rfl)).elim · exact mul_neg_of_neg_of_pos ha (nab ha.le) #align nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nnonneg nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg @@ -835,11 +832,8 @@ theorem nonpos_of_mul_nonpos_right (h : a * b ≤ 0) (ha : 0 < a) : b ≤ 0 := @[simp] theorem zero_le_mul_left (h : 0 < c) : 0 ≤ c * b ↔ 0 ≤ b := by - -- Porting note: this used to be by: - -- convert mul_le_mul_left h - -- simp - -- but the `convert` no longer works. - simpa using (mul_le_mul_left h : c * 0 ≤ c * b ↔ 0 ≤ b) + convert mul_le_mul_left h + simp #align zero_le_mul_left zero_le_mul_left @[simp]