-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem ciSup_mul (c : Cardinal.{v}) : (⨆ i, f i) * c = ⨆ i, f i * c

Proof state:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : IsEmpty ι
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

case inr
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Proof state:
case pos.inr.intro
ι : 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 (range fun x => f x * c)
hs : ℵ₀ ≤ ⨆ i, f i
i : ι
hi : 1 < f i
⊢ ⨆ 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)⟩

Result:
no goals

Proof state:
case pos
ι : 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:
refine le_antisymm ?_ (ciSup_le' this)

Result:
case pos
ι : 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

Proof state:
case neg
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : ¬BddAbove (range f)
hfc : ¬BddAbove (range fun x => f x * c)
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

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

Result:
no goals

Proof state:
case pos
ι : 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 (range fun x => f x * c)
⊢ (⨆ i, f i) * c ≤ ⨆ i, f i * c

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

Result:
case pos.inl
ι : 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 (range fun x => f x * c)
hs : ⨆ i, f i < ℵ₀
⊢ (⨆ i, f i) * c ≤ ⨆ i, f i * c

case pos.inr
ι : 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 (range fun x => f x * c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ (⨆ i, f i) * c ≤ ⨆ i, f i * c

Proof state:
case pos
ι : 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

case neg
ι : 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:
swap

Result:
case neg
ι : 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

case pos
ι : 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

Proof state:
case inl
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : IsEmpty ι
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
simp

Result:
no goals

Proof state:
case inr.inl
ι : Type u
f : ι → Cardinal.{v}
h✝ : Nonempty ι
⊢ (⨆ i, f i) * 0 = ⨆ i, f i * 0

Tactic:
simp

Result:
no goals

Proof state:
case pos.inl
ι : 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 (range fun x => f x * c)
hs : ⨆ i, f i < ℵ₀
⊢ (⨆ i, f i) * c ≤ ⨆ i, f i * c

Tactic:
obtain ⟨i, hi⟩ := exists_eq_of_iSup_eq_of_not_isSuccLimit
  f hf (not_isSuccLimit_of_lt_aleph0 hs) rfl

Result:
case pos.inl.intro
ι : 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 (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

Proof state:
case pos.inl.intro
ι : 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 (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

Result:
no goals

Proof state:
case pos.inr
ι : 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 (range fun x => f x * c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ ⨆ 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)

Result:
case pos.inr.intro
ι : 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 (range fun x => f x * c)
hs : ℵ₀ ≤ ⨆ i, f i
i : ι
hi : 1 < f i
⊢ ⨆ i, f i ≤ ⨆ i, f i * c ∧ c ≤ ⨆ i, f i * c

Proof state:
case inr.inr
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
by_cases hf : BddAbove (range f)

Result:
case pos
ι : 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

case neg
ι : 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

Proof state:
case pos.inr
ι : 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 (range fun x => f x * c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ (⨆ i, f i) * c ≤ ⨆ i, f i * c

Tactic:
rw [mul_eq_max_of_aleph0_le_left hs h0, max_le_iff]

Result:
case pos.inr
ι : 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 (range fun x => f x * c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ ⨆ i, f i ≤ ⨆ i, f i * c ∧ c ≤ ⨆ i, f i * c

Proof state:
case pos
ι : 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 := fun i ↦ mul_le_mul_right' (le_ciSup hf i) c

Result:
case pos
ι : 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

Proof state:
case inr
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
obtain rfl | h0 := eq_or_ne c 0

Result:
case inr.inl
ι : Type u
f : ι → Cardinal.{v}
h✝ : Nonempty ι
⊢ (⨆ i, f i) * 0 = ⨆ i, f i * 0

case inr.inr
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
⊢ (⨆ i, f i) * c = ⨆ i, f i * c