awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
f : WithLp ∞ (α × β)
rw : ‖f.ofLp‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊
rw₁ : max ‖f.ofLp.1‖₊ ‖f.ofLp.2‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊
⊢ ‖f.ofLp‖₊ = ‖f‖₊
have rw₂ : max ‖f.fst‖₊ ‖f.ofLp.2‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊
Tactic: rw [prod_nnnorm_eq_sup, Prod.nnnorm_def, ofLp_fst, ofLp_snd]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
f : WithLp ∞ (α × β)
rw : ‖f.ofLp‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊
rw₁ : max ‖f.ofLp.1‖₊ ‖f.ofLp.2‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊
rw₂ : max ‖f.fst‖₊ ‖f.ofLp.2‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊
⊢ ‖f.ofLp‖₊ = ‖f‖₊
have rw₃ : max ‖f.fst‖₊ ‖f.snd‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊
Tactic: rw [prod_nnnorm_eq_sup, Prod.nnnorm_def, ofLp_fst, ofLp_snd]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
⊢ (↑‖x‖₊ : ℝ) = (↑(‖x.fst‖₊ + ‖x.snd‖₊) : ℝ)
have push_cast : ‖x‖ = ‖x.fst‖ + ‖x.snd‖
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x y : WithLp 1 (α × β)
⊢ dist x y = dist x.fst y.fst + dist x.snd y.snd
have simp_rw : ‖x - y‖ = ‖x.fst - y.fst‖ + ‖x.snd - y.snd‖
Tactic: simp_rw [dist_eq_norm, prod_norm_eq_of_L1, sub_fst, sub_snd]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x y : WithLp 1 (α × β)
simp_rw : ‖x - y‖ = ‖x.fst - y.fst‖ + ‖x.snd - y.snd‖
⊢ dist x y = dist x.fst y.fst + dist x.snd y.snd
have simp_rw₁ : ‖(x - y).fst‖ + ‖(x - y).snd‖ = ‖x.fst - y.fst‖ + ‖x.snd - y.snd‖
Tactic: simp_rw [dist_eq_norm, prod_norm_eq_of_L1, sub_fst, sub_snd]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x y : WithLp 1 (α × β)
simp_rw : ‖x - y‖ = ‖x.fst - y.fst‖ + ‖x.snd - y.snd‖
simp_rw₁ : ‖(x - y).fst‖ + ‖(x - y).snd‖ = ‖x.fst - y.fst‖ + ‖x.snd - y.snd‖
⊢ dist x y = dist x.fst y.fst + dist x.snd y.snd
have simp_rw₂ : ‖x.fst - y.fst‖ + ‖(x - y).snd‖ = ‖x.fst - y.fst‖ + ‖x.snd - y.snd‖
Tactic: simp_rw [dist_eq_norm, prod_norm_eq_of_L1, sub_fst, sub_snd]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x y : WithLp 1 (α × β)
⊢ (↑(nndist x y) : ℝ) = (↑(nndist x.fst y.fst + nndist x.snd y.snd) : ℝ)
have push_cast : dist x y = dist x.fst y.fst + dist x.snd y.snd
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ Eq (α := ℝ≥0∞) 2 (↑2 : ℝ≥0∞)
have norm_cast : Eq (α := ℕ) 2 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ ‖x‖ = √(HPow.hPow (β := ℕ) ‖x.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd‖ 2)
have rw : (HPow.hPow (β := ℕ) ‖x.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd‖ 2) ^ HDiv.hDiv (α := ℝ) 1 (↑2 : ℝ) =
  (HPow.hPow (β := ℕ) ‖x.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd‖ 2) ^ (1 / 2)
