awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x y : WithLp 2 (α × β)
simp_rw : ‖x - y‖ = √(HPow.hPow (β := ℕ) ‖x.fst - y.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd - y.snd‖ 2)
simp_rw₁ :
  √(HPow.hPow (β := ℕ) ‖(x - y).fst‖ 2 + HPow.hPow (β := ℕ) ‖(x - y).snd‖ 2) =
    √(HPow.hPow (β := ℕ) ‖x.fst - y.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd - y.snd‖ 2)
simp_rw₂ :
  √(HPow.hPow (β := ℕ) ‖x.fst - y.fst‖ 2 + HPow.hPow (β := ℕ) ‖(x - y).snd‖ 2) =
    √(HPow.hPow (β := ℕ) ‖x.fst - y.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd - y.snd‖ 2)
⊢ dist x y = √(HPow.hPow (β := ℕ) (dist x.fst y.fst) 2 + HPow.hPow (β := ℕ) (dist x.snd y.snd) 2)

Tactic:
simp_rw [dist_eq_norm, prod_norm_eq_of_L2, sub_fst, sub_snd]

Premises used: dist_eq_norm, WithLp.sub_fst, WithLp.sub_snd, WithLp.prod_norm_eq_of_L2
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x y : WithLp 2 (α × β)
push_cast : dist x y = √(HPow.hPow (β := ℕ) (dist x.fst y.fst) 2 + HPow.hPow (β := ℕ) (dist x.snd y.snd) 2)
⊢ (↑(nndist x y) : ℝ) =
    (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0)
          (HPow.hPow (β := ℕ) (nndist x.fst y.fst) 2 + HPow.hPow (β := ℕ) (nndist x.snd y.snd) 2)) :
      ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x y : WithLp 2 (α × β)
⊢ dist x y = √(HPow.hPow (β := ℕ) (dist x.fst y.fst) 2 + HPow.hPow (β := ℕ) (dist x.snd y.snd) 2)

Tactic:
prod_dist_eq_of_L2 _ _

Premises used: WithLp.prod_dist_eq_of_L2
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x y : WithLp 2 (α × β)
⊢ dist x y = √(HPow.hPow (β := ℕ) (dist x.fst y.fst) 2 + HPow.hPow (β := ℕ) (dist x.snd y.snd) 2)

Tactic:
exact prod_dist_eq_of_L2 _ _

Premises used: WithLp.prod_dist_eq_of_L2
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x y : WithLp 2 (α × β)
⊢ edist x y = (HPow.hPow (β := ℕ) (edist x.fst y.fst) 2 + HPow.hPow (β := ℕ) (edist x.snd y.snd) 2) ^ (1 / 2)

Tactic:
simp [prod_edist_eq_add]

Premises used: WithLp.prod_edist_eq_add
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : α
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
⊢ nnnorm (E := WithLp ∞ (α × β)) (toLp ∞ (x, 0)) = ‖x‖₊

Tactic:
simp [prod_nnnorm_eq_sup]

Premises used: WithLp.prod_nnnorm_eq_sup
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : α
p : ℝ≥0
hp : Fact (1 ≤ (↑p : ℝ≥0∞))
⊢ (↑p : ℝ) ≠ 0

Tactic:
have hp0 : (p : ℝ) ≠ 0 := mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : α
p : ℝ≥0
hp : Fact (1 ≤ (↑p : ℝ≥0∞))
hp0 : (↑p : ℝ) ≠ 0
⊢ nnnorm (E := WithLp (↑p : ℝ≥0∞) (α × β)) (toLp (↑p : ℝ≥0∞) (x, 0)) = ‖x‖₊

Tactic:
simp [prod_nnnorm_eq_add, NNReal.zero_rpow hp0, ← NNReal.rpow_mul, mul_inv_cancel₀ hp0]

