awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c = (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) (↑n : Ordinal.{max u v}) ↔
    c = (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) (↑n : Ordinal.{u})

Tactic:
simp [eqComm]

Premises used: eqComm
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) (OfNat.ofNat n) ≤ lift.{v, u} c ↔
    (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) (OfNat.ofNat n) ≤ c

Tactic:
aleph_natCast_le_lift

Premises used: Cardinal.aleph_natCast_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ lift.{v, u} c ≤ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) (OfNat.ofNat n) ↔
    c ≤ (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) (OfNat.ofNat n)

Tactic:
lift_le_aleph_natCast

Premises used: Cardinal.lift_le_aleph_natCast
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) (OfNat.ofNat n) < lift.{v, u} c ↔
    (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) (OfNat.ofNat n) < c

Tactic:
aleph_natCast_lt_lift

Premises used: Cardinal.aleph_natCast_lt_lift
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ lift.{v, u} c < (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) (OfNat.ofNat n) ↔
    c < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) (OfNat.ofNat n)

Tactic:
lift_lt_aleph_natCast

Premises used: Cardinal.lift_lt_aleph_natCast
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) (OfNat.ofNat n) = lift.{v, u} c ↔
    (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) (OfNat.ofNat n) = c

Tactic:
aleph_natCast_eq_lift

Premises used: Cardinal.aleph_natCast_eq_lift
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ lift.{v, u} c = (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) (OfNat.ofNat n) ↔
    c = (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) (OfNat.ofNat n)

Tactic:
lift_eq_aleph_natCast

Premises used: Cardinal.lift_eq_aleph_natCast
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
⊢ ℶ_ (↑n : Ordinal.{max u v}) ≤ lift.{v, u} c ↔ ℶ_ (↑n : Ordinal.{u}) ≤ c

Tactic:
simpa using lift_le (a := ℶ_ n)

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c ≤ ℶ_ (↑n : Ordinal.{max u v}) ↔ c ≤ ℶ_ (↑n : Ordinal.{u})

Tactic:
simpa using lift_le (b := ℶ_ n)

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
⊢ ℶ_ (↑n : Ordinal.{max u v}) < lift.{v, u} c ↔ ℶ_ (↑n : Ordinal.{u}) < c

Tactic:
simpa using lift_lt (a := ℶ_ n)

Premises used: Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c < ℶ_ (↑n : Ordinal.{max u v}) ↔ c < ℶ_ (↑n : Ordinal.{u})

Tactic:
simpa using lift_lt (b := ℶ_ n)

Premises used: Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
⊢ ℶ_ (↑n : Ordinal.{max u v}) = lift.{v, u} c ↔ ℶ_ (↑n : Ordinal.{u}) = c

Tactic:
simpa using lift_inj (a := ℶ_ n)

Premises used: Cardinal.lift_inj
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c = ℶ_ (↑n : Ordinal.{max u v}) ↔ c = ℶ_ (↑n : Ordinal.{u})

Tactic:
simp [eqComm]

Premises used: eqComm
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ ℶ_ (OfNat.ofNat n) ≤ lift.{v, u} c ↔ ℶ_ (OfNat.ofNat n) ≤ c

Tactic:
beth_natCast_le_lift

Premises used: Cardinal.beth_natCast_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ lift.{v, u} c ≤ ℶ_ (OfNat.ofNat n) ↔ c ≤ ℶ_ (OfNat.ofNat n)

Tactic:
lift_le_beth_natCast

Premises used: Cardinal.lift_le_beth_natCast
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ ℶ_ (OfNat.ofNat n) < lift.{v, u} c ↔ ℶ_ (OfNat.ofNat n) < c

Tactic:
beth_natCast_lt_lift

Premises used: Cardinal.beth_natCast_lt_lift
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ lift.{v, u} c < ℶ_ (OfNat.ofNat n) ↔ c < ℶ_ (OfNat.ofNat n)

Tactic:
lift_lt_beth_natCast

Premises used: Cardinal.lift_lt_beth_natCast
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ ℶ_ (OfNat.ofNat n) = lift.{v, u} c ↔ ℶ_ (OfNat.ofNat n) = c

Tactic:
beth_natCast_eq_lift

