-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem le_iff_derivBFamily (H : ∀ i hi, IsNormal (f i hi)) {a} :
    (∀ i hi, f i hi a ≤ a) ↔ ∃ b, derivBFamily.{u, v} o f b = a

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
h : ∀ (i : o.toType), o.familyOfBFamily f i a ≤ a
i : Ordinal.{u}
hi : i < o
⊢ f i hi a ≤ a

Tactic:
rw [← familyOfBFamily_enum o f]

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
h : ∀ (i : o.toType), o.familyOfBFamily f i a ≤ a
i : Ordinal.{u}
hi : i < o
⊢ o.familyOfBFamily f ((enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩) a ≤ a

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
h : ∀ (i : o.toType), o.familyOfBFamily f i a ≤ a
i : Ordinal.{u}
hi : i < o
⊢ o.familyOfBFamily f ((enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩) a ≤ a

Tactic:
apply h

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a) ↔ ∀ (i : o.toType), o.familyOfBFamily f i a ≤ a

Tactic:
refine ⟨fun h i => h _ _, fun h i hi => ?_⟩

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
h : ∀ (i : o.toType), o.familyOfBFamily f i a ≤ a
i : Ordinal.{u}
hi : i < o
⊢ f i hi a ≤ a

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a) ↔ ∃ b, o.derivBFamily f b = a

Tactic:
unfold derivBFamily

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a) ↔ ∃ b, derivFamily (o.familyOfBFamily f) b = a

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a) ↔ ∃ b, derivFamily (o.familyOfBFamily f) b = a

Tactic:
rw [← le_iff_derivFamily]

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a) ↔ ∀ (i : o.toType), o.familyOfBFamily f i a ≤ a

case H
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ ∀ (i : o.toType), IsNormal (o.familyOfBFamily f i)

Proof state:
case H
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ ∀ (i : o.toType), IsNormal (o.familyOfBFamily f i)

Tactic:
exact fun _ => H _ _

Result:
no goals