awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun (x : Ordinal.{u}) ↦ a * x) c = a ^ ω * c
⊢ nfp (fun (x : Ordinal.{u}) ↦ a * x) (succ (a ^ ω * c)) = a ^ ω * succ c

Tactic:
exact nfp_mul_opow_omega0_add c ha zero_lt_one (one_le_iff_pos.2 (opow_pos _ ha))

Premises used: Iff.mpr, Ordinal.nfp_mul_opow_omega0_add, zero_lt_one, Ordinal.opow_pos, Order.one_le_iff_pos
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (@succ _ PartialOrder.toPreorder _ #α).ord)
⊢ lift.{u, u + 1} #(↑(Iio (@succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1)) ≤ lift.{u + 1, u} #α

Tactic:
have h := lift_mk_le_lift_mk_of_injective <| injOn_iff_injective.1 h_inj
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (@succ _ PartialOrder.toPreorder _ #α).ord)
h : lift.{u, u + 1} #(↑(Iio (@succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1)) ≤ lift.{u + 1, u} #α
⊢ #(↑(Iio (@succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1)) =
    lift.{u + 1, u} (@succ _ PartialOrder.toPreorder _ #α)

Tactic:
simpa only [coe_setOf, card_typein, card_ord] using mk_Iio_ordinal (ord <| succ #α)

Premises used: SuccOrder.succ, Cardinal.mk, Cardinal.mk_Iio_ordinal, Cardinal.ord, Ordinal.card_typein, Cardinal.card_ord, Set.coe_setOf
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (@succ _ PartialOrder.toPreorder _ #α).ord)
h : lift.{u, u + 1} #(↑(Iio (@succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1)) ≤ lift.{u + 1, u} #α
⊢ #(↑(Iio (@succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1)) =
    lift.{u + 1, u} (@succ _ PartialOrder.toPreorder _ #α)

Tactic:
have mk_initialSeg_subtype :
      #(Iio (ord <| succ #α)) = lift.{u + 1} (succ #α) := by
    simpa only [coe_setOf, card_typein, card_ord] using mk_Iio_ordinal (ord <| succ #α)
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (@succ _ PartialOrder.toPreorder _ #α).ord)
h : lift.{u, u + 1} #(↑(Iio (@succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1)) ≤ lift.{u + 1, u} #α
mk_initialSeg_subtype :
  #(↑(Iio (@succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1)) =
    lift.{u + 1, u} (@succ _ PartialOrder.toPreorder _ #α)
⊢ @succ _ PartialOrder.toPreorder _ #α ≤ #α

Tactic:
rw [mk_initialSeg_subtype, lift_lift, lift_le] at h

Premises used: Cardinal.lift_lift, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (@succ _ PartialOrder.toPreorder _ #α).ord)
h : lift.{u, u + 1} #(↑(Iio (@succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1)) ≤ lift.{u + 1, u} #α
mk_initialSeg_subtype :
  #(↑(Iio (@succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1)) =
    lift.{u + 1, u} (@succ _ PartialOrder.toPreorder _ #α)
h₁ : @succ _ PartialOrder.toPreorder _ #α ≤ #α
⊢ #(↑(Iio (@succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1)) =
    lift.{u + 1, u} (@succ _ PartialOrder.toPreorder _ #α)

Tactic:
rw [mk_initialSeg_subtype, lift_lift, lift_le] at h

Premises used: Cardinal.lift_lift, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (@succ _ PartialOrder.toPreorder _ #α).ord)
h : @succ _ PartialOrder.toPreorder _ #α ≤ #α
mk_initialSeg_subtype :
  #(↑(Iio (@succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1)) =
    lift.{u + 1, u} (@succ _ PartialOrder.toPreorder _ #α)
⊢ False

Tactic:
not_le_of_gt (Order.lt_succ #α) h

Premises used: Cardinal.mk, Order.lt_succ, not_le_of_gt
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (@succ _ PartialOrder.toPreorder _ #α).ord)
h : @succ _ PartialOrder.toPreorder _ #α ≤ #α
mk_initialSeg_subtype :
  #(↑(Iio (@succ _ PartialOrder.toPreorder _ #α).ord) : Type (u + 1)) =
    lift.{u + 1, u} (@succ _ PartialOrder.toPreorder _ #α)
⊢ False

Tactic:
exact not_le_of_gt (Order.lt_succ #α) h

Premises used: Cardinal.mk, Order.lt_succ, not_le_of_gt
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a ≤ b
rw :
  x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < a), (f : (a : α) → α) (lfpApprox f x b) ≤
    x ⊔ ⨆ (b_1 : Ordinal.{u}), ⨆ (_ : b_1 < b), (f : (a : α) → α) (lfpApprox f x b_1)
⊢ lfpApprox f x a ≤ lfpApprox f x b

Tactic:
rw [lfpApprox, lfpApprox]

Premises used: OrdinalApprox.lfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a ≤ b
apply :
  ∀ (i : Ordinal.{u}) (j : i < a),
    ∃ (i' : Ordinal.{u}) (_ : i' < b),
      LE.le (α := α) ((f : (a : α) → α) (lfpApprox f x i) : α) ((f : (a : α) → α) (lfpApprox f x i') : α)
⊢ x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < a), (f : (a : α) → α) (lfpApprox f x b) ≤
    x ⊔ ⨆ (b_1 : Ordinal.{u}), ⨆ (_ : b_1 < b), (f : (a : α) → α) (lfpApprox f x b_1)

Tactic:
apply sup_le_sup_left (iSup₂_mono' _)

Premises used: sup_le_sup_left, iSup₂_mono'
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a ≤ b
⊢ ∀ (i : Ordinal.{u}) (j : i < a),
    ∃ (i' : Ordinal.{u}) (_ : i' < b),
      LE.le (α := α) ((f : (a : α) → α) (lfpApprox f x i) : α) ((f : (a : α) → α) (lfpApprox f x i') : α)

Tactic:
grind
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
rw : x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < 0), (f : (a : α) → α) (lfpApprox f x b) = x
⊢ lfpApprox f x 0 = x

Tactic:
rw [lfpApprox]

Premises used: OrdinalApprox.lfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
⊢ x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < 0), (f : (a : α) → α) (lfpApprox f x b) = x

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
rw : x ≤ x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < a), (f : (a : α) → α) (lfpApprox f x b)
⊢ x ≤ lfpApprox f x a

Tactic:
rw [lfpApprox]

Premises used: OrdinalApprox.lfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
⊢ x ≤ x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < a), (f : (a : α) → α) (lfpApprox f x b)

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
⊢ x ≤ x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < a), (f : (a : α) → α) (lfpApprox f x b)

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a < b
nth_rw :
  (f : (a : α) → α) (lfpApprox f x a) ≤
    x ⊔ ⨆ (b_1 : Ordinal.{u}), ⨆ (_ : b_1 < b), (f : (a : α) → α) (lfpApprox f x b_1)
⊢ (f : (a : α) → α) (lfpApprox f x a) ≤ lfpApprox f x b

Tactic:
nth_rw 2 [lfpApprox]

Premises used: OrdinalApprox.lfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a < b
⊢ (f : (a : α) → α) (lfpApprox f x a) ≤
    x ⊔ ⨆ (b_1 : Ordinal.{u}), ⨆ (_ : b_1 < b), (f : (a : α) → α) (lfpApprox f x b_1)

Tactic:
le_sup_of_le_right <| le_iSup₂_of_le a h le_rfl

Premises used: le_rfl, le_sup_of_le_right, le_iSup₂_of_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a < b
⊢ (f : (a : α) → α) (lfpApprox f x a) ≤
    x ⊔ ⨆ (b_1 : Ordinal.{u}), ⨆ (_ : b_1 < b), (f : (a : α) → α) (lfpApprox f x b_1)

Tactic:
exact le_sup_of_le_right <| le_iSup₂_of_le a h le_rfl

Premises used: le_rfl, le_sup_of_le_right, le_iSup₂_of_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
a : Ordinal.{u}
apply : lfpApprox f x (a + 1) ≤ (f : (a : α) → α) (lfpApprox f x a)
⊢ lfpApprox f x (a + 1) = (f : (a : α) → α) (lfpApprox f x a)

Tactic:
apply (apply_lfpApprox_le_lfpApprox_of_lt f (lt_add_one a)).antisymm'

Premises used: LE.le.antisymm', lt_add_one, OrdinalApprox.apply_lfpApprox_le_lfpApprox_of_lt
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
a : Ordinal.{u}
rw :
  x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < a + 1), (f : (a : α) → α) (lfpApprox f x b) ≤ (f : (a : α) → α) (lfpApprox f x a)
⊢ lfpApprox f x (a + 1) ≤ (f : (a : α) → α) (lfpApprox f x a)

Tactic:
rw [lfpApprox]

Premises used: OrdinalApprox.lfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
a : Ordinal.{u}
apply :
  LE.le (α := α) (⨆ (b : Ordinal.{u}), ⨆ (_ : b < a + 1), (f : (a : α) → α) (lfpApprox f x b) : α)
    ((f : (a : α) → α) (lfpApprox f x a) : α)
⊢ x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < a + 1), (f : (a : α) → α) (lfpApprox f x b) ≤ (f : (a : α) → α) (lfpApprox f x a)

Tactic:
apply sup_le <| hx.trans (f.mono (le_lfpApprox f))

Premises used: OrderHom.mono, sup_le, LE.le.trans, OrdinalApprox.le_lfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
a : Ordinal.{u}
⊢ LE.le (α := α) (⨆ (b : Ordinal.{u}), ⨆ (_ : b < a + 1), (f : (a : α) → α) (lfpApprox f x b) : α)
    ((f : (a : α) → α) (lfpApprox f x a) : α)

Tactic:
simpa using fun i h ↦ f.monotone.comp (lfpApprox_mono_right f) h

Premises used: OrderHom.monotone, Monotone.comp, OrdinalApprox.lfpApprox_mono_right
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
apply : lfpApprox f x a ≤ ⨆ (b : (↑(Set.Iio a) : Type (u + 1))), lfpApprox f x (↑b : Ordinal.{u})
⊢ lfpApprox f x a = ⨆ (b : (↑(Set.Iio a) : Type (u + 1))), lfpApprox f x (↑b : Ordinal.{u})

Tactic:
apply (iSup_le fun b => lfpApprox_mono_right f b.2.le).antisymm'

Premises used: LE.le.antisymm', iSup_le, OrdinalApprox.lfpApprox_mono_right
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
rw :
  x ≤ ⨆ (b : (↑(Set.Iio a) : Type (u + 1))), lfpApprox f x (↑b : Ordinal.{u}) ∧
    ∀ (i : Ordinal.{u}),
      LE.le.{u} (α := α) (⨆ (_ : i < a), (f : (a : α) → α) (lfpApprox f x i))
        (⨆ (b : (↑(Set.Iio a) : Type (u + 1))), lfpApprox f x (↑b : Ordinal.{u}))
⊢ lfpApprox f x a ≤ ⨆ (b : (↑(Set.Iio a) : Type (u + 1))), lfpApprox f x (↑b : Ordinal.{u})

Tactic:
rw [lfpApprox, sup_le_iff, iSup_le_iff]

Premises used: OrdinalApprox.lfpApprox, sup_le_iff, iSup_le_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
left : x ≤ ⨆ (b : (↑(Set.Iio a) : Type (u + 1))), lfpApprox f x (↑b : Ordinal.{u})
right :
  ∀ (i : Ordinal.{u}),
    LE.le.{u} (α := α) (⨆ (_ : i < a), (f : (a : α) → α) (lfpApprox f x i))
      (⨆ (b : (↑(Set.Iio a) : Type (u + 1))), lfpApprox f x (↑b : Ordinal.{u}))
⊢ x ≤ ⨆ (b : (↑(Set.Iio a) : Type (u + 1))), lfpApprox f x (↑b : Ordinal.{u}) ∧
    ∀ (i : Ordinal.{u}),
      LE.le.{u} (α := α) (⨆ (_ : i < a), (f : (a : α) → α) (lfpApprox f x i))
        (⨆ (b : (↑(Set.Iio a) : Type (u + 1))), lfpApprox f x (↑b : Ordinal.{u}))

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ x ≤
    lfpApprox f x
      (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio a) 0 ⋯ : { x : Ordinal.{u} // x ∈ Set.Iio a }) :
        Ordinal.{u})

Tactic:
simp [lfpApprox_zero]

Premises used: OrdinalApprox.lfpApprox_zero
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ x ≤ ⨆ (b : (↑(Set.Iio a) : Type (u + 1))), lfpApprox f x (↑b : Ordinal.{u})

Tactic:
refine le_iSup_of_le ⟨0, ha.bot_lt⟩ (by simp [lfpApprox_zero])

Premises used: le_iSup_of_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
b : Ordinal.{u}
hab : b < a
⊢ (f : (a : α) → α) (lfpApprox f x b) ≤
    lfpApprox f x (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio a) (b + 1) ⋯) : Ordinal.{u})

Tactic:
simpa using apply_lfpApprox_le_lfpApprox_of_lt f (lt_add_one b)

Premises used: lt_add_one, OrdinalApprox.apply_lfpApprox_le_lfpApprox_of_lt
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ ∀ (i : Ordinal.{u}),
    LE.le.{u} (α := α) (⨆ (_ : i < a), (f : (a : α) → α) (lfpApprox f x i))
      (⨆ (b : (↑(Set.Iio a) : Type (u + 1))), lfpApprox f x (↑b : Ordinal.{u}))

Tactic:
exact fun b => iSup_mono' fun hab => ⟨⟨b + 1, ha.succ_lt hab⟩, (by
    simpa using apply_lfpApprox_le_lfpApprox_of_lt f (lt_add_one b))⟩

Premises used: iSup_mono', Exists.intro
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
a : Ordinal.{u}
ind : ∀ (i : Ordinal.{u}) (IH : ∀ y < i, lfpApprox f x y ≤ lfpApprox g x y), lfpApprox f x i ≤ lfpApprox g x i
⊢ lfpApprox f x a ≤ lfpApprox g x a

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

Premises used: WellFoundedLT.induction
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ lfpApprox g x y
ind :
  x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x b) ≤
    x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (g : (a : α) → α) (lfpApprox g x b)
⊢ lfpApprox f x i ≤ lfpApprox g x i

Tactic:
rw [lfpApprox, lfpApprox]

Premises used: OrdinalApprox.lfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ lfpApprox g x y
⊢ x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x b) ≤
    x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (g : (a : α) → α) (lfpApprox g x b)

Tactic:
sup_le_sup_left (iSup₂_mono fun j hj ↦ (f.mono (IH j hj)).trans (h _)) _

Premises used: sup_le_sup_left, iSup₂_mono, OrdinalApprox.lfpApprox, OrderHom.mono, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ lfpApprox g x y
⊢ x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x b) ≤
    x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (g : (a : α) → α) (lfpApprox g x b)

Tactic:
exact sup_le_sup_left (iSup₂_mono fun j hj ↦ (f.mono (IH j hj)).trans (h _)) _

Premises used: sup_le_sup_left, iSup₂_mono, OrdinalApprox.lfpApprox, OrderHom.mono, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
a : Ordinal.{u}
ind : ∀ (i : Ordinal.{u}) (IH : ∀ y < i, lfpApprox f x₁ y ≤ lfpApprox f x₂ y), lfpApprox f x₁ i ≤ lfpApprox f x₂ i
⊢ lfpApprox f x₁ a ≤ lfpApprox f x₂ a

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

Premises used: WellFoundedLT.induction
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x₁ y ≤ lfpApprox f x₂ y
ind :
  x₁ ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x₁ b) ≤
    x₂ ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x₂ b)
⊢ lfpApprox f x₁ i ≤ lfpApprox f x₂ i

Tactic:
rw [lfpApprox, lfpApprox]

Premises used: OrdinalApprox.lfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x₁ y ≤ lfpApprox f x₂ y
⊢ x₁ ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x₁ b) ≤
    x₂ ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x₂ b)

Tactic:
sup_le_sup h <| iSup₂_mono fun j hj ↦ f.mono (IH j hj)

Premises used: sup_le_sup, iSup₂_mono, OrderHom.mono
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x₁ y ≤ lfpApprox f x₂ y
⊢ x₁ ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x₁ b) ≤
    x₂ ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x₂ b)

Tactic:
exact sup_le_sup h <| iSup₂_mono fun j hj ↦ f.mono (IH j hj)

Premises used: sup_le_sup, iSup₂_mono, OrderHom.mono
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
hab : a ≤ b
hf : Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (lfpApprox f x a)
⊢ (f : (a : α) → α) (lfpApprox f x a) = lfpApprox f x a

Tactic:
rw [mem_fixedPoints_iff] at hf

Premises used: Function.mem_fixedPoints_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
hab : a ≤ b
hf : (f : (a : α) → α) (lfpApprox f x a) = lfpApprox f x a
ind :
  ∀ (b : Ordinal.{u}) (IH : ∀ y < b, ∀ (hab : a ≤ y), lfpApprox f x y = lfpApprox f x a) (hab : a ≤ b),
    lfpApprox f x b = lfpApprox f x a
⊢ lfpApprox f x b = lfpApprox f x a

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

Premises used: WellFoundedLT.induction
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b_1 : Ordinal.{u}
hf : (f : (a : α) → α) (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, ∀ (hab : a ≤ y), lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
ind : lfpApprox f x b ≤ lfpApprox f x a
⊢ lfpApprox f x b = lfpApprox f x a

Tactic:
apply (lfpApprox_mono_right f hab).antisymm'

Premises used: LE.le.antisymm', OrdinalApprox.lfpApprox_mono_right
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b_1 : Ordinal.{u}
hf : (f : (a : α) → α) (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, ∀ (hab : a ≤ y), lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
ind : x ⊔ ⨆ (b_2 : Ordinal.{u}), ⨆ (_ : b_2 < b), (f : (a : α) → α) (lfpApprox f x b_2) ≤ lfpApprox f x a
⊢ lfpApprox f x b ≤ lfpApprox f x a

Tactic:
rw [lfpApprox]

Premises used: OrdinalApprox.lfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b_1 : Ordinal.{u}
hf : (f : (a : α) → α) (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, ∀ (hab : a ≤ y), lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
ind : ⨆ (b_2 : Ordinal.{u}), ⨆ (_ : b_2 < b), (f : (a : α) → α) (lfpApprox f x b_2) ≤ lfpApprox f x a
⊢ x ⊔ ⨆ (b_2 : Ordinal.{u}), ⨆ (_ : b_2 < b), (f : (a : α) → α) (lfpApprox f x b_2) ≤ lfpApprox f x a

Tactic:
apply sup_le (le_lfpApprox ..)

Premises used: sup_le, OrdinalApprox.le_lfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b_1 : Ordinal.{u}
hf : (f : (a : α) → α) (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, ∀ (hab : a ≤ y), lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
ind : ∀ (i : Ordinal.{u}) (j : i < b), (f : (a : α) → α) (lfpApprox f x i) ≤ lfpApprox f x a
⊢ ⨆ (b_2 : Ordinal.{u}), ⨆ (_ : b_2 < b), (f : (a : α) → α) (lfpApprox f x b_2) ≤ lfpApprox f x a

Tactic:
rw [iSup₂_le_iff]

Premises used: iSup₂_le_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b_1 : Ordinal.{u}
hf : (f : (a : α) → α) (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, ∀ (hab : a ≤ y), lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
i : Ordinal.{u}
hi : i < b
pos : ∀ (hi' : i < a), (f : (a : α) → α) (lfpApprox f x i) ≤ lfpApprox f x a
neg : ∀ (hi' : a ≤ i), (f : (a : α) → α) (lfpApprox f x i) ≤ lfpApprox f x a
⊢ (f : (a : α) → α) (lfpApprox f x i) ≤ lfpApprox f x a

Tactic:
by_cases! hi' : i < a
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b_1 : Ordinal.{u}
hf : (f : (a : α) → α) (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, ∀ (hab : a ≤ y), lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
i : Ordinal.{u}
hi : i < b
hi' : i < a
⊢ (f : (a : α) → α) (lfpApprox f x i) ≤ lfpApprox f x a

Tactic:
apply_lfpApprox_le_lfpApprox_of_lt f hi'

Premises used: OrdinalApprox.apply_lfpApprox_le_lfpApprox_of_lt
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b_1 : Ordinal.{u}
hf : (f : (a : α) → α) (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, ∀ (hab : a ≤ y), lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
i : Ordinal.{u}
hi : i < b
hi' : i < a
⊢ (f : (a : α) → α) (lfpApprox f x i) ≤ lfpApprox f x a

Tactic:
exact apply_lfpApprox_le_lfpApprox_of_lt f hi'

Premises used: OrdinalApprox.apply_lfpApprox_le_lfpApprox_of_lt
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b_1 : Ordinal.{u}
hf : (f : (a : α) → α) (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, ∀ (hab : a ≤ y), lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
i : Ordinal.{u}
hi : i < b
hi' : a ≤ i
⊢ (f : (a : α) → α) (lfpApprox f x i) ≤ lfpApprox f x a

Tactic:
simp [IH i hi hi', hf]
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
⊢ ¬Set.InjOn (lfpApprox f x) (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord)

Tactic:
have h_ninj := not_injective_limitation_set <| lfpApprox f x
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
h_ninj : ¬Set.InjOn (lfpApprox f x) (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord)
⊢ ∃ (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

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

Premises used: Set.injOn_iff_injective, Function.not_injective_iff