awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
rw : ¬ℵ₀ ≤ c
⊢ c < ℵ₀

Tactic:
rw [← not_le]

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

Tactic:
apply lt_irrefl ℵ₀

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

Tactic:
apply (hc.trans (self_le_add_left _ a)).trans_lt

Premises used: self_le_add_left, LE.le.trans, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
rw : a + b < ℵ₀
⊢ a + c < ℵ₀

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

Tactic:
apply add_lt_aleph0 ha hb

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

Tactic:
have hc : c < ℵ₀ := by
      rw [← not_le]
      intro hc
      apply lt_irrefl ℵ₀
      apply (hc.trans (self_le_add_left _ a)).trans_lt
      rw [← h]
      apply add_lt_aleph0 ha hb
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : c < ℵ₀
⊢ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1})

Tactic:
rw [lt_aleph0] at *

Premises used: Cardinal.lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : c < ℵ₀
ha₁ : ∃ (n : ℕ), a = (↑n : Cardinal.{u_1})
⊢ ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})

Tactic:
rw [lt_aleph0] at *

Premises used: Cardinal.lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : c < ℵ₀
ha₁ : ∃ (n : ℕ), a = (↑n : Cardinal.{u_1})
hb₁ : ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
⊢ ∃ (n : ℕ), c = (↑n : Cardinal.{u_1})

Tactic:
rw [lt_aleph0] at *

Premises used: Cardinal.lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : ∃ (n : ℕ), a = (↑n : Cardinal.{u_1})
hb : ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
hc : ∃ (n : ℕ), c = (↑n : Cardinal.{u_1})
inr : ∀ (n : ℕ) (h : (↑n : Cardinal.{u_1}) + b = (↑n : Cardinal.{u_1}) + c), b = c
⊢ b = c

Tactic:
rcases ha with ⟨n, rfl⟩

Premises used: rfl
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
b c : Cardinal.{u_1}
hb : ∃ (n : ℕ), b = (↑n : Cardinal.{u_1})
hc : ∃ (n : ℕ), c = (↑n : Cardinal.{u_1})
n : ℕ
h : (↑n : Cardinal.{u_1}) + b = (↑n : Cardinal.{u_1}) + c
inr :
  ∀ (m : ℕ)
    (h : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) + c),
    (↑m : Cardinal.{u_1}) = c
⊢ b = c

Tactic:
rcases hb with ⟨m, rfl⟩

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

Tactic:
rcases hc with ⟨k, rfl⟩

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

Tactic:
norm_cast at h ⊢
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
n m k : ℕ
h : n + m = n + k
⊢ m = k

Tactic:
apply add_left_cancel h

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

Tactic:
rw [add_comm a b, add_comm c b] at h

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

Tactic:
rw [add_comm a b, add_comm c b] at h

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

Tactic:
Cardinal.eq_of_add_eq_add_left h hb

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

Tactic:
exact Cardinal.eq_of_add_eq_add_left h hb

