Bump mathlib

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

.gitignore

@@ -1,3 +1,4 @@
 /build
 /lake-packages/*
-**.olean
+/.lake/*
+**.olean

ConNF/BaseType/NearLitterPerm.lean

@@ -214,18 +214,22 @@ instance : MulAction NearLitterPerm NearLitter
   one_smul _ := rfl
   mul_smul _ _ _ := rfl
 
+theorem smul_nearLitter_def (π : NearLitterPerm) (N : NearLitter) :
+    π • N = ⟨π • N.1, ↑π.atomPerm⁻¹ ⁻¹' N, π.near N.2.2⟩ :=
+  rfl
+
 @[simp]
 theorem smul_nearLitter_fst (π : NearLitterPerm) (N : NearLitter) : (π • N).fst = π • N.fst :=
   rfl
 
 theorem smul_nearLitter_coe_preimage (π : NearLitterPerm) (N : NearLitter) :
-    π • N = ↑π.atomPerm⁻¹ ⁻¹' N :=
+    (π • N : NearLitter) = ((π.atomPerm⁻¹ : Perm Atom) : Atom → Atom) ⁻¹' N :=
   rfl
 
 /-- The action of a near-litter perm on a near-litter agrees with the pointwise action on its
 atoms. -/
 theorem smul_nearLitter_coe (π : NearLitterPerm) (N : NearLitter) :
-    ((π • N) : Set Atom) = π • (N : Set Atom) := by
+    (π • N : NearLitter) = π • (N : Set Atom) := by
   rw [smul_nearLitter_coe_preimage, preimage_inv]
   rfl
 
@@ -248,7 +252,8 @@ theorem NearLitter.not_mem_snd_iff (N : NearLitter) (a : Atom) : a ∉ (N.snd :
   Iff.rfl
 
 theorem smul_nearLitter_eq_smul_symmDiff_smul (π : NearLitterPerm) (N : NearLitter) :
-    (π • N : Set Atom) = (π • N.fst.toNearLitter : Set Atom) ∆ (π • litterSet N.fst ∆ N.snd) := by
+    (π • N : NearLitter) =
+      ((π • N.fst.toNearLitter : NearLitter) : Set Atom) ∆ (π • litterSet N.fst ∆ N.snd) := by
   ext a : 1
   simp only [mem_symmDiff, mem_smul_set_iff_inv_smul_mem, smul_nearLitter_coe]
   tauto

ConNF/BaseType/Small.lean

@@ -66,7 +66,7 @@ theorem small_iUnion (hι : #ι < #κ) {f : ι → Set α} (hf : ∀ i, Small (f
     mul_lt_of_lt κ_isRegular.aleph0_le hι <| iSup_lt_of_isRegular κ_isRegular hι hf
 
 theorem small_iUnion_Prop {p : Prop} {f : p → Set α} (hf : ∀ i, Small (f i)) : Small (⋃ i, f i) :=
-  by by_cases p <;> simp [h, hf _]
+  by by_cases p <;> simp_all
 
 protected theorem Small.bUnion {s : Set ι} (hs : Small s) {f : ∀ i ∈ s, Set α}
     (hf : ∀ i (hi : i ∈ s), Small (f i hi)) : Small (⋃ (i) (hi : i ∈ s), f i hi) :=

ConNF/Counting/CodingFunction.lean

@@ -72,7 +72,7 @@ theorem ext {χ₁ χ₂ : CodingFunction β}
 
 theorem smul_supports {S : OrdSupport β} {t : Tangle β}
     (h : Supports (Allowable β) (S : Set (SupportCondition β)) t) (ρ : Allowable β) :
-    Supports (Allowable β) (ρ • S : Set (SupportCondition β)) (ρ • t) := by
+    Supports (Allowable β) ((ρ • S : OrdSupport β) : Set (SupportCondition β)) (ρ • t) := by
   intro ρ' hρ'
   have := h (ρ⁻¹ * ρ' * ρ) ?_
   · rw [mul_assoc, mul_smul, inv_smul_eq_iff, mul_smul] at this

ConNF/Counting/OrdSupport.lean

@@ -108,13 +108,14 @@ theorem smul_mem_inv {ρ : Allowable β} {S : OrdSupport β} {c : SupportConditi
   simp only [smul_mem, inv_inv]
 
 @[simp]
-theorem lt_iff_smul {ρ : Allowable β} {S : OrdSupport β} {c d : ρ • S} :
+theorem lt_iff_smul {ρ : Allowable β} {S : OrdSupport β} {c d : (ρ • S : OrdSupport β)} :
     c < d ↔ (⟨ρ⁻¹ • c.val, c.prop⟩ : S) < ⟨ρ⁻¹ • d.val, d.prop⟩ :=
   Iff.rfl
 
 theorem lt_iff_smul' {S : OrdSupport β} {c d : S} (ρ : Allowable β) :
     c < d ↔
-    (⟨ρ • c.val, smul_mem_smul.mpr c.prop⟩ : ρ • S) < ⟨ρ • d.val, smul_mem_smul.mpr d.prop⟩ := by
+    (⟨ρ • c.val, smul_mem_smul.mpr c.prop⟩ : (ρ • S : OrdSupport β)) <
+      ⟨ρ • d.val, smul_mem_smul.mpr d.prop⟩ := by
   simp only [lt_iff_smul, inv_smul_smul, Subtype.coe_eta]
 
 theorem lt_iff_lt_of_smul_eq {S T : OrdSupport β} (c d : T) (h : S = T)
@@ -188,7 +189,7 @@ theorem relIso_apply (S : OrdSupport β) (ρ : Allowable β) (c : { c // c ∈ S
   rfl
 
 @[simp]
-theorem typein_smul (S : OrdSupport β) (ρ : Allowable β) (c : ρ • S) :
+theorem typein_smul (S : OrdSupport β) (ρ : Allowable β) (c : (ρ • S : OrdSupport β)) :
     Ordinal.typein (ρ • S).r c = Ordinal.typein S.r ⟨ρ⁻¹ • c.val, c.prop⟩ := by
   have := Ordinal.relIso_enum (S.relIso ρ)
     (Ordinal.typein S.r ⟨ρ⁻¹ • c.val, c.prop⟩) (Ordinal.typein_lt_type _ _)

ConNF/Foa/Action/Complete.lean

@@ -112,7 +112,7 @@ theorem smul_toNearLitter_eq_of_preciseAt {hφ : φ.Lawful} {π : NearLitterPerm
     mem_litterSet, SetLike.mem_coe]
   constructor
   · intro ha
-    by_cases π.IsException a
+    by_cases h : π.IsException a
     · suffices h' : π⁻¹ • a ∈ φ.atomMap.Dom
       · rw [hφ.atom_mem _ h' L hL] at ha
         have := hπ.map_atom _ (Or.inl (Or.inl h'))
@@ -142,7 +142,7 @@ theorem smul_toNearLitter_eq_of_preciseAt {hφ : φ.Lawful} {π : NearLitterPerm
       rw [this, inv_smul_smul] at ha
       exact ha
   · intro ha
-    by_cases π⁻¹ • a ∈ φ.atomMap.Dom
+    by_cases h : π⁻¹ • a ∈ φ.atomMap.Dom
     · rw [hφ.atom_mem _ h L hL]
       have := hπ.map_atom _ (Or.inl (Or.inl h))
       rw [φ.complete_smul_atom_eq h] at this

ConNF/Foa/Action/FillAtomOrbits.lean

@@ -678,7 +678,7 @@ theorem subset_orbitAtomMap_ran : φ.atomMap.ran ⊆ (φ.orbitAtomMap hφ).ran :
 
 theorem fst_mem_litterPerm_domain_of_mem_map ⦃L : Litter⦄ (hL : (φ.litterMap L).Dom) ⦃a : Atom⦄
     (ha : a ∈ (φ.litterMap L).get hL) : a.1 ∈ (φ.litterPerm hφ).domain := by
-  by_cases a.1 = ((φ.litterMap L).get hL).1
+  by_cases h : a.1 = ((φ.litterMap L).get hL).1
   · rw [h]
     refine' Or.inl (Or.inl (Or.inr ⟨L, hL, _⟩))
     rw [roughLitterMapOrElse_of_dom]

ConNF/Foa/Action/NearLitterAction.lean

@@ -67,7 +67,7 @@ inductive BannedLitter : Litter → Prop
 
 theorem BannedLitter.memMap (a : Atom) (L : Litter) (hL)
     (ha : a ∈ ((φ.litterMap L).get hL : Set Atom)) : φ.BannedLitter a.1 := by
-  by_cases a.1 = ((φ.litterMap L).get hL).1
+  by_cases h : a.1 = ((φ.litterMap L).get hL).1
   · rw [h]
     exact BannedLitter.litterMap L hL
   · exact BannedLitter.diff L hL a ⟨ha, h⟩

ConNF/Foa/Basic/Constrains.lean

@@ -228,7 +228,7 @@ theorem small_constrains {β : Λ} (c : SupportCondition β) : Small {d | d ≺[
       exact ⟨a, h₁, h₂.symm⟩
     · rintro ⟨a, h₁, h₂⟩
       exact ⟨A, N, a, h₁, h₂.symm, rfl⟩
-  · by_cases
+  · by_cases h :
       ∃ (γ : Iic α) (δ : Iio α) (ε : Iio α) (_hδ : (δ : Λ) < γ) (hε : (ε : Λ) < γ) (hδε : δ ≠ ε)
         (B : Path (β : TypeIndex) γ) (t : Tangle δ),
         N = (fuzz (coe_ne_coe.mpr <| coe_ne' hδε) t).toNearLitter ∧

ConNF/Foa/Basic/Hypotheses.lean

@@ -269,7 +269,7 @@ theorem exists_cons_of_length_ne_zero {V : Type _} [Quiver V] {x y : V}
 theorem ofBot_comp {β : IicBot α} {ρ : Allowable β}
     (A : Quiver.Path (β : TypeIndex) (⊥ : IicBot α)) :
     NearLitterPerm.ofBot (Allowable.comp A ρ) = Allowable.toStructPerm ρ A := by
-  by_cases A.length = 0
+  by_cases h : A.length = 0
   · have : β = ⊥ := Subtype.coe_injective (Quiver.Path.eq_of_length_zero A h)
     cases this
     cases path_eq_nil A

ConNF/Foa/Basic/Reduction.lean

@@ -157,7 +157,7 @@ theorem reduction_supports (S : Set (SupportCondition β)) (c : SupportCondition
   intro π hc'
   obtain ⟨B, a | N⟩ := c
   · exact hc' (mem_reduction_of_reduced α _ _ (Reduced.mkAtom a) hc)
-  by_cases N.IsLitter
+  by_cases h : N.IsLitter
   · obtain ⟨L, rfl⟩ := h.exists_litter_eq
     exact hc' (mem_reduction_of_reduced α _ _ (Reduced.mkLitter L) hc)
   simp only [StructPerm.smul_supportCondition_eq_iff, smul_inr, inr.injEq] at hc' ⊢

ConNF/Foa/Complete/CompleteAction.lean

@@ -144,13 +144,13 @@ theorem completeNearLitterMap_eq' (A : ExtendedIndex β) (N : NearLitter) :
     · refine' Or.inl ⟨Or.inl ha₁, _⟩
       simp only [mem_image, not_exists, not_and]
       intro b hb
-      by_cases b ∈ (π A).atomPerm.domain
+      by_cases h : b ∈ (π A).atomPerm.domain
       · rw [completeAtomMap_eq_of_mem_domain h]
         rintro rfl
         exact ha₁.2 ((π A).atomPerm.map_domain h)
       · simp only [mem_iUnion, mem_singleton_iff, not_exists, and_imp] at ha₂
         exact Ne.symm (ha₂ b hb h)
-    · by_cases a ∈ litterSet N.fst
+    · by_cases h : a ∈ litterSet N.fst
       · refine' Or.inl ⟨Or.inr ⟨a, ⟨h, ha₁.2⟩, rfl⟩, _⟩
         simp only [mem_image, not_exists, not_and]
         intro b hb
@@ -176,7 +176,7 @@ theorem completeNearLitterMap_eq' (A : ExtendedIndex β) (N : NearLitter) :
       obtain ha₂ | ha₂ := ha₂
       · exact Or.inl ha₂
       obtain ⟨a, ha₁, ha₂⟩ := ha₂
-      by_cases a ∈ N
+      by_cases h : a ∈ N
       · rw [← ha₂]
         exact Or.inr ⟨a, ⟨h, ha₁.2⟩, rfl⟩
       rw [completeAtomMap_eq_of_not_mem_domain hb₂]
@@ -203,7 +203,7 @@ theorem completeNearLitterMap_eq' (A : ExtendedIndex β) (N : NearLitter) :
       rintro b hb _ rfl
       exact ha₂ ⟨b, hb, rfl⟩
     · refine' Or.inl ⟨_, _⟩
-      · by_cases a ∈ N
+      · by_cases h : a ∈ N
         · exact Or.inr ⟨a, ⟨h, ha₁.2⟩, rfl⟩
         · simp only [mem_image, not_exists, not_and] at ha₂
           have := ha₂ a (Or.inl ⟨ha₁.1, h⟩)
@@ -230,7 +230,7 @@ theorem completeNearLitterMap_eq' (A : ExtendedIndex β) (N : NearLitter) :
           exact
             NearLitterApprox.not_mem_domain_of_mem_largestSublitter _
               (Sublitter.equiv_apply_mem _) this
-      · by_cases a ∈ (π A).atomPerm.domain
+      · by_cases h : a ∈ (π A).atomPerm.domain
         · refine' Or.inl ⟨_, _⟩
           · simp only [completeAtomMap_eq_of_mem_domain h]
             refine' Or.inr ⟨a, ⟨_, h⟩, rfl⟩

ConNF/Foa/Properties/ConstrainedAction.lean

@@ -142,7 +142,8 @@ theorem eq_of_sublitter_bijection_apply_eq {π : NearLitterApprox} {L₁ L₂ L
         (π.largestSublitter L₃).equiv (π.largestSublitter L₄) b →
       L₁ = L₃ → L₂ = L₄ → (a : Atom) = b := by
   rintro h₁ rfl rfl
-  simp only [Subtype.coe_inj, EmbeddingLike.apply_eq_iff_eq] at h₁
+  simp only [NearLitterApprox.coe_largestSublitter, SetLike.coe_eq_coe,
+    EmbeddingLike.apply_eq_iff_eq] at h₁
   rw [h₁]
 
 noncomputable def constrainedAction (π : StructApprox β) (s : Set (SupportCondition β))

ConNF/Foa/Properties/Injective.lean

@@ -82,7 +82,8 @@ theorem _root_.ConNF.NearLitterPerm.Biexact.union {π π' : NearLitterPerm} {s
 theorem _root_.ConNF.NearLitterPerm.Biexact.smul_litter_subset {π π' : NearLitterPerm}
     {atoms : Set Atom} {litters : Set Litter}
     (h : NearLitterPerm.Biexact π π' atoms litters)
-    (L : Litter) (hL : L ∈ litters) : (π • L.toNearLitter : Set Atom) ⊆ π' • L.toNearLitter := by
+    (L : Litter) (hL : L ∈ litters) :
+    ((π • L.toNearLitter : NearLitter) : Set Atom) ⊆ (π' • L.toNearLitter : NearLitter) := by
   rw [NearLitterPerm.smul_nearLitter_coe, NearLitterPerm.smul_nearLitter_coe]
   rintro _ ⟨a, ha, rfl⟩
   simp only [Litter.coe_toNearLitter, mem_litterSet] at ha
@@ -1091,8 +1092,8 @@ theorem completeAtomMap_mem_completeNearLitterMap_toNearLitter' (hπf : π.Free)
       (fst_mem_reflTransConstrained_of_mem_symmDiff hb.1 hL) ?_
     · rw [Sublitter.equiv_congr_left (congr_arg _ this) _,
         Sublitter.equiv_congr_right (congr_arg _ (congr_arg₂ _ rfl this)) _,
-        Subtype.coe_inj, EquivLike.apply_eq_iff_eq] at hab
-      cases hab
+        Subtype.coe_inj] at hab
+      cases (EquivLike.apply_eq_iff_eq _).mp hab
       exact hb.1.elim (fun h' => h'.2 rfl) fun h' => h'.2 rfl
     exact equiv_apply_eq hab
 

ConNF/Foa/Properties/Surjective.lean

@@ -280,7 +280,7 @@ theorem completeNearLitterMap_surjective_extends (hπf : π.Free) (A : ExtendedI
     simp only [NearLitter.coe_mk, Subtype.coe_mk, Litter.coe_toNearLitter]
     rw [image_preimage_eq_of_subset _]
     intro a ha'
-    by_cases a.1 = N.1
+    by_cases h : a.1 = N.1
     · rw [← hN] at h
       exact completeAtomMap_surjective_extends A a ⟨_, h.symm⟩
     · exact ha (Or.inr ⟨ha', h⟩)

ConNF/Fuzz/Construction.lean

@@ -169,7 +169,7 @@ theorem mk_fuzz_deny (hβγ : β ≠ γ) (t : Tangle β) :
     apply_fun Sigma.fst at h
     simp only [Litter.mk.injEq, Subtype.coe_inj, and_self, and_true] at h
     exact h
-  · by_cases β = ⊥ ∧ ∃ a : Atom, HEq a t
+  · by_cases h : β = ⊥ ∧ ∃ a : Atom, HEq a t
     · obtain ⟨_, a, hat⟩ := h
       refine lt_of_le_of_lt ?_ (card_Iic_lt (pos a))
       refine ⟨⟨fun i => ⟨pos (typedNearLitter

ConNF/NewTangle/Cloud.lean

@@ -227,10 +227,9 @@ theorem cloudCode_mk_ne (hγβ : γ ≠ β) (s) : cloudCode β (mk γ s) = mk β
 variable {β c d}
 
 @[simp]
-theorem cloudCode_isEmpty : (cloudCode β c).IsEmpty ↔ c.IsEmpty :=
-  by
+theorem cloudCode_isEmpty : (cloudCode β c).IsEmpty ↔ c.IsEmpty := by
   obtain ⟨γ, s⟩ := c
-  by_cases γ = β
+  by_cases h : γ = β
   · rw [cloudCode_eq]
     exact h
   · rw [cloudCode_ne]

ConNF/NewTangle/CodeEquiv.lean

@@ -399,7 +399,7 @@ theorem exists_even_equiv : ∀ c : Code α, ∃ d : Code α, d ≡ c ∧ d.IsEv
 
 protected theorem IsEven.exists_equiv_extension_eq (heven : c.IsEven) :
     ∃ d : Code α, d ≡ c ∧ d.1 = γ := by
-  by_cases c.1 = γ
+  by_cases h : c.1 = γ
   · exact ⟨c, Equiv.rfl, h⟩
   · exact ⟨cloudCode γ c, Equiv.cloud_left _ heven _ h, rfl⟩
 

ConNF/NewTangle/NewTangle.lean

@@ -303,7 +303,7 @@ variable {ρ : NewAllowable α} {e : Extensions α}
 @[simp]
 theorem smul_extension_apply (ρ : NewAllowable α) (s : Set (Tangle β)) :
     ρ.val γ • extension s γ = extension (ρ.val β • s) γ := by
-  by_cases β = γ
+  by_cases h : β = γ
   · subst h
     simp only [extension_eq, cast_eq]
   · rw [extension_ne _ _ h, extension_ne _ _ h, smul_cloud]

ConNF/Structural/StructPerm.lean

@@ -47,7 +47,7 @@ theorem smul_nearLitter_fst (π : StructPerm ⊥) (N : NearLitter) : (π • N).
   rfl
 
 theorem smul_nearLitter_coe (π : StructPerm ⊥) (N : NearLitter) :
-    ((π • N) : Set Atom) = π • (N : Set Atom) :=
+    (π • N : NearLitter) = π • (N : Set Atom) :=
   NearLitterPerm.smul_nearLitter_coe (Tree.ofBot π) N
 
 theorem smul_nearLitter_snd (π : StructPerm ⊥) (N : NearLitter) :

ConNF/Structural/Tree.lean

@@ -162,6 +162,10 @@ as a functor to the category of all trees on `τ` where the morphisms are group
 def comp (A : Path α β) (a : Tree τ α) : Tree τ β :=
   fun B => a (A.comp B)
 
+theorem comp_def (A : Path α β) (a : Tree τ α) :
+    comp A a = fun B => a (A.comp B) :=
+  rfl
+
 /-- Evaluating the derivative of a structural group element along a path is the same as evaluating
 the original element along the composition of the paths. -/
 @[simp]
@@ -172,16 +176,16 @@ theorem comp_apply (a : Tree τ α) (A : Path α β) (B : ExtendedIndex β) :
 /-- The derivative along the empty path does nothing. -/
 @[simp]
 theorem comp_nil (a : Tree τ α) : comp nil a = a := by
-  simp only [comp, nil_comp, MonoidHom.coe_mk, OneHom.coe_mk]
+  simp only [comp_def, nil_comp, MonoidHom.coe_mk, OneHom.coe_mk]
 
 theorem comp_cons (a : Tree τ α) (p : Path α β) {γ : TypeIndex} (h : γ < β) :
     comp (p.cons h) a = (comp (Hom.toPath h)) (comp p a) := by
-  simp only [comp, MonoidHom.coe_mk, OneHom.coe_mk, Hom.comp_toPath_comp]
+  simp only [comp_def, MonoidHom.coe_mk, OneHom.coe_mk, Hom.comp_toPath_comp]
 
 /-- The derivative map is functorial. -/
 theorem comp_comp (a : Tree τ α) (p : Path α β) (q : Path β γ) :
     comp q (comp p a) = comp (p.comp q) a := by
-  simp only [comp, MonoidHom.coe_mk, OneHom.coe_mk, comp_assoc]
+  simp only [comp_def, MonoidHom.coe_mk, OneHom.coe_mk, comp_assoc]
 
 /-- The derivative map preserves the identity. -/
 @[simp]