-- Mathlib/Order/TransfiniteIteration.lean
lemma top_mem_range_transfiniteIterate
    (hφ' : ∀ i ≠ (⊤ : I), i < φ i) (φtop : φ ⊤ = ⊤)
    (H : ¬ Function.Injective (fun (j : J) ↦ transfiniteIterate φ j i₀)) :
    ∃ (j : J), transfiniteIterate φ j i₀ = ⊤

Proof state:
case neg
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
hj : ¬j₁ = j₂
hj' : j₂ ≤ j₁
⊢ ∃ j₁ j₂, ∃ (_ : j₁ < j₂), transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀

Tactic:
obtain hj' | rfl := hj'.lt_or_eq

Result:
case neg.inl
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
hj : ¬j₁ = j₂
hj'✝ : j₂ ≤ j₁
hj' : j₂ < j₁
⊢ ∃ j₁ j₂, ∃ (_ : j₁ < j₂), transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀

case neg.inr
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
hφ : ∀ (i : I), i ≤ φ i
j₂ : J
eq : transfiniteIterate φ j₂ i₀ = transfiniteIterate φ j₂ i₀
hj : ¬j₂ = j₂
hj' : j₂ ≤ j₂
⊢ ∃ j₁ j₂, ∃ (_ : j₁ < j₂), transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀

Proof state:
case neg.inl
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
hj : ¬j₁ = j₂
hj'✝ : j₂ ≤ j₁
hj' : j₂ < j₁
⊢ ∃ j₁ j₂, ∃ (_ : j₁ < j₂), transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀

Tactic:
exact ⟨j₂, j₁, hj', eq.symm⟩

Result:
no goals

Proof state:
case pos
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
i : I
hi : i = ⊤
⊢ i ≤ φ i

Tactic:
subst hi

Result:
case pos
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
⊢ ⊤ ≤ φ ⊤

Proof state:
case intro.intro.intro
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
hj₁ : ¬IsMax j₁
⊢ transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀

Tactic:
refine lt_of_lt_of_le (hφ' _ (this j₁)) ?_

Result:
case intro.intro.intro
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
hj₁ : ¬IsMax j₁
⊢ φ (transfiniteIterate φ j₁ i₀) ≤ transfiniteIterate φ j₂ i₀

Proof state:
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this✝ : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
this : transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀
⊢ False

Tactic:
simp only [eq, lt_self_iff_false] at this

Result:
no goals

Proof state:
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
hφ : ∀ (i : I), i ≤ φ i
H : ∃ x x_1, ∃ (_ : transfiniteIterate φ x i₀ = transfiniteIterate φ x_1 i₀), ¬x = x_1
⊢ ∃ j₁ j₂, ∃ (_ : j₁ < j₂), transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀

Tactic:
obtain ⟨j₁, j₂, eq, hj⟩ := H

Result:
case intro.intro.intro
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
hj : ¬j₁ = j₂
⊢ ∃ j₁ j₂, ∃ (_ : j₁ < j₂), transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀

Proof state:
case neg
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
i : I
hi : ¬i = ⊤
⊢ i ≤ φ i

Tactic:
exact (hφ' i hi).le

Result:
no goals

Proof state:
case intro.intro.intro
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
⊢ transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀

Tactic:
have hj₁ : ¬ IsMax j₁ := by
  simp only [not_isMax_iff]
  exact ⟨_, hj⟩

Result:
case intro.intro.intro
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
hj₁ : ¬IsMax j₁
⊢ transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀

Proof state:
case intro.intro.intro
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
⊢ ∃ j, transfiniteIterate φ j i₀ = ⊤

Tactic:
by_contra!

Result:
case intro.intro.intro
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
⊢ False