awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
inr :
  (ENNReal.ofReal (dist f.fst g.fst) ^ p.toReal + ENNReal.ofReal (dist f.snd g.snd) ^ p.toReal) ^ p.toReal⁻¹ =
    ENNReal.ofReal ((dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ p.toReal⁻¹)
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
simp only [prod_edist_eq_add, edist_dist, one_div, prod_dist_eq_add, this]

Premises used: WithLp.prod_dist_eq_add, edist_dist, one_div, WithLp.prod_edist_eq_add
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
inr : 0 ≤ dist f.snd g.snd
inr₁ : 0 ≤ p.toReal
inr₂ : 0 ≤ dist f.fst g.fst
inr₃ : 0 ≤ p.toReal
inr₄ : 0 ≤ dist f.fst g.fst ^ p.toReal
inr₅ : 0 ≤ dist f.snd g.snd ^ p.toReal
inr₆ : 0 ≤ dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal
inr₇ : 0 ≤ p.toReal⁻¹
⊢ (ENNReal.ofReal (dist f.fst g.fst) ^ p.toReal + ENNReal.ofReal (dist f.snd g.snd) ^ p.toReal) ^ p.toReal⁻¹ =
    ENNReal.ofReal ((dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ p.toReal⁻¹)

Tactic:
rw [← ENNReal.ofReal_rpow_of_nonneg, ENNReal.ofReal_add, ← ENNReal.ofReal_rpow_of_nonneg,
        ← ENNReal.ofReal_rpow_of_nonneg]

Premises used: ENNReal.ofReal_rpow_of_nonneg, ENNReal.ofReal_add
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ dist f.snd g.snd

Tactic:
simp [Real.rpow_nonneg, add_nonneg]

Premises used: add_nonneg, Real.rpow_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ p.toReal

Tactic:
simp [Real.rpow_nonneg, add_nonneg]

Premises used: add_nonneg, Real.rpow_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ dist f.fst g.fst

Tactic:
simp [Real.rpow_nonneg, add_nonneg]

Premises used: add_nonneg, Real.rpow_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ dist f.fst g.fst ^ p.toReal

Tactic:
simp [Real.rpow_nonneg, add_nonneg]

Premises used: add_nonneg, Real.rpow_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ dist f.snd g.snd ^ p.toReal

Tactic:
simp [Real.rpow_nonneg, add_nonneg]

Premises used: add_nonneg, Real.rpow_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal

Tactic:
simp [Real.rpow_nonneg, add_nonneg]

Premises used: add_nonneg, Real.rpow_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ p.toReal⁻¹

Tactic:
simp [Real.rpow_nonneg, add_nonneg]

Premises used: add_nonneg, Real.rpow_nonneg
-- 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 (α × β)
inl :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : WithLp ∞ (α × β)),
    edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y
inr : ∀ (h : 1 ≤ p.toReal), edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y
⊢ edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y

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

Premises used: ENNReal.dichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
x y : WithLp ∞ (α × β)
⊢ edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y

Tactic:
simp [prod_edist_eq_sup]

Premises used: WithLp.prod_edist_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 (α × β)
h : 1 ≤ p.toReal
⊢ p.toReal * (1 / p.toReal) = 1

Tactic:
have cancel : p.toReal * (1 / p.toReal) = 1 := mul_div_cancel₀ 1 (zero_lt_one.trans_le h).ne'
-- 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 (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
inr :
  edist x.fst y.fst ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ∧
    edist x.snd y.snd ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
⊢ edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y

Tactic:
rw [prod_edist_eq_add (zero_lt_one.trans_le h)]

Premises used: zero_lt_one, LT.lt.trans_le, WithLp.prod_edist_eq_add
-- 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 (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
inr : edist x.fst y.fst ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
inr₁ : edist x.snd y.snd ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
⊢ edist x.fst y.fst ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ∧
    edist x.snd y.snd ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
constructor
-- 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 (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.fst y.fst ≤ (edist x.fst y.fst ^ p.toReal) ^ (1 / p.toReal)

Tactic:
simp only [← ENNReal.rpow_mul, cancel, ENNReal.rpow_one, le_refl]

Premises used: ENNReal.rpow_mul, le_refl, ENNReal.rpow_one
-- 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 (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
h₁ : edist x.fst y.fst ^ p.toReal ≤ edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal
⊢ (edist x.fst y.fst ^ p.toReal) ^ (1 / p.toReal) ≤
    (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
gcongr
-- 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 (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.fst y.fst ^ p.toReal ≤ edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal

Tactic:
simp only [self_le_add_right]

Premises used: self_le_add_right
-- 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 (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
edist : EDist.edist x.fst y.fst ≤ (EDist.edist x.fst y.fst ^ p.toReal) ^ (1 / p.toReal)
edist₁ :
  (EDist.edist x.fst y.fst ^ p.toReal) ^ (1 / p.toReal) ≤
    (EDist.edist x.fst y.fst ^ p.toReal + EDist.edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
⊢ EDist.edist x.fst y.fst ≤ (EDist.edist x.fst y.fst ^ p.toReal + EDist.edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
calc
        edist x.fst y.fst ≤ (edist x.fst y.fst ^ p.toReal) ^ (1 / p.toReal) := by
          simp only [← ENNReal.rpow_mul, cancel, ENNReal.rpow_one, le_refl]
        _ ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) := by
          gcongr
          simp only [self_le_add_right]

Premises used: HDiv.hDiv, WithLp.snd, WithLp.fst, ENNReal.toReal, HPow.hPow, HAdd.hAdd, EDist.edist, OfNat.ofNat
-- 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 (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.snd y.snd ≤ (edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
simp only [← ENNReal.rpow_mul, cancel, ENNReal.rpow_one, le_refl]

Premises used: ENNReal.rpow_mul, le_refl, ENNReal.rpow_one
-- 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 (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
h₁ : edist x.snd y.snd ^ p.toReal ≤ edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal
⊢ (edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
gcongr
-- 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 (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.snd y.snd ^ p.toReal ≤ edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal

Tactic:
simp only [self_le_add_left]

Premises used: self_le_add_left
-- 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 (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
edist : EDist.edist x.snd y.snd ≤ (EDist.edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
edist₁ :
  (EDist.edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    (EDist.edist x.fst y.fst ^ p.toReal + EDist.edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
⊢ EDist.edist x.snd y.snd ≤ (EDist.edist x.fst y.fst ^ p.toReal + EDist.edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
calc
        edist x.snd y.snd ≤ (edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) := by
          simp only [← ENNReal.rpow_mul, cancel, ENNReal.rpow_one, le_refl]
        _ ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) := by
          gcongr
          simp only [self_le_add_left]

Premises used: HDiv.hDiv, WithLp.snd, WithLp.fst, ENNReal.toReal, HPow.hPow, HAdd.hAdd, EDist.edist, OfNat.ofNat
-- 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 (α × β)
rw : edist x.ofLp.1 y.ofLp.1 ≤ edist x y ∧ edist x.ofLp.2 y.ofLp.2 ≤ edist x y
⊢ max (edist x.ofLp.1 y.ofLp.1) (edist x.ofLp.2 y.ofLp.2) ≤ (↑1 : ℝ≥0∞) * edist x y

Tactic:
rw [ENNReal.coe_one, one_mul, sup_le_iff]

Premises used: ENNReal.coe_one, sup_le_iff, one_mul
-- 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.ofLp.1 y.ofLp.1 ≤ edist x y ∧ edist x.ofLp.2 y.ofLp.2 ≤ edist x y

Tactic:
edist_proj_le_edist_aux p x y

Premises used: WithLp.snd, WithLp.fst, _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.ofLp.1 y.ofLp.1 ≤ edist x y ∧ edist x.ofLp.2 y.ofLp.2 ≤ edist x y

Tactic:
exact edist_proj_le_edist_aux p x y

Premises used: _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 (α × β)
inl :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : WithLp ∞ (α × β)),
    edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) 2 (HDiv.hDiv (α := ℝ≥0∞) 1 ∞).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
inr : ∀ (h : 1 ≤ p.toReal), edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) 2 (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
⊢ edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) 2 (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp

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

Premises used: ENNReal.dichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
x y : WithLp ∞ (α × β)
⊢ edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) 2 (HDiv.hDiv (α := ℝ≥0∞) 1 ∞).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp

Tactic:
simp [edist]

Premises used: EDist.edist
-- 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 (α × β)
h : 1 ≤ p.toReal
⊢ 0 < p.toReal

Tactic:
positivity
-- 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 (α × β)
h : 1 ≤ p.toReal
⊢ 0 < p.toReal

Tactic:
have pos : 0 < p.toReal := by positivity
-- 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 (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
⊢ 0 ≤ 1 / p.toReal

Tactic:
positivity
-- 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 (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
⊢ 0 ≤ 1 / p.toReal

Tactic:
have nonneg : 0 ≤ 1 / p.toReal := by positivity
-- 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 (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
⊢ p.toReal * (1 / p.toReal) = 1

Tactic:
have cancel : p.toReal * (1 / p.toReal) = 1 := mul_div_cancel₀ 1 (ne_of_gt pos)
-- 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 (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
inr :
  (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    (↑(HPow.hPow (α := ℝ≥0) 2 (ENNReal.toReal 1 / p.toReal)) : ℝ≥0∞) * edist x.ofLp y.ofLp
⊢ edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) 2 (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp

Tactic:
rw [prod_edist_eq_add pos, ENNReal.toReal_div 1 p]

Premises used: OfNat.ofNat, ENNReal.toReal_div, WithLp.prod_edist_eq_add
-- 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 (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
h₁ : edist x.fst y.fst ≤ edist x.ofLp y.ofLp
h₂ : edist x.snd y.snd ≤ edist x.ofLp y.ofLp
⊢ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    (edist x.ofLp y.ofLp ^ p.toReal + edist x.ofLp y.ofLp ^ p.toReal) ^ (1 / p.toReal)

Tactic:
gcongr
-- 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 (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.fst y.fst ≤ edist x.ofLp y.ofLp

Tactic:
simp [edist]

Premises used: EDist.edist
-- 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 (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.snd y.snd ≤ edist x.ofLp y.ofLp

Tactic:
simp [edist]

Premises used: EDist.edist
-- 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 (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (edist x.ofLp y.ofLp ^ p.toReal + edist x.ofLp y.ofLp ^ p.toReal) ^ (1 / p.toReal) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (1 / p.toReal)) : ℝ≥0∞) * edist x.ofLp y.ofLp

Tactic:
simp only [← two_mul, ENNReal.mul_rpow_of_nonneg _ _ nonneg, ← ENNReal.rpow_mul, cancel,
          ENNReal.rpow_one, ENNReal.coe_rpow_of_nonneg _ nonneg, coe_ofNat]

Premises used: ENNReal.rpow_mul, ENNReal.mul_rpow_of_nonneg, ENNReal.rpow_one, two_mul, ENNReal.coe_rpow_of_nonneg, ENNReal.coe_ofNat
-- 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 (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
edist :
  (EDist.edist x.fst y.fst ^ p.toReal + EDist.edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    (EDist.edist x.ofLp y.ofLp ^ p.toReal + EDist.edist x.ofLp y.ofLp ^ p.toReal) ^ (1 / p.toReal)
edist₁ :
  (EDist.edist x.ofLp y.ofLp ^ p.toReal + EDist.edist x.ofLp y.ofLp ^ p.toReal) ^ (1 / p.toReal) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (1 / p.toReal)) : ℝ≥0∞) * EDist.edist x.ofLp y.ofLp
⊢ (EDist.edist x.fst y.fst ^ p.toReal + EDist.edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    (↑(HPow.hPow (α := ℝ≥0) 2 (1 / p.toReal)) : ℝ≥0∞) *
      max (EDist.edist x.ofLp.1 y.ofLp.1) (EDist.edist x.ofLp.2 y.ofLp.2)

Tactic:
calc
      (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ≤
          (edist (ofLp x) (ofLp y) ^ p.toReal +
          edist (ofLp x) (ofLp y) ^ p.toReal) ^ (1 / p.toReal) := by
        gcongr <;> simp [edist]
      _ = (2 ^ (1 / p.toReal) : ℝ≥0) * edist (ofLp x) (ofLp y) := by
        simp only [← two_mul, ENNReal.mul_rpow_of_nonneg _ _ nonneg, ← ENNReal.rpow_mul, cancel,
          ENNReal.rpow_one, ENNReal.coe_rpow_of_nonneg _ nonneg, coe_ofNat]

Premises used: HDiv.hDiv, WithLp.snd, WithLp.fst, ENNReal.toReal, HPow.hPow, HAdd.hAdd, EDist.edist, OfNat.ofNat, WithLp.ofLp
-- 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 (α := WithLp p (α × β)) ofLp

Tactic:
(prod_antilipschitzWith_ofLp_aux p α β).isUniformInducing
    (prod_lipschitzWith_ofLp_aux p α β).uniformContinuous

Premises used: AntilipschitzWith.isUniformInducing, _private.0.WithLp.prod_lipschitzWith_ofLp_aux, _private.0.WithLp.prod_antilipschitzWith_ofLp_aux, LipschitzWith.uniformContinuous
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
rw :
  Eq (α := Filter (WithLp p (α × β) × WithLp p (α × β)))
    (comap (β := (α × β) × α × β) (fun (x : WithLp p (α × β) × WithLp p (α × β)) ↦ (x.1.ofLp, x.2.ofLp)) (𝓤 (α × β)))
    (𝓤 (WithLp p (α × β)))
⊢ Eq (α := Filter (WithLp p (α × β) × WithLp p (α × β))) (𝓤 (WithLp p (α × β))) (𝓤 (WithLp p (α × β)))

Tactic:
rw [← (isUniformInducing_ofLp_aux p α β).comap_uniformity]

Premises used: IsUniformInducing.comap_uniformity, _private.0.WithLp.isUniformInducing_ofLp_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 β
⊢ Eq (α := Filter (WithLp p (α × β) × WithLp p (α × β)))
    (comap (β := (α × β) × α × β) (fun (x : WithLp p (α × β) × WithLp p (α × β)) ↦ (x.1.ofLp, x.2.ofLp)) (𝓤 (α × β)))
    (𝓤 (WithLp p (α × β)))

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

Tactic:
le_antisymm (prod_antilipschitzWith_ofLp_aux p α β).tendsto_cobounded.le_comap
      (prod_lipschitzWith_ofLp_aux p α β).comap_cobounded_le

Premises used: Filter.Tendsto.le_comap, AntilipschitzWith.tendsto_cobounded, _private.0.WithLp.prod_lipschitzWith_ofLp_aux, _private.0.WithLp.prod_antilipschitzWith_ofLp_aux, LipschitzWith.comap_cobounded_le, le_antisymm
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
⊢ Continuous[instTopologicalSpaceProd, instProdTopologicalSpace p α β] (toLp p)

Tactic:
continuous_induced_rng.2 continuous_id

Premises used: Iff.mpr, continuous_id, continuous_induced_rng
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
⊢ Continuous[instProdTopologicalSpace p α β, instTopologicalSpaceProd] ofLp

Tactic:
continuous_induced_dom

Premises used: continuous_induced_dom
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
⊢ Homeomorph.toEquiv (homeomorphProd p α β) = WithLp.equiv p (α × β)

Tactic:
rfl

Premises used: WithLp.equiv, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
⊢ Continuous[instProdTopologicalSpace p α β, inst] WithLp.fst

Tactic:
continuous_fst.comp <| prod_continuous_ofLp ..

Premises used: Continuous.comp, continuous_fst, WithLp.fst, WithLp.prod_continuous_ofLp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
⊢ Continuous[instProdTopologicalSpace p α β, inst_1] WithLp.snd

Tactic:
continuous_snd.comp <| prod_continuous_ofLp ..

Premises used: Continuous.comp, continuous_snd, WithLp.snd, WithLp.prod_continuous_ofLp
-- 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 : T0Space α
inst_3 : T0Space β
⊢ T0Space (WithLp p (α × β))

Tactic:
(homeomorphProd p α β).symm.t0Space

Premises used: Homeomorph.t0Space, Homeomorph.symm, WithLp.homeomorphProd
-- 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 : T0Space α
inst_3 : T0Space β
inst_4 : SecondCountableTopology α
inst_5 : SecondCountableTopology β
⊢ SecondCountableTopology (WithLp p (α × β))

Tactic:
(homeomorphProd p α β).secondCountableTopology

Premises used: Homeomorph.secondCountableTopology, WithLp.homeomorphProd
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ UniformContinuous (α := α × β) (toLp p)

Tactic:
uniformContinuous_comap' uniformContinuous_id

Premises used: uniformContinuous_id, uniformContinuous_comap'
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ UniformContinuous (α := WithLp p (α × β)) ofLp

Tactic:
uniformContinuous_comap

Premises used: uniformContinuous_comap