leanprover-community · pitmonticone · Feb 28, 2024
diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean
@@ -179,7 +179,7 @@ theorem Prime.five_le_of_ne_two_of_ne_three {p : ℕ} (hp : p.Prime) (h_two : p
     (h_three : p ≠ 3) : 5 ≤ p := by
   by_contra! h
   revert h_two h_three hp
-  -- Porting note: was `decide!`
+  -- Porting note (#11043): was `decide!`
   match p with
   | 0 => decide
   | 1 => decide

diff --git a/Mathlib/Geometry/Euclidean/MongePoint.lean b/Mathlib/Geometry/Euclidean/MongePoint.lean
@@ -473,11 +473,11 @@ planes. -/
 theorem altitude_eq_mongePlane (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃)
     (h₂₃ : i₂ ≠ i₃) : t.altitude i₁ = t.mongePlane i₂ i₃ := by
   have hs : ({i₂, i₃}ᶜ : Finset (Fin 3)) = {i₁} := by
-    -- porting note: was `decide!`
+    -- Porting note (#11043): was `decide!`
     fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃
       <;> simp (config := {decide := true}) at h₁₂ h₁₃ h₂₃ ⊢
   have he : univ.erase i₁ = {i₂, i₃} := by
-    -- porting note: was `decide!`
+    -- Porting note (#11043): was `decide!`
     fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃
       <;> simp (config := {decide := true}) at h₁₂ h₁₃ h₂₃ ⊢
   rw [mongePlane_def, altitude_def, direction_affineSpan, hs, he, centroid_singleton, coe_insert,
@@ -492,7 +492,7 @@ theorem altitude_eq_mongePlane (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h
 theorem orthocenter_mem_altitude (t : Triangle ℝ P) {i₁ : Fin 3} :
     t.orthocenter ∈ t.altitude i₁ := by
   obtain ⟨i₂, i₃, h₁₂, h₂₃, h₁₃⟩ : ∃ i₂ i₃, i₁ ≠ i₂ ∧ i₂ ≠ i₃ ∧ i₁ ≠ i₃ := by
-    -- porting note: was `decide!`
+    -- Porting note (#11043): was `decide!`
     fin_cases i₁ <;> decide
   rw [orthocenter_eq_mongePoint, t.altitude_eq_mongePlane h₁₂ h₁₃ h₂₃]
   exact t.mongePoint_mem_mongePlane
@@ -504,7 +504,7 @@ theorem eq_orthocenter_of_forall_mem_altitude {t : Triangle ℝ P} {i₁ i₂ :
     (h₁₂ : i₁ ≠ i₂) (h₁ : p ∈ t.altitude i₁) (h₂ : p ∈ t.altitude i₂) : p = t.orthocenter := by
   obtain ⟨i₃, h₂₃, h₁₃⟩ : ∃ i₃, i₂ ≠ i₃ ∧ i₁ ≠ i₃ := by
     clear h₁ h₂
-    -- porting note: was `decide!`
+    -- Porting note (#11043): was `decide!`
     fin_cases i₁ <;> fin_cases i₂ <;> decide
   rw [t.altitude_eq_mongePlane h₁₃ h₁₂ h₂₃.symm] at h₁
   rw [t.altitude_eq_mongePlane h₂₃ h₁₂.symm h₁₃.symm] at h₂
@@ -513,7 +513,7 @@ theorem eq_orthocenter_of_forall_mem_altitude {t : Triangle ℝ P} {i₁ i₂ :
     intro i hi
     have hi₁₂ : i₁ = i ∨ i₂ = i := by
       clear h₁ h₂
-      -- porting note: was `decide!`
+      -- Porting note (#11043): was `decide!`
       fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ <;> fin_cases i <;> simp at h₁₂ h₁₃ h₂₃ hi ⊢
     cases' hi₁₂ with hi₁₂ hi₁₂
     · exact hi₁₂ ▸ h₂
@@ -536,7 +536,7 @@ theorem dist_orthocenter_reflection_circumcenter (t : Triangle ℝ P) {i₁ i₂
   have hu : ({i₁, i₂} : Finset (Fin 3)) ⊆ univ := subset_univ _
   obtain ⟨i₃, hi₃, hi₃₁, hi₃₂⟩ :
       ∃ i₃, univ \ ({i₁, i₂} : Finset (Fin 3)) = {i₃} ∧ i₃ ≠ i₁ ∧ i₃ ≠ i₂ := by
-    -- porting note: was `decide!`
+    -- Porting note (#11043): was `decide!`
     fin_cases i₁ <;> fin_cases i₂ <;> simp at h <;> decide
   -- Porting note: Original proof was `simp_rw [← sum_sdiff hu, hi₃]; simp [hi₃₁, hi₃₂]; norm_num`
   rw [← sum_sdiff hu, ← sum_sdiff hu, hi₃, sum_singleton, ← sum_sdiff hu, hi₃]
@@ -590,7 +590,7 @@ theorem altitude_replace_orthocenter_eq_affineSpan {t₁ t₂ : Triangle ℝ P}
     refine' eq_of_le_of_finrank_eq (direction_le (spanPoints_subset_coe_of_subset_coe _)) _
     · have hu : (Finset.univ : Finset (Fin 3)) = {j₁, j₂, j₃} := by
         clear h₁ h₂ h₃
-        -- porting note: was `decide!`
+        -- Porting note (#11043): was `decide!`
         fin_cases j₁ <;> fin_cases j₂ <;> fin_cases j₃
           <;> simp (config := {decide := true}) at hj₁₂ hj₁₃ hj₂₃ ⊢
       rw [← Set.image_univ, ← Finset.coe_univ, hu, Finset.coe_insert, Finset.coe_insert,
@@ -606,7 +606,7 @@ theorem altitude_replace_orthocenter_eq_affineSpan {t₁ t₂ : Triangle ℝ P}
   use mem_affineSpan ℝ (Set.mem_range_self _)
   have hu : Finset.univ.erase j₂ = {j₁, j₃} := by
     clear h₁ h₂ h₃
-    -- porting note: was `decide!`
+    -- Porting note (#11043): was `decide!`
     fin_cases j₁ <;> fin_cases j₂ <;> fin_cases j₃
       <;> simp (config := {decide := true}) at hj₁₂ hj₁₃ hj₂₃ ⊢
   rw [hu, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_singleton, h₁, h₃]
@@ -615,7 +615,7 @@ theorem altitude_replace_orthocenter_eq_affineSpan {t₁ t₂ : Triangle ℝ P}
   refine' hle ((t₁.vectorSpan_isOrtho_altitude_direction i₃) _)
   have hui : Finset.univ.erase i₃ = {i₁, i₂} := by
     clear hle h₂ h₃
-    -- porting note: was `decide!`
+    -- Porting note (#11043): was `decide!`
     fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃
       <;> simp (config := {decide := true}) at hi₁₂ hi₁₃ hi₂₃ ⊢
   rw [hui, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_singleton]
@@ -787,7 +787,7 @@ theorem OrthocentricSystem.eq_insert_orthocenter {s : Set P} (ho : OrthocentricS
   · obtain ⟨j₁, hj₁₂, hj₁₃, hj₁₂₃⟩ :
         ∃ j₁ : Fin 3, j₁ ≠ j₂ ∧ j₁ ≠ j₃ ∧ ∀ j : Fin 3, j = j₁ ∨ j = j₂ ∨ j = j₃ := by
       clear h₂ h₃
-      -- porting note: was `decide!`
+      -- Porting note (#11043): was `decide!`
       fin_cases j₂ <;> fin_cases j₃ <;> simp (config := {decide := true}) at hj₂₃ ⊢
     suffices h : t₀.points j₁ = t.orthocenter by
       have hui : (Set.univ : Set (Fin 3)) = {i₁, i₂, i₃} := by ext x; simpa using h₁₂₃ x

diff --git a/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/GaussSum.lean b/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/GaussSum.lean
@@ -58,7 +58,7 @@ theorem FiniteField.isSquare_two_iff :
     have h₁ := Nat.mod_lt (Fintype.card F) (by decide : 0 < 8)
     revert h₁ h
     generalize Fintype.card F % 8 = n
-    intros; interval_cases n <;> simp_all -- Porting note: was `decide!`
+    intros; interval_cases n <;> simp_all -- Porting note (#11043): was `decide!`
 #align finite_field.is_square_two_iff FiniteField.isSquare_two_iff
 
 /-- The value of the quadratic character at `-2` -/
@@ -88,7 +88,7 @@ theorem FiniteField.isSquare_neg_two_iff :
     have h₁ := Nat.mod_lt (Fintype.card F) (by decide : 0 < 8)
     revert h₁ h
     generalize Fintype.card F % 8 = n
-    intros; interval_cases n <;> simp_all -- Porting note: was `decide!`
+    intros; interval_cases n <;> simp_all -- Porting note (#11043): was `decide!`
 #align finite_field.is_square_neg_two_iff FiniteField.isSquare_neg_two_iff
 
 /-- The relation between the values of the quadratic character of one field `F` at the

diff --git a/Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean b/Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean
@@ -82,7 +82,7 @@ theorem exists_sq_eq_two_iff : IsSquare (2 : ZMod p) ↔ p % 8 = 1 ∨ p % 8 = 7
   have h₂ := mod_lt p (by norm_num : 0 < 8)
   revert h₂ h₁
   generalize p % 8 = m; clear! p
-  intros; interval_cases m <;> simp_all -- Porting note: was `decide!`
+  intros; interval_cases m <;> simp_all -- Porting note (#11043): was `decide!`
 #align zmod.exists_sq_eq_two_iff ZMod.exists_sq_eq_two_iff
 
 /-- `-2` is a square modulo an odd prime `p` iff `p` is congruent to `1` or `3` mod `8`. -/
@@ -93,7 +93,7 @@ theorem exists_sq_eq_neg_two_iff : IsSquare (-2 : ZMod p) ↔ p % 8 = 1 ∨ p %
   have h₂ := mod_lt p (by norm_num : 0 < 8)
   revert h₂ h₁
   generalize p % 8 = m; clear! p
-  intros; interval_cases m <;> simp_all -- Porting note: was `decide!`
+  intros; interval_cases m <;> simp_all -- Porting note (#11043): was `decide!`
 #align zmod.exists_sq_eq_neg_two_iff ZMod.exists_sq_eq_neg_two_iff
 
 end ZMod

diff --git a/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean b/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
@@ -47,7 +47,7 @@ def χ₄ : MulChar (ZMod 4) ℤ where
 /-- `χ₄` takes values in `{0, 1, -1}` -/
 theorem isQuadratic_χ₄ : χ₄.IsQuadratic := by
   intro a
-  -- Porting note: was `decide!`
+  -- Porting note (#11043): was `decide!`
   fin_cases a
   all_goals decide
 #align zmod.is_quadratic_χ₄ ZMod.isQuadratic_χ₄

diff --git a/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean b/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean
@@ -46,7 +46,7 @@ theorem mod_four_eq_three_of_nat_prime_of_prime (p : ℕ) [hp : Fact p.Prime]
         have := Nat.mod_lt p (show 0 < 4 by decide)
         revert this hp3 hp1
         generalize p % 4 = m
-        intros; interval_cases m <;> simp_all -- Porting note: was `decide!`
+        intros; interval_cases m <;> simp_all -- Porting note (#11043): was `decide!`
       let ⟨k, hk⟩ := (ZMod.exists_sq_eq_neg_one_iff (p := p)).2 <| by rw [hp41]; decide
       obtain ⟨k, k_lt_p, rfl⟩ : ∃ (k' : ℕ) (_ : k' < p), (k' : ZMod p) = k := by
         exact ⟨k.val, k.val_lt, ZMod.nat_cast_zmod_val k⟩