feat: patch for new alias command (#6172)

Mathlib.lean

@@ -2959,7 +2959,6 @@ import Mathlib.SetTheory.ZFC.Basic
 import Mathlib.SetTheory.ZFC.Ordinal
 import Mathlib.Tactic
 import Mathlib.Tactic.Abel
-import Mathlib.Tactic.Alias
 import Mathlib.Tactic.ApplyCongr
 import Mathlib.Tactic.ApplyFun
 import Mathlib.Tactic.ApplyWith

Mathlib/Algebra/Divisibility/Basic.lean

@@ -48,7 +48,7 @@ theorem Dvd.intro (c : α) (h : a * c = b) : a ∣ b :=
   Exists.intro c h.symm
 #align dvd.intro Dvd.intro
 
-alias Dvd.intro ← dvd_of_mul_right_eq
+alias dvd_of_mul_right_eq := Dvd.intro
 #align dvd_of_mul_right_eq dvd_of_mul_right_eq
 
 theorem exists_eq_mul_right_of_dvd (h : a ∣ b) : ∃ c, b = a * c :=
@@ -58,7 +58,7 @@ theorem exists_eq_mul_right_of_dvd (h : a ∣ b) : ∃ c, b = a * c :=
 theorem dvd_def : a ∣ b ↔ ∃ c, b = a * c :=
   Iff.rfl
 
-alias dvd_def ← dvd_iff_exists_eq_mul_right
+alias dvd_iff_exists_eq_mul_right := dvd_def
 
 theorem Dvd.elim {P : Prop} {a b : α} (H₁ : a ∣ b) (H₂ : ∀ c, b = a * c → P) : P :=
   Exists.elim H₁ H₂
@@ -71,7 +71,7 @@ theorem dvd_trans : a ∣ b → b ∣ c → a ∣ c
   | ⟨d, h₁⟩, ⟨e, h₂⟩ => ⟨d * e, h₁ ▸ h₂.trans <| mul_assoc a d e⟩
 #align dvd_trans dvd_trans
 
-alias dvd_trans ← Dvd.dvd.trans
+alias Dvd.dvd.trans := dvd_trans
 
 /-- Transitivity of `|` for use in `calc` blocks. -/
 instance : IsTrans α Dvd.dvd :=
@@ -86,7 +86,7 @@ theorem dvd_mul_of_dvd_left (h : a ∣ b) (c : α) : a ∣ b * c :=
   h.trans (dvd_mul_right b c)
 #align dvd_mul_of_dvd_left dvd_mul_of_dvd_left
 
-alias dvd_mul_of_dvd_left ← Dvd.dvd.mul_right
+alias Dvd.dvd.mul_right := dvd_mul_of_dvd_left
 
 theorem dvd_of_mul_right_dvd (h : a * b ∣ c) : a ∣ c :=
   (dvd_mul_right a b).trans h
@@ -134,7 +134,7 @@ theorem one_dvd (a : α) : 1 ∣ a :=
 theorem dvd_of_eq (h : a = b) : a ∣ b := by rw [h]
 #align dvd_of_eq dvd_of_eq
 
-alias dvd_of_eq ← Eq.dvd
+alias Eq.dvd := dvd_of_eq
 #align eq.dvd Eq.dvd
 
 end Monoid
@@ -147,7 +147,7 @@ theorem Dvd.intro_left (c : α) (h : c * a = b) : a ∣ b :=
   Dvd.intro _ (by rw [mul_comm] at h; apply h)
 #align dvd.intro_left Dvd.intro_left
 
-alias Dvd.intro_left ← dvd_of_mul_left_eq
+alias dvd_of_mul_left_eq := Dvd.intro_left
 #align dvd_of_mul_left_eq dvd_of_mul_left_eq
 
 theorem exists_eq_mul_left_of_dvd (h : a ∣ b) : ∃ c, b = c * a :=
@@ -173,7 +173,7 @@ theorem dvd_mul_of_dvd_right (h : a ∣ b) (c : α) : a ∣ c * b := by
   rw [mul_comm]; exact h.mul_right _
 #align dvd_mul_of_dvd_right dvd_mul_of_dvd_right
 
-alias dvd_mul_of_dvd_right ← Dvd.dvd.mul_left
+alias Dvd.dvd.mul_left := dvd_mul_of_dvd_right
 
 attribute [local simp] mul_assoc mul_comm mul_left_comm
 

Mathlib/Algebra/Group/Basic.lean

@@ -814,10 +814,10 @@ theorem div_eq_one : a / b = 1 ↔ a = b :=
 #align div_eq_one div_eq_one
 #align sub_eq_zero sub_eq_zero
 
-alias div_eq_one ↔ _ div_eq_one_of_eq
+alias ⟨_, div_eq_one_of_eq⟩ := div_eq_one
 #align div_eq_one_of_eq div_eq_one_of_eq
 
-alias sub_eq_zero ↔ _ sub_eq_zero_of_eq
+alias ⟨_, sub_eq_zero_of_eq⟩ := sub_eq_zero
 #align sub_eq_zero_of_eq sub_eq_zero_of_eq
 
 @[to_additive]

Mathlib/Algebra/Group/Defs.lean

@@ -979,7 +979,7 @@ theorem div_eq_mul_inv (a b : G) : a / b = a * b⁻¹ :=
 #align div_eq_mul_inv div_eq_mul_inv
 #align sub_eq_add_neg sub_eq_add_neg
 
-alias div_eq_mul_inv ← division_def
+alias division_def := div_eq_mul_inv
 #align division_def division_def
 
 end DivInvMonoid

Mathlib/Algebra/GroupPower/Basic.lean

@@ -103,7 +103,7 @@ theorem pow_two (a : M) : a ^ 2 = a * a := by rw [pow_succ, pow_one]
 #align pow_two pow_two
 #align two_nsmul two_nsmul
 
-alias pow_two ← sq
+alias sq := pow_two
 #align sq sq
 
 @[to_additive three'_nsmul]
@@ -237,7 +237,7 @@ theorem dvd_pow {x y : M} (hxy : x ∣ y) : ∀ {n : ℕ} (_ : n ≠ 0), x ∣ y
     exact hxy.mul_right _
 #align dvd_pow dvd_pow
 
-alias dvd_pow ← Dvd.dvd.pow
+alias Dvd.dvd.pow := dvd_pow
 
 theorem dvd_pow_self (a : M) {n : ℕ} (hn : n ≠ 0) : a ∣ a ^ n :=
   dvd_rfl.pow hn

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -771,7 +771,7 @@ namespace Int
 lemma natAbs_sq (x : ℤ) : (x.natAbs : ℤ) ^ 2 = x ^ 2 := by rw [sq, Int.natAbs_mul_self', sq]
 #align int.nat_abs_sq Int.natAbs_sq
 
-alias natAbs_sq ← natAbs_pow_two
+alias natAbs_pow_two := natAbs_sq
 #align int.nat_abs_pow_two Int.natAbs_pow_two
 
 theorem natAbs_le_self_sq (a : ℤ) : (Int.natAbs a : ℤ) ≤ a ^ 2 := by
@@ -780,13 +780,13 @@ theorem natAbs_le_self_sq (a : ℤ) : (Int.natAbs a : ℤ) ≤ a ^ 2 := by
   apply Nat.le_mul_self
 #align int.abs_le_self_sq Int.natAbs_le_self_sq
 
-alias natAbs_le_self_sq ← natAbs_le_self_pow_two
+alias natAbs_le_self_pow_two := natAbs_le_self_sq
 
 theorem le_self_sq (b : ℤ) : b ≤ b ^ 2 :=
   le_trans le_natAbs (natAbs_le_self_sq _)
 #align int.le_self_sq Int.le_self_sq
 
-alias le_self_sq ← le_self_pow_two
+alias le_self_pow_two := le_self_sq
 #align int.le_self_pow_two Int.le_self_pow_two
 
 theorem pow_right_injective {x : ℤ} (h : 1 < x.natAbs) :

Mathlib/Algebra/GroupPower/Order.lean

@@ -648,7 +648,7 @@ theorem sq_nonneg (a : R) : 0 ≤ a ^ 2 :=
   pow_bit0_nonneg a 1
 #align sq_nonneg sq_nonneg
 
-alias sq_nonneg ← pow_two_nonneg
+alias pow_two_nonneg := sq_nonneg
 #align pow_two_nonneg pow_two_nonneg
 
 theorem pow_bit0_pos {a : R} (h : a ≠ 0) (n : ℕ) : 0 < a ^ bit0 n :=
@@ -659,7 +659,7 @@ theorem sq_pos_of_ne_zero (a : R) (h : a ≠ 0) : 0 < a ^ 2 :=
   pow_bit0_pos h 1
 #align sq_pos_of_ne_zero sq_pos_of_ne_zero
 
-alias sq_pos_of_ne_zero ← pow_two_pos_of_ne_zero
+alias pow_two_pos_of_ne_zero := sq_pos_of_ne_zero
 #align pow_two_pos_of_ne_zero pow_two_pos_of_ne_zero
 
 theorem pow_bit0_pos_iff (a : R) {n : ℕ} (hn : n ≠ 0) : 0 < a ^ bit0 n ↔ a ≠ 0 := by
@@ -758,7 +758,7 @@ theorem two_mul_le_add_sq (a b : R) : 2 * a * b ≤ a ^ 2 + b ^ 2 :=
   sub_nonneg.mp ((sub_add_eq_add_sub _ _ _).subst ((sub_sq a b).subst (sq_nonneg _)))
 #align two_mul_le_add_sq two_mul_le_add_sq
 
-alias two_mul_le_add_sq ← two_mul_le_add_pow_two
+alias two_mul_le_add_pow_two := two_mul_le_add_sq
 #align two_mul_le_add_pow_two two_mul_le_add_pow_two
 
 end LinearOrderedCommRing

Mathlib/Algebra/GroupPower/Ring.lean

@@ -174,7 +174,7 @@ theorem add_sq' (a b : R) : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b := by
   rw [add_sq, add_assoc, add_comm _ (b ^ 2), add_assoc]
 #align add_sq' add_sq'
 
-alias add_sq ← add_pow_two
+alias add_pow_two := add_sq
 #align add_pow_two add_pow_two
 
 end CommSemiring
@@ -219,10 +219,10 @@ theorem neg_sq (a : R) : (-a) ^ 2 = a ^ 2 := by simp [sq]
 theorem neg_one_sq : (-1 : R) ^ 2 = 1 := by simp [neg_sq, one_pow]
 #align neg_one_sq neg_one_sq
 
-alias neg_sq ← neg_pow_two
+alias neg_pow_two := neg_sq
 #align neg_pow_two neg_pow_two
 
-alias neg_one_sq ← neg_one_pow_two
+alias neg_one_pow_two := neg_one_sq
 #align neg_one_pow_two neg_one_pow_two
 
 end HasDistribNeg
@@ -271,14 +271,14 @@ theorem sq_sub_sq (a b : R) : a ^ 2 - b ^ 2 = (a + b) * (a - b) :=
   (Commute.all a b).sq_sub_sq
 #align sq_sub_sq sq_sub_sq
 
-alias sq_sub_sq ← pow_two_sub_pow_two
+alias pow_two_sub_pow_two := sq_sub_sq
 #align pow_two_sub_pow_two pow_two_sub_pow_two
 
 theorem sub_sq (a b : R) : (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2 := by
   rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]
 #align sub_sq sub_sq
 
-alias sub_sq ← sub_pow_two
+alias sub_pow_two := sub_sq
 #align sub_pow_two sub_pow_two
 
 theorem sub_sq' (a b : R) : (a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b := by

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -126,7 +126,7 @@ theorem subsingleton_iff_zero_eq_one : (0 : M₀) = 1 ↔ Subsingleton M₀ :=
   ⟨fun h => haveI := uniqueOfZeroEqOne h; inferInstance, fun h => @Subsingleton.elim _ h _ _⟩
 #align subsingleton_iff_zero_eq_one subsingleton_iff_zero_eq_one
 
-alias subsingleton_iff_zero_eq_one ↔ subsingleton_of_zero_eq_one _
+alias ⟨subsingleton_of_zero_eq_one, _⟩ := subsingleton_iff_zero_eq_one
 #align subsingleton_of_zero_eq_one subsingleton_of_zero_eq_one
 
 theorem eq_of_zero_eq_one (h : (0 : M₀) = 1) (a b : M₀) : a = b :=

Mathlib/Algebra/GroupWithZero/Divisibility.lean

@@ -123,10 +123,10 @@ theorem dvd_antisymm' : a ∣ b → b ∣ a → b = a :=
   flip dvd_antisymm
 #align dvd_antisymm' dvd_antisymm'
 
-alias dvd_antisymm ← Dvd.dvd.antisymm
+alias Dvd.dvd.antisymm := dvd_antisymm
 #align has_dvd.dvd.antisymm Dvd.dvd.antisymm
 
-alias dvd_antisymm' ← Dvd.dvd.antisymm'
+alias Dvd.dvd.antisymm' := dvd_antisymm'
 #align has_dvd.dvd.antisymm' Dvd.dvd.antisymm'
 
 theorem eq_of_forall_dvd (h : ∀ c, a ∣ c ↔ b ∣ c) : a = b :=

Mathlib/Algebra/GroupWithZero/Units/Basic.lean

@@ -254,7 +254,7 @@ theorem isUnit_iff_ne_zero : IsUnit a ↔ a ≠ 0 :=
   Units.exists_iff_ne_zero
 #align is_unit_iff_ne_zero isUnit_iff_ne_zero
 
-alias isUnit_iff_ne_zero ↔ _ Ne.isUnit
+alias ⟨_, Ne.isUnit⟩ := isUnit_iff_ne_zero
 #align ne.is_unit Ne.isUnit
 
 -- porting note: can't add this attribute?

Mathlib/Algebra/ModEq.lean

@@ -62,7 +62,7 @@ theorem modEq_comm : a ≡ b [PMOD p] ↔ b ≡ a [PMOD p] :=
   (Equiv.neg _).exists_congr_left.trans <| by simp [ModEq, ← neg_eq_iff_eq_neg]
 #align add_comm_group.modeq_comm AddCommGroup.modEq_comm
 
-alias modEq_comm ↔ ModEq.symm _
+alias ⟨ModEq.symm, _⟩ := modEq_comm
 #align add_comm_group.modeq.symm AddCommGroup.ModEq.symm
 
 attribute [symm] ModEq.symm
@@ -80,7 +80,7 @@ theorem neg_modEq_neg : -a ≡ -b [PMOD p] ↔ a ≡ b [PMOD p] :=
   modEq_comm.trans <| by simp [ModEq, neg_add_eq_sub]
 #align add_comm_group.neg_modeq_neg AddCommGroup.neg_modEq_neg
 
-alias neg_modEq_neg ↔ ModEq.of_neg ModEq.neg
+alias ⟨ModEq.of_neg, ModEq.neg⟩ := neg_modEq_neg
 #align add_comm_group.modeq.of_neg AddCommGroup.ModEq.of_neg
 #align add_comm_group.modeq.neg AddCommGroup.ModEq.neg
 
@@ -89,7 +89,7 @@ theorem modEq_neg : a ≡ b [PMOD -p] ↔ a ≡ b [PMOD p] :=
   modEq_comm.trans <| by simp [ModEq, ← neg_eq_iff_eq_neg]
 #align add_comm_group.modeq_neg AddCommGroup.modEq_neg
 
-alias modEq_neg ↔ ModEq.of_neg' ModEq.neg'
+alias ⟨ModEq.of_neg', ModEq.neg'⟩ := modEq_neg
 #align add_comm_group.modeq.of_neg' AddCommGroup.ModEq.of_neg'
 #align add_comm_group.modeq.neg' AddCommGroup.ModEq.neg'
 
@@ -175,10 +175,10 @@ theorem nsmul_modEq_nsmul [NoZeroSMulDivisors ℕ α] (hn : n ≠ 0) :
   exists_congr fun m => by rw [← smul_sub, smul_comm, smul_right_inj hn]
 #align add_comm_group.nsmul_modeq_nsmul AddCommGroup.nsmul_modEq_nsmul
 
-alias zsmul_modEq_zsmul ↔ ModEq.zsmul_cancel _
+alias ⟨ModEq.zsmul_cancel, _⟩ := zsmul_modEq_zsmul
 #align add_comm_group.modeq.zsmul_cancel AddCommGroup.ModEq.zsmul_cancel
 
-alias nsmul_modEq_nsmul ↔ ModEq.nsmul_cancel _
+alias ⟨ModEq.nsmul_cancel, _⟩ := nsmul_modEq_nsmul
 #align add_comm_group.modeq.nsmul_cancel AddCommGroup.ModEq.nsmul_cancel
 
 namespace ModEq
@@ -207,18 +207,18 @@ protected theorem sub_iff_right :
   (Equiv.subRight m).symm.exists_congr_left.trans <| by simp [sub_sub_sub_comm, hm, sub_smul, ModEq]
 #align add_comm_group.modeq.sub_iff_right AddCommGroup.ModEq.sub_iff_right
 
-alias ModEq.add_iff_left ↔ add_left_cancel add
+alias ⟨add_left_cancel, add⟩ := ModEq.add_iff_left
 #align add_comm_group.modeq.add_left_cancel AddCommGroup.ModEq.add_left_cancel
 #align add_comm_group.modeq.add AddCommGroup.ModEq.add
 
-alias ModEq.add_iff_right ↔ add_right_cancel _
+alias ⟨add_right_cancel, _⟩ := ModEq.add_iff_right
 #align add_comm_group.modeq.add_right_cancel AddCommGroup.ModEq.add_right_cancel
 
-alias ModEq.sub_iff_left ↔ sub_left_cancel sub
+alias ⟨sub_left_cancel, sub⟩ := ModEq.sub_iff_left
 #align add_comm_group.modeq.sub_left_cancel AddCommGroup.ModEq.sub_left_cancel
 #align add_comm_group.modeq.sub AddCommGroup.ModEq.sub
 
-alias ModEq.sub_iff_right ↔ sub_right_cancel _
+alias ⟨sub_right_cancel, _⟩ := ModEq.sub_iff_right
 #align add_comm_group.modeq.sub_right_cancel AddCommGroup.ModEq.sub_right_cancel
 
 -- porting note: doesn't work
@@ -327,11 +327,11 @@ theorem nat_cast_modEq_nat_cast {a b n : ℕ} : a ≡ b [PMOD (n : α)] ↔ a 
     Int.cast_ofNat]
 #align add_comm_group.nat_cast_modeq_nat_cast AddCommGroup.nat_cast_modEq_nat_cast
 
-alias int_cast_modEq_int_cast ↔ ModEq.of_int_cast ModEq.int_cast
+alias ⟨ModEq.of_int_cast, ModEq.int_cast⟩ := int_cast_modEq_int_cast
 #align add_comm_group.modeq.of_int_cast AddCommGroup.ModEq.of_int_cast
 #align add_comm_group.modeq.int_cast AddCommGroup.ModEq.int_cast
 
-alias nat_cast_modEq_nat_cast ↔ _root_.Nat.ModEq.of_nat_cast ModEq.nat_cast
+alias ⟨_root_.Nat.ModEq.of_nat_cast, ModEq.nat_cast⟩ := nat_cast_modEq_nat_cast
 #align nat.modeq.of_nat_cast Nat.ModEq.of_nat_cast
 #align add_comm_group.modeq.nat_cast AddCommGroup.ModEq.nat_cast
 

Mathlib/Algebra/Order/Field/Basic.lean

@@ -51,15 +51,15 @@ theorem inv_pos : 0 < a⁻¹ ↔ 0 < a :=
   fun a ha => flip lt_of_mul_lt_mul_left ha.le <| by simp [ne_of_gt ha, zero_lt_one]
 #align inv_pos inv_pos
 
-alias inv_pos ↔ _ inv_pos_of_pos
+alias ⟨_, inv_pos_of_pos⟩ := inv_pos
 #align inv_pos_of_pos inv_pos_of_pos
 
 @[simp]
 theorem inv_nonneg : 0 ≤ a⁻¹ ↔ 0 ≤ a := by
   simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]
 #align inv_nonneg inv_nonneg
 
-alias inv_nonneg ↔ _ inv_nonneg_of_nonneg
+alias ⟨_, inv_nonneg_of_nonneg⟩ := inv_nonneg
 #align inv_nonneg_of_nonneg inv_nonneg_of_nonneg
 
 @[simp]
@@ -519,13 +519,13 @@ theorem half_lt_self_iff : a / 2 < a ↔ 0 < a := by
   rw [div_lt_iff (zero_lt_two' α), mul_two, lt_add_iff_pos_left]
 #align half_lt_self_iff half_lt_self_iff
 
-alias half_le_self_iff ↔ _ half_le_self
+alias ⟨_, half_le_self⟩ := half_le_self_iff
 #align half_le_self half_le_self
 
-alias half_lt_self_iff ↔ _ half_lt_self
+alias ⟨_, half_lt_self⟩ := half_lt_self_iff
 #align half_lt_self half_lt_self
 
-alias half_lt_self ← div_two_lt_of_pos
+alias div_two_lt_of_pos := half_lt_self
 #align div_two_lt_of_pos div_two_lt_of_pos
 
 theorem one_half_lt_one : (1 / 2 : α) < 1 :=
@@ -960,12 +960,12 @@ theorem mul_sub_mul_div_mul_nonpos_iff (hc : c ≠ 0) (hd : d ≠ 0) :
   rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_nonpos]
 #align mul_sub_mul_div_mul_nonpos_iff mul_sub_mul_div_mul_nonpos_iff
 
-alias mul_sub_mul_div_mul_neg_iff ↔ div_lt_div_of_mul_sub_mul_div_neg mul_sub_mul_div_mul_neg
+alias ⟨div_lt_div_of_mul_sub_mul_div_neg, mul_sub_mul_div_mul_neg⟩ := mul_sub_mul_div_mul_neg_iff
 #align mul_sub_mul_div_mul_neg mul_sub_mul_div_mul_neg
 #align div_lt_div_of_mul_sub_mul_div_neg div_lt_div_of_mul_sub_mul_div_neg
 
-alias mul_sub_mul_div_mul_nonpos_iff ↔
-  div_le_div_of_mul_sub_mul_div_nonpos mul_sub_mul_div_mul_nonpos
+alias ⟨div_le_div_of_mul_sub_mul_div_nonpos, mul_sub_mul_div_mul_nonpos⟩ :=
+  mul_sub_mul_div_mul_nonpos_iff
 #align div_le_div_of_mul_sub_mul_div_nonpos div_le_div_of_mul_sub_mul_div_nonpos
 #align mul_sub_mul_div_mul_nonpos mul_sub_mul_div_mul_nonpos
 

Mathlib/Algebra/Order/Field/Power.lean

@@ -199,13 +199,13 @@ theorem Odd.zpow_pos_iff (hn : Odd n) : 0 < a ^ n ↔ 0 < a := by
   cases' hn with k hk; simpa only [hk, two_mul] using zpow_bit1_pos_iff
 #align odd.zpow_pos_iff Odd.zpow_pos_iff
 
-alias Even.zpow_pos_iff ↔ _ Even.zpow_pos
+alias ⟨_, Even.zpow_pos⟩ := Even.zpow_pos_iff
 #align even.zpow_pos Even.zpow_pos
 
-alias Odd.zpow_neg_iff ↔ _ Odd.zpow_neg
+alias ⟨_, Odd.zpow_neg⟩ := Odd.zpow_neg_iff
 #align odd.zpow_neg Odd.zpow_neg
 
-alias Odd.zpow_nonpos_iff ↔ _ Odd.zpow_nonpos
+alias ⟨_, Odd.zpow_nonpos⟩ := Odd.zpow_nonpos_iff
 #align odd.zpow_nonpos Odd.zpow_nonpos
 
 theorem Even.zpow_abs {p : ℤ} (hp : Even p) (a : α) : |a| ^ p = a ^ p := by