-- Mathlib/Order/KonigLemma.lean
theorem GradeMinOrder.exists_nat_orderEmbedding_of_forall_covby_finite
    [GradeMinOrder ℕ α] [OrderBot α] [Infinite α] (hfin : ∀ (a : α), {x | a ⋖ x}.Finite) :
    ∃ f : ℕ ↪o α, f 0 = ⊥ ∧ (∀ i, f i ⋖ f (i+1)) ∧ ∀ i, grade ℕ (f i) = i

Proof state:
case intro.intro.zero
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : IsStronglyAtomic α
inst✝² : GradeMinOrder ℕ α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
f : ℕ ↪o α
h0 : f 0 = ⊥
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
⊢ grade ℕ (f 0) = 0

Tactic:
simp [h0]

Result:
no goals

Proof state:
case intro.intro.succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : IsStronglyAtomic α
inst✝² : GradeMinOrder ℕ α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
f : ℕ ↪o α
h0 : f 0 = ⊥
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
i : ℕ
ih : grade ℕ (f i) = i
⊢ grade ℕ (f (i + 1)) = i + 1

Tactic:
simpa [Order.covBy_iff_add_one_eq, ih, eq_comm] using CovBy.grade ℕ <| hf i

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : IsStronglyAtomic α
inst✝² : GradeMinOrder ℕ α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
f : ℕ ↪o α
h0 : f 0 = ⊥
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
⊢ ∃ f, f 0 = ⊥ ∧ (∀ (i : ℕ), f i ⋖ f (i + 1)) ∧ ∀ (i : ℕ), grade ℕ (f i) = i

Tactic:
refine ⟨f, h0, hf, fun i ↦ ?_⟩

Result:
case intro.intro
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : IsStronglyAtomic α
inst✝² : GradeMinOrder ℕ α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
f : ℕ ↪o α
h0 : f 0 = ⊥
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
i : ℕ
⊢ grade ℕ (f i) = i

Proof state:
case intro.intro
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : IsStronglyAtomic α
inst✝² : GradeMinOrder ℕ α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
f : ℕ ↪o α
h0 : f 0 = ⊥
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
i : ℕ
⊢ grade ℕ (f i) = i

Tactic:
induction' i with i ih

Result:
case intro.intro.zero
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : IsStronglyAtomic α
inst✝² : GradeMinOrder ℕ α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
f : ℕ ↪o α
h0 : f 0 = ⊥
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
⊢ grade ℕ (f 0) = 0

case intro.intro.succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : IsStronglyAtomic α
inst✝² : GradeMinOrder ℕ α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
f : ℕ ↪o α
h0 : f 0 = ⊥
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
i : ℕ
ih : grade ℕ (f i) = i
⊢ grade ℕ (f (i + 1)) = i + 1

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : IsStronglyAtomic α
inst✝² : GradeMinOrder ℕ α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
⊢ ∃ f, f 0 = ⊥ ∧ (∀ (i : ℕ), f i ⋖ f (i + 1)) ∧ ∀ (i : ℕ), grade ℕ (f i) = i

Tactic:
obtain ⟨f, h0, hf⟩ := exists_orderEmbedding_covby_of_forall_covby_finite_of_bot hfin

Result:
case intro.intro
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : IsStronglyAtomic α
inst✝² : GradeMinOrder ℕ α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
f : ℕ ↪o α
h0 : f 0 = ⊥
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
⊢ ∃ f, f 0 = ⊥ ∧ (∀ (i : ℕ), f i ⋖ f (i + 1)) ∧ ∀ (i : ℕ), grade ℕ (f i) = i