awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∀ (hq : #(↑(Iio q) : Type u_1) < ℵ₀), #(↑(Iio q) : Type u_1) * #(↑(Iio q) : Type u_1) < #α
ind₁ : ∀ (hq : ℵ₀ ≤ #(↑(Iio q) : Type u_1)), #(↑(Iio q) : Type u_1) * #(↑(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

Premises used: Cardinal.mk, Set.Elem, Cardinal.aleph0, lt_or_ge, Set.Iio
-- 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
hq : #(↑(Iio q) : Type u_1) < ℵ₀
⊢ #(↑(Iio q) : Type u_1) * #(↑(Iio q) : Type u_1) < #α

Tactic:
(mul_lt_aleph0 hq hq).trans_le hc

Premises used: LT.lt.trans_le, Cardinal.mul_lt_aleph0
-- 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
hq : #(↑(Iio q) : Type u_1) < ℵ₀
⊢ #(↑(Iio q) : Type u_1) * #(↑(Iio q) : Type u_1) < #α

Tactic:
exact (mul_lt_aleph0 hq hq).trans_le hc

Premises used: LT.lt.trans_le, Cardinal.mul_lt_aleph0
-- 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
hq : ℵ₀ ≤ #(↑(Iio q) : Type u_1)
⊢ #(↑(Iio q) : Type u_1) < #α

Tactic:
have := mk_Iio_lt q hα
-- 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_2 : 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
hq : ℵ₀ ≤ #(↑(Iio q) : Type u_1)
this : #(↑(Iio q) : Type u_1) < #α
ind ind₁ ind₂ ind₃ : #(↑(Iio q) : Type u_1) < #α
⊢ #(↑(Iio q) : Type u_1) * #(↑(Iio q) : Type u_1) < #α

Tactic:
rwa [IH _ this hq]
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : ℵ₀ ≤ b
⊢ a ≤ a * b

Tactic:
simpa only [mul_one] using mul_le_mul_right (one_le_aleph0.trans hb) a

Premises used: mul_le_mul_right, LE.le.trans, mul_one, Cardinal.one_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : ℵ₀ ≤ b
⊢ b ≤ a * b

Tactic:
simpa only [one_mul] using mul_le_mul_left (one_le_aleph0.trans ha) b

Premises used: mul_le_mul_left, LE.le.trans, one_mul, Cardinal.one_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Type u
inst : Infinite α
inst_1 : Infinite β
⊢ #α * #β = max #α #β

Tactic:
mul_eq_max (aleph0_le_mk α) (aleph0_le_mk β)

Premises used: Cardinal.mul_eq_max, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
o₁ o₂ : Ordinal.{u_1}
rw :
  Eq (α := Cardinal.{u_1})
    (max ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₁) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₂) :
      Cardinal.{u_1})
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (max o₁ o₂) : Cardinal.{u_1})
rw₁ rw₂ :
  Eq (α := Cardinal.{u_1})
    (max ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₁) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₂) :
      Cardinal.{u_1})
    (max ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₁) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₂) :
      Cardinal.{u_1})