Premises used: Cardinal.eq_of_add_eq_add_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : Infinite α
obtain :
  ∀ (α_1 : LinearOrder α) (w : WellFoundedLT α) (hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2),
    ∃ (r : α → α → Prop), (∀ (x : α), #{ y : α // ¬r x y } < #α) ∧ ∀ (y : α), #{ x : α // r x y } < #α
⊢ ∃ (r : α → α → Prop), (∀ (x : α), #{ y : α // ¬r x y } < #α) ∧ ∀ (y : α), #{ x : α // r x y } < #α

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

Premises used: Cardinal.exists_ord_eq_type_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α_1 : Type u_1
inst : Infinite α_1
α : LinearOrder α_1
w : WellFoundedLT α_1
hα : (#α_1).ord = type fun (x1 x2 : α_1) ↦ x1 < x2
⊢ ∃ (r : α_1 → α_1 → Prop), (∀ (x : α_1), #{ y : α_1 // ¬r x y } < #α_1) ∧ ∀ (y : α_1), #{ x : α_1 // r x y } < #α_1

Tactic:
⟨LT.lt, fun x ↦ ?_, fun y ↦ mk_Iio_lt _ hα⟩

Premises used: Cardinal.mk_Iio_lt, And.intro, LT.lt, Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α_1 : Type u_1
inst : Infinite α_1
α : LinearOrder α_1
w : WellFoundedLT α_1
hα : (#α_1).ord = type fun (x1 x2 : α_1) ↦ x1 < x2
refine : ∀ (x : α_1), #{ y : α_1 // ¬x < y } < #α_1
⊢ ∃ (r : α_1 → α_1 → Prop), (∀ (x : α_1), #{ y : α_1 // ¬r x y } < #α_1) ∧ ∀ (y : α_1), #{ x : α_1 // r x y } < #α_1

Tactic:
refine ⟨LT.lt, fun x ↦ ?_, fun y ↦ mk_Iio_lt _ hα⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α_1 : Type u_1
inst : Infinite α_1
α : LinearOrder α_1
w : WellFoundedLT α_1
hα : (#α_1).ord = type fun (x1 x2 : α_1) ↦ x1 < x2
x : α_1
⊢ #{ y : α_1 // ¬x < y } < #α_1

Tactic:
simpa using mk_Iic_lt _ hα (aleph0_le_mk _)

Premises used: Cardinal.mk_Iic_lt, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
i : ι
grw grw₁ : iSup f + c ≤ iSup f + c
⊢ f i + c ≤ (⨆ (i : ι), f i) + c

Tactic:
grw [le_ciSup hf i]

Premises used: le_ciSup
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c

Tactic:
have (i : ι) : f i + c ≤ (⨆ i, f i) + c := by grw [le_ciSup hf i]
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c
⊢ (⨆ (i : ι), f i) + c = ⨆ (i : ι), f i + c

Tactic:
le_antisymm ?_ (ciSup_le' this)

Premises used: ciSup_le', le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c
refine : (⨆ (i : ι), f i) + c ≤ ⨆ (i : ι), f i + c
⊢ (⨆ (i : ι), f i) + c = ⨆ (i : ι), f i + c

Tactic:
refine le_antisymm ?_ (ciSup_le' this)

Premises used: ciSup_le', le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c
⊢ BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x + c)

Tactic:
have bdd : BddAbove (range (f · + c)) := ⟨_, forall_mem_range.mpr this⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x + c)
inl : ∀ (hs : ⨆ (i : ι), f i < ℵ₀), (⨆ (i : ι), f i) + c ≤ ⨆ (i : ι), f i + c
inr : ∀ (hs : ℵ₀ ≤ ⨆ (i : ι), f i), (⨆ (i : ι), f i) + c ≤ ⨆ (i : ι), f i + c
⊢ (⨆ (i : ι), f i) + c ≤ ⨆ (i : ι), f i + c

Tactic:
obtain hs | hs := lt_or_ge (⨆ i, f i) ℵ₀

Premises used: iSup, Cardinal.aleph0, lt_or_ge
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x + c)
hs : ⨆ (i : ι), f i < ℵ₀
inl : ∀ (i : ι) (hi : f i = ⨆ (i : ι), f i), (⨆ (i : ι), f i) + c ≤ ⨆ (i : ι), f i + c
⊢ (⨆ (i : ι), f i) + c ≤ ⨆ (i : ι), f i + c

Tactic:
obtain ⟨i, hi⟩ := exists_eq_ciSup_of_not_isSuccLimit hf (not_isSuccLimit_of_lt_aleph0 hs)

Premises used: exists_eq_ciSup_of_not_isSuccLimit, Cardinal.not_isSuccLimit_of_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x + c)
hs : ⨆ (i : ι), f i < ℵ₀
i : ι
hi : f i = ⨆ (i : ι), f i
⊢ (⨆ (i : ι), f i) + c ≤ ⨆ (i : ι), f i + c

Tactic:
hi ▸ le_ciSup bdd i

Premises used: Eq.rec, le_ciSup
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x + c)
hs : ⨆ (i : ι), f i < ℵ₀
i : ι
hi : f i = ⨆ (i : ι), f i
⊢ (⨆ (i : ι), f i) + c ≤ ⨆ (i : ι), f i + c

Tactic:
exact hi ▸ le_ciSup bdd i
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x + c)
hs : ℵ₀ ≤ ⨆ (i : ι), f i
inr : LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i) (⨆ (i : ι), f i + c) ∧ c ≤ ⨆ (i : ι), f i + c
⊢ (⨆ (i : ι), f i) + c ≤ ⨆ (i : ι), f i + c

Tactic:
rw [add_eq_max hs, max_le_iff]

Premises used: max_le_iff, Cardinal.add_eq_max
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x + c)
hs : ℵ₀ ≤ ⨆ (i : ι), f i
⊢ LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i) (⨆ (i : ι), f i + c) ∧ c ≤ ⨆ (i : ι), f i + c

