awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : IsBoundedSMul 𝕜 α
inst_6 : IsBoundedSMul 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + (‖c‖₊ * ‖f.snd‖₊) ^ p.toReal
have inr : ‖(c • f).fst‖₊ ≤ ‖c‖₊ * ‖f.fst‖₊
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : IsBoundedSMul 𝕜 α
inst_6 : IsBoundedSMul 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : ‖(c • f).fst‖₊ ≤ ‖c‖₊ * ‖f.fst‖₊
⊢ ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + (‖c‖₊ * ‖f.snd‖₊) ^ p.toReal
have inr₁ : ‖(c • f).snd‖₊ ≤ ‖c‖₊ * ‖f.snd‖₊
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f : WithLp ∞ (α × β)), ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
Tactic: rcases p.dichotomy with (rfl | hp)
Cleared hypotheses: p, hp, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f : WithLp ∞ (α × β)), ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inr : ∀ (hp_1 : 1 ≤ p.toReal), ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
Tactic: rcases p.dichotomy with (rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (hypothesis)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have hp0 : 0 < p.toReal
Tactic: have hp0 : 0 < p.toReal := zero_lt_one.trans_le hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (hypothesis)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have hpt : p ≠ ∞
Tactic: have hpt : p ≠ ⊤ := p.toReal_pos_iff_ne_top.mp hp0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inr : (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) = ‖c‖₊ * ‖f‖₊
Tactic: rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne',
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add,
        ← NNReal.mul_rpow, ← NNReal.mul_rpow, smul_fst, smul_snd, nnnorm_smul, nnnorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) = ‖c‖₊ * ‖f‖₊
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inr₁ : (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) =
  ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)
Tactic: rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne',
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add,
        ← NNReal.mul_rpow, ← NNReal.mul_rpow, smul_fst, smul_snd, nnnorm_smul, nnnorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) = ‖c‖₊ * ‖f‖₊
inr₁ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inr₂ : (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ p.toReal⁻¹ =
  ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹
Tactic: rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne',
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add,
        ← NNReal.mul_rpow, ← NNReal.mul_rpow, smul_fst, smul_snd, nnnorm_smul, nnnorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) = ‖c‖₊ * ‖f‖₊
inr₁ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)
inr₂ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ p.toReal⁻¹ =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inr₃ : ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
  (‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
Tactic: rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne',
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add,
        ← NNReal.mul_rpow, ← NNReal.mul_rpow, smul_fst, smul_snd, nnnorm_smul, nnnorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) = ‖c‖₊ * ‖f‖₊
