Theorem: ENat.mul_iSup (Matroid/ForMathlib/ENatTopology.lean)

State before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
⊢ c * ⨆ i, f i = ⨆ i, c * f i
Tactic:
by_cases hf : ∀ i, f i = 0
State after:
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ∀ (i : ι), f i = 0
⊢ c * ⨆ i, f i = ⨆ i, c * f i

case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ¬∀ (i : ι), f i = 0
⊢ c * ⨆ i, f i = ⨆ i, c * f i

State before:
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ¬∀ (i : ι), f i = 0
⊢ c * ⨆ i, f i = ⨆ i, c * f i
Tactic:
refine' (monotone_id.const_mul' _).map_iSup_of_continuousAt _ (mul_zero c)
State after:
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ¬∀ (i : ι), f i = 0
⊢ ContinuousAt (fun x => c * id x) (⨆ i, f i)

State before:
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ¬∀ (i : ι), f i = 0
⊢ ContinuousAt (fun x => c * id x) (⨆ i, f i)
Tactic:
refine' ENat.Tendsto.const_mul tendsto_id (Or.inl _)
State after:
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ¬∀ (i : ι), f i = 0
⊢ id (⨆ i, f i) ≠ 0

State before:
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ¬∀ (i : ι), f i = 0
⊢ id (⨆ i, f i) ≠ 0
Tactic:
exact mt ENat.iSup_eq_zero.1 hf
State after:
no goals

State before:
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ∀ (i : ι), f i = 0
⊢ c * ⨆ i, f i = ⨆ i, c * f i
Tactic:
obtain rfl : f = fun _ ↦ 0
State after:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ∀ (i : ι), f i = 0
⊢ f = fun x => 0

case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
hf : ∀ (i : ι), (fun x => 0) i = 0
⊢ c * ⨆ i, (fun x => 0) i = ⨆ i, c * (fun x => 0) i

State before:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
f : ι → ℕ∞
hf : ∀ (i : ι), f i = 0
⊢ f = fun x => 0

case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
hf : ∀ (i : ι), (fun x => 0) i = 0
⊢ c * ⨆ i, (fun x => 0) i = ⨆ i, c * (fun x => 0) i
Tactic:
exact funext hf
State after:
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
hf : ∀ (i : ι), (fun x => 0) i = 0
⊢ c * ⨆ i, (fun x => 0) i = ⨆ i, c * (fun x => 0) i

State before:
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
s : Set α
n : ℕ∞
ι : Sort u_4
c : ℕ∞
hf : ∀ (i : ι), (fun x => 0) i = 0
⊢ c * ⨆ i, (fun x => 0) i = ⨆ i, c * (fun x => 0) i
Tactic:
simp only [mul_zero, ENat.iSup_zero_eq_zero]
State after:
no goals