Tactic:
⟨ciSup_mono bdd fun i ↦ self_le_add_right _ c,
    (self_le_add_left _ _).trans (le_ciSup bdd <| Classical.arbitrary ι)⟩

Premises used: self_le_add_right, self_le_add_left, le_ciSup, And.intro, Classical.arbitrary, LE.le.trans, ciSup_mono
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ (i : ι), f i) + c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x + c)
hs : ℵ₀ ≤ ⨆ (i : ι), f i
⊢ LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i) (⨆ (i : ι), f i + c) ∧ c ≤ ⨆ (i : ι), f i + c

Tactic:
exact ⟨ciSup_mono bdd fun i ↦ self_le_add_right _ c,
    (self_le_add_left _ _).trans (le_ciSup bdd <| Classical.arbitrary ι)⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
rw : Eq.{v + 2} (α := Cardinal.{v}) (⨆ (i : ι), f i + c) (⨆ (i : ι), c + f i)
⊢ c + ⨆ (i : ι), f i = ⨆ (i : ι), c + f i

Tactic:
rw [add_comm, Cardinal.ciSup_add f hf]

Premises used: add_comm, Cardinal.ciSup_add
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
inst : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ Eq.{v + 2} (α := Cardinal.{v}) (⨆ (i : ι), f i + c) (⨆ (i : ι), c + f i)