Premises used: NNReal.zero_rpow, WithLp.prod_nnnorm_eq_add, mul_inv_cancel₀, NNReal.rpow_mul
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : α
top : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)], nnnorm (E := WithLp ∞ (α × β)) (toLp ∞ (x, 0)) = ‖x‖₊
coe :
  ∀ (p : ℝ≥0) [hp : Fact (1 ≤ (↑p : ℝ≥0∞))], nnnorm (E := WithLp (↑p : ℝ≥0∞) (α × β)) (toLp (↑p : ℝ≥0∞) (x, 0)) = ‖x‖₊
⊢ nnnorm (E := WithLp p (α × β)) (toLp p (x, 0)) = ‖x‖₊

Tactic:
induction p generalizing hp with
  | top =>
    simp [prod_nnnorm_eq_sup]
  | coe p =>
    have hp0 : (p : ℝ) ≠ 0 := mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
    simp [prod_nnnorm_eq_add, NNReal.zero_rpow hp0, ← NNReal.rpow_mul, mul_inv_cancel₀ hp0]

Premises used: WithLp.prod_nnnorm_eq_add, NNReal.rpow_mul, WithLp.prod_nnnorm_eq_sup
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
y : β
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
⊢ nnnorm (E := WithLp ∞ (α × β)) (toLp ∞ (0, y)) = ‖y‖₊

Tactic:
simp [prod_nnnorm_eq_sup]

Premises used: WithLp.prod_nnnorm_eq_sup
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
y : β
p : ℝ≥0
hp : Fact (1 ≤ (↑p : ℝ≥0∞))
⊢ (↑p : ℝ) ≠ 0

Tactic:
have hp0 : (p : ℝ) ≠ 0 := mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
y : β
p : ℝ≥0
hp : Fact (1 ≤ (↑p : ℝ≥0∞))
hp0 : (↑p : ℝ) ≠ 0
⊢ nnnorm (E := WithLp (↑p : ℝ≥0∞) (α × β)) (toLp (↑p : ℝ≥0∞) (0, y)) = ‖y‖₊

Tactic:
simp [prod_nnnorm_eq_add, NNReal.zero_rpow hp0, ← NNReal.rpow_mul, mul_inv_cancel₀ hp0]

Premises used: NNReal.zero_rpow, WithLp.prod_nnnorm_eq_add, mul_inv_cancel₀, NNReal.rpow_mul
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
y : β
top : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)], nnnorm (E := WithLp ∞ (α × β)) (toLp ∞ (0, y)) = ‖y‖₊
coe :
  ∀ (p : ℝ≥0) [hp : Fact (1 ≤ (↑p : ℝ≥0∞))], nnnorm (E := WithLp (↑p : ℝ≥0∞) (α × β)) (toLp (↑p : ℝ≥0∞) (0, y)) = ‖y‖₊
⊢ nnnorm (E := WithLp p (α × β)) (toLp p (0, y)) = ‖y‖₊

Tactic:
induction p generalizing hp with
  | top =>
    simp [prod_nnnorm_eq_sup]
  | coe p =>
    have hp0 : (p : ℝ) ≠ 0 := mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
    simp [prod_nnnorm_eq_add, NNReal.zero_rpow hp0, ← NNReal.rpow_mul, mul_inv_cancel₀ hp0]

Premises used: WithLp.prod_nnnorm_eq_add, NNReal.rpow_mul, WithLp.prod_nnnorm_eq_sup
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : α
⊢ Norm.norm (E := WithLp p (α × β)) (toLp p (x, 0)) = ‖x‖

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_toLp_inl p α β x

Premises used: WithLp.nnnorm_toLp_inl, congr_arg, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
y : β
⊢ Norm.norm (E := WithLp p (α × β)) (toLp p (0, y)) = ‖y‖

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_toLp_inr p α β y

