-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem derivFamily_lt_ord_lift {ι : Type u} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c)
    (hι : lift.{v} #ι < c) (hc' : c ≠ ℵ₀) (hf : ∀ i, ∀ b < c.ord, f i b < c.ord) {a} :
    a < c.ord → derivFamily f a < c.ord

Proof state:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
⊢ lift.{?u.136517, u} #ι < c.ord.cof

Tactic:
rwa [hc.cof_eq]

Result:
no goals

Proof state:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
⊢ a < c.ord → derivFamily f a < c.ord

Tactic:
have hω : ℵ₀ < c.ord.cof := by
  rw [hc.cof_eq]
  exact lt_of_le_of_ne hc.1 hc'.symm

Result:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
hω : ℵ₀ < c.ord.cof
⊢ a < c.ord → derivFamily f a < c.ord

Proof state:
case H₃
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b.IsLimit
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
this : ⨆ a, derivFamily f ↑a = b.bsup fun x x_1 => derivFamily f x
⊢ (b.bsup fun x x_1 => derivFamily f x) < c.ord

Tactic:
exact
  bsup_lt_ord_of_isRegular.{u, v} hc (ord_lt_ord.1 ((ord_card_le b).trans_lt hb')) fun o' ho' =>
    H o' ho' (ho'.trans hb')

Result:
no goals

Proof state:
case H₃
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b.IsLimit
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
⊢ b < c.ord → derivFamily f b < c.ord

Tactic:
intro hb'

Result:
case H₃
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b.IsLimit
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ derivFamily f b < c.ord

Proof state:
case H₁
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
⊢ 0 < c.ord → derivFamily f 0 < c.ord

Tactic:
rw [derivFamily_zero]

Result:
case H₁
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
⊢ 0 < c.ord → nfpFamily f 0 < c.ord

Proof state:
case H₃
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b.IsLimit
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
this : ⨆ a, derivFamily f ↑a = b.bsup fun x x_1 => derivFamily f x
⊢ derivFamily f b < c.ord

Tactic:
rw [derivFamily_limit f hb, this]

Result:
case H₃
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b.IsLimit
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
this : ⨆ a, derivFamily f ↑a = b.bsup fun x x_1 => derivFamily f x
⊢ (b.bsup fun x x_1 => derivFamily f x) < c.ord

Proof state:
case H₂
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b < c.ord → derivFamily f b < c.ord
hb' : succ b < c.ord
⊢ derivFamily f (succ b) < c.ord

Tactic:
rw [derivFamily_succ]

Result:
case H₂
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b < c.ord → derivFamily f b < c.ord
hb' : succ b < c.ord
⊢ nfpFamily f (succ (derivFamily f b)) < c.ord

Proof state:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
⊢ ℵ₀ < c

Tactic:
exact lt_of_le_of_ne hc.1 hc'.symm

Result:
no goals

Proof state:
case H₁
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
⊢ 0 < c.ord → nfpFamily f 0 < c.ord

Tactic:
exact nfpFamily_lt_ord_lift hω (by rwa [hc.cof_eq]) hf

Result:
no goals

Proof state:
case H₂
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b < c.ord → derivFamily f b < c.ord
hb' : succ b < c.ord
⊢ nfpFamily f (succ (derivFamily f b)) < c.ord

Tactic:
exact
  nfpFamily_lt_ord_lift hω (by rwa [hc.cof_eq]) hf
    ((isLimit_ord hc.1).succ_lt (hb ((lt_succ b).trans hb')))

Result:
no goals

Proof state:
case H₂
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b < c.ord → derivFamily f b < c.ord
⊢ succ b < c.ord → derivFamily f (succ b) < c.ord

Tactic:
intro hb'

Result:
case H₂
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b < c.ord → derivFamily f b < c.ord
hb' : succ b < c.ord
⊢ derivFamily f (succ b) < c.ord

Proof state:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
⊢ ℵ₀ < c.ord.cof

Tactic:
rw [hc.cof_eq]

Result:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
⊢ ℵ₀ < c

Proof state:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
hω : ℵ₀ < c.ord.cof
⊢ a < c.ord → derivFamily f a < c.ord

Tactic:
induction a using limitRecOn with
| H₁ =>
  rw [derivFamily_zero]
  exact nfpFamily_lt_ord_lift hω (by rwa [hc.cof_eq]) hf
| H₂ b hb =>
  intro hb'
  rw [derivFamily_succ]
  exact
    nfpFamily_lt_ord_lift hω (by rwa [hc.cof_eq]) hf
      ((isLimit_ord hc.1).succ_lt (hb ((lt_succ b).trans hb')))
| H₃ b hb H =>
  intro hb'
  have : ⨆ a : Iio b, _ = _ :=
    iSup_eq_bsup.{max u v, max u v} (f := fun x (_ : x < b) ↦ derivFamily f x)
  rw [derivFamily_limit f hb, this]
  exact
    bsup_lt_ord_of_isRegular.{u, v} hc (ord_lt_ord.1 ((ord_card_le b).trans_lt hb')) fun o' ho' =>
      H o' ho' (ho'.trans hb')

Result:
no goals