Tactic: rw [prod_norm_eq_of_nat 2 (by norm_cast) _, Real.sqrt_eq_rpow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ (HPow.hPow (β := ℕ) ‖x.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd‖ 2) ^ HDiv.hDiv (α := ℝ) 1 (↑2 : ℝ) =
    (HPow.hPow (β := ℕ) ‖x.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd‖ 2) ^ (1 / 2)
have norm_cast : (HPow.hPow (β := ℕ) ‖x.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd‖ 2) ^ HDiv.hDiv (α := ℝ) 1 2 =
  (HPow.hPow (β := ℕ) ‖x.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd‖ 2) ^ HDiv.hDiv (α := ℝ) 1 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ (↑‖x‖₊ : ℝ) = (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) ‖x.fst‖₊ 2 + HPow.hPow (β := ℕ) ‖x.snd‖₊ 2)) : ℝ)
have push_cast : ‖x‖ = √(HPow.hPow (β := ℕ) ‖x.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd‖ 2)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd‖ 2
have suffices : HPow.hPow (β := ℕ) ‖x‖₊ 2 = HPow.hPow (β := ℕ) ‖x.fst‖₊ 2 + HPow.hPow (β := ℕ) ‖x.snd‖₊ 2
Tactic: suffices ‖x‖₊ ^ 2 = ‖x.fst‖₊ ^ 2 + ‖x.snd‖₊ ^ 2 by
    simpa only [NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ HPow.hPow (β := ℕ) ‖x‖₊ 2 = HPow.hPow (β := ℕ) ‖x.fst‖₊ 2 + HPow.hPow (β := ℕ) ‖x.snd‖₊ 2
have rw : HPow.hPow (α := ℝ≥0) (β := ℕ)
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) ‖x.fst‖₊ 2 + HPow.hPow (β := ℕ) ‖x.snd‖₊ 2) : ℝ≥0) 2 =
  HPow.hPow (β := ℕ) ‖x.fst‖₊ 2 + HPow.hPow (β := ℕ) ‖x.snd‖₊ 2
Tactic: rw [prod_nnnorm_eq_of_L2, NNReal.sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
rw :
  HPow.hPow (α := ℝ≥0) (β := ℕ)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) ‖x.fst‖₊ 2 + HPow.hPow (β := ℕ) ‖x.snd‖₊ 2) : ℝ≥0) 2 =
    HPow.hPow (β := ℕ) ‖x.fst‖₊ 2 + HPow.hPow (β := ℕ) ‖x.snd‖₊ 2
⊢ HPow.hPow (β := ℕ) ‖x‖₊ 2 = HPow.hPow (β := ℕ) ‖x.fst‖₊ 2 + HPow.hPow (β := ℕ) ‖x.snd‖₊ 2
have rw₁ : HPow.hPow (β := ℕ) ‖x.fst‖₊ 2 + HPow.hPow (β := ℕ) ‖x.snd‖₊ 2 =
  HPow.hPow (β := ℕ) ‖x.fst‖₊ 2 + HPow.hPow (β := ℕ) ‖x.snd‖₊ 2
Tactic: rw [prod_nnnorm_eq_of_L2, NNReal.sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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)
have simp_rw : ‖x - y‖ = √(HPow.hPow (β := ℕ) ‖x.fst - y.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd - y.snd‖ 2)
Tactic: simp_rw [dist_eq_norm, prod_norm_eq_of_L2, sub_fst, sub_snd]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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)
⊢ dist x y = √(HPow.hPow (β := ℕ) (dist x.fst y.fst) 2 + HPow.hPow (β := ℕ) (dist x.snd y.snd) 2)
have 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)
Tactic: simp_rw [dist_eq_norm, prod_norm_eq_of_L2, sub_fst, sub_snd]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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)
⊢ dist x y = √(HPow.hPow (β := ℕ) (dist x.fst y.fst) 2 + HPow.hPow (β := ℕ) (dist x.snd y.snd) 2)
have 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)
Tactic: simp_rw [dist_eq_norm, prod_norm_eq_of_L2, sub_fst, sub_snd]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x y : WithLp 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)) :
      ℝ)