⊢ HMul.hMul (α := Cardinal.{u_1}) (β := Cardinal.{u_1})
      ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₁ : Cardinal.{u_1})
      ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₂ : Cardinal.{u_1}) =
    (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (max o₁ o₂)

Tactic:
rw [Cardinal.mul_eq_max (aleph0_le_aleph o₁) (aleph0_le_aleph o₂), aleph_max]

Premises used: Cardinal.mul_eq_max, Cardinal.aleph_max, Cardinal.aleph0_le_aleph
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ ℵ₀ * a = a

Tactic:
(mul_eq_max le_rfl ha).trans (max_eq_right ha)

Premises used: le_rfl, Cardinal.mul_eq_max, max_eq_right, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ a * ℵ₀ = a

Tactic:
(mul_eq_max ha le_rfl).trans (max_eq_left ha)

Premises used: le_rfl, Cardinal.mul_eq_max, max_eq_left, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : Infinite α
⊢ ℵ₀ * #α = #α

Tactic:
aleph0_mul_eq (aleph0_le_mk α)

Premises used: Cardinal.aleph0_mul_eq, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : Infinite α
⊢ #α * ℵ₀ = #α

Tactic:
mul_aleph0_eq (aleph0_le_mk α)

Premises used: Cardinal.mul_aleph0_eq, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
o : Ordinal.{u_1}
⊢ HMul.hMul (β := Cardinal.{u_1}) ℵ₀ ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1}) =
    (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
o : Ordinal.{u_1}
⊢ HMul.hMul (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1}) ℵ₀ =
    (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a ≤ c
hb : b ≤ c
rw : a * b ≤ c * c
⊢ a * b ≤ c

Tactic:
rw [← Cardinal.mul_eq_self hc]

Premises used: Cardinal.mul_eq_self
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a ≤ c
hb : b ≤ c
⊢ a * b ≤ c * c

Tactic:
mul_le_mul' ha hb

Premises used: mul_le_mul'
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a ≤ c
hb : b ≤ c
⊢ a * b ≤ c * c

Tactic:
exact mul_le_mul' ha hb

Premises used: mul_le_mul'
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
apply : max a b * max a b < c
⊢ a * b < c

Tactic:
apply (mul_le_mul' (le_max_left a b) (le_max_right a b)).trans_lt

Premises used: le_max_right, le_max_left, LE.le.trans_lt, mul_le_mul'
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
inl : ∀ (h : max a b < ℵ₀), max a b * max a b < c
inr : ∀ (h : ℵ₀ ≤ max a b), max a b * max a b < c
⊢ max a b * max a b < c

Tactic:
obtain h | h := lt_or_ge (max a b) ℵ₀

Premises used: Cardinal.aleph0, Max.max, lt_or_ge
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : max a b < ℵ₀
⊢ max a b * max a b < c

Tactic:
(mul_lt_aleph0 h h).trans_le hc

Premises used: LT.lt.trans_le, Cardinal.mul_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : max a b < ℵ₀
⊢ max a b * max a b < c

Tactic:
exact (mul_lt_aleph0 h h).trans_le hc

Premises used: LT.lt.trans_le, Cardinal.mul_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : ℵ₀ ≤ max a b
inr : max a b < c
⊢ max a b * max a b < c

Tactic:
rw [mul_eq_self h]

Premises used: Cardinal.mul_eq_self
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : ℵ₀ ≤ max a b
⊢ max a b < c

Tactic:
max_lt ha hb

Premises used: max_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : ℵ₀ ≤ max a b
⊢ max a b < c

Tactic:
exact max_lt ha hb

Premises used: max_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ a * b ≤ max a b * max a b

Tactic:
mul_le_mul' (le_max_left a b) (le_max_right a b)

Premises used: le_max_right, le_max_left, mul_le_mul'
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h₁ : max a b = max a b * max a b
⊢ a * b ≤ max a b

Tactic:
convert! mul_le_mul' (le_max_left a b) (le_max_right a b) using 1

Premises used: le_max_right, le_max_left, mul_le_mul'
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h₁ : ℵ₀ ≤ max a b
⊢ max a b = max a b * max a b

Tactic:
rw [mul_eq_self]

Premises used: Cardinal.mul_eq_self
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ ℵ₀ ≤ max a b

Tactic:
h.trans (le_max_left a b)

Premises used: LE.le.trans, le_max_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ ℵ₀ ≤ max a b

Tactic:
exact h.trans (le_max_left a b)

Premises used: LE.le.trans, le_max_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
inl : ∀ (hb : ℵ₀ ≤ b), a * b = max a b
inr : ∀ (hb : b < ℵ₀), a * b = max a b
⊢ a * b = max a b

Tactic:
rcases le_or_gt ℵ₀ b with hb | hb

Premises used: Cardinal.aleph0, le_or_gt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : ℵ₀ ≤ b
⊢ a * b = max a b

Tactic:
mul_eq_max h hb

Premises used: Cardinal.mul_eq_max
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : ℵ₀ ≤ b
⊢ a * b = max a b

Tactic:
exact mul_eq_max h hb

Premises used: Cardinal.mul_eq_max
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
⊢ a * b = max a b

Tactic:
(mul_le_max_of_aleph0_le_left h).antisymm ?_

Premises used: LE.le.antisymm, Cardinal.mul_le_max_of_aleph0_le_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
inr : max a b ≤ a * b
⊢ a * b = max a b

Tactic:
refine (mul_le_max_of_aleph0_le_left h).antisymm ?_

Premises used: LE.le.antisymm, Cardinal.mul_le_max_of_aleph0_le_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
⊢ b ≤ a

Tactic:
have : b ≤ a := hb.le.trans h
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
inr : a ≤ a * b
⊢ max a b ≤ a * b

Tactic:
rw [max_eq_left this]

Premises used: max_eq_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ a * 1 ≤ a * b

Tactic:
mul_le_mul_right (Cardinal.one_le_iff_ne_zero.mpr h') a

Premises used: Iff.mpr, mul_le_mul_right, Cardinal.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
h₁ : a = a * 1
⊢ a ≤ a * b

Tactic:
convert! mul_le_mul_right (Cardinal.one_le_iff_ne_zero.mpr h') a

Premises used: Iff.mpr, mul_le_mul_right, Cardinal.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
h₁ h₂ : a = a
⊢ a = a * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ b
⊢ a * b ≤ max a b

Tactic:
simpa only [mul_comm b, max_comm b] using mul_le_max_of_aleph0_le_left h

Premises used: Cardinal.mul_le_max_of_aleph0_le_left, mul_comm, max_comm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
rw : b * a = max b a
⊢ a * b = max a b

Tactic:
rw [mul_comm, max_comm]

Premises used: mul_comm, max_comm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ b * a = max b a

Tactic:
mul_eq_max_of_aleph0_le_left h h'

Premises used: Cardinal.mul_eq_max_of_aleph0_le_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ b * a = max b a

Tactic:
exact mul_eq_max_of_aleph0_le_left h h'

Premises used: Cardinal.mul_eq_max_of_aleph0_le_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
inl : ∀ (ha : a ≠ 0) (hb : b ≠ 0) (ha' : ℵ₀ ≤ a), a * b = max a b
inr : ∀ (ha : a ≠ 0) (hb : b ≠ 0) (hb' : ℵ₀ ≤ b), a * b = max a b
⊢ a * b = max a b

Tactic:
rcases aleph0_le_mul_iff.mp h with ⟨ha, hb, ha' | hb'⟩

Premises used: Iff.mp, Cardinal.aleph0_le_mul_iff
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
ha' : ℵ₀ ≤ a
⊢ a * b = max a b

Tactic:
mul_eq_max_of_aleph0_le_left ha' hb

Premises used: Cardinal.mul_eq_max_of_aleph0_le_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
ha' : ℵ₀ ≤ a
⊢ a * b = max a b

Tactic:
exact mul_eq_max_of_aleph0_le_left ha' hb

Premises used: Cardinal.mul_eq_max_of_aleph0_le_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
hb' : ℵ₀ ≤ b
⊢ a * b = max a b

Tactic:
mul_eq_max_of_aleph0_le_right ha hb'

Premises used: Cardinal.mul_eq_max_of_aleph0_le_right
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
hb' : ℵ₀ ≤ b
⊢ a * b = max a b

Tactic:
exact mul_eq_max_of_aleph0_le_right ha hb'

Premises used: Cardinal.mul_eq_max_of_aleph0_le_right
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
inl : 0 * b ≤ max (max 0 b) ℵ₀
inr : ∀ (ha0 : a ≠ 0), a * b ≤ max (max a b) ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
rcases eq_or_ne a 0 with (rfl | ha0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
b : Cardinal.{u_1}
⊢ 0 * b ≤ max (max 0 b) ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
inr : a * 0 ≤ max (max a 0) ℵ₀
inr₁ : ∀ (hb0 : b ≠ 0), a * b ≤ max (max a b) ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
rcases eq_or_ne b 0 with (rfl | hb0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u_1}
ha0 : a ≠ 0
⊢ a * 0 ≤ max (max a 0) ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
inr : ∀ (ha : ℵ₀ ≤ a), a * b ≤ max (max a b) ℵ₀
inr₁ : ∀ (ha : a < ℵ₀), a * b ≤ max (max a b) ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
rcases le_or_gt ℵ₀ a with ha | ha

Premises used: Cardinal.aleph0, le_or_gt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
inr : max a b ≤ max (max a b) ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
rw [mul_eq_max_of_aleph0_le_left ha hb0]

Premises used: Cardinal.mul_eq_max_of_aleph0_le_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ max a b ≤ max (max a b) ℵ₀

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ max a b ≤ max (max a b) ℵ₀

Tactic:
exact le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
inr : ∀ (hb : ℵ₀ ≤ b), a * b ≤ max (max a b) ℵ₀
inr₁ : ∀ (hb : b < ℵ₀), a * b ≤ max (max a b) ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
rcases le_or_gt ℵ₀ b with hb | hb

Premises used: Cardinal.aleph0, le_or_gt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
inr : max a b ≤ max (max a b) ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
rw [mul_comm, mul_eq_max_of_aleph0_le_left hb ha0, max_comm]

Premises used: mul_comm, Cardinal.mul_eq_max_of_aleph0_le_left, max_comm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ max a b ≤ max (max a b) ℵ₀

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ max a b ≤ max (max a b) ℵ₀

Tactic:
exact le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
le_max_of_le_right (mul_lt_aleph0 ha hb).le

Premises used: LT.lt.le, le_max_of_le_right, Cardinal.mul_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
exact le_max_of_le_right (mul_lt_aleph0 ha hb).le

Premises used: LT.lt.le, le_max_of_le_right, Cardinal.mul_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
hb' : b ≠ 0
rw : max a b = a
rw₁ rw₂ : a = a
⊢ a * b = a

Tactic:
rw [mul_eq_max_of_aleph0_le_left ha hb', max_eq_left hb]

Premises used: max_eq_left, Cardinal.mul_eq_max_of_aleph0_le_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a ≤ b
ha' : a ≠ 0
rw : b * a = b
rw₁ rw₂ : b = b
⊢ a * b = b

Tactic:
rw [mul_comm, mul_eq_left hb ha ha']

Premises used: Cardinal.mul_eq_left, mul_comm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ 1 * a ≤ b * a

Tactic:
mul_le_mul_left (Cardinal.one_le_iff_ne_zero.mpr h) a

Premises used: Iff.mpr, Cardinal.one_le_iff_ne_zero, mul_le_mul_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : b ≠ 0
h₁ : a = 1 * a
⊢ a ≤ b * a

Tactic:
convert! mul_le_mul_left (Cardinal.one_le_iff_ne_zero.mpr h) a

Premises used: Iff.mpr, Cardinal.one_le_iff_ne_zero, mul_le_mul_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : b ≠ 0
h₁ h₂ : a = a
⊢ a = 1 * a

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : b ≠ 0
rw : a ≤ b * a
⊢ a ≤ a * b

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ b * a

Tactic:
le_mul_left h

Premises used: Cardinal.le_mul_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ b * a

Tactic:
exact le_mul_left h

Premises used: Cardinal.le_mul_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
rw : a * b = a ↔ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
⊢ a * b = a ↔ max ℵ₀ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
rw [max_le_iff]

Premises used: max_le_iff
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
⊢ a * b = a ↔ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
refine_1 : ∀ (h : a * b = a), (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
refine_2 : (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0 → a * b = a
⊢ a * b = a ↔ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
refine_1 : ∀ (ha : ℵ₀ ≤ a), (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
refine_1₁ : ∀ (ha : a < ℵ₀), (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
rcases le_or_gt ℵ₀ a with ha | ha

Premises used: Cardinal.aleph0, le_or_gt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
b : Cardinal.{u_1}
h : 0 * b = 0
ha : ℵ₀ ≤ 0
⊢ False

Tactic:
ha.not_gt aleph0_pos

Premises used: LE.le.not_gt, Cardinal.aleph0_pos
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
b : Cardinal.{u_1}
h : 0 * b = 0
ha : ℵ₀ ≤ 0
⊢ False

Tactic:
exact ha.not_gt aleph0_pos

Premises used: LE.le.not_gt, Cardinal.aleph0_pos
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
⊢ a ≠ 0

Tactic:
have : a ≠ 0 := by
        rintro rfl
        exact ha.not_gt aleph0_pos
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
refine_1 : (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
refine_1 : ℵ₀ ≤ a ∧ b ≤ a ∧ b ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0

Tactic:
rw [and_assoc]

Premises used: and_assoc
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
right : b ≤ a ∧ b ≠ 0
⊢ ℵ₀ ≤ a ∧ b ≤ a ∧ b ≠ 0

Tactic:
use ha
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
right : b ≤ a
right₁ : b ≠ 0
⊢ b ≤ a ∧ b ≠ 0

Tactic:
constructor
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
right : ¬a < b
⊢ b ≤ a

Tactic:
rw [← not_lt]

Premises used: not_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ¬a < b

Tactic:
fun hb => ne_of_gt (hb.trans_le (le_mul_left this)) h

Premises used: ne_of_gt, Cardinal.le_mul_left, LT.lt.trans_le, Not
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ¬a < b

Tactic:
exact fun hb => ne_of_gt (hb.trans_le (le_mul_left this)) h

Premises used: ne_of_gt