awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
x : Cardinal.{max u_1 v}
⊢ Membership.mem (γ := Set Cardinal.{max u_1 v})
      (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1}))) x ↔
    Membership.mem (γ := Set Cardinal.{max u_1 v})
      (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
      x
have isSuccPrelimit : Membership.mem (γ := Set Cardinal.{max u_1 v})
    (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1}))) x →
  Membership.mem (γ := Set Cardinal.{max u_1 v})
    (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v})) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
x : Cardinal.{max u_1 v}
isSuccPrelimit :
  Membership.mem (γ := Set Cardinal.{max u_1 v})
      (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1}))) x →
    Membership.mem (γ := Set Cardinal.{max u_1 v})
      (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
      x
⊢ Membership.mem (γ := Set Cardinal.{max u_1 v})
      (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1}))) x ↔
    Membership.mem (γ := Set Cardinal.{max u_1 v})
      (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
      x
have isSuccPrelimit₁ : Membership.mem (γ := Set Cardinal.{max u_1 v})
    (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
    x →
  Membership.mem (γ := Set Cardinal.{max u_1 v})
    (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1}))) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi : i ∈ Iio o
⊢ Membership.mem (γ := Set Cardinal.{max u_1 v})
    (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
    ((fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o) i hi))
have isSuccPrelimit : Ordinal.lift.{v, u_1} i ∈ Iio (Ordinal.lift.{v, u_1} o)
Tactic: refine ⟨⟨i.lift, ?_⟩, (IH _ hi).symm⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{max u_1 v}
hi : i ∈ Iio (Ordinal.lift.{v, u_1} o)
⊢ Membership.mem (γ := Set Cardinal.{max u_1 v})
    (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
    ((fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
      (Subtype.mk (p := fun (x : Ordinal.{max u_1 v}) ↦ x ∈ Iio (Ordinal.lift.{v, u_1} o)) i hi))
have isSuccPrelimit : ∀ (i : Ordinal.{u_1}) (hi : Ordinal.lift.{v, u_1} i ∈ Iio (Ordinal.lift.{v, u_1} o)),
  Membership.mem (γ := Set Cardinal.{max u_1 v})
    (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
    ((fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
      (Subtype.mk (p := fun (x : Ordinal.{max u_1 v}) ↦ x ∈ Iio (Ordinal.lift.{v, u_1} o)) (Ordinal.lift.{v, u_1} i)
        hi))
Tactic: obtain ⟨i, rfl⟩ := Ordinal.mem_range_lift_of_le hi.le
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (hypothesis)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi : Ordinal.lift.{v, u_1} i ∈ Iio (Ordinal.lift.{v, u_1} o)
⊢ Membership.mem (γ := Set Cardinal.{max u_1 v})
    (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
    ((fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
      (Subtype.mk (p := fun (x : Ordinal.{max u_1 v}) ↦ x ∈ Iio (Ordinal.lift.{v, u_1} o)) (Ordinal.lift.{v, u_1} i)
        hi))
have hi₁ : i < o
Tactic: rw [mem_Iio, Ordinal.lift_lt] at hi
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)
have succ : ∀ (o : Ordinal.{u_1}),
  ¬IsMax o →
    ∀ (IH : lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)),
      lift.{v, u_1} (preBeth (succ o)) = preBeth (Ordinal.lift.{v, u_1} (succ o))
Tactic: induction o using SuccOrder.prelimitRecOn with
  | succ o _ IH => simp [IH]
  | isSuccPrelimit o ho IH =>
    rw [preBeth_limit ho, preBeth_limit (isSuccPrelimit_lift.2 ho), lift_iSup bddAbove_of_small]
    apply congrArg sSup
    ext x
    constructor <;> rintro ⟨⟨i, hi⟩, rfl⟩
    · refine ⟨⟨i.lift, ?_⟩, (IH _ hi).symm⟩
      simpa
    · obtain ⟨i, rfl⟩ := Ordinal.mem_range_lift_of_le hi.le
      rw [mem_Iio, Ordinal.lift_lt] at hi
      exact ⟨⟨i, hi⟩, IH _ hi⟩
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
succ :
  ∀ (o : Ordinal.{u_1}),
    ¬IsMax o →
      ∀ (IH : lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)),
        lift.{v, u_1} (preBeth (Order.succ o)) = preBeth (Ordinal.lift.{v, u_1} (Order.succ o))
⊢ lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)
have isSuccPrelimit : ∀ (o : Ordinal.{u_1}) (ho : IsSuccPrelimit o)
  (IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)),
  lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)