Tactic:
simp_rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
inst : Nonempty ι
inst_1 : Nonempty ι'
hf : BddAbove (range f)
g : ι' → Cardinal.{v}
hg : BddAbove (range g)
simp_rw : Eq.{v + 2} (α := Cardinal.{v}) (⨆ (i : ι), f i + ⨆ (j : ι'), g j) (⨆ (i : ι), ⨆ (j : ι'), f i + g j)
⊢ HAdd.hAdd (α := Cardinal.{v}) (⨆ (i : ι), f i) (⨆ (j : ι'), g j) = ⨆ (i : ι), ⨆ (j : ι'), f i + g j

Tactic:
simp_rw [Cardinal.ciSup_add f hf, Cardinal.add_ciSup g hg]

Premises used: Cardinal.add_ciSup, Cardinal.ciSup_add
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
inl : IsEmpty ι → (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
inr : Nonempty ι → (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : IsEmpty ι
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
inr : HMul.hMul (α := Cardinal.{v}) (⨆ (i : ι), f i) 0 = ⨆ (i : ι), f i * 0
inr₁ : ∀ (h0 : c ≠ 0), (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c

Tactic:
obtain rfl | h0 := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
h : Nonempty ι
⊢ HMul.hMul (α := Cardinal.{v}) (⨆ (i : ι), f i) 0 = ⨆ (i : ι), f i * 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
pos : ∀ (hf : BddAbove (range f)), (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
neg : ∀ (hf : ¬BddAbove (range f)), (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c

Tactic:
by_cases hf : BddAbove (range f)

Premises used: BddAbove, Set.range
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : ¬BddAbove (range f)
⊢ ¬BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)

Tactic:
have hfc : ¬ BddAbove (range (f · * c)) := fun bdd ↦ hf
      ⟨⨆ i, f i * c, forall_mem_range.mpr fun i ↦ (le_mul_right h0).trans (le_ciSup bdd i)⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : ¬BddAbove (range f)
hfc : ¬BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c

Tactic:
simp [iSup, csSup_of_not_bddAbove, hf, hfc]

Premises used: iSup, csSup_of_not_bddAbove
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
i : ι
grw grw₁ : f i * c ≤ f i * c
⊢ f i * c ≤ (⨆ (i : ι), f i) * c

Tactic:
grw [← le_ciSup hf i]

Premises used: le_ciSup
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
⊢ ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c

Tactic:
have (i : ι) : f i * c ≤ (⨆ i, f i) * c := by grw [← le_ciSup hf i]
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c

Tactic:
le_antisymm ?_ (ciSup_le' this)

Premises used: ciSup_le', le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
pos : (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c
⊢ (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c

Tactic:
refine le_antisymm ?_ (ciSup_le' this)

Premises used: ciSup_le', le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
⊢ BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)

Tactic:
have bdd : BddAbove (range (f · * c)) := ⟨_, forall_mem_range.mpr this⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)
pos : ∀ (hs : ⨆ (i : ι), f i < ℵ₀), (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c
pos₁ : ∀ (hs : ℵ₀ ≤ ⨆ (i : ι), f i), (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c
⊢ (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c

Tactic:
obtain hs | hs := lt_or_ge (⨆ i, f i) ℵ₀

Premises used: iSup, Cardinal.aleph0, lt_or_ge
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)
hs : ⨆ (i : ι), f i < ℵ₀
pos : ∀ (i : ι) (hi : f i = ⨆ (i : ι), f i), (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c
⊢ (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c

Tactic:
obtain ⟨i, hi⟩ := exists_eq_ciSup_of_not_isSuccLimit hf (not_isSuccLimit_of_lt_aleph0 hs)

Premises used: exists_eq_ciSup_of_not_isSuccLimit, Cardinal.not_isSuccLimit_of_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)
hs : ⨆ (i : ι), f i < ℵ₀
i : ι
hi : f i = ⨆ (i : ι), f i
⊢ (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c

Tactic:
hi ▸ le_ciSup bdd i

Premises used: Eq.rec, le_ciSup
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)
hs : ⨆ (i : ι), f i < ℵ₀
i : ι
hi : f i = ⨆ (i : ι), f i
⊢ (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c

Tactic:
exact hi ▸ le_ciSup bdd i
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)
hs : ℵ₀ ≤ ⨆ (i : ι), f i
pos : LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i) (⨆ (i : ι), f i * c) ∧ c ≤ ⨆ (i : ι), f i * c
⊢ (⨆ (i : ι), f i) * c ≤ ⨆ (i : ι), f i * c

Tactic:
rw [mul_eq_max_of_aleph0_le_left hs h0, max_le_iff]

Premises used: max_le_iff, Cardinal.mul_eq_max_of_aleph0_le_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)
hs : ℵ₀ ≤ ⨆ (i : ι), f i
pos :
  ∀ (i : ι) (hi : 1 < f i),
    LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i) (⨆ (i : ι), f i * c) ∧ c ≤ ⨆ (i : ι), f i * c
⊢ LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i) (⨆ (i : ι), f i * c) ∧ c ≤ ⨆ (i : ι), f i * c

Tactic:
obtain ⟨i, hi⟩ := exists_lt_of_lt_ciSup' (one_lt_aleph0.trans_le hs)

Premises used: Cardinal.one_lt_aleph0, LT.lt.trans_le, exists_lt_of_lt_ciSup'
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)
hs : ℵ₀ ≤ ⨆ (i : ι), f i
i : ι
hi : 1 < f i
⊢ LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i) (⨆ (i : ι), f i * c) ∧ c ≤ ⨆ (i : ι), f i * c

Tactic:
⟨ciSup_mono bdd fun i ↦ le_mul_right h0,
    (le_mul_left (zero_lt_one.trans hi).ne').trans (le_ciSup bdd i)⟩

Premises used: Cardinal.le_mul_left, LT.lt.ne', zero_lt_one, le_ciSup, Cardinal.le_mul_right, And.intro, LT.lt.trans, LE.le.trans, ciSup_mono
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ (i : ι), f i) * c
bdd : BddAbove.{v + 1} (α := Cardinal.{v}) (range fun (x : ι) ↦ f x * c)
hs : ℵ₀ ≤ ⨆ (i : ι), f i
i : ι
hi : 1 < f i
⊢ LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i) (⨆ (i : ι), f i * c) ∧ c ≤ ⨆ (i : ι), f i * c

Tactic:
exact ⟨ciSup_mono bdd fun i ↦ le_mul_right h0,
    (le_mul_left (zero_lt_one.trans hi).ne').trans (le_ciSup bdd i)⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
rw : Eq.{v + 2} (α := Cardinal.{v}) (⨆ (i : ι), f i * c) (⨆ (i : ι), c * f i)
⊢ c * ⨆ (i : ι), f i = ⨆ (i : ι), c * f i

Tactic:
rw [mul_comm, Cardinal.ciSup_mul f]

Premises used: Cardinal.ciSup_mul, mul_comm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ Eq.{v + 2} (α := Cardinal.{v}) (⨆ (i : ι), f i * c) (⨆ (i : ι), c * f i)

Tactic:
simp_rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
g : ι' → Cardinal.{v}
simp_rw : Eq.{v + 2} (α := Cardinal.{v}) (⨆ (i : ι), f i * ⨆ (j : ι'), g j) (⨆ (i : ι), ⨆ (j : ι'), f i * g j)
⊢ HMul.hMul (α := Cardinal.{v}) (⨆ (i : ι), f i) (⨆ (j : ι'), g j) = ⨆ (i : ι), ⨆ (j : ι'), f i * g j

Tactic:
simp_rw [Cardinal.ciSup_mul f, Cardinal.mul_ciSup g]

Premises used: Cardinal.mul_ciSup, Cardinal.ciSup_mul
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ lift.{u, v} (⨆ (i : ι), f i)
⊢ lift.{v, u} #ι ≤ ⨆ (i : ι), lift.{u, v} (f i)

Tactic:
rw [lift_iSup bddAbove_of_small] at h

Premises used: Cardinal.lift_iSup, Cardinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ (i : ι), lift.{u, v} (f i)
apply : sum f ≤ lift.{u, v} (⨆ (i : ι), f i)
⊢ sum f = lift.{u, v} (⨆ (i : ι), f i)

Tactic:
apply (lift_iSup_le_sum f).antisymm'

Premises used: LE.le.antisymm', Cardinal.lift_iSup_le_sum
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ (i : ι), lift.{u, v} (f i)
⊢ sum f ≤ lift.{v, u} #ι * ⨆ (i : ι), lift.{u, v} (f i)

Tactic:
sum_le_lift_mk_mul_iSup_lift f

Premises used: Cardinal.sum_le_lift_mk_mul_iSup_lift
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ (i : ι), lift.{u, v} (f i)
h₁ : lift.{u, v} (⨆ (i : ι), f i) = lift.{v, u} #ι * ⨆ (i : ι), lift.{u, v} (f i)
⊢ sum f ≤ lift.{u, v} (⨆ (i : ι), f i)

Tactic:
convert! sum_le_lift_mk_mul_iSup_lift f

Premises used: Cardinal.sum_le_lift_mk_mul_iSup_lift