awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
right : a = 0
⊢ False

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

Tactic:
rw [mul_zero] at h

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : 0 = a
⊢ a = 0

Tactic:
h.symm

Premises used: Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : 0 = a
⊢ a = 0

Tactic:
exact h.symm

Premises used: Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
refine_1 : b = 1 ∨ a = 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
right
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
pos : ∀ (h2a : a = 0), b = 1 ∨ a = 0
neg : ∀ (h2a : ¬a = 0), b = 1 ∨ a = 0
⊢ b = 1 ∨ a = 0

Tactic:
by_cases h2a : a = 0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : a = 0
⊢ b = 1 ∨ a = 0

Tactic:
Or.inr h2a

Premises used: Or.inr
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : a = 0
⊢ b = 1 ∨ a = 0

Tactic:
exact Or.inr h2a

Premises used: Or.inr
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
apply : a = 0
⊢ False

Tactic:
apply h2a
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
⊢ 0 = a

Tactic:
rw [mul_zero] at h

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : 0 = a
⊢ a = 0

Tactic:
h.symm

Premises used: Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : 0 = a
⊢ a = 0

Tactic:
exact h.symm

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

Tactic:
have hb : b ≠ 0 := by
      rintro rfl
      apply h2a
      rw [mul_zero] at h
      exact h.symm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
neg : b = 1
⊢ b = 1 ∨ a = 0

Tactic:
left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ a = 0 ∨ b = 0 ∨ (∃ (n : ℕ), a = (↑n : Cardinal.{u_1})) ∧ ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})

Tactic:
rw [← h, mul_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha

Premises used: Cardinal.mul_lt_aleph0_iff, Cardinal.lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
ha₁ : a = 0 ∨ b = 0 ∨ (∃ (n : ℕ), a = (↑n : Cardinal.{u_1})) ∧ ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
⊢ ¬a = 0

Tactic:
rw [← h, mul_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha

Premises used: Cardinal.mul_lt_aleph0_iff, Cardinal.lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
ha₁ : a = 0 ∨ b = 0 ∨ (∃ (n : ℕ), a = (↑n : Cardinal.{u_1})) ∧ ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
h2a₁ : ¬a = 0
⊢ b ≠ 0

Tactic:
rw [← h, mul_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha

Premises used: Cardinal.mul_lt_aleph0_iff, Cardinal.lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a * b = a
ha : a = 0 ∨ b = 0 ∨ (∃ (n : ℕ), a = (↑n : Cardinal.{u_1})) ∧ ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
h2a : ¬a = 0
hb : b ≠ 0
neg : ∀ (h : 0 * b = 0) (h2a : ¬Eq.{u_1 + 2} (α := Cardinal.{u_1}) 0 0), b = 1
neg₁ : ∀ (h : a * 0 = a) (hb : Ne.{u_1 + 2} (α := Cardinal.{u_1}) 0 0), Eq.{u_1 + 2} (α := Cardinal.{u_1}) 0 1
neg₂ :
  ∀ (n : ℕ) (h2a : ¬Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0) (m : ℕ)
    (hb : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 0)
    (h : HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1})),
    Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 1
⊢ b = 1

Tactic:
rcases ha with (rfl | rfl | ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩)

Premises used: rfl
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
b : Cardinal.{u_1}
hb : b ≠ 0
h : 0 * b = 0
h2a : ¬Eq.{u_1 + 2} (α := Cardinal.{u_1}) 0 0
⊢ b = 1

Tactic:
contradiction
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u_1}
h2a : ¬a = 0
h : a * 0 = a
hb : Ne.{u_1 + 2} (α := Cardinal.{u_1}) 0 0
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) 0 1

Tactic:
contradiction
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n : ℕ
h2a : ¬Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
m : ℕ
hb : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 0
h : HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1})
neg :
  ∀ (h2a : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0) (m : ℕ)
    (hb : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 0)
    (h : HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1})),
    Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 1
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 1

Tactic:
rw [← Ne] at h2a

Premises used: Ne
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n : ℕ
h2a : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
m : ℕ
hb : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 0
h : HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1})
neg :
  ∀ (h2a : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) 1 (↑n : Cardinal.{u_1})) (m : ℕ)
    (hb : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) 1 (↑m : Cardinal.{u_1}))
    (h : HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1})),
    Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 1
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 1

Tactic:
rw [← Cardinal.one_le_iff_ne_zero] at h2a hb

