awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ Eq (α := WithLp p (α × β) ≃ₜ α × β) (UniformEquiv.toHomeomorph (uniformEquivProd p α β)) (homeomorphProd p α β)

Tactic:
rfl

Premises used: WithLp.equiv, setOf, UniformEquiv.toHomeomorph, WithLp.homeomorphProd, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ UniformEquiv.toEquiv (uniformEquivProd p α β) = WithLp.equiv p (α × β)

Tactic:
rfl

Premises used: WithLp.equiv, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace α
inst_3 : CompleteSpace β
⊢ CompleteSpace (WithLp p (α × β))

Tactic:
(uniformEquivProd p α β).completeSpace_iff.2 inferInstance

Premises used: Iff.mpr, inferInstance, WithLp.uniformEquivProd, UniformEquiv.completeSpace_iff
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Semiring 𝕜
inst_3 : AddCommGroup α
inst_4 : AddCommGroup β
inst_5 : Module 𝕜 α
inst_6 : Module 𝕜 β
x : α × β
⊢ (ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p 𝕜 α β) : (a : α × β) → WithLp p (α × β)) x = toLp p x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
hp : p ≠ ∞
x y : WithLp p (α × β)
push_cast : dist x y = (dist x.fst y.fst ^ p.toReal + dist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
⊢ (↑(nndist x y) : ℝ) = (↑((nndist x.fst y.fst ^ p.toReal + nndist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
hp : p ≠ ∞
x y : WithLp p (α × β)
⊢ dist x y = (dist x.fst y.fst ^ p.toReal + dist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
prod_dist_eq_add (p.toReal_pos_iff_ne_top.mpr hp) _ _

Premises used: Iff.mpr, WithLp.prod_dist_eq_add, ENNReal.toReal_pos_iff_ne_top
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
hp : p ≠ ∞
x y : WithLp p (α × β)
⊢ dist x y = (dist x.fst y.fst ^ p.toReal + dist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
exact prod_dist_eq_add (p.toReal_pos_iff_ne_top.mpr hp) _ _

Premises used: Iff.mpr, WithLp.prod_dist_eq_add, ENNReal.toReal_pos_iff_ne_top
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x y : WithLp ∞ (α × β)
push_cast : dist x y = max (dist x.fst y.fst) (dist x.snd y.snd)
⊢ (↑(nndist x y) : ℝ) = (↑(max (nndist x.fst y.fst) (nndist x.snd y.snd)) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x y : WithLp ∞ (α × β)
⊢ dist x y = max (dist x.fst y.fst) (dist x.snd y.snd)

Tactic:
prod_dist_eq_sup _ _

Premises used: WithLp.prod_dist_eq_sup
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x y : WithLp ∞ (α × β)
⊢ dist x y = max (dist x.fst y.fst) (dist x.snd y.snd)

Tactic:
exact prod_dist_eq_sup _ _

Premises used: WithLp.prod_dist_eq_sup
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x y : WithLp p (α × β)
⊢ edist x.fst y.fst ≤ edist x y

Tactic:
(edist_proj_le_edist_aux p x y).1

Premises used: And.left, _private.0.WithLp.edist_proj_le_edist_aux
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x y : WithLp p (α × β)
⊢ edist x.snd y.snd ≤ edist x y

Tactic:
(edist_proj_le_edist_aux p x y).2

Premises used: And.right, _private.0.WithLp.edist_proj_le_edist_aux
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x y : WithLp p (α × β)
⊢ nndist x.fst y.fst ≤ nndist x y

Tactic:
simpa [← coe_nnreal_ennreal_nndist] using edist_fst_le x y

Premises used: WithLp.edist_fst_le, coe_nnreal_ennreal_nndist
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x y : WithLp p (α × β)
⊢ nndist x.snd y.snd ≤ nndist x y

Tactic:
simpa [← coe_nnreal_ennreal_nndist] using edist_snd_le x y

Premises used: coe_nnreal_ennreal_nndist, WithLp.edist_snd_le
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x y : WithLp p (α × β)
⊢ dist x.fst y.fst ≤ dist x y

Tactic:
nndist_fst_le x y

Premises used: WithLp.nndist_fst_le
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x y : WithLp p (α × β)
⊢ dist x.snd y.snd ≤ dist x y

Tactic:
nndist_snd_le x y

Premises used: WithLp.nndist_snd_le
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
⊢ LipschitzWith (α := WithLp p (α × β)) 1 ofLp

Tactic:
prod_lipschitzWith_ofLp_aux p α β

Premises used: LipschitzWith, iInf, Set.Mem, setOf, _private.0.WithLp.prod_lipschitzWith_ofLp_aux, Set.Subset, Filter.join, Filter.comap
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
⊢ AntilipschitzWith (α := α × β) 1 (toLp p)

Tactic:
(prod_lipschitzWith_ofLp p α β).to_rightInverse (ofLp_toLp p)

Premises used: WithLp.prod_lipschitzWith_ofLp, LipschitzWith.to_rightInverse, WithLp.ofLp_toLp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
⊢ AntilipschitzWith (α := WithLp p (α × β)) (HPow.hPow (α := ℝ≥0) 2 (1 / p).toReal) ofLp

Tactic:
prod_antilipschitzWith_ofLp_aux p α β

Premises used: iInf, Set.Mem, setOf, _private.0.WithLp.prod_antilipschitzWith_ofLp_aux, Set.Subset, Filter.join, Filter.comap, AntilipschitzWith
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
⊢ LipschitzWith (α := α × β) (HPow.hPow (α := ℝ≥0) 2 (1 / p).toReal) (toLp p)

Tactic:
(prod_antilipschitzWith_ofLp p α β).to_rightInverse (ofLp_toLp p)

Premises used: AntilipschitzWith.to_rightInverse, WithLp.ofLp_toLp, WithLp.prod_antilipschitzWith_ofLp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x y : WithLp ∞ (α × β)
⊢ edist x.ofLp y.ofLp ≤ edist x y

Tactic:
simpa only [ENNReal.coe_one, one_mul] using prod_lipschitzWith_ofLp ∞ α β x y

Premises used: ENNReal.coe_one, WithLp.prod_lipschitzWith_ofLp, Top.top, one_mul
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x y : WithLp ∞ (α × β)
⊢ edist x y ≤ edist x.ofLp y.ofLp

Tactic:
simpa only [ENNReal.div_top, ENNReal.toReal_zero, NNReal.rpow_zero, ENNReal.coe_one,
        one_mul] using prod_antilipschitzWith_ofLp ∞ α β x y

Premises used: ENNReal.div_top, ENNReal.coe_one, ENNReal.toReal_zero, NNReal.rpow_zero, Top.top, one_mul, WithLp.prod_antilipschitzWith_ofLp
-- 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 β
x y : WithLp p (α × β)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : WithLp ∞ (α × β)), dist x y = ‖-x + y‖
inr : ∀ (h : 1 ≤ p.toReal), dist x y = ‖-x + y‖
⊢ dist x y = ‖-x + y‖

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

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 β
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
x y : WithLp ∞ (α × β)
inl : max ‖-x.fst + y.fst‖ ‖-x.snd + y.snd‖ = max ‖(-x + y).fst‖ ‖(-x + y).snd‖
⊢ dist x y = ‖-x + y‖

Tactic:
simp only [prod_dist_eq_sup, prod_norm_eq_sup, dist_eq_norm, ← norm_neg_add]

Premises used: dist_eq_norm, norm_neg_add, WithLp.prod_dist_eq_sup, WithLp.prod_norm_eq_sup
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
x y : WithLp ∞ (α × β)
⊢ max ‖-x.fst + y.fst‖ ‖-x.snd + y.snd‖ = max ‖(-x + y).fst‖ ‖(-x + y).snd‖

Tactic:
rfl
-- 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 β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
inr :
  (‖-x.fst + y.fst‖ ^ p.toReal + ‖-x.snd + y.snd‖ ^ p.toReal) ^ (1 / p.toReal) =
    (‖(-x + y).fst‖ ^ p.toReal + ‖(-x + y).snd‖ ^ p.toReal) ^ (1 / p.toReal)
⊢ dist x y = ‖-x + y‖

Tactic:
simp only [prod_dist_eq_add (zero_lt_one.trans_le h),
        prod_norm_eq_add (zero_lt_one.trans_le h), dist_eq_norm, ← norm_neg_add]

Premises used: dist_eq_norm, norm_neg_add, WithLp.prod_norm_eq_add, WithLp.prod_dist_eq_add, zero_lt_one, LT.lt.trans_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 β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ (‖-x.fst + y.fst‖ ^ p.toReal + ‖-x.snd + y.snd‖ ^ p.toReal) ^ (1 / p.toReal) =
    (‖(-x + y).fst‖ ^ p.toReal + ‖(-x + y).snd‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
⊢ IsUniformInducing (α := α × β) (toLp p)

Tactic:
(prod_antilipschitzWith_toLp p α β).isUniformInducing
    (prod_lipschitzWith_toLp p α β).uniformContinuous

Premises used: AntilipschitzWith.isUniformInducing, WithLp.prod_antilipschitzWith_toLp, WithLp.prod_lipschitzWith_toLp, LipschitzWith.uniformContinuous
-- 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 : WithLp p (α × β)
⊢ ‖x.fst‖ₑ ≤ ‖x‖ₑ

Tactic:
simpa using edist_fst_le x 0

Premises used: WithLp.edist_fst_le, OfNat.ofNat
-- 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 : WithLp p (α × β)
⊢ ‖x.snd‖ₑ ≤ ‖x‖ₑ

Tactic:
simpa using edist_snd_le x 0

Premises used: OfNat.ofNat, WithLp.edist_snd_le
-- 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 : WithLp p (α × β)
⊢ ‖x.fst‖₊ ≤ ‖x‖₊

Tactic:
simpa using nndist_fst_le x 0

Premises used: WithLp.nndist_fst_le, OfNat.ofNat
-- 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 : WithLp p (α × β)
⊢ ‖x.snd‖₊ ≤ ‖x‖₊

Tactic:
simpa using nndist_snd_le x 0

Premises used: OfNat.ofNat, WithLp.nndist_snd_le
-- 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 : WithLp p (α × β)
⊢ ‖x.fst‖ ≤ ‖x‖

Tactic:
simpa using dist_fst_le x 0

Premises used: OfNat.ofNat, WithLp.dist_fst_le
-- 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 : WithLp p (α × β)
⊢ ‖x.snd‖ ≤ ‖x‖

Tactic:
simpa using dist_snd_le x 0

Premises used: WithLp.dist_snd_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : NormedAddCommGroup α
inst_1 : NormedAddCommGroup β
⊢ UniformSpace.toTopologicalSpace = instProdTopologicalSpace p α β

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : NormedAddCommGroup α
inst_1 : NormedAddCommGroup β
⊢ PseudoMetricSpace.toUniformSpace = instProdUniformSpace p α β

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : NormedAddCommGroup α
inst_1 : NormedAddCommGroup β
⊢ PseudoMetricSpace.toBornology = instProdBornology p α β

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : Norm α
inst_1 : Norm β
n : ℕ
h : p = (↑n : ℝ≥0∞)
f : WithLp p (α × β)
⊢ 0 < p.toReal

Tactic:
have := p.toReal_pos_iff_ne_top.mpr (ne_of_eq_of_ne h <| ENNReal.natCast_ne_top n)
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : Norm α
inst_1 : Norm β
n : ℕ
h : p = (↑n : ℝ≥0∞)
f : WithLp p (α × β)
this : 0 < p.toReal
⊢ ‖f‖ = (‖f.fst‖ ^ n + ‖f.snd‖ ^ n) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
simp only [one_div, h, Real.rpow_natCast, ENNReal.toReal_natCast,
    prod_norm_eq_add this]

Premises used: WithLp.prod_norm_eq_add, ENNReal.toReal_natCast, one_div, Real.rpow_natCast
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
f : WithLp p (α × β)
a : (↑‖f‖₊ : ℝ) = (↑((‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)) : ℝ)
⊢ ‖f‖₊ = (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
f : WithLp p (α × β)
⊢ (↑‖f‖₊ : ℝ) = (↑((‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)) : ℝ)

Tactic:
simp [prod_norm_eq_add (p.toReal_pos_iff_ne_top.mpr hp)]

Premises used: Iff.mpr, WithLp.prod_norm_eq_add, ENNReal.toReal_pos_iff_ne_top
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
f : WithLp ∞ (α × β)
a : (↑‖f‖₊ : ℝ) = (↑(max ‖f.fst‖₊ ‖f.snd‖₊) : ℝ)
⊢ ‖f‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
f : WithLp ∞ (α × β)
a a₁ a₂ a₃ : ‖f‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊
⊢ (↑‖f‖₊ : ℝ) = (↑(max ‖f.fst‖₊ ‖f.snd‖₊) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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‖₊
rw₃ rw₄ : max ‖f.fst‖₊ ‖f.snd‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊
⊢ ‖f.ofLp‖₊ = ‖f‖₊

Tactic:
rw [prod_nnnorm_eq_sup, Prod.nnnorm_def, ofLp_fst, ofLp_snd]

Premises used: WithLp.ofLp_fst, Prod.nnnorm_def, WithLp.prod_nnnorm_eq_sup, WithLp.ofLp_snd
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
f : α × β
⊢ nnnorm (E := WithLp ∞ (α × β)) (toLp ∞ f) = ‖f‖₊

Tactic:
(prod_nnnorm_ofLp _).symm

Premises used: WithLp.prod_nnnorm_ofLp, Eq.symm
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
f : WithLp ∞ (α × β)
⊢ ‖f.ofLp‖ = ‖f‖

Tactic:
congr_arg NNReal.toReal <| prod_nnnorm_ofLp f

Premises used: WithLp.prod_nnnorm_ofLp, congr_arg, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
f : α × β
⊢ Norm.norm (E := WithLp ∞ (α × β)) (toLp ∞ f) = ‖f‖

Tactic:
(prod_norm_ofLp _).symm

Premises used: WithLp.prod_norm_ofLp, Eq.symm
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
⊢ ‖x‖ = ‖x.fst‖ + ‖x.snd‖

Tactic:
simp [prod_norm_eq_add]

Premises used: WithLp.prod_norm_eq_add
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
push_cast : ‖x‖ = ‖x.fst‖ + ‖x.snd‖
⊢ (↑‖x‖₊ : ℝ) = (↑(‖x.fst‖₊ + ‖x.snd‖₊) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
⊢ ‖x‖ = ‖x.fst‖ + ‖x.snd‖

Tactic:
prod_norm_eq_of_L1 x

Premises used: WithLp.prod_norm_eq_of_L1
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
⊢ ‖x‖ = ‖x.fst‖ + ‖x.snd‖

Tactic:
exact prod_norm_eq_of_L1 x

Premises used: WithLp.prod_norm_eq_of_L1
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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‖
simp_rw₂ : ‖x.fst - 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

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

Premises used: dist_eq_norm, WithLp.sub_fst, WithLp.prod_norm_eq_of_L1, WithLp.sub_snd
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x y : WithLp 1 (α × β)
push_cast : dist x y = dist x.fst y.fst + dist x.snd y.snd
⊢ (↑(nndist x y) : ℝ) = (↑(nndist x.fst y.fst + nndist x.snd y.snd) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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

Tactic:
prod_dist_eq_of_L1 _ _

Premises used: WithLp.prod_dist_eq_of_L1
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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

Tactic:
exact prod_dist_eq_of_L1 _ _

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

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 : WithLp 2 (α × β)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℕ) 2 2
⊢ Eq (α := ℝ≥0∞) 2 (↑2 : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
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)
⊢ ‖x‖ = √(HPow.hPow (β := ℕ) ‖x.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd‖ 2)

Tactic:
rw [prod_norm_eq_of_nat 2 (by norm_cast) _, Real.sqrt_eq_rpow]

Premises used: WithLp.prod_norm_eq_of_nat, OfNat.ofNat, Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
norm_cast norm_cast₁ norm_cast₂ 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
⊢ (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:
norm_cast
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
push_cast : ‖x‖ = √(HPow.hPow (β := ℕ) ‖x.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd‖ 2)
⊢ (↑‖x‖₊ : ℝ) = (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) ‖x.fst‖₊ 2 + HPow.hPow (β := ℕ) ‖x.snd‖₊ 2)) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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)

Tactic:
prod_norm_eq_of_L2 x

Premises used: 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 : WithLp 2 (α × β)
⊢ ‖x‖ = √(HPow.hPow (β := ℕ) ‖x.fst‖ 2 + HPow.hPow (β := ℕ) ‖x.snd‖ 2)

Tactic:
exact prod_norm_eq_of_L2 x

Premises used: 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 : WithLp 2 (α × β)
this : HPow.hPow (β := ℕ) ‖x‖₊ 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

Tactic:
simpa only [NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) this

Premises used: NNReal.coe_sum, congr_arg, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
suffices : HPow.hPow (β := ℕ) ‖x‖₊ 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

Tactic:
suffices ‖x‖₊ ^ 2 = ‖x.fst‖₊ ^ 2 + ‖x.snd‖₊ ^ 2 by
    simpa only [NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) this
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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
rw₁ rw₂ :
  HPow.hPow (β := ℕ) ‖x.fst‖₊ 2 + HPow.hPow (β := ℕ) ‖x.snd‖₊ 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

Tactic:
rw [prod_nnnorm_eq_of_L2, NNReal.sq_sqrt]

Premises used: WithLp.prod_nnnorm_eq_of_L2, NNReal.sq_sqrt