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 : 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
⊢ (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⁻¹)
have inr₂ : 0 ≤ dist f.fst g.fst
Tactic: rw [← ENNReal.ofReal_rpow_of_nonneg, ENNReal.ofReal_add, ← ENNReal.ofReal_rpow_of_nonneg,
        ← ENNReal.ofReal_rpow_of_nonneg]
-- 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 : 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
⊢ (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⁻¹)
have inr₄ : 0 ≤ dist f.fst g.fst ^ p.toReal
Tactic: rw [← ENNReal.ofReal_rpow_of_nonneg, ENNReal.ofReal_add, ← ENNReal.ofReal_rpow_of_nonneg,
        ← ENNReal.ofReal_rpow_of_nonneg]
-- 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 : 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
⊢ (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⁻¹)
have inr₅ : 0 ≤ dist f.snd g.snd ^ p.toReal
Tactic: rw [← ENNReal.ofReal_rpow_of_nonneg, ENNReal.ofReal_add, ← ENNReal.ofReal_rpow_of_nonneg,
        ← ENNReal.ofReal_rpow_of_nonneg]
-- 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 : 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
⊢ (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⁻¹)
have inr₆ : 0 ≤ dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal
Tactic: rw [← ENNReal.ofReal_rpow_of_nonneg, ENNReal.ofReal_add, ← ENNReal.ofReal_rpow_of_nonneg,
        ← ENNReal.ofReal_rpow_of_nonneg]
-- 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 : 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
⊢ (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⁻¹)
have inr₇ : 0 ≤ p.toReal⁻¹
Tactic: rw [← ENNReal.ofReal_rpow_of_nonneg, ENNReal.ofReal_add, ← ENNReal.ofReal_rpow_of_nonneg,
        ← ENNReal.ofReal_rpow_of_nonneg]