Premises used: WithLp.nnnorm_toLp_inr, congr_arg, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x₁ x₂ : α
rw : ‖HSub.hSub (α := WithLp p (α × β)) (toLp p (x₁, 0)) (toLp p (x₂, 0))‖₊ = nndist x₁ x₂
rw₁ : ‖HSub.hSub (α := WithLp p (α × β)) (toLp p (x₁, 0)) (toLp p (x₂, 0))‖₊ = ‖x₁ - x₂‖₊
rw₂ : ‖toLp p (HSub.hSub (α := α × β) (x₁, 0) (x₂, 0))‖₊ = ‖x₁ - x₂‖₊
rw₃ : ‖toLp p (x₁ - x₂, HSub.hSub (α := β) 0 0)‖₊ = ‖x₁ - x₂‖₊
rw₄ : nnnorm (E := WithLp p (α × β)) (toLp p (x₁ - x₂, 0)) = ‖x₁ - x₂‖₊
rw₅ rw₆ : ‖x₁ - x₂‖₊ = ‖x₁ - x₂‖₊
⊢ nndist (α := WithLp p (α × β)) (toLp p (x₁, 0)) (toLp p (x₂, 0)) = nndist x₁ x₂

Tactic:
rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← toLp_sub, Prod.mk_sub_mk, sub_zero,
    nnnorm_toLp_inl]

Premises used: sub_zero, Prod.mk_sub_mk, WithLp.nnnorm_toLp_inl, nndist_eq_nnnorm, WithLp.toLp_sub
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
y₁ y₂ : β
rw : ‖HSub.hSub (α := WithLp p (α × β)) (toLp p (0, y₁)) (toLp p (0, y₂))‖₊ = nndist y₁ y₂
rw₁ : ‖HSub.hSub (α := WithLp p (α × β)) (toLp p (0, y₁)) (toLp p (0, y₂))‖₊ = ‖y₁ - y₂‖₊
rw₂ : ‖toLp p (HSub.hSub (α := α × β) (0, y₁) (0, y₂))‖₊ = ‖y₁ - y₂‖₊
rw₃ : ‖toLp p (HSub.hSub (α := α) 0 0, y₁ - y₂)‖₊ = ‖y₁ - y₂‖₊
rw₄ : nnnorm (E := WithLp p (α × β)) (toLp p (0, y₁ - y₂)) = ‖y₁ - y₂‖₊
rw₅ rw₆ : ‖y₁ - y₂‖₊ = ‖y₁ - y₂‖₊
⊢ nndist (α := WithLp p (α × β)) (toLp p (0, y₁)) (toLp p (0, y₂)) = nndist y₁ y₂

Tactic:
rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← toLp_sub, Prod.mk_sub_mk, sub_zero,
    nnnorm_toLp_inr]

Premises used: WithLp.nnnorm_toLp_inr, sub_zero, Prod.mk_sub_mk, nndist_eq_nnnorm, WithLp.toLp_sub
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x₁ x₂ : α
⊢ dist (α := WithLp p (α × β)) (toLp p (x₁, 0)) (toLp p (x₂, 0)) = dist x₁ x₂

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) <| nndist_toLp_fst p α β x₁ x₂

Premises used: congr_arg, NNReal.toReal, WithLp.nndist_toLp_fst
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
y₁ y₂ : β
⊢ dist (α := WithLp p (α × β)) (toLp p (0, y₁)) (toLp p (0, y₂)) = dist y₁ y₂

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) <| nndist_toLp_snd p α β y₁ y₂

Premises used: WithLp.nndist_toLp_snd, congr_arg, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x₁ x₂ : α
⊢ edist (α := WithLp p (α × β)) (toLp p (x₁, 0)) (toLp p (x₂, 0)) = edist x₁ x₂

Tactic:
simp only [edist_nndist, nndist_toLp_fst p α β x₁ x₂]

Premises used: edist_nndist, WithLp.nndist_toLp_fst
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
y₁ y₂ : β
⊢ edist (α := WithLp p (α × β)) (toLp p (0, y₁)) (toLp p (0, y₂)) = edist y₁ y₂