Tactic: induction o using SuccOrder.prelimitRecOn with
  | succ o _ IH => simp [IH]
  | isSuccPrelimit o ho IH =>
    rw [preBeth_limit ho, preBeth_limit (isSuccPrelimit_lift.2 ho), lift_iSup bddAbove_of_small]
    apply congrArg sSup
    ext x
    constructor <;> rintro ⟨⟨i, hi⟩, rfl⟩
    · refine ⟨⟨i.lift, ?_⟩, (IH _ hi).symm⟩
      simpa
    · obtain ⟨i, rfl⟩ := Ordinal.mem_range_lift_of_le hi.le
      rw [mem_Iio, Ordinal.lift_lt] at hi
      exact ⟨⟨i, hi⟩, IH _ hi⟩
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ IsStrongLimit.{u_1} (ℶ_ o) ↔ IsSuccPrelimit o
have rw : IsStrongLimit.{u_1} (preBeth (ω + o)) ↔ IsSuccPrelimit o
Tactic: rw [beth_eq_preBeth, isStrongLimit_preBeth, isSuccLimit_add_iff_of_isSuccLimit isSuccLimit_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
rw : IsStrongLimit.{u_1} (preBeth (ω + o)) ↔ IsSuccPrelimit o
⊢ IsStrongLimit.{u_1} (ℶ_ o) ↔ IsSuccPrelimit o
have rw₁ : IsSuccLimit (ω + o) ↔ IsSuccPrelimit o
Tactic: rw [beth_eq_preBeth, isStrongLimit_preBeth, isSuccLimit_add_iff_of_isSuccLimit isSuccLimit_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
rw : IsStrongLimit.{u_1} (preBeth (ω + o)) ↔ IsSuccPrelimit o
rw₁ : IsSuccLimit (ω + o) ↔ IsSuccPrelimit o
⊢ IsStrongLimit.{u_1} (ℶ_ o) ↔ IsSuccPrelimit o
have rw₂ : IsSuccPrelimit o ↔ IsSuccPrelimit o
Tactic: rw [beth_eq_preBeth, isStrongLimit_preBeth, isSuccLimit_add_iff_of_isSuccLimit isSuccLimit_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ lift.{v, u_1} (ℶ_ o) = ℶ_ (Ordinal.lift.{v, u_1} o)
have rw : lift.{v, u_1} (preBeth (ω + o)) = ℶ_ (Ordinal.lift.{v, u_1} o)
Tactic: rw [beth_eq_preBeth, beth_eq_preBeth, lift_preBeth, Ordinal.lift_add, lift_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
rw : lift.{v, u_1} (preBeth (ω + o)) = ℶ_ (Ordinal.lift.{v, u_1} o)
⊢ lift.{v, u_1} (ℶ_ o) = ℶ_ (Ordinal.lift.{v, u_1} o)
have rw₁ : lift.{v, u_1} (preBeth (ω + o)) = preBeth (ω + Ordinal.lift.{v, u_1} o)
Tactic: rw [beth_eq_preBeth, beth_eq_preBeth, lift_preBeth, Ordinal.lift_add, lift_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
rw : lift.{v, u_1} (preBeth (ω + o)) = ℶ_ (Ordinal.lift.{v, u_1} o)
rw₁ : lift.{v, u_1} (preBeth (ω + o)) = preBeth (ω + Ordinal.lift.{v, u_1} o)
⊢ lift.{v, u_1} (ℶ_ o) = ℶ_ (Ordinal.lift.{v, u_1} o)
have rw₂ : preBeth (Ordinal.lift.{v, u_1} (ω + o)) = preBeth (ω + Ordinal.lift.{v, u_1} o)
Tactic: rw [beth_eq_preBeth, beth_eq_preBeth, lift_preBeth, Ordinal.lift_add, lift_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
rw : lift.{v, u_1} (preBeth (ω + o)) = ℶ_ (Ordinal.lift.{v, u_1} o)
rw₁ : lift.{v, u_1} (preBeth (ω + o)) = preBeth (ω + Ordinal.lift.{v, u_1} o)
rw₂ : preBeth (Ordinal.lift.{v, u_1} (ω + o)) = preBeth (ω + Ordinal.lift.{v, u_1} o)
⊢ lift.{v, u_1} (ℶ_ o) = ℶ_ (Ordinal.lift.{v, u_1} o)
have rw₃ : preBeth (Ordinal.lift.{v, u_1} ω + Ordinal.lift.{v, u_1} o) = preBeth (ω + Ordinal.lift.{v, u_1} o)
Tactic: rw [beth_eq_preBeth, beth_eq_preBeth, lift_preBeth, Ordinal.lift_add, lift_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
rw : lift.{v, u_1} (preBeth (ω + o)) = ℶ_ (Ordinal.lift.{v, u_1} o)
rw₁ : lift.{v, u_1} (preBeth (ω + o)) = preBeth (ω + Ordinal.lift.{v, u_1} o)
rw₂ : preBeth (Ordinal.lift.{v, u_1} (ω + o)) = preBeth (ω + Ordinal.lift.{v, u_1} o)
rw₃ : preBeth (Ordinal.lift.{v, u_1} ω + Ordinal.lift.{v, u_1} o) = preBeth (ω + Ordinal.lift.{v, u_1} o)
⊢ lift.{v, u_1} (ℶ_ o) = ℶ_ (Ordinal.lift.{v, u_1} o)
have rw₄ : preBeth (ω + Ordinal.lift.{v, u_1} o) = preBeth (ω + Ordinal.lift.{v, u_1} o)
Tactic: rw [beth_eq_preBeth, beth_eq_preBeth, lift_preBeth, Ordinal.lift_add, lift_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (hypothesis)
Goal:
o : Ordinal.{u_1}
ho : HPow.hPow (β := ℕ) ω 2 ≤ o
⊢ preBeth o = ℶ_ o
have ho₁ : HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1}) ≤ o
Tactic: rw [← opow_natCast] at ho
Cleared hypotheses: ho
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1}) ≤ o
⊢ preBeth o = ℶ_ o
have rw : ω < HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1})
Tactic: rw [beth, add_of_omega0_opow_le _ ho]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ c * c = c
have ind : ∀ (c : Cardinal.{u_1}) (IH : ∀ y < c, ∀ (hc : ℵ₀ ≤ y), y * y = y) (hc : ℵ₀ ≤ c), c * c = c
Tactic: induction c using WellFoundedLT.induction with | ind c IH
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
IH : ∀ y < c, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ c
⊢ c * c = c
have ind : c * c ≤ c
Tactic: refine le_antisymm ?_ (by simpa using mul_le_mul_right (one_le_aleph0.trans hc) c)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
IH : ∀ y < c, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ c
⊢ c * c ≤ c
have ind : ∀ (α : Type u_1) (IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y) (hc : ℵ₀ ≤ #α), #α * #α ≤ #α
Tactic: induction c using Cardinal.inductionOn with | mk α
Cleared hypotheses: c, IH, hc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
⊢ #α * #α ≤ #α
have ind : ∀ (w : LinearOrder α) (w_1 : WellFoundedLT α) (hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2), #α * #α ≤ #α
Tactic: obtain ⟨_, _, hα⟩ := exists_ord_eq_type_lt α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
⊢ NoMaxOrder α
have rw : IsSuccPrelimit (#α).ord
Tactic: rw [← isSuccPrelimit_type_lt_iff, ← hα]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
⊢ #α * #α ≤ #α
have this : NoMaxOrder α
Tactic: have : NoMaxOrder α := by
    rw [← isSuccPrelimit_type_lt_iff, ← hα]
    exact (isSuccLimit_ord hc).isSuccPrelimit
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) :=
  {
    toFun := fun (p : α × α) ↦
      (toLex : (a : α × Lex (α × α)) → Lex (α × Lex (α × α)))
        ((g p, (toLex : (a : α × α) → Lex (α × α)) p) : α × Lex (α × α)),
    inj' := ⋯ }
s : (x y : α × α) → Prop :=
  (⇑f : (a : α × α) → Lex (α × Lex (α × α))) ⁻¹'o fun (x1 x2 : Lex (α × Lex (α × α))) ↦ x1 < x2
⊢ #α * #α ≤ #α
have this₁ : IsWellOrder (α × α) s
Tactic: have : IsWellOrder _ s := (RelEmbedding.preimage ..).isWellOrder
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this_1 : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) :=
  {
    toFun := fun (p : α × α) ↦
      (toLex : (a : α × Lex (α × α)) → Lex (α × Lex (α × α)))
        ((g p, (toLex : (a : α × α) → Lex (α × α)) p) : α × Lex (α × α)),
    inj' := ⋯ }
s : (x y : α × α) → Prop :=
  (⇑f : (a : α × α) → Lex (α × Lex (α × α))) ⁻¹'o fun (x1 x2 : Lex (α × Lex (α × α))) ↦ x1 < x2
this : IsWellOrder (α × α) s
⊢ #α * #α ≤ #α
have ind : ∀ (o : Ordinal.{u_1}) (h : o < type s), o < type fun (x1 x2 : α) ↦ x1 < x2
Tactic: refine @card_le_card (type s) (typeLT α) <| le_of_forall_lt fun o h ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this_1 : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) :=
  {
    toFun := fun (p : α × α) ↦
      (toLex : (a : α × Lex (α × α)) → Lex (α × Lex (α × α)))
        ((g p, (toLex : (a : α × α) → Lex (α × α)) p) : α × Lex (α × α)),
    inj' := ⋯ }
s : (x y : α × α) → Prop :=
  (⇑f : (a : α × α) → Lex (α × Lex (α × α))) ⁻¹'o fun (x1 x2 : Lex (α × Lex (α × α))) ↦ x1 < x2
this : IsWellOrder (α × α) s
o : Ordinal.{u_1}
h : o < type s
⊢ o < type fun (x1 x2 : α) ↦ x1 < x2
have ind : ∀ (p : α × α)
  (h :
    ((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1}) p <
      type s),
  ((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1}) p <
    type fun (x1 x2 : α) ↦ x1 < x2
Tactic: obtain ⟨p, rfl⟩ := typein_surj s h
Cleared hypotheses: o, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this_1 : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) :=
  {
    toFun := fun (p : α × α) ↦
      (toLex : (a : α × Lex (α × α)) → Lex (α × Lex (α × α)))
        ((g p, (toLex : (a : α × α) → Lex (α × α)) p) : α × Lex (α × α)),
    inj' := ⋯ }
s : (x y : α × α) → Prop :=
  (⇑f : (a : α × α) → Lex (α × Lex (α × α))) ⁻¹'o fun (x1 x2 : Lex (α × Lex (α × α))) ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h :
  ((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1}) p <
    type s
⊢ ((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1}) p <
    type fun (x1 x2 : α) ↦ x1 < x2
have ind : ∀ (q : α) (hq' : g p < q),
  ((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1}) p <
    type fun (x1 x2 : α) ↦ x1 < x2
Tactic: obtain ⟨q, hq'⟩ := exists_gt (g p)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this_1 : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) :=
  {
    toFun := fun (p : α × α) ↦
      (toLex : (a : α × Lex (α × α)) → Lex (α × Lex (α × α)))
        ((g p, (toLex : (a : α × α) → Lex (α × α)) p) : α × Lex (α × α)),
    inj' := ⋯ }
s : (x y : α × α) → Prop :=
  (⇑f : (a : α × α) → Lex (α × Lex (α × α))) ⁻¹'o fun (x1 x2 : Lex (α × Lex (α × α))) ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h :
  ((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1}) p <
    type s
q : α
hq' : g p < q
⊢ ((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1}) p <
    type fun (x1 x2 : α) ↦ x1 < x2
have ind : card
    (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1})
      p) <
  #α
Tactic: rw [← hα, lt_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this_1 : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) :=
  {
    toFun := fun (p : α × α) ↦
      (toLex : (a : α × Lex (α × α)) → Lex (α × Lex (α × α)))
        ((g p, (toLex : (a : α × α) → Lex (α × α)) p) : α × Lex (α × α)),
    inj' := ⋯ }
s : (x y : α × α) → Prop :=
  (⇑f : (a : α × α) → Lex (α × Lex (α × α))) ⁻¹'o fun (x1 x2 : Lex (α × Lex (α × α))) ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h :
  ((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1}) p <
    type s
q : α
hq' : g p < q
⊢ card
      (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1})
        p) <
    #α
have ind : card
    (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1})
      p) ≤
  #(↑(Iio q) : Type u_1) * #(↑(Iio q) : Type u_1)
Tactic: apply lt_of_le_of_lt (b := #(Iio q) * #(Iio q))
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this_1 : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) :=
  {
    toFun := fun (p : α × α) ↦
      (toLex : (a : α × Lex (α × α)) → Lex (α × Lex (α × α)))
        ((g p, (toLex : (a : α × α) → Lex (α × α)) p) : α × Lex (α × α)),
    inj' := ⋯ }
s : (x y : α × α) → Prop :=
  (⇑f : (a : α × α) → Lex (α × Lex (α × α))) ⁻¹'o fun (x1 x2 : Lex (α × Lex (α × α))) ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h :
  ((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1}) p <
    type s
q : α
hq' : g p < q
ind :
  card
      (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1})
        p) ≤
    #(↑(Iio q) : Type u_1) * #(↑(Iio q) : Type u_1)
