-- 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:
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 : ¬∀ ⦃a₁ a₂ : J⦄, transfiniteIterate φ a₁ i₀ = transfiniteIterate φ a₂ i₀ → a₁ = a₂
hφ : ∀ (i : I), i ≤ φ i
⊢ ∃ j₁ j₂, ∃ (_ : j₁ < j₂), transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀

Tactic:
simp only [not_forall] at H

Result:
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₀

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φ : ∀ (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₀

Tactic:
by_cases hj' : j₁ < j₂

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φ : ∀ (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₀

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₀

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φ : ∀ (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:
exact ⟨j₁, j₂, hj', eq⟩

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 : ¬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₀ ≠ ⊤
⊢ ¬IsMax j₁

Tactic:
simp only [not_isMax_iff]

Result:
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₀ ≠ ⊤
⊢ ∃ b, j₁ < b

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₀
⊢ ⊤ ≤ φ ⊤

Tactic:
rw [φtop]

Result:
no goals

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:
simp only [not_lt] at hj'

Result:
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₀

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₀ ≠ ⊤
⊢ ∃ b, j₁ < b

Tactic:
exact ⟨_, hj⟩

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 : ¬Function.Injective fun j => transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
⊢ ∃ j₁ j₂, ∃ (_ : j₁ < j₂), transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀

Tactic:
dsimp [Function.Injective] at H

Result:
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 : ¬∀ ⦃a₁ a₂ : J⦄, transfiniteIterate φ a₁ i₀ = transfiniteIterate φ a₂ i₀ → a₁ = a₂
hφ : ∀ (i : I), i ≤ φ i
⊢ ∃ j₁ j₂, ∃ (_ : j₁ < j₂), transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀

Proof state:
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₀

Tactic:
simp at hj

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₀ ≠ ⊤
⊢ False

Tactic:
suffices transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀ by
  simp only [eq, lt_self_iff_false] at this

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₀ ≠ ⊤
⊢ transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