inr₁ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)
inr₂ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ p.toReal⁻¹ =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹
inr₃ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    (‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inr₄ : ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
  ‖c‖₊ ^ p.toReal * ((‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
Tactic: rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne',
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add,
        ← NNReal.mul_rpow, ← NNReal.mul_rpow, smul_fst, smul_snd, nnnorm_smul, nnnorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) = ‖c‖₊ * ‖f‖₊
inr₁ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)
inr₂ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ p.toReal⁻¹ =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹
inr₃ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    (‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
inr₄ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * ((‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inr₅ : ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
  ‖c‖₊ ^ p.toReal * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (p.toReal⁻¹ * p.toReal)
Tactic: rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne',
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add,
        ← NNReal.mul_rpow, ← NNReal.mul_rpow, smul_fst, smul_snd, nnnorm_smul, nnnorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) = ‖c‖₊ * ‖f‖₊
inr₁ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)
inr₂ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ p.toReal⁻¹ =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹
inr₃ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    (‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
inr₄ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * ((‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
inr₅ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (p.toReal⁻¹ * p.toReal)
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inr₆ : ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
  ‖c‖₊ ^ p.toReal * HPow.hPow (β := ℝ) (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) 1
Tactic: rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne',
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add,
        ← NNReal.mul_rpow, ← NNReal.mul_rpow, smul_fst, smul_snd, nnnorm_smul, nnnorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) = ‖c‖₊ * ‖f‖₊
inr₁ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)
inr₂ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ p.toReal⁻¹ =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹
inr₃ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    (‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
inr₄ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * ((‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
inr₅ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (p.toReal⁻¹ * p.toReal)
inr₆ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * HPow.hPow (β := ℝ) (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) 1
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inr₇ : ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal = ‖c‖₊ ^ p.toReal * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal)
Tactic: rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne',
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add,
        ← NNReal.mul_rpow, ← NNReal.mul_rpow, smul_fst, smul_snd, nnnorm_smul, nnnorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) = ‖c‖₊ * ‖f‖₊
inr₁ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)
inr₂ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ p.toReal⁻¹ =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹
inr₃ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    (‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
inr₄ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * ((‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
inr₅ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (p.toReal⁻¹ * p.toReal)
inr₆ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * HPow.hPow (β := ℝ) (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) 1
inr₇ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal = ‖c‖₊ ^ p.toReal * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal)
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inr₈ : ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
  ‖c‖₊ ^ p.toReal * ‖f.fst‖₊ ^ p.toReal + ‖c‖₊ ^ p.toReal * ‖f.snd‖₊ ^ p.toReal
Tactic: rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne',
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add,
        ← NNReal.mul_rpow, ← NNReal.mul_rpow, smul_fst, smul_snd, nnnorm_smul, nnnorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) = ‖c‖₊ * ‖f‖₊
inr₁ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)
inr₂ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ p.toReal⁻¹ =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹
inr₃ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    (‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
inr₄ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * ((‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
inr₅ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (p.toReal⁻¹ * p.toReal)
inr₆ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * HPow.hPow (β := ℝ) (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) 1
inr₇ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal = ‖c‖₊ ^ p.toReal * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal)
inr₈ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * ‖f.fst‖₊ ^ p.toReal + ‖c‖₊ ^ p.toReal * ‖f.snd‖₊ ^ p.toReal
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inr₉ : ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
  (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + ‖c‖₊ ^ p.toReal * ‖f.snd‖₊ ^ p.toReal
Tactic: rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne',
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add,
        ← NNReal.mul_rpow, ← NNReal.mul_rpow, smul_fst, smul_snd, nnnorm_smul, nnnorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) = ‖c‖₊ * ‖f‖₊
inr₁ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)
inr₂ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ p.toReal⁻¹ =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹
inr₃ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    (‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
inr₄ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * ((‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
inr₅ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (p.toReal⁻¹ * p.toReal)
inr₆ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * HPow.hPow (β := ℝ) (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) 1
inr₇ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal = ‖c‖₊ ^ p.toReal * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal)
inr₈ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * ‖f.fst‖₊ ^ p.toReal + ‖c‖₊ ^ p.toReal * ‖f.snd‖₊ ^ p.toReal
inr₉ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + ‖c‖₊ ^ p.toReal * ‖f.snd‖₊ ^ p.toReal
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inr₁₀ : ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal = (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + (‖c‖₊ * ‖f.snd‖₊) ^ p.toReal
Tactic: rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne',
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add,
        ← NNReal.mul_rpow, ← NNReal.mul_rpow, smul_fst, smul_snd, nnnorm_smul, nnnorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
inr : (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) = ‖c‖₊ * ‖f‖₊
inr₁ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)
inr₂ :
  (‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal) ^ p.toReal⁻¹ =
    ‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹
inr₃ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    (‖c‖₊ * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
inr₄ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * ((‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ p.toReal⁻¹) ^ p.toReal
inr₅ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (p.toReal⁻¹ * p.toReal)
inr₆ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * HPow.hPow (β := ℝ) (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) 1
inr₇ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal = ‖c‖₊ ^ p.toReal * (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal)
inr₈ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    ‖c‖₊ ^ p.toReal * ‖f.fst‖₊ ^ p.toReal + ‖c‖₊ ^ p.toReal * ‖f.snd‖₊ ^ p.toReal
inr₉ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal =
    (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + ‖c‖₊ ^ p.toReal * ‖f.snd‖₊ ^ p.toReal
inr₁₀ :
  ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal = (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + (‖c‖₊ * ‖f.snd‖₊) ^ p.toReal
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inr₁₁ : ‖c • f.fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal = (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + (‖c‖₊ * ‖f.snd‖₊) ^ p.toReal
Tactic: rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne',
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add,
        ← NNReal.mul_rpow, ← NNReal.mul_rpow, smul_fst, smul_snd, nnnorm_smul, nnnorm_smul]