-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem veblenWith_succ (o : Ordinal) : veblenWith f (Order.succ o) = deriv (veblenWith f o)

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ veblenWith f (Order.succ o) = deriv (veblenWith f o)

Tactic:
rw [deriv_eq_enumOrd (hf.veblenWith o), veblenWith_of_ne_zero f (succ_ne_zero _),
  derivFamily_eq_enumOrd]

Result:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ enumOrd (⋂ i, Function.fixedPoints (veblenWith f ↑i)) = enumOrd (Function.fixedPoints (veblenWith f o))

f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ ∀ (i : ↑(Set.Iio (Order.succ o))), IsNormal (veblenWith f ↑i)

Proof state:
case h.h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
⊢ (∀ (i : ↑(Set.Iio (Order.succ o))), a ∈ Function.fixedPoints (veblenWith f ↑i)) ↔
    a ∈ Function.fixedPoints (veblenWith f o)

Tactic:
use fun ha ↦ ha ⟨o, Order.lt_succ o⟩

Result:
case mpr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
⊢ a ∈ Function.fixedPoints (veblenWith f o) →
    ∀ (i : ↑(Set.Iio (Order.succ o))), a ∈ Function.fixedPoints (veblenWith f ↑i)

Proof state:
case mpr.mk.inl
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a b : Ordinal.{u}
ha : veblenWith f b a = a
hb : b < Order.succ b
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb⟩)

Tactic:
rw [Function.mem_fixedPoints_iff, ha]

Result:
no goals

Proof state:
case h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ ⋂ i, Function.fixedPoints (veblenWith f ↑i) = Function.fixedPoints (veblenWith f o)

Tactic:
ext a

Result:
case h.h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
⊢ a ∈ ⋂ i, Function.fixedPoints (veblenWith f ↑i) ↔ a ∈ Function.fixedPoints (veblenWith f o)

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ enumOrd (⋂ i, Function.fixedPoints (veblenWith f ↑i)) = enumOrd (Function.fixedPoints (veblenWith f o))

Tactic:
apply congr_arg

Result:
case h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ ⋂ i, Function.fixedPoints (veblenWith f ↑i) = Function.fixedPoints (veblenWith f o)

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ ∀ (i : ↑(Set.Iio (Order.succ o))), IsNormal (veblenWith f ↑i)

Tactic:
exact fun o ↦ hf.veblenWith o.1

Result:
no goals

Proof state:
case mpr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
⊢ a ∈ Function.fixedPoints (veblenWith f o) →
    ∀ (i : ↑(Set.Iio (Order.succ o))), a ∈ Function.fixedPoints (veblenWith f ↑i)

Tactic:
rintro (ha : _ = _) ⟨b, hb : b < _⟩

Result:
case mpr.mk
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb : b < Order.succ o
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb⟩)

Proof state:
case mpr.mk.inr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb✝ : b < Order.succ o
hb : b < o
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb✝⟩)

Tactic:
rw [← ha]

Result:
case mpr.mk.inr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb✝ : b < Order.succ o
hb : b < o
⊢ veblenWith f o a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb✝⟩)

Proof state:
case h.h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
⊢ a ∈ ⋂ i, Function.fixedPoints (veblenWith f ↑i) ↔ a ∈ Function.fixedPoints (veblenWith f o)

Tactic:
rw [Set.mem_iInter]

Result:
case h.h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
⊢ (∀ (i : ↑(Set.Iio (Order.succ o))), a ∈ Function.fixedPoints (veblenWith f ↑i)) ↔
    a ∈ Function.fixedPoints (veblenWith f o)

Proof state:
case mpr.mk
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb : b < Order.succ o
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb⟩)

Tactic:
obtain rfl | hb := Order.lt_succ_iff_eq_or_lt.1 hb

Result:
case mpr.mk.inl
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a b : Ordinal.{u}
ha : veblenWith f b a = a
hb : b < Order.succ b
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb⟩)

case mpr.mk.inr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb✝ : b < Order.succ o
hb : b < o
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb✝⟩)

Proof state:
case mpr.mk.inr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o a : Ordinal.{u}
ha : veblenWith f o a = a
b : Ordinal.{u}
hb✝ : b < Order.succ o
hb : b < o
⊢ veblenWith f o a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb✝⟩)

Tactic:
exact veblenWith_veblenWith_of_lt hf hb _

Result:
no goals