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 : 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
⊢ ‖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
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
⊢ ‖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
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
⊢ ‖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:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
x : WithLp p (α × β)
⊢ 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 (α × β))
have rw : toLp p (x.fst, x.snd) = x
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
⊢ HSub.hSub (α := AddMonoid.End (WithLp p (α × β))) 1 idemFst = idemSnd
have rw : HAdd.hAdd (α := AddMonoid.End (WithLp p (α × β))) idemFst idemSnd - idemFst = idemSnd
Tactic: rw [← idemFst_add_idemSnd, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
rw : HAdd.hAdd (α := AddMonoid.End (WithLp p (α × β))) idemFst idemSnd - idemFst = idemSnd
⊢ HSub.hSub (α := AddMonoid.End (WithLp p (α × β))) 1 idemFst = idemSnd
have rw₁ : Eq (α := AddMonoid.End (WithLp p (α × β))) idemSnd idemSnd
Tactic: rw [← idemFst_add_idemSnd, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
⊢ HSub.hSub (α := AddMonoid.End (WithLp p (α × β))) 1 idemSnd = idemFst
have rw : HAdd.hAdd (α := AddMonoid.End (WithLp p (α × β))) idemFst idemSnd - idemSnd = idemFst
Tactic: rw [← idemFst_add_idemSnd, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
rw : HAdd.hAdd (α := AddMonoid.End (WithLp p (α × β))) idemFst idemSnd - idemSnd = idemFst
⊢ HSub.hSub (α := AddMonoid.End (WithLp p (α × β))) 1 idemSnd = idemFst
have rw₁ : Eq (α := AddMonoid.End (WithLp p (α × β))) idemFst idemFst
Tactic: rw [← idemFst_add_idemSnd, add_sub_cancel_right]
-- 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 ∞ (α × β)
⊢ ‖x‖ =
    max (Norm.norm (E := WithLp ∞ (α × β)) ((idemFst : (a : WithLp ∞ (α × β)) → WithLp ∞ (α × β)) x : WithLp ∞ (α × β)))
      (Norm.norm (E := WithLp ∞ (α × β)) ((idemSnd : (a : WithLp ∞ (α × β)) → WithLp ∞ (α × β)) x : WithLp ∞ (α × β)))
have rw : max (Norm.norm (E := WithLp ∞ (α × β)) (toLp ∞ (x.fst, 0))) (Norm.norm (E := WithLp ∞ (α × β)) (toLp ∞ (0, x.snd))) =
  max (Norm.norm (E := WithLp ∞ (α × β)) ((idemFst : (a : WithLp ∞ (α × β)) → WithLp ∞ (α × β)) x : WithLp ∞ (α × β)))
    (Norm.norm (E := WithLp ∞ (α × β)) ((idemSnd : (a : WithLp ∞ (α × β)) → WithLp ∞ (α × β)) x : WithLp ∞ (α × β)))
Tactic: rw [WithLp.prod_norm_eq_sup, ← WithLp.norm_toLp_fst ∞ α β x.fst,
    ← WithLp.norm_toLp_snd ∞ α β x.snd]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
inst_2 : Fact (1 ≤ p)
hp : 0 < p.toReal
x : WithLp p (α × β)
⊢ ‖x‖ =
    (Norm.norm (E := WithLp p (α × β)) ((idemFst : (a : WithLp p (α × β)) → WithLp p (α × β)) x : WithLp p (α × β)) ^
          p.toReal +
        Norm.norm (E := WithLp p (α × β)) ((idemSnd : (a : WithLp p (α × β)) → WithLp p (α × β)) x : WithLp p (α × β)) ^
          p.toReal) ^
      (1 / p.toReal)
have rw : (Norm.norm (E := WithLp p (α × β)) (toLp p (x.fst, 0)) ^ p.toReal +
      Norm.norm (E := WithLp p (α × β)) (toLp p (0, x.snd)) ^ p.toReal) ^
    (1 / p.toReal) =
  (Norm.norm (E := WithLp p (α × β)) ((idemFst : (a : WithLp p (α × β)) → WithLp p (α × β)) x : WithLp p (α × β)) ^
        p.toReal +
      Norm.norm (E := WithLp p (α × β)) ((idemSnd : (a : WithLp p (α × β)) → WithLp p (α × β)) x : WithLp p (α × β)) ^
        p.toReal) ^
    (1 / p.toReal)
Tactic: rw [WithLp.prod_norm_eq_add hp, ← WithLp.norm_toLp_fst p α β x.fst,
    ← WithLp.norm_toLp_snd p α β x.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‖ =
    Norm.norm (E := WithLp 1 (α × β)) ((idemFst : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β)) +
      Norm.norm (E := WithLp 1 (α × β)) ((idemSnd : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β))
have rw : (Norm.norm (E := WithLp 1 (α × β)) ((idemFst : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β)) ^
        ENNReal.toReal 1 +
      Norm.norm (E := WithLp 1 (α × β)) ((idemSnd : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β)) ^
        ENNReal.toReal 1) ^
    (1 / ENNReal.toReal 1) =
  Norm.norm (E := WithLp 1 (α × β)) ((idemFst : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β)) +
    Norm.norm (E := WithLp 1 (α × β)) ((idemSnd : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β))
Tactic: rw [prod_norm_eq_add_idemFst (lt_of_lt_of_eq zero_lt_one toReal_one.symm)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α_1 : Type u_2
β_1 : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α_1
inst_1 : SeminormedAddCommGroup β_1
α : Type u_4
β : Type u_5
inst_2 : SeminormedAddCommGroup α
inst_3 : SeminormedAddCommGroup β
x y : α × β
⊢ dist x y = ‖toLp p (-x + y)‖
have rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
Tactic: rw [dist_pseudoMetricSpaceToProd, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α_1 : Type u_2
β_1 : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α_1
inst_1 : SeminormedAddCommGroup β_1
α : Type u_4
β : Type u_5
inst_2 : SeminormedAddCommGroup α
inst_3 : SeminormedAddCommGroup β
x y : α × β
rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
⊢ dist x y = ‖toLp p (-x + y)‖
have rw₁ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖
Tactic: rw [dist_pseudoMetricSpaceToProd, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α_1 : Type u_2
β_1 : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α_1
inst_1 : SeminormedAddCommGroup β_1
α : Type u_4
β : Type u_5
inst_2 : SeminormedAddCommGroup α
inst_3 : SeminormedAddCommGroup β
x y : α × β
rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
rw₁ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖
⊢ dist x y = ‖toLp p (-x + y)‖
have rw₂ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖
Tactic: rw [dist_pseudoMetricSpaceToProd, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α_1 : Type u_2
β_1 : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α_1
inst_1 : SeminormedAddCommGroup β_1
α : Type u_4
β : Type u_5
inst_2 : SeminormedAddCommGroup α
inst_3 : SeminormedAddCommGroup β
x y : α × β
rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
rw₁ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖
rw₂ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖
⊢ dist x y = ‖toLp p (-x + y)‖
have rw₃ : ‖-toLp p x + toLp p y‖ = ‖-toLp p x + toLp p y‖
Tactic: rw [dist_pseudoMetricSpaceToProd, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
R : Type u_6
inst_2 : SeminormedRing R
inst_3 : Module R α
inst_4 : Module R β
inst_5 : IsBoundedSMul R α
inst_6 : IsBoundedSMul R β
this : PseudoMetricSpace (α × β) := pseudoMetricSpaceToProd p α β
⊢ IsBoundedSMul R (α × β)
have refine_1 : ∀ (x : R) (y z : α × β), dist (x • y) (x • z) ≤ dist x 0 * dist y z
Tactic: refine ⟨fun x y z ↦ ?_, fun x y z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
R : Type u_6
inst_2 : SeminormedRing R
inst_3 : Module R α
inst_4 : Module R β
inst_5 : IsBoundedSMul R α
inst_6 : IsBoundedSMul R β
this : PseudoMetricSpace (α × β) := pseudoMetricSpaceToProd p α β
refine_1 : ∀ (x : R) (y z : α × β), dist (x • y) (x • z) ≤ dist x 0 * dist y z
⊢ IsBoundedSMul R (α × β)
have refine_2 : ∀ (x y : R) (z : α × β), dist (x • z) (y • z) ≤ dist x y * dist z 0
Tactic: refine ⟨fun x y z ↦ ?_, fun x y z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (hypothesis)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α_1 : Type u_2
β_1 : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α_1
inst_1 : SeminormedAddCommGroup β_1
α : Type u_4
β : Type u_5
inst_2 : NormedAddCommGroup α
inst_3 : NormedAddCommGroup β
x y : α × β
h : dist x y = 0
⊢ x = y
have h₁ : dist (toLp p x) (toLp p y) = 0
Tactic: rw [dist_pseudoMetricSpaceToProd] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α_1 : Type u_2
β_1 : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α_1
inst_1 : SeminormedAddCommGroup β_1
α : Type u_4
β : Type u_5
inst_2 : NormedAddCommGroup α
inst_3 : NormedAddCommGroup β
x y : α × β
⊢ dist x y = ‖toLp p (-x + y)‖
have rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
Tactic: rw [dist_pseudoMetricSpaceToProd, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α_1 : Type u_2
β_1 : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α_1
inst_1 : SeminormedAddCommGroup β_1
α : Type u_4
β : Type u_5
inst_2 : NormedAddCommGroup α
inst_3 : NormedAddCommGroup β
x y : α × β
rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
⊢ dist x y = ‖toLp p (-x + y)‖
have rw₁ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖
Tactic: rw [dist_pseudoMetricSpaceToProd, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α_1 : Type u_2
β_1 : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α_1
inst_1 : SeminormedAddCommGroup β_1
α : Type u_4
β : Type u_5
inst_2 : NormedAddCommGroup α
inst_3 : NormedAddCommGroup β
x y : α × β
rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
rw₁ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖
⊢ dist x y = ‖toLp p (-x + y)‖
have rw₂ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖
Tactic: rw [dist_pseudoMetricSpaceToProd, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α_1 : Type u_2
β_1 : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α_1
inst_1 : SeminormedAddCommGroup β_1
α : Type u_4
β : Type u_5
inst_2 : NormedAddCommGroup α
inst_3 : NormedAddCommGroup β
x y : α × β
rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
rw₁ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖
rw₂ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖
⊢ dist x y = ‖toLp p (-x + y)‖
have rw₃ : ‖-toLp p x + toLp p y‖ = ‖-toLp p x + toLp p y‖
Tactic: rw [dist_pseudoMetricSpaceToProd, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace α'
inst_3 : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
x1 x2 : WithLp p (α × β)
⊢ edist (WithLp.map p (Prod.map f g) x1) (WithLp.map p (Prod.map f g) x2) = edist x1 x2
have inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (x1 x2 : WithLp 0 (α × β)),
  edist (WithLp.map 0 (Prod.map f g) x1) (WithLp.map 0 (Prod.map f g) x2) = edist x1 x2
Tactic: rcases p.trichotomy with rfl | rfl | hp
Cleared hypotheses: p, hp, x1, x2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace α'
inst_3 : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
x1 x2 : WithLp p (α × β)
inl :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (x1 x2 : WithLp 0 (α × β)),
    edist (WithLp.map 0 (Prod.map f g) x1) (WithLp.map 0 (Prod.map f g) x2) = edist x1 x2
⊢ edist (WithLp.map p (Prod.map f g) x1) (WithLp.map p (Prod.map f g) x2) = edist x1 x2
have inr : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x1 x2 : WithLp ∞ (α × β)),
  edist (WithLp.map ∞ (Prod.map f g) x1) (WithLp.map ∞ (Prod.map f g) x2) = edist x1 x2
Tactic: rcases p.trichotomy with rfl | rfl | hp
Cleared hypotheses: p, hp, x1, x2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace α'
inst_3 : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
x1 x2 : WithLp p (α × β)
inl :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (x1 x2 : WithLp 0 (α × β)),
    edist (WithLp.map 0 (Prod.map f g) x1) (WithLp.map 0 (Prod.map f g) x2) = edist x1 x2
inr :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x1 x2 : WithLp ∞ (α × β)),
    edist (WithLp.map ∞ (Prod.map f g) x1) (WithLp.map ∞ (Prod.map f g) x2) = edist x1 x2
⊢ edist (WithLp.map p (Prod.map f g) x1) (WithLp.map p (Prod.map f g) x2) = edist x1 x2
have inr₁ : ∀ (hp_1 : 0 < p.toReal), edist (WithLp.map p (Prod.map f g) x1) (WithLp.map p (Prod.map f g) x2) = edist x1 x2
Tactic: rcases p.trichotomy with rfl | rfl | hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace α'
inst_3 : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
x1 x2 : WithLp 0 (α × β)
⊢ edist (WithLp.map 0 (Prod.map f g) x1) (WithLp.map 0 (Prod.map f g) x2) = edist x1 x2
have inl : ¬LE.le (α := ℝ≥0∞) 1 0
Tactic: absurd hp.elim
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
x x_1 : WithLp p (α × β)
⊢ edist ((WithLp.congr p (Equiv.prodComm α β)).toFun x) ((WithLp.congr p (Equiv.prodComm α β)).toFun x_1) = edist x x_1
have inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (x x_2 : WithLp 0 (α × β)),
  edist (Equiv.toFun (WithLp.congr 0 (Equiv.prodComm α β)) x) (Equiv.toFun (WithLp.congr 0 (Equiv.prodComm α β)) x_2) =
    edist x x_2
Tactic: rcases p.trichotomy with rfl | rfl | hp
Cleared hypotheses: p, hp, x, x_1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
x x_1 : WithLp p (α × β)
inl :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (x x_2 : WithLp 0 (α × β)),
    edist (Equiv.toFun (WithLp.congr 0 (Equiv.prodComm α β)) x)
        (Equiv.toFun (WithLp.congr 0 (Equiv.prodComm α β)) x_2) =
      edist x x_2
⊢ edist ((WithLp.congr p (Equiv.prodComm α β)).toFun x) ((WithLp.congr p (Equiv.prodComm α β)).toFun x_1) = edist x x_1
have inr : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x x_2 : WithLp ∞ (α × β)),
  edist (Equiv.toFun (WithLp.congr ∞ (Equiv.prodComm α β)) x) (Equiv.toFun (WithLp.congr ∞ (Equiv.prodComm α β)) x_2) =
    edist x x_2
Tactic: rcases p.trichotomy with rfl | rfl | hp
Cleared hypotheses: p, hp, x, x_1