-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem lipschitzWith_equiv_aux : LipschitzWith 1 (WithLp.equiv p (∀ i, β i))

Proof state:
case inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ ∀ (b : ι), edist (x b) (y b) ≤ edist x y

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

Result:
case inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ ∀ (b : ι), edist (x b) (y b) ≤ (∑ i : ι, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal)

Proof state:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
⊢ edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) y) ≤ ↑1 * edist x y

Tactic:
simp_rw [ENNReal.coe_one, one_mul, edist_pi_def, Finset.sup_le_iff, Finset.mem_univ,
  forall_true_left, WithLp.equiv_pi_apply]

Result:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
⊢ ∀ (b : ι), edist (x b) (y b) ≤ edist x y

Proof state:
case inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
⊢ ∀ (b : ι), edist (x b) (y b) ≤ 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_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ ∀ (b : ι), edist (x b) (y b) ≤ edist x y

Proof state:
case h₁
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
i : ι
⊢ edist (x i) (y i) ^ p.toReal ≤ ∑ i : ι, edist (x i) (y i) ^ p.toReal

Tactic:
exact Finset.single_le_sum (fun i _ => (bot_le : (0 : ℝ≥0∞) ≤ _)) (Finset.mem_univ i)

Result:
no goals

Proof state:
case inl
ι : Type u_2
β : ι → Type u_4
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
x y : WithLp ⊤ ((i : ι) → β i)
⊢ ∀ (b : ι), edist (x b) (y b) ≤ edist x y

Tactic:
simpa only [edist_eq_iSup] using le_iSup fun i => edist (x i) (y i)

Result:
no goals

Proof state:
case inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
i : ι
⊢ edist (x i) (y i) ≤ (∑ i : ι, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal)

Tactic:
calc
  edist (x i) (y i) = (edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) := by
    simp [← ENNReal.rpow_mul, cancel, -one_div]
  _ ≤ (∑ i, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) := by
    gcongr
    exact Finset.single_le_sum (fun i _ => (bot_le : (0 : ℝ≥0∞) ≤ _)) (Finset.mem_univ i)

Result:
no goals

Proof state:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
i : ι
⊢ (edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) ≤ (∑ i : ι, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal)

Tactic:
gcongr

Result:
case h₁
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
i : ι
⊢ edist (x i) (y i) ^ p.toReal ≤ ∑ i : ι, edist (x i) (y i) ^ p.toReal

Proof state:
case inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ ∀ (b : ι), edist (x b) (y b) ≤ (∑ i : ι, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal)

Tactic:
intro i

Result:
case inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
i : ι
⊢ edist (x i) (y i) ≤ (∑ i : ι, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal)

Proof state:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
⊢ LipschitzWith 1 ⇑(WithLp.equiv p ((i : ι) → β i))

Tactic:
intro x y

Result:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
⊢ edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) y) ≤ ↑1 * edist x y

Proof state:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
i : ι
⊢ edist (x i) (y i) = (edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal)

Tactic:
simp [← ENNReal.rpow_mul, cancel, -one_div]

Result:
no goals

Proof state:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
⊢ ∀ (b : ι), edist (x b) (y b) ≤ edist x y

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

Result:
case inl
ι : Type u_2
β : ι → Type u_4
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
x y : WithLp ⊤ ((i : ι) → β i)
⊢ ∀ (b : ι), edist (x b) (y b) ≤ edist x y

case inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
⊢ ∀ (b : ι), edist (x b) (y b) ≤ edist x y