⊢ card
      (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1})
        p) <
    #α
have ind₁ : #(↑(Iio q) : Type u_1) * #(↑(Iio q) : Type u_1) < #α
Tactic: apply lt_of_le_of_lt (b := #(Iio q) * #(Iio q))
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this_1 : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) :=
  {
    toFun := fun (p : α × α) ↦
      (toLex : (a : α × Lex (α × α)) → Lex (α × Lex (α × α)))
        ((g p, (toLex : (a : α × α) → Lex (α × α)) p) : α × Lex (α × α)),
    inj' := ⋯ }
s : (x y : α × α) → Prop :=
  (⇑f : (a : α × α) → Lex (α × Lex (α × α))) ⁻¹'o fun (x1 x2 : Lex (α × Lex (α × α))) ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h :
  ((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1}) p <
    type s
q : α
hq' : g p < q
⊢ card
      (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1})
        p) ≤
    #(↑(Iio q) : Type u_1) * #(↑(Iio q) : Type u_1)
have apply : {x : α × α | s x p} ⊆ Iio q ×ˢ Iio q
Tactic: apply (Set.embeddingOfSubset { x | s x p } ..).cardinal_le.trans_eq (mk_setProd ..)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this_1 : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) :=
  {
    toFun := fun (p : α × α) ↦
      (toLex : (a : α × Lex (α × α)) → Lex (α × Lex (α × α)))
        ((g p, (toLex : (a : α × α) → Lex (α × α)) p) : α × Lex (α × α)),
    inj' := ⋯ }
s : (x y : α × α) → Prop :=
  (⇑f : (a : α × α) → Lex (α × Lex (α × α))) ⁻¹'o fun (x1 x2 : Lex (α × Lex (α × α))) ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h :
  ((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1}) p <
    type s
q : α
hq' : g p < q
⊢ {x : α × α | s x p} ⊆ Iio q ×ˢ Iio q
have simp : ∀ (a b : α), g (a, b) < g p ∨ g (a, b) = g p ∧ (a < p.1 ∨ a = p.1 ∧ b < p.2) → a < q ∧ b < q
Tactic: simp [s, f, Prod.Lex.lt_iff, subset_def]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this_1 : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) :=
  {
    toFun := fun (p : α × α) ↦
      (toLex : (a : α × Lex (α × α)) → Lex (α × Lex (α × α)))
        ((g p, (toLex : (a : α × α) → Lex (α × α)) p) : α × Lex (α × α)),
    inj' := ⋯ }
s : (x y : α × α) → Prop :=
  (⇑f : (a : α × α) → Lex (α × Lex (α × α))) ⁻¹'o fun (x1 x2 : Lex (α × Lex (α × α))) ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h :
  ((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α × α) → Ordinal.{u_1}) p <
    type s
q : α
hq' : g p < q
⊢ #(↑(Iio q) : Type u_1) * #(↑(Iio q) : Type u_1) < #α
have ind : ∀ (hq : #(↑(Iio q) : Type u_1) < ℵ₀), #(↑(Iio q) : Type u_1) * #(↑(Iio q) : Type u_1) < #α
Tactic: rcases lt_or_ge #(Iio q) ℵ₀ with hq | hq