Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ (ENNReal.ofReal (dist f.fst g.fst) ^ p.toReal + ENNReal.ofReal (dist f.snd g.snd) ^ p.toReal) ^ p.toReal⁻¹ =
    (ENNReal.ofReal (dist f.fst g.fst ^ p.toReal) + ENNReal.ofReal (dist f.snd g.snd ^ p.toReal)) ^ p.toReal⁻¹

pp: case inr.hp
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ dist f.fst g.fst ^ p.toReal

pp: case inr.hq
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ dist f.snd g.snd ^ p.toReal

pp: case inr.hx_nonneg
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal

pp: case inr.hp_nonneg
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ p.toReal⁻¹

Tactic:
← ENNReal.ofReal_rpow_of_nonneg,

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ (ENNReal.ofReal (dist f.fst g.fst) ^ p.toReal + ENNReal.ofReal (dist f.snd g.snd) ^ p.toReal) ^ p.toReal⁻¹ =
    (ENNReal.ofReal (dist f.fst g.fst) ^ p.toReal + ENNReal.ofReal (dist f.snd g.snd ^ p.toReal)) ^ p.toReal⁻¹

case inr.hx_nonneg
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ dist f.fst g.fst

case inr.hp_nonneg
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ p.toReal

case inr.hp
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ dist f.fst g.fst ^ p.toReal

case inr.hq
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ dist f.snd g.snd ^ p.toReal

case inr.hx_nonneg
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal

case inr.hp_nonneg
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ p.toReal⁻¹