have push_cast : dist x y = √(HPow.hPow (β := ℕ) (dist x.fst y.fst) 2 + HPow.hPow (β := ℕ) (dist x.snd y.snd) 2)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : α
p : ℝ≥0
hp : Fact (1 ≤ (↑p : ℝ≥0∞))
⊢ nnnorm (E := WithLp (↑p : ℝ≥0∞) (α × β)) (toLp (↑p : ℝ≥0∞) (x, 0)) = ‖x‖₊
have hp0 : (↑p : ℝ) ≠ 0
Tactic: have hp0 : (p : ℝ) ≠ 0 := mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : α
⊢ nnnorm (E := WithLp p (α × β)) (toLp p (x, 0)) = ‖x‖₊
have top : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)], nnnorm (E := WithLp ∞ (α × β)) (toLp ∞ (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]
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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‖₊
⊢ nnnorm (E := WithLp p (α × β)) (toLp p (x, 0)) = ‖x‖₊
have coe : ∀ (p : ℝ≥0) [hp : Fact (1 ≤ (↑p : ℝ≥0∞))], nnnorm (E := WithLp (↑p : ℝ≥0∞) (α × β)) (toLp (↑p : ℝ≥0∞) (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]
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
y : β
p : ℝ≥0
hp : Fact (1 ≤ (↑p : ℝ≥0∞))
⊢ nnnorm (E := WithLp (↑p : ℝ≥0∞) (α × β)) (toLp (↑p : ℝ≥0∞) (0, y)) = ‖y‖₊
have hp0 : (↑p : ℝ) ≠ 0
Tactic: have hp0 : (p : ℝ) ≠ 0 := mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
y : β
⊢ nnnorm (E := WithLp p (α × β)) (toLp p (0, y)) = ‖y‖₊
have top : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)], nnnorm (E := WithLp ∞ (α × β)) (toLp ∞ (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]
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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‖₊
⊢ nnnorm (E := WithLp p (α × β)) (toLp p (0, y)) = ‖y‖₊
have coe : ∀ (p : ℝ≥0) [hp : Fact (1 ≤ (↑p : ℝ≥0∞))], nnnorm (E := WithLp (↑p : ℝ≥0∞) (α × β)) (toLp (↑p : ℝ≥0∞) (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]
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x₁ x₂ : α
⊢ nndist (α := WithLp p (α × β)) (toLp p (x₁, 0)) (toLp p (x₂, 0)) = nndist x₁ x₂
have rw : ‖HSub.hSub (α := 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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₂
⊢ nndist (α := WithLp p (α × β)) (toLp p (x₁, 0)) (toLp p (x₂, 0)) = nndist x₁ x₂
have rw₁ : ‖HSub.hSub (α := WithLp p (α × β)) (toLp p (x₁, 0)) (toLp p (x₂, 0))‖₊ = ‖x₁ - x₂‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← toLp_sub, Prod.mk_sub_mk, sub_zero,
    nnnorm_toLp_inl]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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₂‖₊
⊢ nndist (α := WithLp p (α × β)) (toLp p (x₁, 0)) (toLp p (x₂, 0)) = nndist x₁ x₂
have rw₂ : ‖toLp p (HSub.hSub (α := α × β) (x₁, 0) (x₂, 0))‖₊ = ‖x₁ - x₂‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← toLp_sub, Prod.mk_sub_mk, sub_zero,
    nnnorm_toLp_inl]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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₂‖₊
⊢ nndist (α := WithLp p (α × β)) (toLp p (x₁, 0)) (toLp p (x₂, 0)) = nndist x₁ x₂
have rw₃ : ‖toLp p (x₁ - x₂, HSub.hSub (α := β) 0 0)‖₊ = ‖x₁ - x₂‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← toLp_sub, Prod.mk_sub_mk, sub_zero,
    nnnorm_toLp_inl]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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₂‖₊
