awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ (a : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))) (b :
    (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))),
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) a =
        (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) b ∧
      a ≠ b
let :
  ∀ (a b : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1)))
    (h_fab :
      (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) a =
        (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) b)
    (h_nab : a ≠ b), ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x 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
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ (a : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))) (b :
    (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))),
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) a =
        (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) b ∧
      a ≠ b
a b : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))
h_fab :
  (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) a =
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) b
h_nab : a ≠ b
h :
  (↑a : Ordinal.{u}) < (succ #α).ord ∧
    ∃ b < (succ #α).ord, (↑a : Ordinal.{u}) ≠ b ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x b
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

Tactic:
use a.val

Premises used: Subtype.val
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ (a : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))) (b :
    (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))),
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) a =
        (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) b ∧
      a ≠ b
a b : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))
h_fab :
  (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) a =
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) b
h_nab : a ≠ b
h : ∃ b < (succ #α).ord, (↑a : Ordinal.{u}) ≠ b ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x b
⊢ (↑a : Ordinal.{u}) < (succ #α).ord ∧
    ∃ b < (succ #α).ord, (↑a : Ordinal.{u}) ≠ b ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x b

Tactic:
apply And.intro a.prop

Premises used: Subtype.prop, And.intro
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ (a : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))) (b :
    (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))),
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) a =
        (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) b ∧
      a ≠ b
a b : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))
h_fab :
  (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) a =
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) b
h_nab : a ≠ b
h :
  (↑b : Ordinal.{u}) < (succ #α).ord ∧
    (↑a : Ordinal.{u}) ≠ (↑b : Ordinal.{u}) ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x (↑b : Ordinal.{u})
⊢ ∃ b < (succ #α).ord, (↑a : Ordinal.{u}) ≠ b ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x b

Tactic:
use b.val

Premises used: Subtype.val
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ (a : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))) (b :
    (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))),
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) a =
        (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) b ∧
      a ≠ b
a b : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))
h_fab :
  (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) a =
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) b
h_nab : a ≠ b
h : (↑a : Ordinal.{u}) ≠ (↑b : Ordinal.{u}) ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x (↑b : Ordinal.{u})
⊢ (↑b : Ordinal.{u}) < (succ #α).ord ∧
    (↑a : Ordinal.{u}) ≠ (↑b : Ordinal.{u}) ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x (↑b : Ordinal.{u})

Tactic:
apply And.intro b.prop

Premises used: Subtype.prop, And.intro
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ (a : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))) (b :
    (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))),
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) a =
        (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) b ∧
      a ≠ b
a b : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))
h_fab :
  (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) a =
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) b
h_nab : a ≠ b
h : (↑a : Ordinal.{u}) ≠ (↑b : Ordinal.{u})
h₁ : lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x (↑b : Ordinal.{u})
⊢ (↑a : Ordinal.{u}) ≠ (↑b : Ordinal.{u}) ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x (↑b : Ordinal.{u})

Tactic:
apply And.intro

Premises used: And.intro
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ (a : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))) (b :
    (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))),
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) a =
        (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) b ∧
      a ≠ b
a b : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))
h_fab :
  (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) a =
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) b
h_nab : a ≠ b
h_eq : (↑a : Ordinal.{u}) = (↑b : Ordinal.{u})
⊢ a = b

Tactic:
rw [Subtype.coe_inj] at h_eq

Premises used: Subtype.coe_inj
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ (a : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))) (b :
    (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))),
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) a =
        (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) b ∧
      a ≠ b
a b : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))
h_fab :
  (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) a =
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) b
h_nab : a ≠ b
h_eq : a = b
⊢ False

Tactic:
h_nab h_eq
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ (a : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))) (b :
    (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))),
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) a =
        (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) b ∧
      a ≠ b
a b : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))
h_fab :
  (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) a =
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) b
h_nab : a ≠ b
h_eq : a = b
⊢ False

Tactic:
exact h_nab h_eq
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ (a : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))) (b :
    (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))),
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) a =
        (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) b ∧
      a ≠ b
a b : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))
h_fab :
  (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) a =
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) b
h_nab : a ≠ b
⊢ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x (↑b : Ordinal.{u})

Tactic:
h_fab

