awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Ordinal.{u}) < (succ #α).ord ∧
    ∃ b < (succ #α).ord, (↑a : Ordinal.{u}) ≠ b ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x b
have h : ∃ b < (succ #α).ord, (↑a : Ordinal.{u}) ≠ b ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x b
Tactic: apply And.intro a.prop
-- 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
⊢ ∃ b < (succ #α).ord, (↑a : Ordinal.{u}) ≠ b ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x b
have h : (↑b : Ordinal.{u}) < (succ #α).ord ∧
  (↑a : Ordinal.{u}) ≠ (↑b : Ordinal.{u}) ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x (↑b : Ordinal.{u})
Tactic: use b.val
-- 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
⊢ (↑b : Ordinal.{u}) < (succ #α).ord ∧
    (↑a : Ordinal.{u}) ≠ (↑b : Ordinal.{u}) ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x (↑b : Ordinal.{u})
have h : (↑a : Ordinal.{u}) ≠ (↑b : Ordinal.{u}) ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x (↑b : Ordinal.{u})
Tactic: apply And.intro b.prop
-- 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 : Ordinal.{u}) ≠ (↑b : Ordinal.{u}) ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x (↑b : Ordinal.{u})
have h : (↑a : Ordinal.{u}) ≠ (↑b : Ordinal.{u})
Tactic: apply And.intro
-- 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
h : (↑a : Ordinal.{u}) ≠ (↑b : Ordinal.{u})
⊢ (↑a : Ordinal.{u}) ≠ (↑b : Ordinal.{u}) ∧ lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x (↑b : Ordinal.{u})
have h₁ : lfpApprox f x (↑a : Ordinal.{u}) = lfpApprox f x (↑b : Ordinal.{u})
Tactic: apply And.intro
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (hypothesis)
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})
⊢ False
have h_eq₁ : a = b
Tactic: rw [Subtype.coe_inj] at h_eq
Cleared hypotheses: h_eq
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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)
have rw : lfpApprox f x (a + 1) = lfpApprox f x a
Tactic: rw [mem_fixedPoints_iff, ← lfpApprox_add_one f hx]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (hypothesis)
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 c)
have H : 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)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
⊢ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (lfpApprox f x (succ #α).ord)
have 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)
Tactic: let ⟨a, ha, b, hb, hne, hf⟩ := exists_lfpApprox_eq_lfpApprox f x
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (hypothesis)
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
⊢ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (lfpApprox f x (succ #α).ord)
have x₁ : 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
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x a : α
ha : Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a
hxa : x ≤ a
i : Ordinal.{u}
⊢ lfpApprox f x i ≤ a
have ind : ∀ (i : Ordinal.{u}) (IH : ∀ y < i, lfpApprox f x y ≤ a), lfpApprox f x i ≤ a
Tactic: induction i using WellFoundedLT.induction with | ind i IH
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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
⊢ lfpApprox f x i ≤ a
have ind : x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x b) ≤ a
Tactic: rw [lfpApprox]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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
⊢ x ⊔ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x b) ≤ a
have ind : ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x b) ≤ a
Tactic: apply sup_le hxa
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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
⊢ ⨆ (b : Ordinal.{u}), ⨆ (_ : b < i), (f : (a : α) → α) (lfpApprox f x b) ≤ a
have ind : ∀ (i_1 : Ordinal.{u}) (j : i_1 < i),
  LE.le (α := α) ((f : (a : α) → α) (lfpApprox f x i_1) : α) ((f : (a : α) → α) a : α)
