-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_eq_zero_iff {f : lp E p} : ‖f‖ = 0 ↔ f = 0

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
⊢ f = 0

Tactic:
rcases p.trichotomy with (rfl | rfl | hp)

Result:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
⊢ f = 0

case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
h : ‖f‖ = 0
⊢ f = 0

case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
⊢ f = 0

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : (fun i => ‖↑f i‖ ^ p.toReal) = 0
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
i : α
⊢ ↑f i = 0 ∧ p.toReal ≠ 0

Tactic:
simpa [Real.rpow_eq_zero_iff_of_nonneg (norm_nonneg (f i))] using congr_fun hf i

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
i : α
⊢ {i | ¬↑f i = 0} = ∅

Tactic:
simpa [lp.norm_eq_card_dsupport f] using h

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
⊢ HasSum (fun i => ‖↑f i‖ ^ p.toReal) 0

Tactic:
have := lp.hasSum_norm hp f

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
this : HasSum (fun i => ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
⊢ HasSum (fun i => ‖↑f i‖ ^ p.toReal) 0

Proof state:
case inr.inr.h.h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : (fun i => ‖↑f i‖ ^ p.toReal) = 0
this✝ : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
i : α
this : ↑f i = 0 ∧ p.toReal ≠ 0
⊢ ↑f i = ↑0 i

Tactic:
exact this.1

Result:
no goals

Proof state:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
h : ‖f‖ = 0
⊢ f = 0

Tactic:
rcases isEmpty_or_nonempty α with _i | _i

Result:
case inr.inl.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
h : ‖f‖ = 0
_i : IsEmpty α
⊢ f = 0

case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
h : ‖f‖ = 0
_i : Nonempty α
⊢ f = 0

Proof state:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
h : ‖f‖ = 0
_i : Nonempty α
⊢ IsLUB (Set.range fun i => ‖↑f i‖) 0

Tactic:
simpa [h] using lp.isLUB_norm f

Result:
no goals

Proof state:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : (fun i => ‖↑f i‖ ^ p.toReal) = 0
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ f = 0

Tactic:
ext i

Result:
case inr.inr.h.h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : (fun i => ‖↑f i‖ ^ p.toReal) = 0
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
i : α
⊢ ↑f i = ↑0 i

Proof state:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
⊢ f = 0

Tactic:
have hf : HasSum (fun i : α => ‖f i‖ ^ p.toReal) 0 := by
  have := lp.hasSum_norm hp f
  rwa [h, Real.zero_rpow hp.ne'] at this

Result:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : HasSum (fun i => ‖↑f i‖ ^ p.toReal) 0
⊢ f = 0

Proof state:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : HasSum (fun i => ‖↑f i‖ ^ p.toReal) 0
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ f = 0

Tactic:
rw [hasSum_zero_iff_of_nonneg this] at hf

Result:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : (fun i => ‖↑f i‖ ^ p.toReal) = 0
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ f = 0

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ ‖f‖ = 0 ↔ f = 0

Tactic:
refine ⟨fun h => ?_, by rintro rfl; exact norm_zero⟩

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
⊢ f = 0

Proof state:
case inl.h.h
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
i : α
this : {i | ¬↑f i = 0} = ∅
⊢ ↑f i = ↑0 i

Tactic:
have : (¬f i = 0) = False := congr_fun this i

Result:
case inl.h.h
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
i : α
this✝ : {i | ¬↑f i = 0} = ∅
this : (¬↑f i = 0) = False
⊢ ↑f i = ↑0 i

Proof state:
case inr.inl.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
h : ‖f‖ = 0
_i : IsEmpty α
⊢ f = 0

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
case inr.inl.inr.h.h
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
h : ‖f‖ = 0
_i : Nonempty α
H : IsLUB (Set.range fun i => ‖↑f i‖) 0
i : α
⊢ ↑f i = ↑0 i

Tactic:
have : ‖f i‖ = 0 := le_antisymm (H.1 ⟨i, rfl⟩) (norm_nonneg _)

Result:
case inr.inl.inr.h.h
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
h : ‖f‖ = 0
_i : Nonempty α
H : IsLUB (Set.range fun i => ‖↑f i‖) 0
i : α
this : ‖↑f i‖ = 0
⊢ ↑f i = ↑0 i

Proof state:
case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
h : ‖f‖ = 0
_i : Nonempty α
⊢ f = 0

Tactic:
have H : IsLUB (Set.range fun i => ‖f i‖) 0 := by simpa [h] using lp.isLUB_norm f

Result:
case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
h : ‖f‖ = 0
_i : Nonempty α
H : IsLUB (Set.range fun i => ‖↑f i‖) 0
⊢ f = 0

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ f = 0 → ‖f‖ = 0

Tactic:
rintro rfl

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0

Proof state:
case inl.h.h
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
i : α
⊢ ↑f i = ↑0 i

Tactic:
have : { i : α | ¬f i = 0 } = ∅ := by simpa [lp.norm_eq_card_dsupport f] using h

Result:
case inl.h.h
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
i : α
this : {i | ¬↑f i = 0} = ∅
⊢ ↑f i = ↑0 i

Proof state:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
⊢ f = 0

Tactic:
ext i

Result:
case inl.h.h
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
i : α
⊢ ↑f i = ↑0 i

Proof state:
case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
h : ‖f‖ = 0
_i : Nonempty α
H : IsLUB (Set.range fun i => ‖↑f i‖) 0
⊢ f = 0

Tactic:
ext i

Result:
case inr.inl.inr.h.h
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
h : ‖f‖ = 0
_i : Nonempty α
H : IsLUB (Set.range fun i => ‖↑f i‖) 0
i : α
⊢ ↑f i = ↑0 i

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
this : HasSum (fun i => ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
⊢ HasSum (fun i => ‖↑f i‖ ^ p.toReal) 0

Tactic:
rwa [h, Real.zero_rpow hp.ne'] at this

Result:
no goals