-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_lipschitzWith_equiv_aux [PseudoEMetricSpace α] [PseudoEMetricSpace β] :
    LipschitzWith 1 (WithLp.equiv p (α × β))

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.1 y.1 ≤ (edist x.1 y.1 ^ p.toReal) ^ (1 / p.toReal)

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

Result:
no goals

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.2 y.2 ≤ (edist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal)

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

Result:
no goals

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
⊢ LipschitzWith 1 ⇑(WithLp.equiv p (α × β))

Tactic:
intro x y

Result:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
⊢ edist ((WithLp.equiv p (α × β)) x) ((WithLp.equiv p (α × β)) y) ≤ ↑1 * edist x y

Proof state:
case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ edist ((WithLp.equiv p (α × β)) x) ((WithLp.equiv p (α × β)) y) ≤ ↑1 * edist x y

Tactic:
have cancel : p.toReal * (1 / p.toReal) = 1 := mul_div_cancel₀ 1 (zero_lt_one.trans_le h).ne'

Result:
case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist ((WithLp.equiv p (α × β)) x) ((WithLp.equiv p (α × β)) y) ≤ ↑1 * edist x y

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (edist x.1 y.1 ^ p.toReal) ^ (1 / p.toReal) ≤ (edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal)

Tactic:
gcongr

Result:
case h₁
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.1 y.1 ^ p.toReal ≤ edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ p.toReal

Proof state:
case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist ((WithLp.equiv p (α × β)) x).1 ((WithLp.equiv p (α × β)) y).1 ≤
      (edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal) ∧
    edist ((WithLp.equiv p (α × β)) x).2 ((WithLp.equiv p (α × β)) y).2 ≤
      (edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal)

Tactic:
constructor

Result:
case inr.left
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist ((WithLp.equiv p (α × β)) x).1 ((WithLp.equiv p (α × β)) y).1 ≤
    (edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal)

case inr.right
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist ((WithLp.equiv p (α × β)) x).2 ((WithLp.equiv p (α × β)) y).2 ≤
    (edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal)

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
⊢ edist ((WithLp.equiv p (α × β)) x) ((WithLp.equiv p (α × β)) y) ≤ ↑1 * edist x y

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

Result:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
hp : Fact (1 ≤ ⊤)
x y : WithLp ⊤ (α × β)
⊢ edist ((WithLp.equiv ⊤ (α × β)) x) ((WithLp.equiv ⊤ (α × β)) y) ≤ ↑1 * edist x y

case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ edist ((WithLp.equiv p (α × β)) x) ((WithLp.equiv p (α × β)) y) ≤ ↑1 * edist x y

Proof state:
case inr.right
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist ((WithLp.equiv p (α × β)) x).2 ((WithLp.equiv p (α × β)) y).2 ≤
    (edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ 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]

Result:
no goals

Proof state:
case inr.left
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist ((WithLp.equiv p (α × β)) x).1 ((WithLp.equiv p (α × β)) y).1 ≤
    (edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ 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]

Result:
no goals

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (edist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal) ≤ (edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal)

Tactic:
gcongr

Result:
case h₁
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.2 y.2 ^ p.toReal ≤ edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ p.toReal

Proof state:
case h₁
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.2 y.2 ^ p.toReal ≤ edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ p.toReal

Tactic:
simp only [self_le_add_left]

Result:
no goals

Proof state:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
hp : Fact (1 ≤ ⊤)
x y : WithLp ⊤ (α × β)
⊢ edist ((WithLp.equiv ⊤ (α × β)) x) ((WithLp.equiv ⊤ (α × β)) y) ≤ ↑1 * edist x y

Tactic:
simp [edist]

Result:
no goals

Proof state:
case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist ((WithLp.equiv p (α × β)) x) ((WithLp.equiv p (α × β)) y) ≤ ↑1 * edist x y

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

Result:
case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist ((WithLp.equiv p (α × β)) x) ((WithLp.equiv p (α × β)) y) ≤
    ↑1 * (edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal)