Bump mathlib

Signed-off-by: zeramorphic <[email protected]>

ConNF/Counting/Spec.lean

@@ -529,7 +529,7 @@ theorem specifies_iff (σ : Spec β) (S : Support β) :
     σ.Specifies S ↔
     σ.max = S.max ∧ ∀ (i : κ) (hσ : i < σ.max) (hS : i < S.max),
       SpecifiesCondition S (σ.f i hσ) (S.f i hS) := by
-  rw [Specifies, Specifies'_iff]
+  rw [Specifies, specifies'_iff]
   rfl
 
 theorem Specifies.max_eq_max {σ : Spec β} {S : Support β} (h : σ.Specifies S) :

ConNF/Counting/StrongSupport.lean

@@ -191,7 +191,7 @@ def bannedLitters (T : Support β) (A : ExtendedIndex β) : Set Litter :=
 
 theorem bannedLitter_iff_mem_bannedLitters (T : Support β) (A : ExtendedIndex β) (L : Litter) :
     BannedLitter T A L ↔ L ∈ bannedLitters T A := by
-  simp only [BannedLitter_iff, bannedLitters,
+  simp only [bannedLitter_iff, bannedLitters,
     mem_union, mem_iUnion, Set.mem_singleton_iff, exists_prop]
   constructor
   · rintro (h | ⟨a, N, ha, hN, rfl⟩)

ConNF/FOA/Action/FillAtomRange.lean

@@ -36,7 +36,7 @@ structure WithoutPreimage (a : Atom) : Prop where
   not_mem_ran : a ∉ φ.atomMap.ran
 
 theorem withoutPreimage_small : Small {a | φ.WithoutPreimage a} := by
-  simp only [WithoutPreimage_iff, setOf_and]
+  simp only [withoutPreimage_iff, setOf_and]
   rw [← inter_assoc]
   refine' Small.mono (inter_subset_left _ _) _
   suffices
@@ -90,7 +90,7 @@ structure MappedOutside (L : Litter) (hL : (φ.litterMap L).Dom) (a : Atom) : Pr
 and that are not already in the domain. -/
 theorem mappedOutside_small (L : Litter) (hL : (φ.litterMap L).Dom) :
     Small {a | φ.MappedOutside L hL a} := by
-  simp only [MappedOutside_iff, setOf_and]
+  simp only [mappedOutside_iff, setOf_and]
   rw [← inter_assoc]
   refine' Small.mono (inter_subset_left _ _) _
   refine' Small.mono _ ((φ.litterMap L).get hL).2.prop
@@ -203,7 +203,7 @@ theorem supportedAction_eq_of_mem_preimageLitterSubset {a : Atom}
   rw [Or.elim'_right, Or.elim'_left]
   intro h'
   have := φ.preimageLitter_not_banned
-  rw [BannedLitter_iff] at this
+  rw [bannedLitter_iff] at this
   push_neg at this
   exact this.1 a h' (φ.preimageLitterSubset_subset ha).symm
 
@@ -225,7 +225,7 @@ theorem supportedAction_eq_of_mem_mappedOutsideSubset {a : Atom}
       (φ.preimageLitterSubset_subset h)
     cases this
     have := φ.preimageLitter_not_banned
-    rw [BannedLitter_iff] at this
+    rw [bannedLitter_iff] at this
     push_neg at this
     cases this.2.1 hL
   · exact ((mappedOutsideSubset_spec _ _ hL).1 ha).2

ConNF/FOA/Action/NearLitterAction.lean

@@ -74,7 +74,7 @@ theorem BannedLitter.memMap (a : Atom) (L : Litter) (hL)
 
 /-- There are only a small amount of banned litters. -/
 theorem bannedLitter_small : Small {L | φ.BannedLitter L} := by
-  simp only [BannedLitter_iff, mem_diff, SetLike.mem_coe, mem_litterSet]
+  simp only [bannedLitter_iff, mem_diff, SetLike.mem_coe, mem_litterSet]
   refine' Small.union _ (Small.union _ (Small.union _ (Small.union _ _)))
   · refine' lt_of_le_of_lt _ φ.atomMap_dom_small
     refine' ⟨⟨fun a => ⟨_, a.prop.choose_spec.1⟩, fun a₁ a₂ h => _⟩⟩

ConNF/FOA/Basic/Constrains.lean

@@ -74,7 +74,7 @@ inductive HasPosition : Litter → μ → Prop
 
 theorem hasPosition_subsingleton {L : Litter} {ν₁ ν₂ : μ}
     (h₁ : HasPosition L ν₁) (h₂ : HasPosition L ν₂) : ν₁ = ν₂ := by
-  rw [HasPosition_iff] at h₁ h₂
+  rw [hasPosition_iff] at h₁ h₂
   cases h₁ with
   | inl h₁ =>
       obtain ⟨δ, _, ε, _, hδε, t, rfl, rfl⟩ := h₁
@@ -110,7 +110,7 @@ theorem hasPosition_of_litterConstrains {L₁ L₂ : Litter} (h : LitterConstrai
 theorem hasPosition_lt_of_litterConstrains {L₁ L₂ : Litter} (h : LitterConstrains L₁ L₂)
     {ν₁ ν₂ : μ} (h₁ : HasPosition L₁ ν₁) (h₂ : HasPosition L₂ ν₂) :
     ν₁ < ν₂ := by
-  rw [HasPosition_iff] at h₁ h₂
+  rw [hasPosition_iff] at h₁ h₂
   cases h with
   | fuzz_atom hδε t ht =>
       cases h₂ with
@@ -198,7 +198,7 @@ theorem constrains_nearLitter {c : SupportCondition β} {A : ExtendedIndex β}
       ∃ a ∈ litterSet N.fst ∆ N.snd, c = ⟨A, inl a⟩ := by
   constructor
   · intro h
-    rw [Constrains_iff] at h
+    rw [constrains_iff] at h
     obtain ⟨A, a, rfl, hc⟩ | ⟨A, N, hN, rfl, hc⟩ | ⟨A, N, a, ha, rfl, hc⟩ |
         ⟨γ, _, δ, _, ε, _, hδ, hε, hδε, A, t, c, _, rfl, hc'⟩ |
         ⟨γ, _, ε, _, hγ, A, a, rfl, hc⟩ := h
@@ -258,7 +258,7 @@ theorem constrains_wf (β : Λ) : WellFounded ((· ≺ ·) : SupportCondition β
     intro L ih A
     constructor
     intro c hc
-    rw [Constrains_iff] at hc
+    rw [constrains_iff] at hc
     obtain ⟨A, a, rfl, hc⟩ | ⟨A, N, hN, rfl, hc⟩ | ⟨A, N, a, ha, rfl, hc⟩ |
         ⟨γ, _, δ, _, ε, _, hδ, hε, hδε, A, t, c, hc, rfl, hc'⟩ |
         ⟨γ, _, ε, _, hγ, A, a, rfl, hc⟩ := hc
@@ -374,7 +374,7 @@ theorem lt_nearLitter' {β : Λ} {N : NearLitter} {B : ExtendedIndex β}
 theorem small_constrains {β : Λ} (c : SupportCondition β) : Small {d | d ≺ c} := by
   obtain ⟨A, a | N⟩ := c
   · simp only [constrains_atom, setOf_eq_eq_singleton, small_singleton]
-  simp_rw [Constrains_iff]
+  simp_rw [constrains_iff]
   refine Small.union ?_ (Small.union ?_ (Small.union ?_ (Small.union ?_ ?_))) <;>
     rw [small_setOf]
   · change Small {c | ∃ b B, _ ∧ _ = _}

ConNF/FOA/Basic/Flexible.lean

@@ -50,7 +50,7 @@ theorem mk_flexible (A : ExtendedIndex β) : #{L | Flexible A L} = #μ := by
   refine le_antisymm ((Cardinal.mk_subtype_le _).trans mk_litter.le) ?_
   refine ⟨⟨fun ν => ⟨⟨ν, ⊥, α, bot_ne_coe⟩, ?_⟩, ?_⟩⟩
   · intro h
-    rw [Inflexible_iff] at h
+    rw [inflexible_iff] at h
     obtain ⟨γ, _, δ, _, ε, _, _, hε, hδε, A, t, rfl, h⟩ | ⟨γ, _, ε, _, hε, A, t, rfl, h⟩ := h
     all_goals
       apply_fun Litter.γ at h

ConNF/FOA/Properties/Injective.lean

@@ -23,7 +23,7 @@ theorem atom_injective_extends {c d : SupportCondition β} (hcd : (ihsAction π
     exact (π A).atomPerm.injOn ha hb h
   · rw [completeAtomMap_eq_of_mem_domain ha, completeAtomMap_eq_of_not_mem_domain hb] at h
     cases
-      (π A).not_mem_domain_of_mem_largestSublitter (Subtype.coe_eq_iff.mp h.symm).choose
+      (π A).notr_mem_domain_of_mem_largestSublitter (Subtype.coe_eq_iff.mp h.symm).choose
         ((π A).atomPerm.map_domain ha)
   · rw [completeAtomMap_eq_of_not_mem_domain ha, completeAtomMap_eq_of_mem_domain hb] at h
     cases
@@ -286,7 +286,7 @@ theorem constrainedAction_comp_mapFlexible (hπf : π.Free) {γ : Λ} {s : Set (
     obtain ⟨⟨δ, ε, hε, C, hC⟩, a, rfl⟩ := hL₃
     contrapose hL₂
     rw [not_flexible_iff] at hL₂ ⊢
-    rw [Inflexible_iff] at hL₂
+    rw [inflexible_iff] at hL₂
     obtain ⟨δ', _, ε', _, ζ', _, _, hζ', hεζ', C', t', rfl, h'⟩ |
         ⟨δ', _, ε', _, hε', C', a', rfl, h'⟩ := hL₂
     · have := congr_arg Litter.β h'
@@ -303,7 +303,7 @@ theorem constrainedAction_comp_mapFlexible (hπf : π.Free) {γ : Λ} {s : Set (
     obtain ⟨⟨δ, ε, ζ, hε, hζ, hεζ, C, hC⟩, t, rfl⟩ := hL₃
     contrapose hL₂
     rw [not_flexible_iff] at hL₂ ⊢
-    rw [Inflexible_iff] at hL₂
+    rw [inflexible_iff] at hL₂
     obtain ⟨δ', _, ε', _, ζ', _, hε', hζ', hεζ', C', t', rfl, h'⟩ |
         ⟨δ', _, ε', _, hε', C', a', rfl, h'⟩ := hL₂
     · rw [Path.comp_cons, Path.comp_cons] at hC

ConNF/NewTangle/Cloud.lean

@@ -270,7 +270,7 @@ infixl:62 " ↝₀ " => CloudRel
 
 theorem cloudRel_subsingleton (hc : c.members.Nonempty) : {d : Code | d ↝₀ c}.Subsingleton := by
   intro d hd e he
-  simp only [CloudRel_iff] at hd he
+  simp only [cloudRel_iff] at hd he
   obtain ⟨β, hβ, hdβ, rfl⟩ := hd
   obtain ⟨γ, hγ, heγ, h⟩ := he
   have := ((Code.ext_iff _ _).1 h).1
@@ -292,7 +292,7 @@ theorem CloudRel.nonempty_iff : c ↝₀ d → (c.members.Nonempty ↔ d.members
   exact cloudCode_nonempty.symm
 
 theorem cloudRelEmptyEmpty (hγβ : γ ≠ β) : mk γ ∅ ↝₀ mk β ∅ :=
-  (CloudRel_iff _ _).2
+  (cloudRel_iff _ _).2
     ⟨β, inferInstance, hγβ, by
       ext : 1
       · rfl
@@ -317,7 +317,7 @@ infixl:62 " ↝ " => CloudRel'
 
 @[simp]
 theorem cloudRel_coe_coe {c d : NonemptyCode} : (c : Code) ↝₀ d ↔ c ↝ d := by
-  rw [CloudRel_iff, CloudRel'_iff]
+  rw [cloudRel_iff, cloudRel'_iff]
   aesop
 
 theorem cloud_subrelation : Subrelation (· ↝ ·) (InvImage (· < ·) (codeMinMap : NonemptyCode → μ))
@@ -335,7 +335,7 @@ only one code which is related (on the left) to any given code under the `cloud`
 theorem cloudRel'_subsingleton (c : NonemptyCode) :
     {d : NonemptyCode | d ↝ c}.Subsingleton := by
   intro d hd e he
-  simp only [Ne.def, CloudRel'_iff, mem_setOf_eq] at hd he
+  simp only [Ne.def, cloudRel'_iff, mem_setOf_eq] at hd he
   obtain ⟨β, hβ, hdβ, rfl⟩ := hd
   obtain ⟨γ, hγ, heγ, h⟩ := he
   rw [Subtype.ext_iff] at h

ConNF/NewTangle/CodeEquiv.lean

@@ -66,7 +66,7 @@ mutual
 end
 
 theorem isEven_of_forall_not (h : ∀ d, ¬d ↝₀ c) : IsEven c :=
-  (IsEven_iff c).2 fun _ hd => (h _ hd).elim
+  (isEven_iff c).2 fun _ hd => (h _ hd).elim
 
 @[simp]
 theorem isEven_of_eq_bot (c : Code) (hc : c.1 = ⊥) : c.IsEven :=
@@ -77,7 +77,7 @@ theorem isEven_bot (s : Set Atom) : IsEven (mk ⊥ s : Code) :=
   isEven_of_eq_bot _ rfl
 
 theorem not_isOdd_bot (s : Set Atom) : ¬IsOdd (mk ⊥ s : Code) := by
-  simp_rw [IsOdd_iff, CloudRel_iff]
+  simp_rw [isOdd_iff, cloudRel_iff]
   rintro ⟨d, ⟨γ, _, h⟩, _⟩
   exact bot_ne_coe (congr_arg Code.β h.2)
 
@@ -90,7 +90,7 @@ theorem IsEmpty.isEven_iff (hc : c.IsEmpty) : IsEven c ↔ (c.1 : TypeIndex) = 
   · rfl
   · simp [Code.IsEmpty] at hc
     cases hc
-    have := not_isOdd_bot ∅ ((IsEven_iff _).1 h ⟨⊥, ∅⟩ ?_)
+    have := not_isOdd_bot ∅ ((isEven_iff _).1 h ⟨⊥, ∅⟩ ?_)
     · cases this
     convert CloudRel.intro β _
     · aesop
@@ -99,11 +99,11 @@ theorem IsEmpty.isEven_iff (hc : c.IsEmpty) : IsEven c ↔ (c.1 : TypeIndex) = 
 @[simp]
 theorem IsEmpty.isOdd_iff (hc : c.IsEmpty) : IsOdd c ↔ (c.1 : TypeIndex) ≠ ⊥ := by
   obtain ⟨β, s⟩ := c
-  refine' ⟨_, fun h => (IsOdd_iff _).2 ⟨mk ⊥ ∅, _, isEven_bot _⟩⟩
+  refine' ⟨_, fun h => (isOdd_iff _).2 ⟨mk ⊥ ∅, _, isEven_bot _⟩⟩
   · rintro h (rfl : β = _)
     exact not_isOdd_bot _ h
   · lift β to Λ using h
-    refine (CloudRel_iff _ _).2 ⟨β, inferInstance, ?_⟩
+    refine (cloudRel_iff _ _).2 ⟨β, inferInstance, ?_⟩
     simp only [ne_eq, bot_ne_coe, not_false_eq_true, cloudCode_mk_ne, cloud_empty, mk.injEq,
       heq_eq_eq, true_and]
     exact hc
@@ -118,7 +118,7 @@ theorem isOdd_empty_iff : IsOdd (mk β ∅) ↔ (β : TypeIndex) ≠ ⊥ :=
 
 private theorem not_isOdd_nonempty : ∀ c : NonemptyCode, ¬c.1.IsOdd ↔ c.1.IsEven
   | c => by
-    rw [IsOdd_iff, IsEven_iff]
+    rw [isOdd_iff, isEven_iff]
     push_neg
     apply forall_congr' _
     intro d
@@ -153,14 +153,14 @@ theorem isEven_or_isOdd (c : Code) : c.IsEven ∨ c.IsOdd := by
   exact em _
 
 protected theorem _root_.ConNF.CloudRel.isOdd (hc : c.IsEven) (h : c ↝₀ d) : d.IsOdd :=
-  (IsOdd_iff d).2 ⟨_, h, hc⟩
+  (isOdd_iff d).2 ⟨_, h, hc⟩
 
 protected theorem IsEven.cloudCode (hc : c.IsEven) (hcγ : c.1 ≠ γ) : (cloudCode γ c).IsOdd :=
   (CloudRel.intro _ hcγ).isOdd hc
 
 protected theorem IsOdd.cloudCode (hc : c.IsOdd) (hc' : c.members.Nonempty) (hcγ : c.1 ≠ γ) :
     (cloudCode γ c).IsEven :=
-  (IsEven_iff _).2 fun d hd => by rwa [(cloudRel_cloudCode _ hc' hcγ).1 hd]
+  (isEven_iff _).2 fun d hd => by rwa [(cloudRel_cloudCode _ hc' hcγ).1 hd]
 
 protected theorem IsEven.cloudCode_ne (hc : c.IsEven) (hd : d.IsEven) (hcγ : c.1 ≠ γ) :
     cloudCode γ c ≠ d := by rintro rfl; exact hd.not_isOdd (hc.cloudCode hcγ)
@@ -185,7 +185,7 @@ theorem cloudCode_ne_singleton {t} (hcβ : c.1 ≠ β) : cloudCode γ c ≠ mk 
 @[simp]
 theorem isEven_singleton (t) : (mk β {t}).IsEven := by
   refine' isEven_of_forall_not fun c hc => _
-  obtain ⟨γ, _, h⟩ := (CloudRel_iff _ _).1 hc
+  obtain ⟨γ, _, h⟩ := (cloudRel_iff _ _).1 hc
   have := congr_arg Code.β h.2
   cases this
   exact cloudCode_ne_singleton h.1 h.2.symm
@@ -251,9 +251,9 @@ protected theorem _root_.ConNF.Code.IsEmpty.equiv (hc : c.IsEmpty) (hd : d.IsEmp
 
 /-- Code equivalence is transitive. -/
 theorem trans {c d e : Code} : c ≡ d → d ≡ e → c ≡ e := by
-  rw [Equiv_iff, Equiv_iff]
+  rw [equiv_iff, equiv_iff]
   rintro (rfl | ⟨hc, β, _, hcβ, rfl⟩ | ⟨hc, β, _, hcβ, rfl⟩ | ⟨d, hd, γ, _, hdγ, ε, _, hdε, rfl, rfl⟩)
-  · exact (Equiv_iff _ _).2
+  · exact (equiv_iff _ _).2
   · rintro (rfl | ⟨hc', γ, _, hcγ, rfl⟩ | ⟨-, γ, _, hcγ, rfl⟩ | ⟨_, hc', γ, _, hcγ, ε, _, _, rfl, rfl⟩)
     · exact cloud_left _ hc β hcβ
     · cases (hc'.cloudCode hcγ).not_isEven hc
@@ -310,13 +310,13 @@ theorem ext : ∀ {c d : Code}, c ≡ d → c.1 = d.1 → c = d
 @[simp]
 theorem bot_left_iff {s} :
     mk ⊥ s ≡ c ↔ mk ⊥ s = c ∨ ∃ β : Λ, ∃ _ : LtLevel β, c = mk β (cloud bot_ne_coe s) := by
-  simp [Equiv_iff, cloudCode_ne_bot.symm]
+  simp [equiv_iff, cloudCode_ne_bot.symm]
   rw [eq_comm]
 
 @[simp]
 theorem bot_right_iff {s} :
     c ≡ mk ⊥ s ↔ c = mk ⊥ s ∨ ∃ β : Λ, ∃ _ : LtLevel β, c = mk β (cloud bot_ne_coe s) := by
-  simp [Equiv_iff, cloudCode_ne_bot.symm]
+  simp [equiv_iff, cloudCode_ne_bot.symm]
   rw [eq_comm]
 
 @[simp]
@@ -341,7 +341,7 @@ theorem singleton_iff {g} :
       (c.1 : TypeIndex) = (γ : Λ) ∧ β ≠ γ ∧ c = cloudCode γ (mk β {g}) := by
   classical
   refine ⟨fun h => ?_, ?_⟩
-  · rw [Equiv_iff] at h
+  · rw [equiv_iff] at h
     simp only [isEven_singleton, ne_eq, exists_and_left, true_and] at h
     obtain rfl | ⟨γ, hβγ, _, _, rfl⟩ | ⟨_, γ, γne, _, h⟩ | ⟨d, -, γ, _, _, δ, δne, _, _, h⟩ :=
       h
@@ -382,7 +382,7 @@ theorem exists_even_equiv : ∀ c : Code, ∃ d : Code, d ≡ c ∧ d.IsEven :=
   · exact ⟨_, Equiv.empty_empty _ _, isEven_bot _⟩
   obtain heven | hodd := isEven_or_isOdd ⟨β, s⟩
   · exact ⟨_, Equiv.rfl, heven⟩
-  simp_rw [IsOdd_iff, CloudRel_iff] at hodd
+  simp_rw [isOdd_iff, cloudRel_iff] at hodd
   obtain ⟨d, ⟨γ, _, hdγ, hc⟩, hd⟩ := id hodd
   exact ⟨d, (Equiv.cloud_right _ hd _ hdγ).trans (Equiv.of_eq hc.symm), hd⟩
 

ConNF/NewTangle/NewAllowable.lean

@@ -392,7 +392,7 @@ end NewAllowable
 
 theorem CloudRel.smul : c ↝₀ d → ρ • c ↝₀ ρ • d := by
   rintro ⟨γ, hγ⟩
-  exact (CloudRel_iff _ _).2 ⟨_, inferInstance, hγ, ρ.smul_cloudCode hγ⟩
+  exact (cloudRel_iff _ _).2 ⟨_, inferInstance, hγ, ρ.smul_cloudCode hγ⟩
 
 @[simp]
 theorem smul_cloudRel : ρ • c ↝₀ ρ • d ↔ c ↝₀ d := by
@@ -404,7 +404,7 @@ namespace Code
 
 theorem isEven_smul_nonempty : ∀ c : NonemptyCode, (ρ • c.val).IsEven ↔ c.val.IsEven
   | ⟨c, hc⟩ => by
-    simp_rw [Code.IsEven_iff]
+    simp_rw [Code.isEven_iff]
     constructor <;> intro h d hd
     · have := hd.nonempty_iff.2 hc
       have _ : ⟨d, this⟩ ↝ ⟨c, hc⟩ := cloudRel_coe_coe.1 hd

ConNF/NewTangle/NewTangle.lean

@@ -164,7 +164,7 @@ theorem ext_code : ∀ {t₁ t₂ : Semitangle}, reprCode t₁ ≡ reprCode t₂
     cases even₁.not_isOdd ((isEven_bot _).cloudCode bot_ne_coe)
   | ⟨e₁, Preference.proper γ even₁ hA₁⟩, ⟨e₂, Preference.proper δ even₂ hA₂⟩, h => by
     dsimp at h
-    simp only [Equiv_iff, WithBot.coe_ne_bot, ne_eq, Subtype.mk.injEq, coe_inj, Subtype.coe_inj,
+    simp only [equiv_iff, WithBot.coe_ne_bot, ne_eq, Subtype.mk.injEq, coe_inj, Subtype.coe_inj,
       Subtype.exists, mem_Iio] at h
     obtain h | ⟨_, γ, _, hδγ, h⟩ | ⟨_, δ, _, hγδ, h⟩ |
       ⟨c, hc, γ, hcγ, hc', δ, hcδ, h⟩ := h
@@ -467,7 +467,7 @@ def newTypedNearLitter (N : NearLitter) : NewTangle :=
       congr 1
       simp only [Support.singleton_enum, Enumeration.mem_carrier_iff, κ_lt_one_iff, exists_prop,
         exists_eq_left, NewAllowable.smul_supportCondition_eq_iff, forall_eq, Sum.smul_inr,
-        Sum.inr.injEq] at h 
+        Sum.inr.injEq] at h
       apply_fun SetLike.coe at h
       refine Eq.trans ?_ h
       rw [NearLitterPerm.smul_nearLitter_coe]