-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sup_eq_lsub_iff_succ {ι : Type u} (f : ι → Ordinal.{max u v}) :
    sup.{_, v} f = lsub.{_, v} f ↔ ∀ a < lsub.{_, v} f, succ a < lsub.{_, v} f

Proof state:
case refine_1
ι : Type u
f : ι → Ordinal.{max u v}
h : sup f = lsub f
⊢ ∀ a < sup f, succ a < sup f

Tactic:
exact fun a => sup_not_succ_of_ne_sup fun i => (lsub_le_iff.1 (le_of_eq h.symm) i).ne

Result:
no goals

Proof state:
case refine_2
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
⊢ False

Tactic:
have :=
  hf _
    (by
      rw [← heq]
      exact lt_succ (sup f))

Result:
case refine_2
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
this : succ (sup f) < lsub f
⊢ False

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ sup f = lsub f ↔ ∀ a < lsub f, succ a < lsub f

Tactic:
refine ⟨fun h => ?_, fun hf => le_antisymm (sup_le_lsub f) (lsub_le fun i => ?_)⟩

Result:
case refine_1
ι : Type u
f : ι → Ordinal.{max u v}
h : sup f = lsub f
⊢ ∀ a < lsub f, succ a < lsub f

case refine_2
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
⊢ f i < sup f

Proof state:
case refine_2
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : sup f ≤ f i
⊢ False

Tactic:
have heq := (sup_succ_eq_lsub f).2 ⟨i, le_antisymm (le_sup _ _) hle⟩

Result:
case refine_2
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
⊢ False

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
⊢ ?m.243281 < lsub f

Tactic:
rw [← heq]

Result:
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
⊢ ?m.243281 < succ (sup f)

Proof state:
case refine_1
ι : Type u
f : ι → Ordinal.{max u v}
h : sup f = lsub f
⊢ ∀ a < lsub f, succ a < lsub f

Tactic:
rw [← h]

Result:
case refine_1
ι : Type u
f : ι → Ordinal.{max u v}
h : sup f = lsub f
⊢ ∀ a < sup f, succ a < sup f

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
⊢ ?m.243281 < succ (sup f)

Tactic:
exact lt_succ (sup f)

Result:
no goals

Proof state:
case refine_2
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
⊢ f i < sup f

Tactic:
by_contra! hle

Result:
case refine_2
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : sup f ≤ f i
⊢ False

Proof state:
case refine_2
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
this : lsub f < lsub f
⊢ False

Tactic:
exact this.false

Result:
no goals

Proof state:
case refine_2
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
this : succ (sup f) < lsub f
⊢ False

Tactic:
rw [heq] at this

Result:
case refine_2
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
this : lsub f < lsub f
⊢ False