Tactic:
simp only [edist_nndist, nndist_toLp_snd p α β y₁ y₂]

Premises used: WithLp.nndist_toLp_snd, edist_nndist
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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 : IsBoundedSMul 𝕜 α
inst_6 : IsBoundedSMul 𝕜 β
c : 𝕜
f : WithLp p (α × β)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f : WithLp ∞ (α × β)), ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
inr : ∀ (hp_1 : 1 ≤ p.toReal), ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

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

Premises used: ENNReal.dichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : IsBoundedSMul 𝕜 α
inst_6 : IsBoundedSMul 𝕜 β
c : 𝕜
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f : WithLp ∞ (α × β)
inl : ‖c • f.ofLp‖₊ ≤ ‖c‖₊ * ‖f.ofLp‖₊
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

Tactic:
simp only [← prod_nnnorm_ofLp, ofLp_smul]

Premises used: WithLp.ofLp_smul, WithLp.prod_nnnorm_ofLp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : IsBoundedSMul 𝕜 α
inst_6 : IsBoundedSMul 𝕜 β
c : 𝕜
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f : WithLp ∞ (α × β)
⊢ ‖c • f.ofLp‖₊ ≤ ‖c‖₊ * ‖f.ofLp‖₊

Tactic:
norm_smul_le _ _

Premises used: norm_smul_le
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : IsBoundedSMul 𝕜 α
inst_6 : IsBoundedSMul 𝕜 β
c : 𝕜
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f : WithLp ∞ (α × β)
⊢ ‖c • f.ofLp‖₊ ≤ ‖c‖₊ * ‖f.ofLp‖₊

Tactic:
exact norm_smul_le _ _

Premises used: norm_smul_le
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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
⊢ 0 < p.toReal

Tactic:
have hp0 : 0 < p.toReal := zero_lt_one.trans_le hp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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
⊢ p ≠ ∞

Tactic:
have hpt : p ≠ ⊤ := p.toReal_pos_iff_ne_top.mp hp0
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + (‖c‖₊ * ‖f.snd‖₊) ^ p.toReal
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

Tactic:
rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_le_iff hp0,
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add,
        ← NNReal.mul_rpow, ← NNReal.mul_rpow]

Premises used: WithLp.prod_nnnorm_eq_add, NNReal.rpow_mul, NNReal.rpow_inv_le_iff, LT.lt.ne', one_div, mul_add, NNReal.rpow_one, NNReal.mul_rpow, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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‖₊
inr₁ : ‖(c • f).snd‖₊ ≤ ‖c‖₊ * ‖f.snd‖₊
⊢ ‖(c • f).fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + (‖c‖₊ * ‖f.snd‖₊) ^ p.toReal

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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‖₊ ≤ ‖c‖₊ * ‖f.fst‖₊

Tactic:
nnnorm_smul_le _ _

Premises used: WithLp.fst, nnnorm_smul_le
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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‖₊ ≤ ‖c‖₊ * ‖f.fst‖₊

Tactic:
exact nnnorm_smul_le _ _

Premises used: nnnorm_smul_le
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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).snd‖₊ ≤ ‖c‖₊ * ‖f.snd‖₊

Tactic:
nnnorm_smul_le _ _

Premises used: WithLp.snd, nnnorm_smul_le
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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).snd‖₊ ≤ ‖c‖₊ * ‖f.snd‖₊

Tactic:
exact nnnorm_smul_le _ _

Premises used: nnnorm_smul_le
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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‖₊
inr : ∀ (hp_1 : 1 ≤ p.toReal), ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

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

Premises used: ENNReal.dichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
inst_5 : NormSMulClass 𝕜 α
inst_6 : NormSMulClass 𝕜 β
c : 𝕜
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f : WithLp ∞ (α × β)
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

