awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : WithLp p (α × β)
h : 0 < p.toReal
⊢ edist f f = 0

Tactic:
simp [prod_edist_eq_add h, ENNReal.zero_rpow_of_pos h,
      ENNReal.zero_rpow_of_pos (inv_pos.2 <| h)]

Premises used: Iff.mpr, ENNReal.zero_rpow_of_pos, inv_pos, WithLp.prod_edist_eq_add
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g : WithLp p (α × β)
inl : ∀ (f g : WithLp 0 (α × β)), edist f g = edist g f
inr : ∀ (f g : WithLp ∞ (α × β)), edist f g = edist g f
inr₁ : ∀ (h : 0 < p.toReal), edist f g = edist g f
⊢ edist f g = edist g f

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

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g : WithLp 0 (α × β)
⊢ edist f g = edist g f

Tactic:
simp only [prod_edist_eq_card, edist_comm]

Premises used: WithLp.prod_edist_eq_card, PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g : WithLp ∞ (α × β)
⊢ edist f g = edist g f

Tactic:
simp only [prod_edist_eq_sup, edist_comm]

Premises used: PseudoEMetricSpace.edist_comm, WithLp.prod_edist_eq_sup
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g : WithLp p (α × β)
h : 0 < p.toReal
⊢ edist f g = edist g f

Tactic:
simp only [prod_edist_eq_add h, edist_comm]

Premises used: PseudoEMetricSpace.edist_comm, WithLp.prod_edist_eq_add
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g : WithLp p (α × β)
inl : ∀ (f g : WithLp 0 (α × β)), edist f g = edist g f
inr : ∀ (f g : WithLp ∞ (α × β)), edist f g = edist g f
inr₁ : ∀ (h : 0 < p.toReal), edist f g = edist g f
inr₂ : ∀ (f g : WithLp ∞ (α × β)), edist f g = edist g f
inr₃ inr₄ : ∀ (h : 0 < p.toReal), edist f g = edist g f
⊢ edist f g = edist g f

Tactic:
classical
  rcases p.trichotomy with (rfl | rfl | h)
  · simp only [prod_edist_eq_card, edist_comm]
  · simp only [prod_edist_eq_sup, edist_comm]
  · simp only [prod_edist_eq_add h, edist_comm]

Premises used: WithLp.prod_edist_eq_card, PseudoEMetricSpace.edist_comm, WithLp.prod_edist_eq_sup, ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : Dist α
inst_1 : Dist β
f g : WithLp 0 (α × β)
⊢ (if Eq (α := ℝ≥0∞) 0 0 then
      HAdd.hAdd (α := ℝ) (if dist f.fst g.fst = 0 then 0 else 1) (if dist f.snd g.snd = 0 then 0 else 1)
    else
      if Eq (α := ℝ≥0∞) 0 ∞ then max (dist f.fst g.fst) (dist f.snd g.snd)
      else (dist f.fst g.fst ^ ENNReal.toReal 0 + dist f.snd g.snd ^ ENNReal.toReal 0) ^ (1 / ENNReal.toReal 0)) =
    HAdd.hAdd (α := ℝ) (if dist f.fst g.fst = 0 then 0 else 1) (if dist f.snd g.snd = 0 then 0 else 1)

Tactic:
if_pos rfl

Premises used: if_pos, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : Dist α
inst_1 : Dist β
f g : WithLp 0 (α × β)
⊢ dist f g = HAdd.hAdd (α := ℝ) (if dist f.fst g.fst = 0 then 0 else 1) (if dist f.snd g.snd = 0 then 0 else 1)

Tactic:
convert! if_pos rfl

