-- Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
theorem exists_lfpApprox_eq_lfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <| succ #α,
    a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

Tactic:
use a.val

Result:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑a < (succ #α).ord ∧ ∃ b < (succ #α).ord, ↑a ≠ b ∧ lfpApprox f x ↑a = lfpApprox f x b

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

Tactic:
have h_ninj := not_injective_limitation_set <| lfpApprox f x

Result:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj : ¬Set.InjOn (lfpApprox f x) (Set.Iio (SuccOrder.succ #α).ord)
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

Proof state:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ∃ b < (succ #α).ord, ↑a ≠ b ∧ lfpApprox f x ↑a = lfpApprox f x b

Tactic:
use b.val

Result:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑b < (succ #α).ord ∧ ↑a ≠ ↑b ∧ lfpApprox f x ↑a = lfpApprox f x ↑b

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj : ¬Set.InjOn (lfpApprox f x) (Set.Iio (SuccOrder.succ #α).ord)
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

Tactic:
rw [Set.injOn_iff_injective, Function.not_injective_iff] at h_ninj

Result:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

Proof state:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑a < (succ #α).ord ∧ ∃ b < (succ #α).ord, ↑a ≠ b ∧ lfpApprox f x ↑a = lfpApprox f x b

Tactic:
apply And.intro a.prop

Result:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ∃ b < (succ #α).ord, ↑a ≠ b ∧ lfpApprox f x ↑a = lfpApprox f x b

Proof state:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑a ≠ ↑b ∧ lfpApprox f x ↑a = lfpApprox f x ↑b

Tactic:
apply And.intro

Result:
case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑a ≠ ↑b

case h.right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ lfpApprox f x ↑a = lfpApprox f x ↑b

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

Tactic:
let ⟨a, b, h_fab, h_nab⟩ := h_ninj

Result:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

Proof state:
case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑a ≠ ↑b

Tactic:
intro h_eq

Result:
case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).restrict (lfpApprox f x) b
h_nab : a ≠ b
h_eq : ↑a = ↑b
⊢ False