awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : WithLp p (α × β)
⊢ edist f f = 0
have inl : ∀ (f : WithLp 0 (α × β)), edist f f = 0
Tactic: rcases p.trichotomy with (rfl | rfl | h)
Cleared hypotheses: p, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : WithLp p (α × β)
inl : ∀ (f : WithLp 0 (α × β)), edist f f = 0
⊢ edist f f = 0
have inr : ∀ (f : WithLp ∞ (α × β)), edist f f = 0
Tactic: rcases p.trichotomy with (rfl | rfl | h)
Cleared hypotheses: p, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : WithLp p (α × β)
inl : ∀ (f : WithLp 0 (α × β)), edist f f = 0
inr : ∀ (f : WithLp ∞ (α × β)), edist f f = 0
⊢ edist f f = 0
have inr₁ : ∀ (h : 0 < p.toReal), edist f f = 0
Tactic: rcases p.trichotomy with (rfl | rfl | h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g : WithLp p (α × β)
⊢ edist f g = edist g f
have inl : ∀ (f g : WithLp 0 (α × β)), edist f g = edist g f
Tactic: rcases p.trichotomy with (rfl | rfl | h)
Cleared hypotheses: p, f, g
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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
⊢ edist f g = edist g f
have inr : ∀ (f g : WithLp ∞ (α × β)), edist f g = edist g f
Tactic: rcases p.trichotomy with (rfl | rfl | h)
Cleared hypotheses: p, f, g
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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
⊢ edist f g = edist g f
have inr₁ : ∀ (h : 0 < p.toReal), edist f g = edist g f
Tactic: rcases p.trichotomy with (rfl | rfl | h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g : WithLp p (α × β)
⊢ edist f g = edist g f
have inl : ∀ (f g : WithLp 0 (α × β)), 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]
Cleared hypotheses: p, f, g
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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
⊢ edist f g = edist g f
have inr : ∀ (f g : WithLp ∞ (α × β)), 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]
Cleared hypotheses: p, f, g
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
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
⊢ edist f g = edist g f
have inr₁ : ∀ (h : 0 < p.toReal), 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]
-- 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 : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g h : WithLp p (α × β)
⊢ edist f h ≤ edist f g + edist g h
have inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g h : WithLp ∞ (α × β)), edist f h ≤ edist f g + edist g h
Tactic: rcases p.dichotomy with (rfl | hp)
Cleared hypotheses: p, hp, f, g, h
-- 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 : 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
⊢ edist f h ≤ edist f g + edist g h
have inr : ∀ (hp : 1 ≤ p.toReal), edist f h ≤ edist f g + edist g h
Tactic: rcases p.dichotomy with (rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ edist f h ≤ edist f g + edist g h
have 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)
Tactic: simp only [prod_edist_eq_add (zero_lt_one.trans_le hp)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ (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)
have h₁ : edist f.fst h.fst ≤ edist f.fst g.fst + edist g.fst h.fst
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : 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
⊢ (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)
have h₂ : edist f.snd h.snd ≤ edist f.snd g.snd + edist g.snd h.snd
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (hypothesis)
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 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)
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (hypothesis)
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)
⊢ ((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)
have 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)
Tactic: simp only [Finset.mem_singleton, not_false_eq_true, Finset.sum_insert,
            Finset.sum_singleton, reduceCtorEq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ (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)
have edist : (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: 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp_1 : Fact (1 ≤ p)
inst : 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 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)
have 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)
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
-- 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 (α × β)
⊢ 0 ≤ dist f g
have inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g : WithLp ∞ (α × β)), 0 ≤ dist f g
Tactic: rcases p.dichotomy with (rfl | h)
Cleared hypotheses: p, hp, f, g
-- 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 (α × β)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g : WithLp ∞ (α × β)), 0 ≤ dist f g
⊢ 0 ≤ dist f g
have inr : ∀ (h : 1 ≤ p.toReal), 0 ≤ dist f g
Tactic: rcases p.dichotomy with (rfl | h)
-- 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
⊢ 0 ≤ dist f g
have 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⁻¹
Tactic: simp only [dist, one_div, dite_eq_ite]
-- 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
⊢ 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⁻¹
have pos : ∀ (hp' : p = 0), dist f.fst g.fst = 0 → dist f.snd g.snd = 0 → 0 ≤ HAdd.hAdd (α := ℝ) 0 0
Tactic: split_ifs with hp'
-- 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
pos : ∀ (hp' : p = 0), dist f.fst g.fst = 0 → dist f.snd g.snd = 0 → 0 ≤ HAdd.hAdd (α := ℝ) 0 0
⊢ 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⁻¹
have neg : ∀ (hp' : p = 0), dist f.fst g.fst = 0 → ¬dist f.snd g.snd = 0 → 0 ≤ HAdd.hAdd (α := ℝ) 0 1
Tactic: split_ifs with hp'
-- 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
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
⊢ 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⁻¹
have pos₁ : ∀ (hp' : p = 0), ¬dist f.fst g.fst = 0 → dist f.snd g.snd = 0 → 0 ≤ HAdd.hAdd (α := ℝ) 1 0
Tactic: split_ifs with hp'
-- 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
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
⊢ 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⁻¹
have neg₁ : ∀ (hp' : p = 0), ¬dist f.fst g.fst = 0 → ¬dist f.snd g.snd = 0 → 0 ≤ HAdd.hAdd (α := ℝ) 1 1
Tactic: split_ifs with hp'
-- 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
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
⊢ 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⁻¹
have pos₂ : ∀ (hp' : ¬p = 0), p = ∞ → 0 ≤ max (dist f.fst g.fst) (dist f.snd g.snd)
Tactic: split_ifs with hp'
-- 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
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)
⊢ 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⁻¹
have neg₂ : ∀ (hp' : ¬p = 0), ¬p = ∞ → 0 ≤ (dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ p.toReal⁻¹
Tactic: split_ifs with hp'
-- 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 (α × β)
⊢ edist f g = ENNReal.ofReal (dist f g)
have inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g : WithLp ∞ (α × β)), edist f g = ENNReal.ofReal (dist f g)
Tactic: rcases p.dichotomy with (rfl | h)
Cleared hypotheses: p, hp, f, g
-- 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 (α × β)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g : WithLp ∞ (α × β)), edist f g = ENNReal.ofReal (dist f g)
⊢ edist f g = ENNReal.ofReal (dist f g)
have inr : ∀ (h : 1 ≤ p.toReal), edist f g = ENNReal.ofReal (dist f g)
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 : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : WithLp ∞ (α × β)
⊢ edist f g = ENNReal.ofReal (dist f g)
have inl : ∀ (r : ℝ≥0), edist f g ≤ (↑r : ℝ≥0∞) ↔ ENNReal.ofReal (dist f g) ≤ (↑r : ℝ≥0∞)
Tactic: refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_
-- 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
⊢ 0 < p.toReal
have rw : p ≠ ∞
Tactic: rw [ENNReal.toReal_pos_iff_ne_top]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (hypothesis)
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
⊢ edist f g = ENNReal.ofReal (dist f g)
have this : 0 < p.toReal
Tactic: have : 0 < p.toReal := by rw [ENNReal.toReal_pos_iff_ne_top]; rintro rfl; norm_num at h
-- 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
⊢ edist f g = ENNReal.ofReal (dist f g)
have 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⁻¹)
Tactic: simp only [prod_edist_eq_add, edist_dist, one_div, prod_dist_eq_add, this]
-- 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
⊢ (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
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
⊢ (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]