awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
a₁ : a * a ^ ω * succ b ≤ a ^ ω * succ b
a₂ : a ^ (1 + ω) * succ b ≤ a ^ ω * succ b
⊢ a * (a ^ ω * succ b) ≤ a ^ ω * succ b
have a₃ : a ^ ω * succ b ≤ a ^ ω * succ b
Tactic: rw [← mul_assoc, ← opow_one_add, one_add_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * succ b ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c)
have a₁ : ∀ (d : Ordinal.{u_1}) (hd : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * d),
  a ^ ω * succ b ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c)
Tactic: obtain ⟨d, hd⟩ :=
      mul_eq_right_iff_opow_omega0_dvd.1 (nfp_fp (isNormal_mul_right ha) (a ^ ω * b + c))
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * succ b ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c)
have a₁ : a ^ ω * succ b ≤ a ^ ω * d
Tactic: rw [hd]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * succ b ≤ a ^ ω * d
have a₁ : succ b ≤ d
Tactic: apply mul_le_mul_right
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (hypothesis)
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
⊢ succ b ≤ d
have this : a ^ ω * b + c ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c)
Tactic: have := le_nfp (a * ·) (a ^ ω * b + c)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (hypothesis)
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c)
⊢ succ b ≤ d
have this₁ : a ^ ω * b + c ≤ a ^ ω * d
Tactic: rw [hd] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (hypothesis)
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ a ^ ω * d
⊢ succ b ≤ d
have this₁ : a ^ ω * b + 0 < a ^ ω * d
Tactic: have := (add_lt_add_right hc (a ^ ω * b)).trans_le this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (hypothesis)
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this_1 : a ^ ω * b + c ≤ a ^ ω * d
this : a ^ ω * b + 0 < a ^ ω * d
⊢ succ b ≤ d
have this₁ : b < d
Tactic: rw [add_zero, mul_lt_mul_iff_right₀ (opow_pos ω ha)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u}
ha : 0 < a
b : Ordinal.{u}
⊢ deriv (fun (x : Ordinal.{u}) ↦ a * x) b = a ^ ω * b
have revert : ∀ (b : Ordinal.{u}), deriv (fun (x : Ordinal.{u}) ↦ a * x) b = a ^ ω * b
Tactic: revert b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u}
ha : 0 < a
⊢ ∀ (b : Ordinal.{u}), deriv (fun (x : Ordinal.{u}) ↦ a * x) b = a ^ ω * b
have rw : deriv (fun (x : Ordinal.{u}) ↦ a * x) ⊥ = a ^ ω * ⊥ ∧
  ∀ (a_1 : Ordinal.{u}),
    deriv (fun (x : Ordinal.{u}) ↦ a * x) a_1 = a ^ ω * a_1 →
      deriv (fun (x : Ordinal.{u}) ↦ a * x) (succ a_1) = a ^ ω * succ a_1
Tactic: rw [← funext_iff,
    IsNormal.ext_iff (isNormal_deriv _) (isNormal_mul_right (opow_pos ω ha))]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun (x : Ordinal.{u}) ↦ a * x) ⊥ = a ^ ω * ⊥ ∧
    ∀ (a_1 : Ordinal.{u}),
      deriv (fun (x : Ordinal.{u}) ↦ a * x) a_1 = a ^ ω * a_1 →
        deriv (fun (x : Ordinal.{u}) ↦ a * x) (succ a_1) = a ^ ω * succ a_1
have refine_1 : deriv (fun (x : Ordinal.{u}) ↦ a * x) ⊥ = a ^ ω * ⊥
Tactic: refine ⟨?_, fun c h => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u}
ha : 0 < a
refine_1 : deriv (fun (x : Ordinal.{u}) ↦ a * x) ⊥ = a ^ ω * ⊥
⊢ deriv (fun (x : Ordinal.{u}) ↦ a * x) ⊥ = a ^ ω * ⊥ ∧
    ∀ (a_1 : Ordinal.{u}),
      deriv (fun (x : Ordinal.{u}) ↦ a * x) a_1 = a ^ ω * a_1 →
        deriv (fun (x : Ordinal.{u}) ↦ a * x) (succ a_1) = a ^ ω * succ a_1
have refine_2 : ∀ (c : Ordinal.{u}) (h : deriv (fun (x : Ordinal.{u}) ↦ a * x) c = a ^ ω * c),
  deriv (fun (x : Ordinal.{u}) ↦ a * x) (succ c) = a ^ ω * succ c