Premises used: Cardinal.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n : ℕ
h2a : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) 1 (↑n : Cardinal.{u_1})
m : ℕ
hb : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) 1 (↑m : Cardinal.{u_1})
h : HMul.hMul (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1})
neg : ∀ (h2a : 1 ≤ n) (hb : 1 ≤ m) (h : n * m = n), m = 1
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 1

Tactic:
norm_cast at h2a hb h ⊢
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
apply : m ≤ 1
⊢ m = 1

Tactic:
apply le_antisymm _ hb

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
rw : ¬1 < m
⊢ m ≤ 1

Tactic:
rw [← not_lt]

Premises used: not_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
apply : ∀ (h2b : 1 < m), n < n * m
⊢ ¬1 < m

Tactic:
apply fun h2b => ne_of_gt _ h

Premises used: ne_of_gt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
h2b : 1 < m
left : n
| n < n * m

Tactic:
left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
h2b : 1 < m
rw : n * 1
| n

Tactic:
rw [← mul_one n]

Premises used: mul_one
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
h2b : 1 < m
rw : n * 1
| n < n * m

Tactic:
left; rw [← mul_one n]

Premises used: mul_one
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
conv_rhs : ∀ (a : 1 < m), n * 1 < n * m
⊢ ∀ (h2b : 1 < m), n < n * m

Tactic:
conv_rhs => left; rw [← mul_one n]

Premises used: mul_one
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
rw : ∀ (a : 1 < m), 1 < m
rw₁ : 0 < n
⊢ ∀ (a : 1 < m), n * 1 < n * m

Tactic:
rw [Nat.mul_lt_mul_left]

Premises used: Nat.mul_lt_mul_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ ∀ (a : 1 < m), 1 < m

Tactic:
id

Premises used: id
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ ∀ (a : 1 < m), 1 < m

Tactic:
exact id

Premises used: id
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 0 < n

Tactic:
apply Nat.lt_of_succ_le h2a

Premises used: Nat.lt_of_succ_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
hb : b ≠ 0
ha : ℵ₀ ≤ a
hab : b ≤ a
refine_2 : max a b = a
refine_2₁ refine_2₂ : a = a
⊢ a * b = a

Tactic:
rw [mul_eq_max_of_aleph0_le_left ha hb, max_eq_left hab]

Premises used: max_eq_left, Cardinal.mul_eq_max_of_aleph0_le_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u_1}
⊢ a * 1 = a

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
b : Cardinal.{u_1}
⊢ 0 * b = 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c + c ≤ c

Tactic:
simpa [two_mul, mul_eq_self h] using mul_le_mul_left (natCast_le_aleph0 (n := 2).trans h) c

Premises used: two_mul, Cardinal.mul_eq_self, mul_le_mul_left, LE.le.trans, Cardinal.natCast_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ a + b = max a b

Tactic:
le_antisymm
      (add_eq_self (ha.trans (le_max_left a b)) ▸
        add_le_add (le_max_left _ _) (le_max_right _ _)) <|
    max_le (self_le_add_right _ _) (self_le_add_left _ _)

Premises used: self_le_add_right, self_le_add_left, le_antisymm, max_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ b
rw : b + a = max a b
rw₁ : b + a = max b a
rw₂ rw₃ : max b a = max b a
⊢ a + b = max a b

Tactic:
rw [add_comm, max_comm, add_eq_max ha]

Premises used: add_comm, Cardinal.add_eq_max, max_comm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Type u
inst : Infinite α
⊢ #α + #β = max #α #β

Tactic:
add_eq_max (aleph0_le_mk α)

Premises used: Cardinal.add_eq_max, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Type u
inst : Infinite β
⊢ #α + #β = max #α #β

Tactic:
add_eq_max' (aleph0_le_mk β)

Premises used: Cardinal.add_eq_max', Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : Infinite α
⊢ #α + #α = #α

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
inl : ∀ (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}
ha : ℵ₀ ≤ a
inl : max a b ≤ max (max a b) ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
rw [add_eq_max ha]

Premises used: Cardinal.add_eq_max
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
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}
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}
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}
ha : a < ℵ₀
hb : ℵ₀ ≤ b
inr : max a b ≤ max (max a b) ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
rw [add_comm, add_eq_max hb, max_comm]

Premises used: add_comm, Cardinal.add_eq_max, max_comm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
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}
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}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
le_max_of_le_right (add_lt_aleph0 ha hb).le

Premises used: LT.lt.le, le_max_of_le_right, Cardinal.add_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
exact le_max_of_le_right (add_lt_aleph0 ha hb).le