-- 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 : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x y : WithLp p (α × β)
⊢ edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y
have 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
Tactic: rcases p.dichotomy with (rfl | h)
Cleared hypotheses: p, hp, x, y
-- 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 : 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
⊢ edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y
have inr : ∀ (h : 1 ≤ p.toReal), edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y
Tactic: rcases p.dichotomy with (rfl | h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (hypothesis)
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
⊢ edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y
have cancel : 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'
-- 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 : 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 y ∧ edist x.snd y.snd ≤ edist x y
have 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)
Tactic: rw [prod_edist_eq_add (zero_lt_one.trans_le h)]
-- 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 : 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 + 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)
have inr : edist x.fst y.fst ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
Tactic: constructor
-- 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 : 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.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)
have inr₁ : edist x.snd y.snd ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
Tactic: constructor
-- 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 : 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) ^ (1 / p.toReal) ≤
    (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
have h₁ : edist x.fst y.fst ^ p.toReal ≤ edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal
Tactic: gcongr
-- 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 : 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 + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
have edist : edist x.fst y.fst ≤ (edist x.fst y.fst ^ 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]
-- 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 : 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 x.fst y.fst ≤ (EDist.edist x.fst y.fst ^ p.toReal + EDist.edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
have 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)
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]
-- 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 : 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) ^ (1 / p.toReal) ≤
    (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
have h₁ : edist x.snd y.snd ^ p.toReal ≤ edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal
Tactic: gcongr
-- 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 : 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.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
have edist : edist x.snd y.snd ≤ (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]
-- 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 : 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 x.snd y.snd ≤ (EDist.edist x.fst y.fst ^ p.toReal + EDist.edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
have 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)
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]
-- 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 : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x y : WithLp p (α × β)
⊢ max (edist x.ofLp.1 y.ofLp.1) (edist x.ofLp.2 y.ofLp.2) ≤ (↑1 : ℝ≥0∞) * edist x y
have rw : edist x.ofLp.1 y.ofLp.1 ≤ edist x y ∧ edist x.ofLp.2 y.ofLp.2 ≤ edist x y
Tactic: rw [ENNReal.coe_one, one_mul, sup_le_iff]
-- 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 : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x y : WithLp p (α × β)
⊢ edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) 2 (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
have 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
Tactic: rcases p.dichotomy with (rfl | h)
Cleared hypotheses: p, hp, x, y
-- 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 : 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
⊢ edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) 2 (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
have inr : ∀ (h : 1 ≤ p.toReal), edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) 2 (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
Tactic: rcases p.dichotomy with (rfl | h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (hypothesis)
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
⊢ edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) 2 (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
have pos : 0 < p.toReal
Tactic: have pos : 0 < p.toReal := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (hypothesis)
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
⊢ edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) 2 (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
have nonneg : 0 ≤ 1 / p.toReal
Tactic: have nonneg : 0 ≤ 1 / p.toReal := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (hypothesis)
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
⊢ edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) 2 (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
have cancel : p.toReal * (1 / p.toReal) = 1
Tactic: have cancel : p.toReal * (1 / p.toReal) = 1 := mul_div_cancel₀ 1 (ne_of_gt pos)
-- 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 : 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 y ≤ (↑(HPow.hPow (α := ℝ≥0) 2 (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
have 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
Tactic: rw [prod_edist_eq_add pos, ENNReal.toReal_div 1 p]
-- 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 : 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 ^ 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)
have h₁ : edist x.fst y.fst ≤ edist x.ofLp y.ofLp
Tactic: gcongr
-- 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 : 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
⊢ (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)
have h₂ : edist x.snd y.snd ≤ edist x.ofLp y.ofLp
Tactic: gcongr
-- 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 : 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 ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    (↑(HPow.hPow (α := ℝ≥0) 2 (1 / p.toReal)) : ℝ≥0∞) * max (edist x.ofLp.1 y.ofLp.1) (edist x.ofLp.2 y.ofLp.2)
have edist : (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: 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]
-- 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 : 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 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)
have 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
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]
-- 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 : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
⊢ Eq (α := Filter (WithLp p (α × β) × WithLp p (α × β))) (𝓤 (WithLp p (α × β))) (𝓤 (WithLp p (α × β)))
have rw : Eq (α := Filter (WithLp p (α × β) × WithLp p (α × β)))
  (comap (β := (α × β) × α × β) (fun (x : WithLp p (α × β) × WithLp p (α × β)) ↦ (x.1.ofLp, x.2.ofLp)) (𝓤 (α × β)))
  (𝓤 (WithLp p (α × β)))
Tactic: rw [← (isUniformInducing_ofLp_aux p α β).comap_uniformity]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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 (α × β)
⊢ (↑(nndist x y) : ℝ) = (↑((nndist x.fst y.fst ^ p.toReal + nndist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)) : ℝ)
have push_cast : dist x y = (dist x.fst y.fst ^ p.toReal + dist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
α : Type u_2
β : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x y : WithLp ∞ (α × β)
⊢ (↑(nndist x y) : ℝ) = (↑(max (nndist x.fst y.fst) (nndist x.snd y.snd)) : ℝ)
have push_cast : dist x y = max (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:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x y : WithLp p (α × β)
⊢ dist x y = ‖-x + y‖
have inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : WithLp ∞ (α × β)), dist x y = ‖-x + y‖
Tactic: rcases p.dichotomy with (rfl | h)
Cleared hypotheses: p, hp, x, y
-- 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 β
x y : WithLp p (α × β)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : WithLp ∞ (α × β)), dist x y = ‖-x + y‖
⊢ dist x y = ‖-x + y‖
have inr : ∀ (h : 1 ≤ p.toReal), dist x y = ‖-x + y‖
Tactic: rcases p.dichotomy with (rfl | h)
-- 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 β
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
x y : WithLp ∞ (α × β)
⊢ dist x y = ‖-x + y‖
have inl : max ‖-x.fst + y.fst‖ ‖-x.snd + y.snd‖ = max ‖(-x + y).fst‖ ‖(-x + y).snd‖
Tactic: simp only [prod_dist_eq_sup, prod_norm_eq_sup, dist_eq_norm, ← norm_neg_add]
-- 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 β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ dist x y = ‖-x + y‖
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (hypothesis)
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 (α × β)
⊢ ‖f‖ = (‖f.fst‖ ^ n + ‖f.snd‖ ^ n) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
have this : 0 < p.toReal
Tactic: have := p.toReal_pos_iff_ne_top.mpr (ne_of_eq_of_ne h <| ENNReal.natCast_ne_top n)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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)
have a : (↑‖f‖₊ : ℝ) = (↑((‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)) : ℝ)
Tactic: ext
-- 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 ∞ (α × β)
⊢ ‖f‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊
have a : (↑‖f‖₊ : ℝ) = (↑(max ‖f.fst‖₊ ‖f.snd‖₊) : ℝ)
Tactic: ext
-- 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 ∞ (α × β)
⊢ (↑‖f‖₊ : ℝ) = (↑(max ‖f.fst‖₊ ‖f.snd‖₊) : ℝ)
have a : ‖f‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊
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 β
f : WithLp ∞ (α × β)
⊢ ‖f.ofLp‖₊ = ‖f‖₊
have rw : ‖f.ofLp‖₊ = 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‖₊
⊢ ‖f.ofLp‖₊ = ‖f‖₊
have rw₁ : max ‖f.ofLp.1‖₊ ‖f.ofLp.2‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊
Tactic: rw [prod_nnnorm_eq_sup, Prod.nnnorm_def, ofLp_fst, ofLp_snd]