Tactic: refine ⟨?_, fun c h => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun (x : Ordinal.{u}) ↦ a * x) ⊥ = a ^ ω * ⊥
have refine_1 : deriv (fun (x : Ordinal.{u}) ↦ a * x) 0 = a ^ ω * 0
Tactic: rw [bot_eq_zero, deriv_zero_right, nfp_mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u}
ha : 0 < a
refine_1 : deriv (fun (x : Ordinal.{u}) ↦ a * x) 0 = a ^ ω * 0
⊢ deriv (fun (x : Ordinal.{u}) ↦ a * x) ⊥ = a ^ ω * ⊥
have refine_1₁ : nfp (fun (x : Ordinal.{u}) ↦ a * x) 0 = a ^ ω * 0
Tactic: rw [bot_eq_zero, deriv_zero_right, nfp_mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u}
ha : 0 < a
refine_1 : deriv (fun (x : Ordinal.{u}) ↦ a * x) 0 = a ^ ω * 0
refine_1₁ : nfp (fun (x : Ordinal.{u}) ↦ a * x) 0 = a ^ ω * 0
⊢ deriv (fun (x : Ordinal.{u}) ↦ a * x) ⊥ = a ^ ω * ⊥
have refine_1₂ : 0 = a ^ ω * 0
Tactic: rw [bot_eq_zero, deriv_zero_right, nfp_mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u}
ha : 0 < a
refine_1 : deriv (fun (x : Ordinal.{u}) ↦ a * x) 0 = a ^ ω * 0
refine_1₁ : nfp (fun (x : Ordinal.{u}) ↦ a * x) 0 = a ^ ω * 0
refine_1₂ : 0 = a ^ ω * 0
⊢ deriv (fun (x : Ordinal.{u}) ↦ a * x) ⊥ = a ^ ω * ⊥
have refine_1₃ : Eq.{u + 2} (α := Ordinal.{u}) 0 0
Tactic: rw [bot_eq_zero, deriv_zero_right, nfp_mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun (x : Ordinal.{u}) ↦ a * x) c = a ^ ω * c
⊢ deriv (fun (x : Ordinal.{u}) ↦ a * x) (succ c) = a ^ ω * succ c
have refine_2 : nfp (fun (x : Ordinal.{u}) ↦ a * x) (succ (a ^ ω * c)) = a ^ ω * succ c
Tactic: rw [deriv_succ, h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (hypothesis)
Goal:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (@succ _ PartialOrder.toPreorder _ #α).ord)
⊢ False
have h : 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
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (hypothesis)
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} #α
⊢ False
have mk_initialSeg_subtype : #(↑(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 #α)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (hypothesis)
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 _ #α)
⊢ False
have h₁ : @succ _ PartialOrder.toPreorder _ #α ≤ #α
Tactic: rw [mk_initialSeg_subtype, lift_lift, lift_le] at h
Cleared hypotheses: h, mk_initialSeg_subtype
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a ≤ b
⊢ lfpApprox f x a ≤ lfpApprox f x b
have 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)
Tactic: rw [lfpApprox, lfpApprox]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a ≤ b
⊢ 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)
have 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') : α)
Tactic: apply sup_le_sup_left (iSup₂_mono' _)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
⊢ lfpApprox f x 0 = x
have rw : x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < 0), (f : (a : α) → α) (lfpApprox f x b) = x
Tactic: rw [lfpApprox]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
⊢ x ≤ lfpApprox f x a
have rw : x ≤ x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < a), (f : (a : α) → α) (lfpApprox f x b)
Tactic: rw [lfpApprox]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a < b
⊢ (f : (a : α) → α) (lfpApprox f x a) ≤ lfpApprox f x b
have nth_rw : (f : (a : α) → α) (lfpApprox f x a) ≤ x ⊔ ⨆ (b_1 : Ordinal.{u}), ⨆ (_ : b_1 < b), (f : (a : α) → α) (lfpApprox f x b_1)
Tactic: nth_rw 2 [lfpApprox]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
a : Ordinal.{u}
⊢ lfpApprox f x (a + 1) = (f : (a : α) → α) (lfpApprox f x a)
have apply : 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'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
a : Ordinal.{u}
⊢ lfpApprox f x (a + 1) ≤ (f : (a : α) → α) (lfpApprox f x a)
have rw : x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < a + 1), (f : (a : α) → α) (lfpApprox f x b) ≤ (f : (a : α) → α) (lfpApprox f x a)
Tactic: rw [lfpApprox]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
a : Ordinal.{u}
⊢ x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < a + 1), (f : (a : α) → α) (lfpApprox f x b) ≤ (f : (a : α) → α) (lfpApprox f x a)
have apply : LE.le (α := α) (⨆ (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))
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ lfpApprox f x a = ⨆ (b : (↑(Set.Iio a) : Type (u + 1))), lfpApprox f x (↑b : Ordinal.{u})
have apply : 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'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ lfpApprox f x a ≤ ⨆ (b : (↑(Set.Iio a) : Type (u + 1))), lfpApprox f x (↑b : Ordinal.{u})
have 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}))
Tactic: rw [lfpApprox, sup_le_iff, iSup_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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}) ∧
    ∀ (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}))