Premises used: if_pos, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : Dist α
inst_1 : Dist β
hp : 0 < p.toReal
f g : WithLp p (α × β)
⊢ dist f g = (dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
let hp' := ENNReal.toReal_pos_iff.mp hp
  (if_neg hp'.1.ne').trans (if_neg hp'.2.ne)

Premises used: ENNReal.toReal_pos_iff, dite, LT.lt.ne', And.right, And.left, Iff.mp, if_neg, Eq.trans, LT.lt.ne, ite
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : Dist α
inst_1 : Dist β
f g : WithLp ∞ (α × β)
⊢ dist f g = max (dist f.fst g.fst) (dist f.snd g.snd)

Tactic:
rfl

Premises used: dite, rfl, ite
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : Norm α
inst_1 : Norm β
f : WithLp 0 (α × β)
⊢ (if Eq (α := ℝ≥0∞) 0 0 then HAdd.hAdd (α := ℝ) (if ‖f.fst‖ = 0 then 0 else 1) (if ‖f.snd‖ = 0 then 0 else 1)
    else
      if Eq (α := ℝ≥0∞) 0 ∞ then max ‖f.fst‖ ‖f.snd‖
      else (‖f.fst‖ ^ ENNReal.toReal 0 + ‖f.snd‖ ^ ENNReal.toReal 0) ^ (1 / ENNReal.toReal 0)) =
    HAdd.hAdd (α := ℝ) (if ‖f.fst‖ = 0 then 0 else 1) (if ‖f.snd‖ = 0 then 0 else 1)

Tactic:
if_pos rfl

Premises used: if_pos, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : Norm α
inst_1 : Norm β
f : WithLp 0 (α × β)
⊢ ‖f‖ = HAdd.hAdd (α := ℝ) (if ‖f.fst‖ = 0 then 0 else 1) (if ‖f.snd‖ = 0 then 0 else 1)

Tactic:
convert! if_pos rfl

Premises used: if_pos, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : Norm α
inst_1 : Norm β
f : WithLp ∞ (α × β)
⊢ ‖f‖ = max ‖f.fst‖ ‖f.snd‖

Tactic:
rfl

Premises used: dite, rfl, ite
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : Norm α
inst_1 : Norm β
hp : 0 < p.toReal
f : WithLp p (α × β)
⊢ ‖f‖ = (‖f.fst‖ ^ p.toReal + ‖f.snd‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
let hp' := ENNReal.toReal_pos_iff.mp hp
  (if_neg hp'.1.ne').trans (if_neg hp'.2.ne)

Premises used: ENNReal.toReal_pos_iff, dite, LT.lt.ne', And.right, And.left, Iff.mp, if_neg, Eq.trans, LT.lt.ne, ite
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g h : WithLp p (α × β)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g h : WithLp ∞ (α × β)), edist f h ≤ edist f g + edist g h
inr : ∀ (hp : 1 ≤ p.toReal), edist f h ≤ edist f g + edist g h
⊢ edist f h ≤ edist f g + edist g h

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

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

Tactic:
sup_le ((edist_triangle _ g.fst _).trans <| add_le_add le_sup_left le_sup_left)
        ((edist_triangle _ g.snd _).trans <| add_le_add le_sup_right le_sup_right)

Premises used: le_sup_left, add_le_add, le_sup_right, WithLp.snd, WithLp.fst, sup_le, LE.le.trans, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g h : WithLp ∞ (α × β)
⊢ max (edist f.fst h.fst) (edist f.snd h.snd) ≤
    max (edist f.fst g.fst) (edist f.snd g.snd) + max (edist g.fst h.fst) (edist g.snd h.snd)

Tactic:
exact sup_le ((edist_triangle _ g.fst _).trans <| add_le_add le_sup_left le_sup_left)
        ((edist_triangle _ g.snd _).trans <| add_le_add le_sup_right le_sup_right)

Premises used: le_sup_left, add_le_add, le_sup_right, WithLp.snd, WithLp.fst, sup_le, LE.le.trans, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
inr :
  (edist f.fst h.fst ^ p.toReal + edist f.snd h.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    (edist f.fst g.fst ^ p.toReal + edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal) +
      (edist g.fst h.fst ^ p.toReal + edist g.snd h.snd ^ p.toReal) ^ (1 / p.toReal)
⊢ edist f h ≤ edist f g + edist g h

Tactic:
simp only [prod_edist_eq_add (zero_lt_one.trans_le hp)]

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_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
h₁ : edist f.fst h.fst ≤ edist f.fst g.fst + edist g.fst h.fst
h₂ : edist f.snd h.snd ≤ edist f.snd g.snd + edist g.snd h.snd
⊢ (edist f.fst h.fst ^ p.toReal + edist f.snd h.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    ((edist f.fst g.fst + edist g.fst h.fst) ^ p.toReal + (edist f.snd g.snd + edist g.snd h.snd) ^ p.toReal) ^
      (1 / p.toReal)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ edist f.fst h.fst ≤ edist f.fst g.fst + edist g.fst h.fst

Tactic:
apply edist_triangle

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ edist f.snd h.snd ≤ edist f.snd g.snd + edist g.snd h.snd

Tactic:
apply edist_triangle

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ HPow.hPow (α := ℝ≥0∞)
      (∑ i ∈ {0, 1},
        HAdd.hAdd (α := ℝ≥0∞) ((fun (x : ℕ) ↦ if x = 0 then edist f.fst g.fst else edist f.snd g.snd) i)
            ((fun (x : ℕ) ↦ if x = 0 then edist g.fst h.fst else edist g.snd h.snd) i) ^
          p.toReal)
      (1 / p.toReal) ≤
    HPow.hPow (α := ℝ≥0∞)
        (∑ i ∈ {0, 1},
          HPow.hPow (α := ℝ≥0∞) ((fun (x : ℕ) ↦ if x = 0 then edist f.fst g.fst else edist f.snd g.snd) i) p.toReal)
        (1 / p.toReal) +
      HPow.hPow (α := ℝ≥0∞)
        (∑ i ∈ {0, 1},
          HPow.hPow (α := ℝ≥0∞) ((fun (x : ℕ) ↦ if x = 0 then edist g.fst h.fst else edist g.snd h.snd) i) p.toReal)
        (1 / p.toReal)

Tactic:
have := ENNReal.Lp_add_le {0, 1}
            (if · = 0 then edist f.fst g.fst else edist f.snd g.snd)
            (if · = 0 then edist g.fst h.fst else edist g.snd h.snd) hp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
this :
  HPow.hPow (α := ℝ≥0∞)
      (∑ i ∈ {0, 1},
        HAdd.hAdd (α := ℝ≥0∞) ((fun (x : ℕ) ↦ if x = 0 then edist f.fst g.fst else edist f.snd g.snd) i)
            ((fun (x : ℕ) ↦ if x = 0 then edist g.fst h.fst else edist g.snd h.snd) i) ^
          p.toReal)
      (1 / p.toReal) ≤
    HPow.hPow (α := ℝ≥0∞)
        (∑ i ∈ {0, 1},
          HPow.hPow (α := ℝ≥0∞) ((fun (x : ℕ) ↦ if x = 0 then edist f.fst g.fst else edist f.snd g.snd) i) p.toReal)
        (1 / p.toReal) +
      HPow.hPow (α := ℝ≥0∞)
        (∑ i ∈ {0, 1},
          HPow.hPow (α := ℝ≥0∞) ((fun (x : ℕ) ↦ if x = 0 then edist g.fst h.fst else edist g.snd h.snd) i) p.toReal)
        (1 / p.toReal)
⊢ (((if True then edist f.fst g.fst else edist f.snd g.snd) + if True then edist g.fst h.fst else edist g.snd h.snd) ^
          p.toReal +
        ((if False then edist f.fst g.fst else edist f.snd g.snd) +
            if False then edist g.fst h.fst else edist g.snd h.snd) ^
          p.toReal) ^
      (1 / p.toReal) ≤
    ((if True then edist f.fst g.fst else edist f.snd g.snd) ^ p.toReal +
          (if False then edist f.fst g.fst else edist f.snd g.snd) ^ p.toReal) ^
        (1 / p.toReal) +
      ((if True then edist g.fst h.fst else edist g.snd h.snd) ^ p.toReal +
          (if False then edist g.fst h.fst else edist g.snd h.snd) ^ p.toReal) ^
        (1 / p.toReal)

Tactic:
simp only [Finset.mem_singleton, not_false_eq_true, Finset.sum_insert,
            Finset.sum_singleton, reduceCtorEq] at this

Premises used: reduceCtorEq, Finset.mem_singleton, Finset.sum_singleton, Finset.sum_insert, not_false_eq_true
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
this :
  (((if True then edist f.fst g.fst else edist f.snd g.snd) + if True then edist g.fst h.fst else edist g.snd h.snd) ^
          p.toReal +
        ((if False then edist f.fst g.fst else edist f.snd g.snd) +
            if False then edist g.fst h.fst else edist g.snd h.snd) ^
          p.toReal) ^
      (1 / p.toReal) ≤
    ((if True then edist f.fst g.fst else edist f.snd g.snd) ^ p.toReal +
          (if False then edist f.fst g.fst else edist f.snd g.snd) ^ p.toReal) ^
        (1 / p.toReal) +
      ((if True then edist g.fst h.fst else edist g.snd h.snd) ^ p.toReal +
          (if False then edist g.fst h.fst else edist g.snd h.snd) ^ p.toReal) ^
        (1 / p.toReal)
⊢ ((edist f.fst g.fst + edist g.fst h.fst) ^ p.toReal + (edist f.snd g.snd + edist g.snd h.snd) ^ p.toReal) ^
      (1 / p.toReal) ≤
    (edist f.fst g.fst ^ p.toReal + edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal) +
      (edist g.fst h.fst ^ p.toReal + edist g.snd h.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
this

Premises used: ite
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
this :
  (((if True then edist f.fst g.fst else edist f.snd g.snd) + if True then edist g.fst h.fst else edist g.snd h.snd) ^
          p.toReal +
        ((if False then edist f.fst g.fst else edist f.snd g.snd) +
            if False then edist g.fst h.fst else edist g.snd h.snd) ^
          p.toReal) ^
      (1 / p.toReal) ≤
    ((if True then edist f.fst g.fst else edist f.snd g.snd) ^ p.toReal +
          (if False then edist f.fst g.fst else edist f.snd g.snd) ^ p.toReal) ^
        (1 / p.toReal) +
      ((if True then edist g.fst h.fst else edist g.snd h.snd) ^ p.toReal +
          (if False then edist g.fst h.fst else edist g.snd h.snd) ^ p.toReal) ^
        (1 / p.toReal)
⊢ ((edist f.fst g.fst + edist g.fst h.fst) ^ p.toReal + (edist f.snd g.snd + edist g.snd h.snd) ^ p.toReal) ^
      (1 / p.toReal) ≤
    (edist f.fst g.fst ^ p.toReal + edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal) +
      (edist g.fst h.fst ^ p.toReal + edist g.snd h.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
exact this
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
edist :
  (EDist.edist f.fst h.fst ^ p.toReal + EDist.edist f.snd h.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    ((EDist.edist f.fst g.fst + EDist.edist g.fst h.fst) ^ p.toReal +
        (EDist.edist f.snd g.snd + EDist.edist g.snd h.snd) ^ p.toReal) ^
      (1 / p.toReal)
edist₁ :
  ((EDist.edist f.fst g.fst + EDist.edist g.fst h.fst) ^ p.toReal +
        (EDist.edist f.snd g.snd + EDist.edist g.snd h.snd) ^ p.toReal) ^
      (1 / p.toReal) ≤
    (EDist.edist f.fst g.fst ^ p.toReal + EDist.edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal) +
      (EDist.edist g.fst h.fst ^ p.toReal + EDist.edist g.snd h.snd ^ p.toReal) ^ (1 / p.toReal)
⊢ (EDist.edist f.fst h.fst ^ p.toReal + EDist.edist f.snd h.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    (EDist.edist f.fst g.fst ^ p.toReal + EDist.edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal) +
      (EDist.edist g.fst h.fst ^ p.toReal + EDist.edist g.snd h.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
calc
        (edist f.fst h.fst ^ p.toReal + edist f.snd h.snd ^ p.toReal) ^ (1 / p.toReal) ≤
            ((edist f.fst g.fst + edist g.fst h.fst) ^ p.toReal +
              (edist f.snd g.snd + edist g.snd h.snd) ^ p.toReal) ^ (1 / p.toReal) := by
          gcongr <;> apply edist_triangle
        _ ≤
            (edist f.fst g.fst ^ p.toReal + edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal) +
              (edist g.fst h.fst ^ p.toReal + edist g.snd h.snd ^ p.toReal) ^ (1 / p.toReal) := by
          have := ENNReal.Lp_add_le {0, 1}
            (if · = 0 then edist f.fst g.fst else edist f.snd g.snd)
            (if · = 0 then edist g.fst h.fst else edist g.snd h.snd) hp
          simp only [Finset.mem_singleton, not_false_eq_true, Finset.sum_insert,
            Finset.sum_singleton, reduceCtorEq] at this
          exact this

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:
α : Type u_2
β : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f g : WithLp ∞ (α × β)
⊢ max (edist f.fst g.fst) (edist f.snd g.snd) < ∞

Tactic:
simp [edist, PseudoMetricSpace.edist_dist]

Premises used: EDist.edist, PseudoMetricSpace.edist_dist
-- 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 (α × β)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g : WithLp ∞ (α × β)), 0 ≤ dist f g
inr : ∀ (h : 1 ≤ p.toReal), 0 ≤ dist f g
⊢ 0 ≤ dist f g

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 : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : WithLp ∞ (α × β)
⊢ 0 ≤ dist f g

Tactic:
simp [prod_dist_eq_sup]

Premises used: WithLp.prod_dist_eq_sup
-- 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
inr :
  0 ≤
    if p = 0 then HAdd.hAdd (α := ℝ) (if dist f.fst g.fst = 0 then 0 else 1) (if dist f.snd g.snd = 0 then 0 else 1)
    else
      if p = ∞ then max (dist f.fst g.fst) (dist f.snd g.snd)
      else (dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ p.toReal⁻¹
⊢ 0 ≤ dist f g

Tactic:
simp only [dist, one_div, dite_eq_ite]

Premises used: one_div, Dist.dist, dite_eq_ite
-- 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
pos : ∀ (hp' : p = 0), dist f.fst g.fst = 0 → dist f.snd g.snd = 0 → 0 ≤ HAdd.hAdd (α := ℝ) 0 0
neg : ∀ (hp' : p = 0), dist f.fst g.fst = 0 → ¬dist f.snd g.snd = 0 → 0 ≤ HAdd.hAdd (α := ℝ) 0 1
pos₁ : ∀ (hp' : p = 0), ¬dist f.fst g.fst = 0 → dist f.snd g.snd = 0 → 0 ≤ HAdd.hAdd (α := ℝ) 1 0
neg₁ : ∀ (hp' : p = 0), ¬dist f.fst g.fst = 0 → ¬dist f.snd g.snd = 0 → 0 ≤ HAdd.hAdd (α := ℝ) 1 1
pos₂ : ∀ (hp' : ¬p = 0), p = ∞ → 0 ≤ max (dist f.fst g.fst) (dist f.snd g.snd)
neg₂ : ∀ (hp' : ¬p = 0), ¬p = ∞ → 0 ≤ (dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ p.toReal⁻¹
⊢ 0 ≤
    if p = 0 then HAdd.hAdd (α := ℝ) (if dist f.fst g.fst = 0 then 0 else 1) (if dist f.snd g.snd = 0 then 0 else 1)
    else
      if p = ∞ then max (dist f.fst g.fst) (dist f.snd g.snd)
      else (dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ p.toReal⁻¹

Tactic:
split_ifs with hp'
-- 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
hp' : p = 0
h_1 : dist f.fst g.fst = 0
h_2 : dist f.snd g.snd = 0
⊢ 0 ≤ HAdd.hAdd (α := ℝ) 0 0

Tactic:
positivity
-- 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
hp' : p = 0
h_1 : dist f.fst g.fst = 0
h_2 : ¬dist f.snd g.snd = 0
⊢ 0 ≤ HAdd.hAdd (α := ℝ) 0 1

Tactic:
positivity
-- 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
hp' : p = 0
h_1 : ¬dist f.fst g.fst = 0
h_2 : dist f.snd g.snd = 0
⊢ 0 ≤ HAdd.hAdd (α := ℝ) 1 0

Tactic:
positivity
-- 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
hp' : p = 0
h_1 : ¬dist f.fst g.fst = 0
h_2 : ¬dist f.snd g.snd = 0
⊢ 0 ≤ HAdd.hAdd (α := ℝ) 1 1

Tactic:
positivity
-- 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
hp' : ¬p = 0
h_1 : p = ∞
⊢ 0 ≤ max (dist f.fst g.fst) (dist f.snd g.snd)

Tactic:
positivity
-- 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
hp' : ¬p = 0
h_1 : ¬p = ∞
⊢ 0 ≤ (dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ p.toReal⁻¹

Tactic:
positivity
-- 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 (α × β)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g : WithLp ∞ (α × β)), edist f g = ENNReal.ofReal (dist f g)
inr : ∀ (h : 1 ≤ p.toReal), edist f g = ENNReal.ofReal (dist f g)
⊢ edist f g = ENNReal.ofReal (dist f g)

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 : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : WithLp ∞ (α × β)
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_

Premises used: ENNReal.eq_of_forall_le_nnreal_iff
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : WithLp ∞ (α × β)
inl : ∀ (r : ℝ≥0), edist f g ≤ (↑r : ℝ≥0∞) ↔ ENNReal.ofReal (dist f g) ≤ (↑r : ℝ≥0∞)
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_

Premises used: ENNReal.eq_of_forall_le_nnreal_iff
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : WithLp ∞ (α × β)
r : ℝ≥0
⊢ edist f g ≤ (↑r : ℝ≥0∞) ↔ ENNReal.ofReal (dist f g) ≤ (↑r : ℝ≥0∞)

Tactic:
simp [prod_edist_eq_sup, prod_dist_eq_sup]

Premises used: WithLp.prod_edist_eq_sup, WithLp.prod_dist_eq_sup
-- 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
rw : p ≠ ∞
⊢ 0 < p.toReal

Tactic:
rw [ENNReal.toReal_pos_iff_ne_top]

Premises used: ENNReal.toReal_pos_iff_ne_top
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : WithLp ∞ (α × β)
h : 1 ≤ ENNReal.toReal ∞
⊢ False

Tactic:
norm_num at h
-- 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
⊢ 0 < p.toReal

Tactic:
have : 0 < p.toReal := by rw [ENNReal.toReal_pos_iff_ne_top]; rintro rfl; norm_num at h