Premises used: LT.lt.le, le_max_of_le_right, Cardinal.add_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a ≤ c
h2 : b ≤ c
⊢ a + b ≤ c

Tactic:
(add_le_add h1 h2).trans <| le_of_eq <| add_eq_self hc

Premises used: add_le_add, Cardinal.add_eq_self, LE.le.trans, le_of_eq
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ max a b
rw : max a b < c
⊢ max a b + max a b < c

Tactic:
rw [add_eq_self h]

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

Tactic:
max_lt h1 h2

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

Tactic:
exact max_lt h1 h2

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

Tactic:
add_lt_of_lt hb ha (one_lt_aleph0.trans_le hb)

Premises used: Cardinal.one_lt_aleph0, Cardinal.add_lt_of_lt, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a < b
⊢ 1 + a < b

Tactic:
add_lt_of_lt hb (one_lt_aleph0.trans_le hb) ha

Premises used: Cardinal.one_lt_aleph0, Cardinal.add_lt_of_lt, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
a₁ : b ≤ c
a₂ : c ≤ b
⊢ b = c

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
a₁ : b ≤ a + b
⊢ b ≤ c

Tactic:
rw [← h]
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b ≤ a + b

Tactic:
apply self_le_add_left

Premises used: self_le_add_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
a₁ : ¬b < c
⊢ c ≤ b

Tactic:
rw [← not_lt]

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

Tactic:
have : a + b < c := add_lt_of_lt hc ha hb
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
hb : b < c
this : a + b < c
⊢ False

Tactic:
simp [h] at this
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
rw : max a b = a
rw₁ rw₂ : a = a
⊢ a + b = a

Tactic:
rw [add_eq_max ha, max_eq_left hb]

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

Tactic:
rw [add_comm, add_eq_left hb ha]

Premises used: add_comm, Cardinal.add_eq_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
rw : a + b = a ↔ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
⊢ a + b = a ↔ max ℵ₀ b ≤ a ∨ b = 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

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
refine_2 : ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0 → a + b = a
⊢ a + b = a ↔ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 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
refine_1₁ : ∀ (ha : a < ℵ₀), ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0

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}
h : a + b = a
ha : ℵ₀ ≤ a
refine_1 : ℵ₀ ≤ a ∧ b ≤ a
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0

Tactic:
left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
right : b ≤ a
⊢ ℵ₀ ≤ a ∧ b ≤ a

Tactic:
use ha
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
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
apply : ∀ (hb : a < b), a < a + b
⊢ ¬a < b

Tactic:
apply fun hb => ne_of_gt _ h

Premises used: ne_of_gt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
hb : a < b
⊢ a < a + b

Tactic:
hb.trans_le (self_le_add_left b a)

Premises used: self_le_add_left, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
hb : a < b
⊢ a < a + b

Tactic:
exact hb.trans_le (self_le_add_left b a)

Premises used: self_le_add_left, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a + b = a
ha : a < ℵ₀
refine_1 : b = 0
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0

Tactic:
right
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a + b = a
ha : a < ℵ₀
⊢ (∃ (n : ℕ), a = (↑n : Cardinal.{u_1})) ∧ ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})

Tactic:
rw [← h, add_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha

Premises used: Cardinal.add_lt_aleph0_iff, Cardinal.lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h : a + b = a
ha : (∃ (n : ℕ), a = (↑n : Cardinal.{u_1})) ∧ ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
refine_1 :
  ∀ (n m : ℕ) (h : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1})),
    Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 0
⊢ b = 0

Tactic:
rcases ha with ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩

Premises used: rfl
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n m : ℕ
h : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1})
refine_1 : ∀ (h : n + m = n), m = 0
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) 0

Tactic:
norm_cast at h ⊢
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n m : ℕ
h : n + m = n
refine_1 : n + m = n + 0
refine_1₁ : ℕ
refine_1₂ : n = n + 0
refine_1₃ refine_1₄ : n = n
⊢ m = 0

Tactic:
rw [← add_right_inj, h, add_zero]

Premises used: add_zero, add_right_inj
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h1 : ℵ₀ ≤ a
h2 : b ≤ a
refine_2 : max a b = a
refine_2₁ refine_2₂ : a = a
⊢ a + b = a

Tactic:
rw [add_eq_max h1, max_eq_left h2]

Premises used: max_eq_left, Cardinal.add_eq_max
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
h3 : b = 0
refine_2 : a + 0 = a
refine_2₁ refine_2₂ : a = a
⊢ a + b = a

Tactic:
rw [h3, add_zero]

