-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mex_lt_ord_succ_mk {ι : Type u} (f : ι → Ordinal.{u}) :
    mex.{_, u} f < (succ #ι).ord

Proof state:
ι : Type u
f : ι → Ordinal.{u}
⊢ mex f < (succ #ι).ord

Tactic:
by_contra! h

Result:
ι : Type u
f : ι → Ordinal.{u}
h : (succ #ι).ord ≤ mex f
⊢ False

Proof state:
ι : Type u
f : ι → Ordinal.{u}
h : (succ #ι).ord ≤ mex f
⊢ succ #ι ≤ #ι

Tactic:
have H := fun a => exists_of_lt_mex ((typein_lt_self a).trans_le h)

Result:
ι : Type u
f : ι → Ordinal.{u}
h : (succ #ι).ord ≤ mex f
H : ∀ (a : (succ #ι).ord.toType), ∃ i, f i = (typein fun x1 x2 => x1 < x2).toRelEmbedding a
⊢ succ #ι ≤ #ι

Proof state:
case h.e'_3
ι : Type u
f : ι → Ordinal.{u}
h : (succ #ι).ord ≤ mex f
H : ∀ (a : (succ #ι).ord.toType), ∃ i, f i = (typein fun x1 x2 => x1 < x2).toRelEmbedding a
g : (succ #ι).ord.toType → ι := fun a => Classical.choose ⋯
hg : Injective g
⊢ succ #ι = #(succ #ι).ord.toType

Tactic:
rw [Cardinal.mk_ord_toType (succ #ι)]

Result:
no goals

Proof state:
ι : Type u
f : ι → Ordinal.{u}
h : (succ #ι).ord ≤ mex f
H : ∀ (a : (succ #ι).ord.toType), ∃ i, f i = (typein fun x1 x2 => x1 < x2).toRelEmbedding a
g : (succ #ι).ord.toType → ι := fun a => Classical.choose ⋯
hg : Injective g
⊢ succ #ι ≤ #ι

Tactic:
convert Cardinal.mk_le_of_injective hg

Result:
case h.e'_3
ι : Type u
f : ι → Ordinal.{u}
h : (succ #ι).ord ≤ mex f
H : ∀ (a : (succ #ι).ord.toType), ∃ i, f i = (typein fun x1 x2 => x1 < x2).toRelEmbedding a
g : (succ #ι).ord.toType → ι := fun a => Classical.choose ⋯
hg : Injective g
⊢ succ #ι = #(succ #ι).ord.toType

Proof state:
ι : Type u
f : ι → Ordinal.{u}
h : (succ #ι).ord ≤ mex f
H : ∀ (a : (succ #ι).ord.toType), ∃ i, f i = (typein fun x1 x2 => x1 < x2).toRelEmbedding a
⊢ succ #ι ≤ #ι

Tactic:
let g : (succ #ι).ord.toType → ι := fun a => Classical.choose (H a)

Result:
ι : Type u
f : ι → Ordinal.{u}
h : (succ #ι).ord ≤ mex f
H : ∀ (a : (succ #ι).ord.toType), ∃ i, f i = (typein fun x1 x2 => x1 < x2).toRelEmbedding a
g : (succ #ι).ord.toType → ι := fun a => Classical.choose ⋯
⊢ succ #ι ≤ #ι

Proof state:
ι : Type u
f : ι → Ordinal.{u}
h : (succ #ι).ord ≤ mex f
⊢ False

Tactic:
apply (lt_succ #ι).not_le

Result:
ι : Type u
f : ι → Ordinal.{u}
h : (succ #ι).ord ≤ mex f
⊢ succ #ι ≤ #ι

Proof state:
ι : Type u
f : ι → Ordinal.{u}
h : (succ #ι).ord ≤ mex f
H : ∀ (a : (succ #ι).ord.toType), ∃ i, f i = (typein fun x1 x2 => x1 < x2).toRelEmbedding a
g : (succ #ι).ord.toType → ι := fun a => Classical.choose ⋯
a b : (succ #ι).ord.toType
h' : g a = g b
Hf : ∀ (x : (succ #ι).ord.toType), f (g x) = (typein fun x1 x2 => x1 < x2).toRelEmbedding x
⊢ a = b

Tactic:
apply_fun f at h'

Result:
ι : Type u
f : ι → Ordinal.{u}
h : (succ #ι).ord ≤ mex f
H : ∀ (a : (succ #ι).ord.toType), ∃ i, f i = (typein fun x1 x2 => x1 < x2).toRelEmbedding a
g : (succ #ι).ord.toType → ι := fun a => Classical.choose ⋯
a b : (succ #ι).ord.toType
Hf : ∀ (x : (succ #ι).ord.toType), f (g x) = (typein fun x1 x2 => x1 < x2).toRelEmbedding x
h' : f (g a) = f (g b)
⊢ a = b

Proof state:
ι : Type u
f : ι → Ordinal.{u}
h : (succ #ι).ord ≤ mex f
H : ∀ (a : (succ #ι).ord.toType), ∃ i, f i = (typein fun x1 x2 => x1 < x2).toRelEmbedding a
g : (succ #ι).ord.toType → ι := fun a => Classical.choose ⋯
a b : (succ #ι).ord.toType
Hf : ∀ (x : (succ #ι).ord.toType), f (g x) = (typein fun x1 x2 => x1 < x2).toRelEmbedding x
h' : f (g a) = f (g b)
⊢ a = b

Tactic:
rwa [Hf, Hf, typein_inj] at h'

Result:
no goals