Premises used: Cardinal.beth_natCast_eq_lift
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ lift.{v, u} c = ℶ_ (OfNat.ofNat n) ↔ c = ℶ_ (OfNat.ofNat n)

Tactic:
lift_eq_beth_natCast

Premises used: Cardinal.lift_eq_beth_natCast
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
⊢ (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) 1 ≤ lift.{v, u} o ↔ (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) 1 ≤ o

Tactic:
simpa using lift_le (a := ω₁)

Premises used: Ordinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
⊢ lift.{v, u} o ≤ (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) 1 ↔ o ≤ (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) 1

Tactic:
simpa using lift_le (b := ω₁)

Premises used: Ordinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
⊢ (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) 1 < lift.{v, u} o ↔ (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) 1 < o

Tactic:
simpa using lift_lt (a := ω₁)

Premises used: Ordinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
⊢ lift.{v, u} o < (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) 1 ↔ o < (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) 1

Tactic:
simpa using lift_lt (b := ω₁)

Premises used: Ordinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
⊢ (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) 1 = lift.{v, u} o ↔ (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) 1 = o

Tactic:
simpa using lift_inj (a := ω₁)

Premises used: Ordinal.lift_inj
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
⊢ lift.{v, u} o = (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) 1 ↔ o = (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) 1

Tactic:
simp [eqComm]

Premises used: eqComm
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
n : ℕ
⊢ (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) (↑n : Ordinal.{max u v}) ≤ lift.{v, u} o ↔
    (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) (↑n : Ordinal.{u}) ≤ o

Tactic:
simpa using lift_le (a := ω_ n)

Premises used: Ordinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
n : ℕ
⊢ lift.{v, u} o ≤ (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) (↑n : Ordinal.{max u v}) ↔
    o ≤ (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) (↑n : Ordinal.{u})

Tactic:
simpa using lift_le (b := ω_ n)

Premises used: Ordinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
n : ℕ
⊢ (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) (↑n : Ordinal.{max u v}) < lift.{v, u} o ↔
    (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) (↑n : Ordinal.{u}) < o

Tactic:
simpa using lift_lt (a := ω_ n)

Premises used: Ordinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
n : ℕ
⊢ lift.{v, u} o < (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) (↑n : Ordinal.{max u v}) ↔
    o < (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) (↑n : Ordinal.{u})

Tactic:
simpa using lift_lt (b := ω_ n)

Premises used: Ordinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
n : ℕ
⊢ (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) (↑n : Ordinal.{max u v}) = lift.{v, u} o ↔
    (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) (↑n : Ordinal.{u}) = o

Tactic:
simpa using lift_inj (a := ω_ n)

Premises used: Ordinal.lift_inj
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
n : ℕ
⊢ lift.{v, u} o = (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) (↑n : Ordinal.{max u v}) ↔
    o = (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) (↑n : Ordinal.{u})

Tactic:
simp [eqComm]

Premises used: eqComm
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) (OfNat.ofNat n) ≤ lift.{v, u} o ↔
    (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) (OfNat.ofNat n) ≤ o

Tactic:
omega_natCast_le_lift

Premises used: Ordinal.omega_natCast_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ lift.{v, u} o ≤ (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) (OfNat.ofNat n) ↔
    o ≤ (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) (OfNat.ofNat n)

Tactic:
lift_le_omega_natCast

Premises used: Ordinal.lift_le_omega_natCast
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) (OfNat.ofNat n) < lift.{v, u} o ↔
    (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) (OfNat.ofNat n) < o

Tactic:
omega_natCast_lt_lift

Premises used: Ordinal.omega_natCast_lt_lift
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ lift.{v, u} o < (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) (OfNat.ofNat n) ↔
    o < (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) (OfNat.ofNat n)

Tactic:
lift_lt_omega_natCast

Premises used: Ordinal.lift_lt_omega_natCast
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) (OfNat.ofNat n) = lift.{v, u} o ↔
    (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) (OfNat.ofNat n) = o

Tactic:
omega_natCast_eq_lift

Premises used: Ordinal.omega_natCast_eq_lift
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ lift.{v, u} o = (ω_ : (a : Ordinal.{max u v}) → Ordinal.{max u v}) (OfNat.ofNat n) ↔
    o = (ω_ : (a : Ordinal.{u}) → Ordinal.{u}) (OfNat.ofNat n)