Premises used: add_zero
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u_1}
rw : b + a = b ↔ max ℵ₀ a ≤ b ∨ a = 0
rw₁ rw₂ : max ℵ₀ a ≤ b ∨ a = 0 ↔ max ℵ₀ a ≤ b ∨ a = 0
⊢ a + b = b ↔ max ℵ₀ a ≤ b ∨ a = 0

Tactic:
rw [add_comm, add_eq_left_iff]

Premises used: add_comm, Cardinal.add_eq_left_iff
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u_1}
n : ℕ
ha : ℵ₀ ≤ a
⊢ a + (↑n : Cardinal.{u_1}) = a

Tactic:
add_eq_left ha (natCast_le_aleph0.trans ha)

Premises used: Cardinal.add_eq_left, LE.le.trans, Cardinal.natCast_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u_1}
n : ℕ
ha : ℵ₀ ≤ a
rw : a + (↑n : Cardinal.{u_1}) = a
rw₁ rw₂ : a = a
⊢ (↑n : Cardinal.{u_1}) + a = a

Tactic:
rw [add_comm, add_nat_eq n ha]

Premises used: add_comm, Cardinal.add_nat_eq
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ a + 1 = a

Tactic:
add_one_of_aleph0_le ha

Premises used: Cardinal.add_one_of_aleph0_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : Infinite α
⊢ #α + 1 = #α

Tactic:
add_one_eq (aleph0_le_mk α)

Premises used: Cardinal.add_one_eq, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
i : α
h : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
hα : ℵ₀ ≤ #α
rw : #(↑(Iio i) : Type u_1) + 1 < #α
⊢ #(↑(Iic i) : Type u_1) < #α

Tactic:
rw [← Iio_insert, mk_insert self_notMem_Iio]

Premises used: Set.self_notMem_Iio, Cardinal.mk_insert, Set.Iio_insert
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
i : α
h : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
hα : ℵ₀ ≤ #α
⊢ #(↑(Iio i) : Type u_1) + 1 < #α

Tactic:
add_one_lt_of_lt hα (mk_Iio_lt i h)

Premises used: Cardinal.mk_Iio_lt, Cardinal.add_one_lt_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
i : α
h : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
hα : ℵ₀ ≤ #α
⊢ #(↑(Iio i) : Type u_1) + 1 < #α

Tactic:
exact add_one_lt_of_lt hα (mk_Iio_lt i h)

Premises used: Cardinal.mk_Iio_lt, Cardinal.add_one_lt_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedGT α
i : α
h : (#α).ord = type fun (x1 x2 : αᵒᵈ) ↦ x1 < x2
hα : ℵ₀ ≤ #α
⊢ #(↑(Ici i) : Type u_1) < #α

Tactic:
mk_Iic_lt (OrderDual.toDual i) h hα

Premises used: OrderDual.toDual, Set.Ici, setOf, Cardinal.mk_Iic_lt, OrderDual, DFunLike.coe
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
inl : ∀ (hb : ℵ₀ ≤ b), b = c
inr : ∀ (hb : b < ℵ₀), b = c
⊢ b = c

Tactic:
rcases le_or_gt ℵ₀ b with hb | hb

Premises used: Cardinal.aleph0, le_or_gt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a < b

Tactic:
have : a < b := ha.trans_le hb
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
⊢ a + c = b

Tactic:
rw [add_eq_right hb this.le, eq_comm] at h

Premises used: LT.lt.le, eq_comm, Cardinal.add_eq_right
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
h₁ : a + c = b
⊢ a < ℵ₀

Tactic:
rw [add_eq_right hb this.le, eq_comm] at h

Premises used: LT.lt.le, eq_comm, Cardinal.add_eq_right
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
h₁ : a + c = b
ha₁ : a < ℵ₀
⊢ ℵ₀ ≤ b

Tactic:
rw [add_eq_right hb this.le, eq_comm] at h

Premises used: LT.lt.le, eq_comm, Cardinal.add_eq_right
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
h₁ : a + c = b
ha₁ : a < ℵ₀
hb₁ : ℵ₀ ≤ b
⊢ a < b

Tactic:
rw [add_eq_right hb this.le, eq_comm] at h

Premises used: LT.lt.le, eq_comm, Cardinal.add_eq_right
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + c = b
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
inl inl₁ : b = b
⊢ b = c

Tactic:
rw [eq_of_add_eq_of_aleph0_le h this hb]

Premises used: Cardinal.eq_of_add_eq_of_aleph0_le