Premises used: Set.restrict
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ (a : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))) (b :
    (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))),
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) a =
        (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
          (lfpApprox f x) b ∧
      a ≠ b
a b : (↑(Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1))
h_fab :
  (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) a =
    (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord).restrict (π := fun (a : Ordinal.{u}) ↦ α)
      (lfpApprox f x) b
h_nab : a ≠ b
⊢ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x (↑b : Ordinal.{u})

Tactic:
exact h_fab
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
hx : x ≤ (f : (a : α) → α) x
hab : a < b
hac : a ≤ c
hf : lfpApprox f x a = lfpApprox f x b
rw : lfpApprox f x (a + 1) = lfpApprox f x a
⊢ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (lfpApprox f x a)

Tactic:
rw [mem_fixedPoints_iff, ← lfpApprox_add_one f hx]

Premises used: Function.mem_fixedPoints_iff, OrdinalApprox.lfpApprox_add_one
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
hx : x ≤ (f : (a : α) → α) x
hab : a < b
hac : a ≤ c
hf : lfpApprox f x a = lfpApprox f x b
⊢ lfpApprox f x (a + 1) = lfpApprox f x a

Tactic:
(lfpApprox_mono_right f).eq_of_ge_of_le
      hf (lt_add_one a).le (add_one_le_of_lt hab)

Premises used: lt_add_one, LT.lt.le, Monotone.eq_of_ge_of_le, OrdinalApprox.lfpApprox_mono_right, Order.add_one_le_of_lt
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
hx : x ≤ (f : (a : α) → α) x
hab : a < b
hac : a ≤ c
hf : lfpApprox f x a = lfpApprox f x b
⊢ lfpApprox f x (a + 1) = lfpApprox f x a

Tactic:
exact (lfpApprox_mono_right f).eq_of_ge_of_le
      hf (lt_add_one a).le (add_one_le_of_lt hab)

Premises used: lt_add_one, LT.lt.le, Monotone.eq_of_ge_of_le, OrdinalApprox.lfpApprox_mono_right, Order.add_one_le_of_lt
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
hx : x ≤ (f : (a : α) → α) x
hab : a < b
hac : a ≤ c
hf : lfpApprox f x a = lfpApprox f x b
⊢ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (lfpApprox f x a)

Tactic:
have H : lfpApprox f x a ∈ fixedPoints f := by
    rw [mem_fixedPoints_iff, ← lfpApprox_add_one f hx]
    exact (lfpApprox_mono_right f).eq_of_ge_of_le
      hf (lt_add_one a).le (add_one_le_of_lt hab)
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
hx : x ≤ (f : (a : α) → α) x
hab : a < b
hac : a ≤ c
hf : lfpApprox f x a = lfpApprox f x b
H : Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (lfpApprox f x a)
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (lfpApprox f x a)
⊢ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (lfpApprox f x c)

Tactic:
rwa [lfpApprox_eq_of_mem_fixedPoints f hac H]

Premises used: OrdinalApprox.lfpApprox_eq_of_mem_fixedPoints
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
let :
  ∀ (a : Ordinal.{u}) (ha : a < (succ #α).ord) (b : Ordinal.{u}) (hb : b < (succ #α).ord) (hne : a ≠ b)
    (hf : lfpApprox f x a = lfpApprox f x b),
    Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (lfpApprox f x (succ #α).ord)
⊢ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (lfpApprox f x (succ #α).ord)

Tactic:
let ⟨a, ha, b, hb, hne, hf⟩ := exists_lfpApprox_eq_lfpApprox f x
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
a : Ordinal.{u}
ha : a < (succ #α).ord
b : Ordinal.{u}
hb : b < (succ #α).ord
hne : a ≠ b
hf : lfpApprox f x a = lfpApprox f x b
hab : a ≤ b
⊢ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (lfpApprox f x (succ #α).ord)

Tactic:
lfpApprox_mem_fixedPoints_of_eq f hx (hne.lt_of_le hab) ha.le hf

Premises used: LT.lt.le, OrdinalApprox.lfpApprox_mem_fixedPoints_of_eq, Ne.lt_of_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
a : Ordinal.{u}
ha : a < (succ #α).ord
b : Ordinal.{u}
hb : b < (succ #α).ord
hne : a ≠ b
hf : lfpApprox f x a = lfpApprox f x b
hab : a ≤ b
⊢ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (lfpApprox f x (succ #α).ord)

Tactic:
exact lfpApprox_mem_fixedPoints_of_eq f hx (hne.lt_of_le hab) ha.le hf

Premises used: LT.lt.le, OrdinalApprox.lfpApprox_mem_fixedPoints_of_eq, Ne.lt_of_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
a : Ordinal.{u}
ha : a < (succ #α).ord
b : Ordinal.{u}
hb : b < (succ #α).ord
hne : a ≠ b
hf : lfpApprox f x a = lfpApprox f x b
hba : b ≤ a
⊢ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (lfpApprox f x (succ #α).ord)

Tactic:
lfpApprox_mem_fixedPoints_of_eq f hx (hne.symm.lt_of_le hba) hb.le hf.symm

Premises used: LT.lt.le, Ne.symm, OrdinalApprox.lfpApprox_mem_fixedPoints_of_eq, Eq.symm, Ne.lt_of_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
a : Ordinal.{u}
ha : a < (succ #α).ord
b : Ordinal.{u}
hb : b < (succ #α).ord
hne : a ≠ b
hf : lfpApprox f x a = lfpApprox f x b
hba : b ≤ a
⊢ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (lfpApprox f x (succ #α).ord)

Tactic:
exact lfpApprox_mem_fixedPoints_of_eq f hx (hne.symm.lt_of_le hba) hb.le hf.symm

Premises used: LT.lt.le, Ne.symm, OrdinalApprox.lfpApprox_mem_fixedPoints_of_eq, Eq.symm, Ne.lt_of_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
a : Ordinal.{u}
ha : a < (succ #α).ord
b : Ordinal.{u}
hb : b < (succ #α).ord
hne : a ≠ b
hf : lfpApprox f x a = lfpApprox f x b
⊢ a ≤ b ∨ b ≤ a

Tactic:
cases le_total a b with
  | inl hab => exact lfpApprox_mem_fixedPoints_of_eq f hx (hne.lt_of_le hab) ha.le hf
  | inr hba => exact lfpApprox_mem_fixedPoints_of_eq f hx (hne.symm.lt_of_le hba) hb.le hf.symm

Premises used: le_total
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x a : α
ha : Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a
hxa : x ≤ a
i : Ordinal.{u}
ind : ∀ (i : Ordinal.{u}) (IH : ∀ y < i, lfpApprox f x y ≤ a), lfpApprox f x i ≤ a
⊢ lfpApprox f x i ≤ a

Tactic:
induction i using WellFoundedLT.induction with | ind i IH

Premises used: WellFoundedLT.induction
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x a : α
ha : Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
ind : x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x b) ≤ a
⊢ lfpApprox f x i ≤ a

Tactic:
rw [lfpApprox]

Premises used: OrdinalApprox.lfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x a : α
ha : Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
ind : ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x b) ≤ a
⊢ x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x b) ≤ a

Tactic:
apply sup_le hxa

Premises used: sup_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x a : α
ha : Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
ind :
  ∀ (i_1 : Ordinal.{u}) (j : i_1 < i),
    LE.le (α := α) ((f : (a : α) → α) (lfpApprox f x i_1) : α) ((f : (a : α) → α) a : α)
⊢ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x b) ≤ a

Tactic:
rw [iSup₂_le_iff, ← ha.eq]

Premises used: Function.IsFixedPt.eq, iSup₂_le_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x a : α
ha : Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
⊢ ∀ (i_1 : Ordinal.{u}) (j : i_1 < i),
    LE.le (α := α) ((f : (a : α) → α) (lfpApprox f x i_1) : α) ((f : (a : α) → α) a : α)

Tactic:
fun y hy ↦ f.mono (IH y hy)

Premises used: OrderHom.mono
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x a : α
ha : Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
⊢ ∀ (i_1 : Ordinal.{u}) (j : i_1 < i),
    LE.le (α := α) ((f : (a : α) → α) (lfpApprox f x i_1) : α) ((f : (a : α) → α) a : α)

Tactic:
exact fun y hy ↦ f.mono (IH y hy)

Premises used: OrderHom.mono
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
a : lfpApprox f ⊥ (succ #α).ord ≤ (lfp : (a : α →o α) → α) f
a₁ : (lfp : (a : α →o α) → α) f ≤ lfpApprox f ⊥ (succ #α).ord
⊢ lfpApprox f ⊥ (succ #α).ord = (lfp : (a : α →o α) → α) f

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h : Eq (α := α) ((lfp : (a : α →o α) → α) f : α) ((↑⊥ : α) : α)
⊢ ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), (lfp : (a : α →o α) → α) f = (↑y : α)

Tactic:
use ⊥
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ Eq (α := α) ((lfp : (a : α →o α) → α) f : α) ((↑⊥ : α) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ Eq (α := α) ((lfp : (a : α →o α) → α) f : α) ((↑⊥ : α) : α)

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), (lfp : (a : α →o α) → α) f = (↑y : α)

Tactic:
have h_lfp : ∃ y : fixedPoints f, f.lfp = y := by use ⊥; exact rfl
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h_lfp : ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), (lfp : (a : α →o α) → α) f = (↑y : α)
a :
  ∀ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)) (h_y : (lfp : (a : α →o α) → α) f = (↑y : α)),
    lfpApprox f ⊥ (succ #α).ord ≤ (lfp : (a : α →o α) → α) f
⊢ lfpApprox f ⊥ (succ #α).ord ≤ (lfp : (a : α →o α) → α) f

Tactic:
let ⟨y, h_y⟩ := h_lfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h_lfp : ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), (lfp : (a : α →o α) → α) f = (↑y : α)
y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)
h_y : (lfp : (a : α →o α) → α) f = (↑y : α)
a : lfpApprox f ⊥ (succ #α).ord ≤ (↑y : α)
⊢ lfpApprox f ⊥ (succ #α).ord ≤ (lfp : (a : α →o α) → α) f

Tactic:
rw [h_y]