Bump mathlib

Signed-off-by: zeramorphic <zeramorphic@proton.me>

ConNF/Basic/InductiveConstruction.lean

@@ -22,7 +22,10 @@ structure IndHyp (i : I) (t : ∀ j, r j i → Part (α j)) : Prop where
     (λ k h' ↦ (t k (Trans.trans h' h)).get (dom k _))
 
 def core : ∀ i, Part (α i) :=
-  inst.fix λ i t ↦ ⟨IndHyp i t, λ h ↦ f i (λ j h' ↦ (t j h').get (h.dom j h')) h.prop⟩
+  inst.fix _ λ i t ↦ {
+    Dom := IndHyp i t
+    get := λ h ↦ f i (λ j h' ↦ (t j h').get (h.dom j h')) h.prop
+  }
 
 theorem core_eq (i : I) :
     core f i = ⟨IndHyp i (λ j _ ↦ core f j),
@@ -38,7 +41,7 @@ theorem core_get_eq (i : I) (h : (core f i).Dom) :
   exact h.symm
 
 theorem core_dom (hp : ∀ i d h, p i (f i d h) d) : ∀ i, (core f i).Dom := by
-  refine inst.fix ?_
+  refine inst.fix _ ?_
   intro i ih
   rw [core_eq]
   refine ⟨ih, ?_⟩

ConNF/Basic/Ordinal.lean

@@ -1,5 +1,6 @@
 import ConNF.Basic.WellOrder
-import Mathlib.SetTheory.Cardinal.Ordinal
+import Mathlib.SetTheory.Cardinal.Aleph
+import Mathlib.SetTheory.Cardinal.Arithmetic
 
 noncomputable section
 universe u v
@@ -54,7 +55,7 @@ theorem isLimit_iff_noMaxOrder {α : Type u} [Nonempty α] [Preorder α] [IsWell
 
 theorem type_Iio_lt {α : Type u} [LtWellOrder α] (x : α) :
     type (Subrel ((· < ·) : α → α → Prop) (Set.Iio x)) < type ((· < ·) : α → α → Prop) :=
-  typein_lt_type _ x
+  @typein_lt_type _ _ (inferInstanceAs (IsWellOrder α (· < ·))) x
 
 def iicOrderIso {α : Type u} [LtWellOrder α] (x : α) :
     (Subrel ((· < ·) : α → α → Prop) (Set.Iic x)) ≃r
@@ -93,29 +94,6 @@ theorem type_Iic_lt {α : Type u} [LtWellOrder α] [NoMaxOrder α] (x : α) :
 ## Lifting ordinals
 -/
 
-@[simp]
-theorem typein_ordinal (o : Ordinal.{u}) :
-    -- TODO: Why can't Lean find this instance?
-    letI := inferInstanceAs (IsWellOrder Ordinal (· < ·))
-    typein (· < ·) o = lift.{u + 1} o := by
-  letI := inferInstanceAs (IsWellOrder Ordinal (· < ·))
-  induction o using Ordinal.induction with
-  | h o ih =>
-    apply le_antisymm
-    · by_contra! h
-      have := ih (enum ((· < ·) : Ordinal → Ordinal → Prop)
-          ⟨lift.{u + 1} o, h.trans (typein_lt_type _ o)⟩) ?_
-      · simp only [typein_enum, lift_inj] at this
-        conv_rhs at h => rw [this]
-        simp only [typein_enum, lt_self_iff_false] at h
-      · conv_rhs => rw [← enum_typein (· < ·) o]
-        exact enum_lt_enum.mpr h
-    · by_contra! h
-      rw [Ordinal.lt_lift_iff] at h
-      obtain ⟨o', ho'₁, ho'₂⟩ := h
-      rw [← ih o' ho'₂, typein_inj] at ho'₁
-      exact ho'₂.ne ho'₁
-
 instance ULift.isTrichotomous {α : Type u} {r : α → α → Prop} [IsTrichotomous α r] :
     IsTrichotomous (ULift.{v} α) (InvImage r ULift.down) := by
   constructor
@@ -158,7 +136,7 @@ theorem lift_typein_apply {α : Type u} {β : Type v} {r : α → α → Prop} {
     obtain ⟨y, hy⟩ := f.mem_range_of_rel x.down.prop
     refine ⟨ULift.up ⟨y, ?_⟩, ?_⟩
     · have := x.down.prop
-      rwa [Set.mem_setOf_eq, ← hy, f.map_rel_iff] at this
+      rwa [← hy, f.map_rel_iff] at this
     · apply ULift.down_injective
       apply Subtype.coe_injective
       simp only [Set.mem_setOf_eq, Set.coe_setOf, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk]
@@ -179,7 +157,7 @@ theorem type_Iio (o : Ordinal.{u}) :
   have := Ordinal.lift_type_eq.{u + 1, u, u + 1}
     (r := ((· < ·) : Set.Iio o → Set.Iio o → Prop))
     (s := ((· < ·) : o.toType → o.toType → Prop))
-  rw [lift_id, type_lt] at this
+  rw [lift_id, type_toType] at this
   rw [this]
   exact ⟨o.enumIsoToType.toRelIsoLT⟩
 
@@ -243,7 +221,7 @@ def iioAddMonoid : AddMonoid (Set.Iio c.ord) where
   __ := iioZero h
 
 theorem nat_lt_ord (h : ℵ₀ ≤ c) (n : ℕ) : n < c.ord := by
-  apply (nat_lt_omega n).trans_le
+  apply (nat_lt_omega0 n).trans_le
   apply ord_mono at h
   rwa [ord_aleph0] at h
 

ConNF/Basic/Transfer.lean

@@ -24,46 +24,30 @@ theorem lt_def [LT β] (x y : α) :
   Iff.rfl
 
 protected def min [Min β] : Min α where
-  min x y := e.symm (min (e x) (e y))
+  min x y := e.symm (e x ⊓ e y)
 
 theorem min_def [Min β] (x y : α) :
     letI := e.min
-    min x y = e.symm (min (e x) (e y)) :=
-  rfl
-
-protected def max [Max β] : Max α where
-  max x y := e.symm (max (e x) (e y))
-
-theorem max_def [Max β] (x y : α) :
-    letI := e.max
-    max x y = e.symm (max (e x) (e y)) :=
-  rfl
-
-protected def inf [Inf β] : Inf α where
-  inf x y := e.symm (e x ⊓ e y)
-
-theorem inf_def [Inf β] (x y : α) :
-    letI := e.inf
     x ⊓ y = e.symm (e x ⊓ e y) :=
   rfl
 
-theorem apply_inf [Inf β] (x y : α) :
-    letI := e.inf
+theorem apply_min [Min β] (x y : α) :
+    letI := e.min
     e (x ⊓ y) = e x ⊓ e y := by
-  rw [inf_def, apply_symm_apply]
+  rw [min_def, apply_symm_apply]
 
-protected def sup [Sup β] : Sup α where
-  sup x y := e.symm (e x ⊔ e y)
+protected def max [Max β] : Max α where
+  max x y := e.symm (e x ⊔ e y)
 
-theorem sup_def [Sup β] (x y : α) :
-    letI := e.sup
+theorem max_def [Max β] (x y : α) :
+    letI := e.max
     x ⊔ y = e.symm (e x ⊔ e y) :=
   rfl
 
-theorem apply_sup [Sup β] (x y : α) :
-    letI := e.sup
+theorem apply_max [Max β] (x y : α) :
+    letI := e.max
     e (x ⊔ y) = e x ⊔ e y := by
-  rw [sup_def, apply_symm_apply]
+  rw [max_def, apply_symm_apply]
 
 protected def compare [Ord β] : Ord α where
   compare x y := compare (e x) (e y)
@@ -107,10 +91,10 @@ protected def partialOrder [PartialOrder β] : PartialOrder α :=
   PartialOrder.lift e e.injective
 
 protected def linearOrder [LinearOrder β] : LinearOrder α :=
-  letI := e.sup
-  letI := e.inf
+  letI := e.max
+  letI := e.min
   letI := e.compare
-  LinearOrder.liftWithOrd e e.injective e.apply_sup e.apply_inf e.compare_def
+  LinearOrder.liftWithOrd e e.injective e.apply_max e.apply_min e.compare_def
 
 protected def ltWellOrder [LtWellOrder β] : LtWellOrder α where
   wf := InvImage.wf e (inferInstanceAs <| IsWellFounded β (· < ·)).wf

ConNF/Counting/Conclusions.lean

@@ -26,7 +26,7 @@ theorem card_codingFunction (β : TypeIndex) [LeLevel β] :
   revert β
   intro β
   induction β using WellFoundedLT.induction
-  case a β ih =>
+  case ind β ih =>
   intro
   cases β using WithBot.recBotCoe
   case bot => exact card_bot_codingFunction_lt

ConNF/Counting/SMulSpec.lean

@@ -75,8 +75,7 @@ theorem inflexible_of_inflexible_smul {A : β ↝ ⊥} {N₁ N₂ : NearLitter}
 
 theorem litter_eq_of_flexible_smul {A : β ↝ ⊥} {N₁ N₂ N₃ N₄ : NearLitter}
     (h₁₂ : convNearLitters S (ρᵁ • S) A N₁ N₂) (h₃₄ : convNearLitters S (ρᵁ • S) A N₃ N₄)
-    (h₁ : ¬Inflexible A N₁ᴸ) (h₂ : ¬Inflexible A N₂ᴸ)
-    (h₃ : ¬Inflexible A N₃ᴸ) (h₄ : ¬Inflexible A N₄ᴸ) (h₁₃ : N₁ᴸ = N₃ᴸ) :
+    (h₁₃ : N₁ᴸ = N₃ᴸ) :
     N₂ᴸ = N₄ᴸ := by
   rw [convNearLitters_smul_iff_left] at h₁₂ h₃₄
   rw [h₁₂.2, h₃₄.2, BasePerm.smul_nearLitter_litter, BasePerm.smul_nearLitter_litter, h₁₃]
@@ -131,7 +130,9 @@ theorem sameSpecLe_smul :
   case convAtoms_injective => exact S.smul_convAtoms_injective ρ
   case atomMemRel_le => exact S.atomMemRel_smul_le ρ
   case inflexible_of_inflexible => exact S.inflexible_of_inflexible_smul ρ
-  case litter_eq_of_flexible => exact S.litter_eq_of_flexible_smul ρ
+  case litter_eq_of_flexible =>
+    intros
+    apply S.litter_eq_of_flexible_smul ρ <;> assumption
   case atoms_of_inflexible => exact S.atoms_of_inflexible_smul ρ
   case nearLitters_of_inflexible => exact S.nearLitters_of_inflexible_smul ρ
 

ConNF/FOA/BaseApprox.lean

@@ -510,9 +510,9 @@ def upperBound (c : Set BaseApprox) (hc : IsChain (· ≤ ·) c) : BaseApprox wh
   exceptions := ⨆ ψ ∈ c, ψ.exceptions
   litters := ⨆ ψ ∈ c, ψᴸ
   exceptions_permutative := biSup_permutative_of_isChain
-    (λ ψ _ ↦ ψ.exceptions_permutative) (hc.image _ _ (λ _ _ h ↦ h.1.le))
+    (λ ψ _ ↦ ψ.exceptions_permutative) (hc.image _ _ _ (λ _ _ h ↦ h.1.le))
   litters_permutative' := biSup_permutative_of_isChain
-    (λ ψ _ ↦ ψ.litters_permutative) (hc.image _ _ (λ _ _ h ↦ h.2))
+    (λ ψ _ ↦ ψ.litters_permutative) (hc.image _ _ _ (λ _ _ h ↦ h.2))
   exceptions_small := upperBound_exceptions_small c hc
 
 theorem le_upperBound (c : Set BaseApprox) (hc : IsChain (· ≤ ·) c) :

ConNF/FOA/StrApprox.lean

@@ -61,7 +61,7 @@ end addOrbit
 
 /-- An upper bound for a chain of approximations. -/
 def upperBound (c : Set (StrApprox β)) (hc : IsChain (· ≤ ·) c) : StrApprox β :=
-  λ A ↦ BaseApprox.upperBound ((· A) '' c) (hc.image _ _ (λ _ _ h ↦ h A))
+  λ A ↦ BaseApprox.upperBound ((· A) '' c) (hc.image _ _ _ (λ _ _ h ↦ h A))
 
 theorem le_upperBound (c : Set (StrApprox β)) (hc : IsChain (· ≤ ·) c) :
     ∀ ψ ∈ c, ψ ≤ upperBound c hc :=

ConNF/FOA/StrApproxFOA.lean

@@ -364,7 +364,7 @@ theorem exists_exactlyApproximates_of_total (ψ : StrApprox β) (hψ₁ : ψ.Coh
   revert β
   intro β
   induction β using (inferInstanceAs <| IsWellFounded TypeIndex (· < ·)).induction
-  case a _ _ β ih =>
+  case ind _ _ β ih =>
   induction β using WithBot.recBotCoe with
   | bot =>
     intro _ ψ _ hψ₂
@@ -420,7 +420,7 @@ theorem freedomOfAction : FreedomOfAction β := by
   revert β
   intro β
   induction β using (inferInstanceAs <| IsWellFounded TypeIndex (· < ·)).induction
-  case a _ _ β ih =>
+  case ind _ _ β ih =>
     intro _ ψ hψ
     obtain ⟨χ, hχ₁, hχ₂, hχ₃⟩ := exists_total ψ hψ ih
     obtain ⟨ρ, hρ⟩ := exists_exactlyApproximates_of_total χ hχ₂ hχ₃

ConNF/Setup/Deny.lean

@@ -31,7 +31,7 @@ theorem initialWellOrder_type {X : Type _} :
     letI := initialWellOrder X
     type ((· < ·) : X → X → Prop) = (#X).ord := by
   have := Equiv.ltWellOrder_type (initialEquiv (X := X))
-  rwa [Ordinal.lift_id, Ordinal.lift_id, type_lt] at this
+  rwa [Ordinal.lift_id, Ordinal.lift_id, type_toType] at this
 
 theorem initialWellOrder_card_Iio {X : Type _} :
     letI := initialWellOrder X

ConNF/Setup/Params.lean

@@ -46,22 +46,23 @@ def Params.minimal : Params where
     rw [mk_out]
     exact isRegular_aleph_one
   μ_isStrongLimit := by
-    rw [mk_out]
-    exact isStrongLimit_beth <| IsLimit.isSuccPrelimit <| ord_aleph_isLimit 1
+    rw [mk_out, ord_aleph]
+    exact isStrongLimit_beth <| IsLimit.isSuccPrelimit <| isLimit_omega 1
   κ_lt_μ := by
-    rw [mk_out, mk_out]
+    rw [mk_out, mk_out, ord_aleph]
     apply (aleph_le_beth 1).trans_lt
     rw [beth_strictMono.lt_iff_lt]
-    exact (ord_aleph_isLimit 1).one_lt
+    exact (isLimit_omega 1).one_lt
   κ_le_μ_ord_cof := by
     rw [mk_out, mk_out]
-    have := beth_normal.cof_le (aleph 1).ord
+    have := isNormal_beth.cof_le (aleph 1).ord
     rwa [isRegular_aleph_one.cof_eq] at this
   Λ_type_le_μ_ord_cof := by
     rw [type_nat_lt, mk_out]
-    have := beth_normal.cof_le (aleph 1).ord
+    apply (omega0_le_of_isLimit (isLimit_omega 1)).trans
+    have := isNormal_beth.cof_le (aleph 1).ord
     rw [isRegular_aleph_one.cof_eq, ← ord_le_ord] at this
-    exact (omega_le_of_isLimit (ord_aleph_isLimit 1)).trans this
+    rwa [ord_aleph] at this ⊢
 
 def Params.inaccessible.{v} : Params where
   Λ := (Cardinal.univ.{v, v + 1}).ord.toType
@@ -73,8 +74,8 @@ def Params.inaccessible.{v} : Params where
   Λ_noMaxOrder := by
     apply noMaxOrder_of_isLimit
     change (type ((· < ·) : (Cardinal.univ.{v, v + 1}).ord.toType → _ → Prop)).IsLimit
-    rw [type_lt]
-    apply ord_isLimit
+    rw [type_toType]
+    apply isLimit_ord
     exact univ_inaccessible.1.le
   aleph0_lt_κ := by
     rw [mk_uLift, mk_out, ← lift_aleph0.{v + 1, v}, lift_strictMono.lt_iff_lt]
@@ -94,7 +95,7 @@ def Params.inaccessible.{v} : Params where
     exact (lift_lt_univ _).le
   Λ_type_le_μ_ord_cof := by
     change type ((· < ·) : (Cardinal.univ.{v, v + 1}).ord.toType → _ → Prop) ≤ _
-    rw [type_lt, mk_out, univ_inaccessible.2.1.cof_eq]
+    rw [type_toType, mk_out, univ_inaccessible.2.1.cof_eq]
 
 export Params (Λ κ μ aleph0_lt_κ κ_isRegular μ_isStrongLimit κ_lt_μ κ_le_μ_ord_cof
   Λ_type_le_μ_ord_cof)

ConNF/Setup/Small.lean

@@ -35,7 +35,7 @@ theorem Small.lt : Small s → #s < #κ :=
 -/
 
 theorem small_of_subsingleton (h : s.Subsingleton) : Small s :=
-  h.cardinal_mk_le_one.trans_lt <| one_lt_aleph0.trans_le aleph0_lt_κ.le
+  h.cardinalMk_le_one.trans_lt <| one_lt_aleph0.trans_le aleph0_lt_κ.le
 
 @[simp]
 theorem small_empty : Small (∅ : Set α) :=

ConNF/Setup/StrSet.lean

@@ -94,7 +94,7 @@ theorem strPerm_smul_coe {α : Λ} (π : StrPerm α) (x : StrSet α) :
 
 theorem one_strPerm_smul {α : TypeIndex} (x : StrSet α) : strPerm_smul 1 x = x := by
   induction α using WellFoundedLT.induction
-  case a α ih =>
+  case ind α ih =>
     cases α using WithBot.recBotCoe
     case bot => rw [strPerm_smul_bot_def, Tree.one_apply, one_smul, Equiv.symm_apply_apply]
     case coe α =>
@@ -105,7 +105,7 @@ theorem one_strPerm_smul {α : TypeIndex} (x : StrSet α) : strPerm_smul 1 x = x
 theorem mul_strPerm_smul {α : TypeIndex} (π₁ π₂ : StrPerm α) (x : StrSet α) :
     strPerm_smul (π₁ * π₂) x = strPerm_smul π₁ (strPerm_smul π₂ x) := by
   induction α using WellFoundedLT.induction
-  case a α ih =>
+  case ind α ih =>
     cases α using WithBot.recBotCoe
     case bot =>
       simp only [strPerm_smul_bot_def, Tree.mul_apply, mul_smul, Equiv.apply_symm_apply]

ConNF/Setup/TypeIndex.lean

@@ -34,7 +34,7 @@ instance : WellFoundedRelation TypeIndex where
 protected theorem TypeIndex.type :
     type ((· < ·) : TypeIndex → TypeIndex → Prop) = type ((· < ·) : Λ → Λ → Prop) := by
   rw [type_withBot]
-  exact one_add_of_omega_le <| omega_le_of_isLimit Λ_type_isLimit
+  exact one_add_of_omega0_le <| omega0_le_of_isLimit Λ_type_isLimit
 
 @[simp]
 protected theorem TypeIndex.card :