chore: bump Std to Std#340 (#8104)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Archive/MiuLanguage/DecisionNec.lean

@@ -145,7 +145,7 @@ theorem goodm_of_rule2 (xs : Miustr) (_ : Derivable (M :: xs)) (h₂ : Goodm (M
   · cases' h₂ with mhead mtail
     contrapose! mtail
     rw [cons_append] at mtail
-    exact (or_self_iff _).mp (mem_append.mp mtail)
+    exact or_self_iff.mp (mem_append.mp mtail)
 #align miu.goodm_of_rule2 Miu.goodm_of_rule2
 
 theorem goodm_of_rule3 (as bs : Miustr) (h₁ : Derivable (as ++ ↑[I, I, I] ++ bs))

Mathlib/Algebra/Group/Commute/Units.lean

@@ -94,8 +94,7 @@ theorem isUnit_mul_iff (h : Commute a b) : IsUnit (a * b) ↔ IsUnit a ∧ IsUni
 
 @[to_additive (attr := simp)]
 theorem _root_.isUnit_mul_self_iff : IsUnit (a * a) ↔ IsUnit a :=
-  (Commute.refl a).isUnit_mul_iff.trans (and_self_iff _)
-  -- porting note: `and_self_iff` now has an implicit argument instead of an explicit one.
+  (Commute.refl a).isUnit_mul_iff.trans and_self_iff
 #align is_unit_mul_self_iff isUnit_mul_self_iff
 #align is_add_unit_add_self_iff isAddUnit_add_self_iff
 

Mathlib/Algebra/Hom/Centroid.lean

@@ -509,7 +509,7 @@ def commRing (h : ∀ a b : α, (∀ r : α, a * r * b = 0) → a = 0 ∨ b = 0)
   { CentroidHom.instRing with
     mul_comm := fun f g ↦ by
       ext
-      refine' sub_eq_zero.1 ((or_self_iff _).1 <| (h _ _) fun r ↦ _)
+      refine' sub_eq_zero.1 (or_self_iff.1 <| (h _ _) fun r ↦ _)
       rw [mul_assoc, sub_mul, sub_eq_zero, ← map_mul_right, ← map_mul_right, coe_mul, coe_mul,
         comp_mul_comm] }
 #align centroid_hom.comm_ring CentroidHom.commRing

Mathlib/Data/Finset/Basic.lean

@@ -1658,7 +1658,7 @@ theorem inter_right_comm (s₁ s₂ s₃ : Finset α) : s₁ ∩ s₂ ∩ s₃ =
 
 @[simp]
 theorem inter_self (s : Finset α) : s ∩ s = s :=
-  ext fun _ => mem_inter.trans <| and_self_iff _
+  ext fun _ => mem_inter.trans <| and_self_iff
 #align finset.inter_self Finset.inter_self
 
 @[simp]

Mathlib/Data/Finset/Sym.lean

@@ -100,7 +100,7 @@ theorem sym2_singleton (a : α) : ({a} : Finset α).sym2 = {Sym2.diag a} := by
 @[simp]
 theorem diag_mem_sym2_mem_iff : (∀ b, b ∈ Sym2.diag a → b ∈ s) ↔ a ∈ s := by
   rw [← mem_sym2_iff]
-  exact mk'_mem_sym2_iff.trans <| and_self_iff _
+  exact mk'_mem_sym2_iff.trans <| and_self_iff
 
 theorem diag_mem_sym2_iff : Sym2.diag a ∈ s.sym2 ↔ a ∈ s := by simp [diag_mem_sym2_mem_iff]
 #align finset.diag_mem_sym2_iff Finset.diag_mem_sym2_iff

Mathlib/Data/Set/Basic.lean

@@ -763,7 +763,7 @@ theorem mem_union (x : α) (a b : Set α) : x ∈ a ∪ b ↔ x ∈ a ∨ x ∈
 
 @[simp]
 theorem union_self (a : Set α) : a ∪ a = a :=
-  ext fun _ => or_self_iff _
+  ext fun _ => or_self_iff
 #align set.union_self Set.union_self
 
 @[simp]
@@ -917,7 +917,7 @@ theorem mem_of_mem_inter_right {x : α} {a b : Set α} (h : x ∈ a ∩ b) : x 
 
 @[simp]
 theorem inter_self (a : Set α) : a ∩ a = a :=
-  ext fun _ => and_self_iff _
+  ext fun _ => and_self_iff
 #align set.inter_self Set.inter_self
 
 @[simp]

Mathlib/GroupTheory/Perm/Support.lean

@@ -142,7 +142,7 @@ theorem nodup_of_pairwise_disjoint {l : List (Perm α)} (h1 : (1 : Perm α) ∉
   suffices (σ : Perm α) = 1 by
     rw [this] at h_mem
     exact h1 h_mem
-  exact ext fun a => (or_self_iff _).mp (h_disjoint a)
+  exact ext fun a => or_self_iff.mp (h_disjoint a)
 #align equiv.perm.nodup_of_pairwise_disjoint Equiv.Perm.nodup_of_pairwise_disjoint
 
 theorem pow_apply_eq_self_of_apply_eq_self {x : α} (hfx : f x = x) : ∀ n : ℕ, (f ^ n) x = x

Mathlib/Init/CCLemmas.lean

@@ -31,7 +31,7 @@ theorem and_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∧ b) = Fals
   h.symm ▸ propext (and_false_iff _)
 
 theorem and_eq_of_eq {a b : Prop} (h : a = b) : (a ∧ b) = a :=
-  h ▸ propext (and_self_iff _)
+  h ▸ propext and_self_iff
 
 theorem or_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a ∨ b) = True :=
   h.symm ▸ propext (true_or_iff _)
@@ -46,7 +46,7 @@ theorem or_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∨ b) = a :=
   h.symm ▸ propext (or_false_iff _)
 
 theorem or_eq_of_eq {a b : Prop} (h : a = b) : (a ∨ b) = a :=
