From cf70dec4d9dbd090fe72c8244373c88f1c86c653 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 29 Oct 2024 14:36:06 +0000 Subject: [PATCH] chore: cleanup a few porting notes (#18380) --- Mathlib/Algebra/Expr.lean | 2 -- Mathlib/Algebra/Free.lean | 1 - Mathlib/Algebra/GeomSum.lean | 3 --- Mathlib/Algebra/Group/Int.lean | 5 +---- 4 files changed, 1 insertion(+), 10 deletions(-) diff --git a/Mathlib/Algebra/Expr.lean b/Mathlib/Algebra/Expr.lean index 73a6d49606b8e..df4e9330035a2 100644 --- a/Mathlib/Algebra/Expr.lean +++ b/Mathlib/Algebra/Expr.lean @@ -9,8 +9,6 @@ import Qq /-! # Helpers to invoke functions involving algebra at tactic time This file provides instances on `x y : Q($α)` such that `x + y = q($x + $y)`. - -Porting note: This has been rewritten to use `Qq` instead of `Expr`. -/ open Qq diff --git a/Mathlib/Algebra/Free.lean b/Mathlib/Algebra/Free.lean index d7c8967bbf9a0..78cdb51b06d87 100644 --- a/Mathlib/Algebra/Free.lean +++ b/Mathlib/Algebra/Free.lean @@ -260,7 +260,6 @@ end Category end FreeMagma --- Porting note: changed String to Lean.Format #adaptation_note /-- around nightly-2024-02-25, we need to write `mul x y` in the second pattern, instead of `x * y`. -/ /-- Representation of an element of a free magma. -/ diff --git a/Mathlib/Algebra/GeomSum.lean b/Mathlib/Algebra/GeomSum.lean index 02480271a1392..3cbed430844f5 100644 --- a/Mathlib/Algebra/GeomSum.lean +++ b/Mathlib/Algebra/GeomSum.lean @@ -31,8 +31,6 @@ which `x` and `y` commute. Even versions not using division or subtraction, vali are recorded. -/ --- Porting note: corrected type in the description of `geom_sum₂_Ico` (in the doc string only). - universe u variable {α : Type u} @@ -72,7 +70,6 @@ theorem one_geom_sum (n : ℕ) : ∑ i ∈ range n, (1 : α) ^ i = n := by simp theorem op_geom_sum (x : α) (n : ℕ) : op (∑ i ∈ range n, x ^ i) = ∑ i ∈ range n, op x ^ i := by simp --- Porting note: linter suggested to change left hand side @[simp] theorem op_geom_sum₂ (x y : α) (n : ℕ) : ∑ i ∈ range n, op y ^ (n - 1 - i) * op x ^ i = ∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i) := by diff --git a/Mathlib/Algebra/Group/Int.lean b/Mathlib/Algebra/Group/Int.lean index 7748ade5f0533..d0d47342d4add 100644 --- a/Mathlib/Algebra/Group/Int.lean +++ b/Mathlib/Algebra/Group/Int.lean @@ -146,13 +146,10 @@ lemma ofNat_isUnit {n : ℕ} : IsUnit (n : ℤ) ↔ IsUnit n := by simp [isUnit_ lemma isUnit_mul_self (hu : IsUnit u) : u * u = 1 := (isUnit_eq_one_or hu).elim (fun h ↦ h.symm ▸ rfl) fun h ↦ h.symm ▸ rfl --- Porting note: this was proven in mathlib3 with `tidy` which hasn't been ported yet lemma isUnit_add_isUnit_eq_isUnit_add_isUnit {a b c d : ℤ} (ha : IsUnit a) (hb : IsUnit b) (hc : IsUnit c) (hd : IsUnit d) : a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c := by rw [isUnit_iff] at ha hb hc hd - cases ha <;> cases hb <;> cases hc <;> cases hd <;> - subst a <;> subst b <;> subst c <;> subst d <;> - simp (config := {decide := true}) + aesop lemma eq_one_or_neg_one_of_mul_eq_neg_one (h : u * v = -1) : u = 1 ∨ u = -1 := Or.elim (eq_one_or_neg_one_of_mul_eq_neg_one' h) (fun H => Or.inl H.1) fun H => Or.inr H.1