Tactic:
lift_eq_omega_natCast

Premises used: Ordinal.lift_eq_omega_natCast
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ind : ∀ (c : Cardinal.{u_1}) (IH : ∀ y < c, ∀ (hc : ℵ₀ ≤ y), y * y = y) (hc : ℵ₀ ≤ c), c * c = c
⊢ c * c = c

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

Premises used: WellFoundedLT.induction
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
IH : ∀ y < c, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ c
⊢ c ≤ c * c

Tactic:
simpa using mul_le_mul_right (one_le_aleph0.trans hc) c

Premises used: mul_le_mul_right, LE.le.trans, Cardinal.one_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
IH : ∀ y < c, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ c
ind : c * c ≤ c
⊢ c * c = c

Tactic:
refine le_antisymm ?_ (by simpa using mul_le_mul_right (one_le_aleph0.trans hc) c)

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
IH : ∀ y < c, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ c
ind : ∀ (α : Type u_1) (IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y) (hc : ℵ₀ ≤ #α), #α * #α ≤ #α
⊢ c * c ≤ c

Tactic:
induction c using Cardinal.inductionOn with | mk α

Premises used: Cardinal.mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
IH : ∀ y < #α, ∀ (hc : ℵ₀ ≤ y), y * y = y
hc : ℵ₀ ≤ #α
ind : ∀ (w : LinearOrder α) (w_1 : WellFoundedLT α) (hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2), #α * #α ≤ #α
⊢ #α * #α ≤ #α

Tactic:
obtain ⟨_, _, hα⟩ := exists_ord_eq_type_lt α

Premises used: Cardinal.exists_ord_eq_type_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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
rw : IsSuccPrelimit (#α).ord
⊢ NoMaxOrder α

Tactic:
rw [← isSuccPrelimit_type_lt_iff, ← hα]

Premises used: Ordinal.isSuccPrelimit_type_lt_iff
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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
⊢ IsSuccPrelimit (#α).ord

Tactic:
(isSuccLimit_ord hc).isSuccPrelimit

Premises used: Cardinal.isSuccLimit_ord, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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
⊢ IsSuccPrelimit (#α).ord

Tactic:
exact (isSuccLimit_ord hc).isSuccPrelimit

Premises used: Cardinal.isSuccLimit_ord, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 α

Tactic:
have : NoMaxOrder α := by
    rw [← isSuccPrelimit_type_lt_iff, ← hα]
    exact (isSuccLimit_ord hc).isSuccPrelimit
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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
⊢ IsWellOrder (α × α) s

Tactic:
have : IsWellOrder _ s := (RelEmbedding.preimage ..).isWellOrder
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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
⊢ #α * #α ≤ #α

Tactic:
@card_le_card (type s) (typeLT α) <| le_of_forall_lt fun o h ↦ ?_

Premises used: Ordinal.card_le_card, le_of_forall_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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
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 ↦ ?_

Premises used: Ordinal.card_le_card, le_of_forall_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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
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
⊢ o < type fun (x1 x2 : α) ↦ x1 < x2

Tactic:
obtain ⟨p, rfl⟩ := typein_surj s h

Premises used: Ordinal.typein_surj, rfl
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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
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
⊢ ((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)

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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) <
    #α
⊢ ((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:
rw [← hα, lt_ord]

Premises used: Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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)
ind₁ : #(↑(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) <
    #α

Tactic:
apply lt_of_le_of_lt (b := #(Iio q) * #(Iio q))

Premises used: lt_of_le_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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
apply : {x : α × α | s x p} ⊆ Iio q ×ˢ Iio 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)

Tactic:
apply (Set.embeddingOfSubset { x | s x p } ..).cardinal_le.trans_eq (mk_setProd ..)

Premises used: LE.le.trans_eq, setOf, Cardinal.mk_setProd, Function.Embedding.cardinal_le, Set.embeddingOfSubset
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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
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
⊢ {x : α × α | s x p} ⊆ Iio q ×ˢ Iio q

Tactic:
simp [s, f, Prod.Lex.lt_iff, subset_def]

Premises used: Set.subset_def, Prod.Lex.lt_iff
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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
⊢ ∀ (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:
grind