⊢ nndist (α := WithLp p (α × β)) (toLp p (x₁, 0)) (toLp p (x₂, 0)) = nndist x₁ x₂
have rw₄ : nnnorm (E := WithLp p (α × β)) (toLp p (x₁ - x₂, 0)) = ‖x₁ - x₂‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← toLp_sub, Prod.mk_sub_mk, sub_zero,
    nnnorm_toLp_inl]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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₂‖₊
⊢ nndist (α := WithLp p (α × β)) (toLp p (x₁, 0)) (toLp p (x₂, 0)) = nndist x₁ x₂
have rw₅ : ‖x₁ - x₂‖₊ = ‖x₁ - x₂‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← toLp_sub, Prod.mk_sub_mk, sub_zero,
    nnnorm_toLp_inl]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
y₁ y₂ : β
⊢ nndist (α := WithLp p (α × β)) (toLp p (0, y₁)) (toLp p (0, y₂)) = nndist y₁ y₂
have rw : ‖HSub.hSub (α := 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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₂
⊢ nndist (α := WithLp p (α × β)) (toLp p (0, y₁)) (toLp p (0, y₂)) = nndist y₁ y₂
have rw₁ : ‖HSub.hSub (α := WithLp p (α × β)) (toLp p (0, y₁)) (toLp p (0, y₂))‖₊ = ‖y₁ - y₂‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← toLp_sub, Prod.mk_sub_mk, sub_zero,
    nnnorm_toLp_inr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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₂‖₊
⊢ nndist (α := WithLp p (α × β)) (toLp p (0, y₁)) (toLp p (0, y₂)) = nndist y₁ y₂
have rw₂ : ‖toLp p (HSub.hSub (α := α × β) (0, y₁) (0, y₂))‖₊ = ‖y₁ - y₂‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← toLp_sub, Prod.mk_sub_mk, sub_zero,
    nnnorm_toLp_inr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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₂‖₊
⊢ nndist (α := WithLp p (α × β)) (toLp p (0, y₁)) (toLp p (0, y₂)) = nndist y₁ y₂
have rw₃ : ‖toLp p (HSub.hSub (α := α) 0 0, y₁ - y₂)‖₊ = ‖y₁ - y₂‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← toLp_sub, Prod.mk_sub_mk, sub_zero,
    nnnorm_toLp_inr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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₂‖₊
⊢ nndist (α := WithLp p (α × β)) (toLp p (0, y₁)) (toLp p (0, y₂)) = nndist y₁ y₂
have rw₄ : nnnorm (E := WithLp p (α × β)) (toLp p (0, y₁ - y₂)) = ‖y₁ - y₂‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← toLp_sub, Prod.mk_sub_mk, sub_zero,
    nnnorm_toLp_inr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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₂‖₊
⊢ nndist (α := WithLp p (α × β)) (toLp p (0, y₁)) (toLp p (0, y₂)) = nndist y₁ y₂
have rw₅ : ‖y₁ - y₂‖₊ = ‖y₁ - y₂‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← toLp_sub, Prod.mk_sub_mk, sub_zero,
    nnnorm_toLp_inr]
-- 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 : IsBoundedSMul 𝕜 α
inst_6 : IsBoundedSMul 𝕜 β
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 : IsBoundedSMul 𝕜 α
inst_6 : IsBoundedSMul 𝕜 β
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 (goal)
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‖₊ ≤ ‖c‖₊ * ‖f‖₊
have inl : ‖c • f.ofLp‖₊ ≤ ‖c‖₊ * ‖f.ofLp‖₊
Tactic: simp only [← prod_nnnorm_ofLp, ofLp_smul]
-- 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 : IsBoundedSMul 𝕜 α
inst_6 : IsBoundedSMul 𝕜 β
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 : IsBoundedSMul 𝕜 α
inst_6 : IsBoundedSMul 𝕜 β
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 : IsBoundedSMul 𝕜 α
inst_6 : IsBoundedSMul 𝕜 β
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 ≤ (‖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_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]