Tactic:
simp only [← prod_nnnorm_ofLp, WithLp.ofLp_smul, nnnorm_smul]

Premises used: WithLp.ofLp_smul, WithLp.prod_nnnorm_ofLp, nnnorm_smul
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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
⊢ 0 < p.toReal

Tactic:
have hp0 : 0 < p.toReal := zero_lt_one.trans_le hp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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
⊢ p ≠ ∞

Tactic:
have hpt : p ≠ ⊤ := p.toReal_pos_iff_ne_top.mp hp0
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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
inr₁₁ :
  ‖c • f.fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal = (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + (‖c‖₊ * ‖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
inr₁₃ :
  (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + ‖c • f.snd‖₊ ^ p.toReal = (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + (‖c‖₊ * ‖f.snd‖₊) ^ p.toReal
inr₁₄ 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‖₊

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]

Premises used: WithLp.smul_snd, WithLp.prod_nnnorm_eq_add, nnnorm_smul, NNReal.rpow_mul, NNReal.rpow_inv_eq_iff, LT.lt.ne', WithLp.smul_fst, one_div, mul_add, NNReal.rpow_one, NNReal.mul_rpow, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p_1 : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p_1)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
⊢ Eq (α := WithLp p (α × β)) (toLp p (WithLp.fst.{u_2, u_3} (p := p) (β := β) 0, 0)) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p_1 : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p_1)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
⊢ ∀ (x y : WithLp p (α × β)),
    toLp p ((x + y).fst, 0) = HAdd.hAdd (α := WithLp p (α × β)) (toLp p (x.fst, 0)) (toLp p (y.fst, 0))

Tactic:
simp [← toLp_add]

Premises used: WithLp.toLp_add
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p_1 : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p_1)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
⊢ Eq (α := WithLp p (α × β)) (toLp p (0, WithLp.snd.{u_2, u_3} (p := p) (α := α) 0)) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p_1 : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p_1)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
⊢ ∀ (x y : WithLp p (α × β)),
    toLp p (0, (x + y).snd) = HAdd.hAdd (α := WithLp p (α × β)) (toLp p (0, x.snd)) (toLp p (0, y.snd))

Tactic:
simp [← toLp_add]

Premises used: WithLp.toLp_add
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
x : WithLp p (α × β)
⊢ Eq (α := WithLp p (α × β)) ((idemFst : (a : WithLp p (α × β)) → WithLp p (α × β)) x : WithLp p (α × β))
    (toLp p (x.fst, 0) : WithLp p (α × β))

Tactic:
rfl

Premises used: AddMonoid.End.instFunLike._aux_1, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
x : WithLp p (α × β)
⊢ Eq (α := WithLp p (α × β)) ((idemSnd : (a : WithLp p (α × β)) → WithLp p (α × β)) x : WithLp p (α × β))
    (toLp p (0, x.snd) : WithLp p (α × β))

Tactic:
rfl

Premises used: AddMonoid.End.instFunLike._aux_1, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
x : WithLp p (α × β)
rw : toLp p (x.fst, x.snd) = x
⊢ Eq (α := WithLp p (α × β))
    ((HAdd.hAdd (α := AddMonoid.End (WithLp p (α × β))) idemFst idemSnd : (a : WithLp p (α × β)) → WithLp p (α × β)) x :
      WithLp p (α × β))
    ((1 : (a : WithLp p (α × β)) → WithLp p (α × β)) x : WithLp p (α × β))

Tactic:
rw [AddMonoidHom.add_apply, idemFst_apply, idemSnd_apply, AddMonoid.End.coe_one, id_eq,
      ← toLp_add, Prod.mk_add_mk, zero_add, add_zero]

Premises used: Prod.mk_add_mk, zero_add, AddMonoid.End.coe_one, WithLp.idemSnd_apply, WithLp.toLp_add, WithLp.idemFst_apply, AddMonoidHom.add_apply, add_zero, id_eq