have left : x ≤ ⨆ (b : (↑(Set.Iio a) : Type (u + 1))), lfpApprox f x (↑b : Ordinal.{u})
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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})
⊢ 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}))
have 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}))
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
a : Ordinal.{u}
⊢ lfpApprox f x a ≤ lfpApprox g x a
have ind : ∀ (i : Ordinal.{u}) (IH : ∀ y < i, lfpApprox f x y ≤ lfpApprox g x y), lfpApprox f x i ≤ lfpApprox g x i
Tactic: induction a using WellFoundedLT.induction with | ind i IH
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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
⊢ lfpApprox f x i ≤ lfpApprox g x i
have 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)
Tactic: rw [lfpApprox, lfpApprox]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
a : Ordinal.{u}
⊢ lfpApprox f x₁ a ≤ lfpApprox f x₂ a
have ind : ∀ (i : Ordinal.{u}) (IH : ∀ y < i, lfpApprox f x₁ y ≤ lfpApprox f x₂ y), lfpApprox f x₁ i ≤ lfpApprox f x₂ i
Tactic: induction a using WellFoundedLT.induction with | ind i IH
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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
⊢ lfpApprox f x₁ i ≤ lfpApprox f x₂ i
have 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)
Tactic: rw [lfpApprox, lfpApprox]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (hypothesis)
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)
⊢ lfpApprox f x b = lfpApprox f x a
have hf₁ : (f : (a : α) → α) (lfpApprox f x a) = lfpApprox f x a
Tactic: rw [mem_fixedPoints_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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
⊢ lfpApprox f x b = lfpApprox f x a
have 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
Tactic: induction b using WellFoundedLT.induction with | ind b IH
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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
⊢ lfpApprox f x b = lfpApprox f x a
have ind : lfpApprox f x b ≤ lfpApprox f x a
Tactic: apply (lfpApprox_mono_right f hab).antisymm'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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
⊢ lfpApprox f x b ≤ lfpApprox f x a
have ind : x ⊔ ⨆ (b_2 : Ordinal.{u}), ⨆ (_ : b_2 < b), (f : (a : α) → α) (lfpApprox f x b_2) ≤ lfpApprox f x a
Tactic: rw [lfpApprox]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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
⊢ x ⊔ ⨆ (b_2 : Ordinal.{u}), ⨆ (_ : b_2 < b), (f : (a : α) → α) (lfpApprox f x b_2) ≤ lfpApprox f x a
have ind : ⨆ (b_2 : Ordinal.{u}), ⨆ (_ : b_2 < b), (f : (a : α) → α) (lfpApprox f x b_2) ≤ lfpApprox f x a
Tactic: apply sup_le (le_lfpApprox ..)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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
⊢ ⨆ (b_2 : Ordinal.{u}), ⨆ (_ : b_2 < b), (f : (a : α) → α) (lfpApprox f x b_2) ≤ lfpApprox f x a
have ind : ∀ (i : Ordinal.{u}) (j : i < b), (f : (a : α) → α) (lfpApprox f x i) ≤ lfpApprox f x a
Tactic: rw [iSup₂_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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
⊢ (f : (a : α) → α) (lfpApprox f x i) ≤ lfpApprox f x a
have pos : ∀ (hi' : i < a), (f : (a : α) → α) (lfpApprox f x i) ≤ lfpApprox f x a
Tactic: by_cases! hi' : i < a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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
⊢ (f : (a : α) → α) (lfpApprox f x i) ≤ lfpApprox f x a
have neg : ∀ (hi' : a ≤ i), (f : (a : α) → α) (lfpApprox f x i) ≤ lfpApprox f x a
Tactic: by_cases! hi' : i < a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (hypothesis)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b
have h_ninj : ¬Set.InjOn (lfpApprox f x) (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord)
Tactic: have h_ninj := not_injective_limitation_set <| lfpApprox f x
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (hypothesis)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
h_ninj : ¬Set.InjOn (lfpApprox f x) (Set.Iio (@SuccOrder.succ _ PartialOrder.toPreorder _ #α).ord)
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b
have 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
Tactic: rw [Set.injOn_iff_injective, Function.not_injective_iff] at h_ninj
Cleared hypotheses: h_ninj
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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 < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b
have 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
Tactic: let ⟨a, b, h_fab, h_nab⟩ := h_ninj
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b
have h : (↑a : Ordinal.{u}) < (succ #α).ord ∧
  ∃ b < (succ #α).ord, (↑a : Ordinal.{u}) ≠ b ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x b
Tactic: use a.val