Tactic: rw [iSup₂_le_iff, ← ha.eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ lfpApprox f ⊥ (succ #α).ord = (lfp : (a : α →o α) → α) f
have a : lfpApprox f ⊥ (succ #α).ord ≤ (lfp : (a : α →o α) → α) f
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
a : lfpApprox f ⊥ (succ #α).ord ≤ (lfp : (a : α →o α) → α) f
⊢ lfpApprox f ⊥ (succ #α).ord = (lfp : (a : α →o α) → α) f
have a₁ : (lfp : (a : α →o α) → α) f ≤ lfpApprox f ⊥ (succ #α).ord
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), (lfp : (a : α →o α) → α) f = (↑y : α)
have h : Eq (α := α) ((lfp : (a : α →o α) → α) f : α) ((↑⊥ : α) : α)
Tactic: use ⊥
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (hypothesis)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ lfpApprox f ⊥ (succ #α).ord ≤ (lfp : (a : α →o α) → α) f
have h_lfp : ∃ (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
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h_lfp : ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), (lfp : (a : α →o α) → α) f = (↑y : α)
⊢ lfpApprox f ⊥ (succ #α).ord ≤ (lfp : (a : α →o α) → α) f
have a : ∀ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)) (h_y : (lfp : (a : α →o α) → α) f = (↑y : α)),
  lfpApprox f ⊥ (succ #α).ord ≤ (lfp : (a : α →o α) → α) f
Tactic: let ⟨y, h_y⟩ := h_lfp
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
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 : α)
⊢ lfpApprox f ⊥ (succ #α).ord ≤ (lfp : (a : α →o α) → α) f
have a : lfpApprox f ⊥ (succ #α).ord ≤ (↑y : α)
Tactic: rw [h_y]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (hypothesis)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ (lfp : (a : α →o α) → α) f ≤ lfpApprox f ⊥ (succ #α).ord
have h_fix : ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), lfpApprox f ⊥ (succ #α).ord = (↑y : α)
Tactic: have h_fix : ∃ y : fixedPoints f, lfpApprox f ⊥ (ord <| succ #α) = y := by
      simpa only [Subtype.exists, mem_fixedPoints, exists_prop, exists_eq_right'] using
        lfpApprox_ord_mem_fixedPoint f bot_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h_fix : ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), lfpApprox f ⊥ (succ #α).ord = (↑y : α)
⊢ (lfp : (a : α →o α) → α) f ≤ lfpApprox f ⊥ (succ #α).ord
have a : ∀ (x : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)) (h_x : lfpApprox f ⊥ (succ #α).ord = (↑x : α)),
  (lfp : (a : α →o α) → α) f ≤ lfpApprox f ⊥ (succ #α).ord
Tactic: let ⟨x, h_x⟩ := h_fix
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h_fix : ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), lfpApprox f ⊥ (succ #α).ord = (↑y : α)
x : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)
h_x : lfpApprox f ⊥ (succ #α).ord = (↑x : α)
⊢ (lfp : (a : α →o α) → α) f ≤ lfpApprox f ⊥ (succ #α).ord
have a : (lfp : (a : α →o α) → α) f ≤ (↑x : α)
Tactic: rw [h_x]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ Membership.mem (α := α) (Set.range (lfpApprox f ⊥)) ((lfp : (a : α →o α) → α) f : α)
have h : lfpApprox f ⊥ (succ #α).ord = (lfp : (a : α →o α) → α) f
Tactic: use ord <| succ #α
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPointApproximants (hypothesis)
Goal:
α : Type u
inst : CompleteLattice α
f g : α →o α
h : f ≤ g
⊢ gfpApprox f ≤ gfpApprox g
have this : LE.le (α := αᵒᵈ →o αᵒᵈ) ((OrderHom.dual : (a : α →o α) → αᵒᵈ →o αᵒᵈ) g : αᵒᵈ →o αᵒᵈ)
  ((OrderHom.dual : (a : α →o α) → αᵒᵈ →o αᵒᵈ) f : αᵒᵈ →o αᵒᵈ)
Tactic: have : g.dual ≤ f.dual := h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
⊢ ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1 = o
have a₁ : ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1 ≤ o
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
a₁ : ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1 ≤ o
⊢ ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1 = o
have a₂ : o ≤ ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
⊢ ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1 ≤ o
have a₁ : ∀ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) < o
Tactic: simp_rw [Ordinal.iSup_le_iff, add_one_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
⊢ o ≤ ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1
have a₁ : ∀ (b : Ordinal.{u_1}) (hb : b < o), b < ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1
Tactic: refine le_of_forall_lt fun b hb ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
b : Ordinal.{u_1}
hb : b < o
⊢ b < ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1
have a₁ : ∀ (c : (↑(Iio a) : Type (u_1 + 1))) (hc : b ≤ (↑(f c) : Ordinal.{u_1})),
  b < ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1
Tactic: obtain ⟨_, ⟨c, rfl⟩, hc : b ≤ _⟩ := hf.isCofinal_range ⟨b, hb⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
b : Ordinal.{u_1}
hb : b < o
c : (↑(Iio a) : Type (u_1 + 1))
hc : b ≤ (↑(f c) : Ordinal.{u_1})
⊢ b < ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1
have a₁ : (↑(f c) : Ordinal.{u_1}) < ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1
Tactic: apply hc.trans_lt
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
b : Ordinal.{u_1}
hb : b < o
c : (↑(Iio a) : Type (u_1 + 1))
hc : b ≤ (↑(f c) : Ordinal.{u_1})
⊢ (↑(f c) : Ordinal.{u_1}) < ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1
have a₁ : (↑(f c) : Ordinal.{u_1}) + 1 ≤ ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1
Tactic: rw [← add_one_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
⊢ o.cof.ord = a
have apply : o.cof.ord ≤ a
Tactic: apply hf.le_ord_cof.antisymm'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
⊢ o.cof.ord ≤ a
have rw : a.cof.ord ≤ a
Tactic: rw [← hf.iSup_add_one_eq, cof_iSup_Iio_add_one hf.strictMono]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
ha : 1 < a
⊢ ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) = o
have rw : IsSuccPrelimit a
Tactic: rw [← iSup_Iio_add_one hf.strictMono, hf.iSup_add_one_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
ha : 1 < a
⊢ IsSuccPrelimit a
have rw : IsSuccPrelimit o.cof.ord
Tactic: rw [← hf.ord_cof]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
ha : 1 < a
⊢ IsSuccPrelimit o.cof.ord
have apply : ℵ₀ ≤ o.cof
Tactic: apply (isSuccLimit_ord _).isSuccPrelimit
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
ha : 1 < a
⊢ ℵ₀ ≤ o.cof
have rwa : 1 < o.cof
Tactic: rwa [aleph0_le_cof_iff, ← ord_lt_ord, hf.ord_cof, ord_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
ha : 1 < a
rwa : 1 < o.cof
⊢ ℵ₀ ≤ o.cof
have rwa₁ : ord 1 < o.cof.ord
Tactic: rwa [aleph0_le_cof_iff, ← ord_lt_ord, hf.ord_cof, ord_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
ha : 1 < a
rwa : 1 < o.cof
rwa₁ : ord 1 < o.cof.ord
⊢ ℵ₀ ≤ o.cof
have rwa₂ : ord 1 < a
Tactic: rwa [aleph0_le_cof_iff, ← ord_lt_ord, hf.ord_cof, ord_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a b o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
g : (↑(Iio b) : Type (u_1 + 1)) → (↑(Iio a) : Type (u_1 + 1))
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ b ≤ o.cof.ord
have rw : a.cof.ord ≤ a
Tactic: rw [hf.ord_cof, ← hg.ord_cof]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a b o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
g : (↑(Iio b) : Type (u_1 + 1)) → (↑(Iio a) : Type (u_1 + 1))
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ IsCofinal (range (f ∘ g))
have rw : IsCofinal (f '' range g)
Tactic: rw [range_comp]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
⊢ a ≤ (g o).cof.ord
have rw : a ≤ o.cof.ord
Tactic: rw [cof_map_of_isNormal hg ho, hf.ord_cof]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
rw : a ≤ o.cof.ord
⊢ a ≤ (g o).cof.ord
have rw₁ : a ≤ a
Tactic: rw [cof_map_of_isNormal hg ho, hf.ord_cof]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (hypothesis)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
b : Ordinal.{u_1}
hb : b ∈ Iio (g o)
⊢ ∃ (y : (↑(Iio (g o)) : Type (u_1 + 1))),
    Membership.mem (γ := Set (↑(Iio (g o)) : Type (u_1 + 1)))
        (range fun (i : (↑(Iio a) : Type (u_1 + 1))) ↦
          Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) (g (↑(f i) : Ordinal.{u_1})) ⋯)
        y ∧
      Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) b hb ≤ y
have hb₁ : ∃ a' < o, b < g a'
Tactic: rw [mem_Iio, hg.lt_iff_exists_lt ho] at hb