-  h ▸ propext (or_self_iff _)
+  h ▸ propext or_self_iff
 
 theorem imp_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a → b) = b :=
   h.symm ▸ propext ⟨fun h ↦ h trivial, fun h₁ _ ↦ h₁⟩

Mathlib/Init/Logic.lean

@@ -152,7 +152,6 @@ theorem false_and_iff : False ∧ p ↔ False := iff_of_eq (false_and _)
 #align false_and false_and_iff
 #align not_and_self not_and_self_iff
 #align and_not_self and_not_self_iff
-theorem and_self_iff : p ∧ p ↔ p := iff_of_eq (and_self _)
 #align and_self and_self_iff
 
 #align or.imp Or.impₓ -- reorder implicits
@@ -187,7 +186,6 @@ theorem false_or_iff : False ∨ p ↔ p := iff_of_eq (false_or _)
 #align false_or false_or_iff
 theorem or_false_iff : p ∨ False ↔ p := iff_of_eq (or_false _)
 #align or_false or_false_iff
-theorem or_self_iff : p ∨ p ↔ p := iff_of_eq (or_self _)
 #align or_self or_self_iff
 
 theorem not_or_of_not : ¬a → ¬b → ¬(a ∨ b) := fun h1 h2 ↦ not_or.2 ⟨h1, h2⟩

Mathlib/NumberTheory/PythagoreanTriples.lean

@@ -374,13 +374,13 @@ private theorem coprime_sq_sub_mul_of_even_odd {m n : ℤ} (h : Int.gcd m n = 1)
       -- Porting note: norm_num is not enough to close this
       field_simp [sq, Int.sub_emod, Int.mul_emod, hm, hn]
     apply mt (Int.dvd_gcd (Int.coe_nat_dvd_left.mpr hpm)) hnp
-    apply (or_self_iff _).mp
+    apply or_self_iff.mp
     apply Int.Prime.dvd_mul' hp
     rw [(by ring : n * n = -(m ^ 2 - n ^ 2) + m * m)]
     exact hp1.neg_right.add ((Int.coe_nat_dvd_left.2 hpm).mul_right _)
   rw [Int.gcd_comm] at hnp
   apply mt (Int.dvd_gcd (Int.coe_nat_dvd_left.mpr hpn)) hnp
-  apply (or_self_iff _).mp
+  apply or_self_iff.mp
   apply Int.Prime.dvd_mul' hp
   rw [(by ring : m * m = m ^ 2 - n ^ 2 + n * n)]
   apply dvd_add hp1