-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem antilipschitzWith_equiv_aux :
    AntilipschitzWith ((Fintype.card ι : ℝ≥0) ^ (1 / p).toReal) (WithLp.equiv p (∀ i, β i))

Proof state:
case h₁.h.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
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
i : ι
a✝ : i ∈ Finset.univ
⊢ edist (x i) (y i) ≤ edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) y)

Tactic:
exact Finset.le_sup (f := fun i => edist (x i) (y i)) (Finset.mem_univ 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
pos : 0 < p.toReal
⊢ edist x y ≤
    ↑(↑(Fintype.card ι) ^ (1 / p).toReal) *
      edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) y)

Tactic:
have nonneg : 0 ≤ 1 / p.toReal := one_div_nonneg.2 (le_of_lt pos)

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
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
⊢ edist x y ≤
    ↑(↑(Fintype.card ι) ^ (1 / p).toReal) *
      edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) 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
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
this : ↑(Fintype.card ι) = ↑↑(Fintype.card ι)
⊢ ↑(Fintype.card ι) ^ (1 / p.toReal) * edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) y) =
    ↑(↑(Fintype.card ι) ^ (1 / p.toReal)) *
      edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) y)

Tactic:
rw [this, ENNReal.coe_rpow_of_nonneg _ nonneg]

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
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x y ≤
    ↑(↑(Fintype.card ι) ^ (1 / p).toReal) *
      edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) y)

Tactic:
rw [edist_eq_sum pos, ENNReal.toReal_div 1 p]

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
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (∑ i : ι, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) ≤
    ↑(↑(Fintype.card ι) ^ (ENNReal.toReal 1 / p.toReal)) *
      edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) 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
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (∑ i : ι, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) ≤
    ↑(↑(Fintype.card ι) ^ (ENNReal.toReal 1 / p.toReal)) *
      edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) y)

Tactic:
simp only [edist, ← one_div, ENNReal.one_toReal]

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
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (∑ i : ι, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) ≤
    ↑(↑(Fintype.card ι) ^ (1 / p.toReal)) *
      Finset.univ.sup fun b => edist ((WithLp.equiv p ((i : ι) → β i)) x b) ((WithLp.equiv p ((i : ι) → β i)) y b)

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
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
⊢ edist x y ≤
    ↑(↑(Fintype.card ι) ^ (1 / p).toReal) *
      edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) y)

Tactic:
have cancel : p.toReal * (1 / p.toReal) = 1 := mul_div_cancel₀ 1 (ne_of_gt pos)

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
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x y ≤
    ↑(↑(Fintype.card ι) ^ (1 / p).toReal) *
      edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) 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
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (∑ i : ι, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) ≤
    ↑(↑(Fintype.card ι) ^ (1 / p.toReal)) *
      Finset.univ.sup fun b => edist ((WithLp.equiv p ((i : ι) → β i)) x b) ((WithLp.equiv p ((i : ι) → β i)) y b)

Tactic:
calc
  (∑ i, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) ≤
      (∑ _i, edist (WithLp.equiv p _ x) (WithLp.equiv p _ y) ^ p.toReal) ^ (1 / p.toReal) := by
    gcongr with i
    exact Finset.le_sup (f := fun i => edist (x i) (y i)) (Finset.mem_univ i)
  _ =
      ((Fintype.card ι : ℝ≥0) ^ (1 / p.toReal) : ℝ≥0) *
        edist (WithLp.equiv p _ x) (WithLp.equiv p _ y) := by
    simp only [nsmul_eq_mul, Finset.card_univ, ENNReal.rpow_one, Finset.sum_const,
      ENNReal.mul_rpow_of_nonneg _ _ nonneg, ← ENNReal.rpow_mul, cancel]
    have : (Fintype.card ι : ℝ≥0∞) = (Fintype.card ι : ℝ≥0) :=
      (ENNReal.coe_natCast (Fintype.card ι)).symm
    rw [this, ENNReal.coe_rpow_of_nonneg _ nonneg]

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)
⊢ ∀ (i : ι), edist (x i) (y i) ≤ edist ((WithLp.equiv ⊤ ((i : ι) → β i)) x) ((WithLp.equiv ⊤ ((i : ι) → β i)) y)

Tactic:
exact fun i => Finset.le_sup (f := fun i => edist (x i) (y i)) (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)
⊢ edist x y ≤
    ↑(↑(Fintype.card ι) ^ (1 / p).toReal) *
      edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) 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)
⊢ edist x y ≤
    ↑(↑(Fintype.card ι) ^ (1 / ⊤).toReal) *
      edist ((WithLp.equiv ⊤ ((i : ι) → β i)) x) ((WithLp.equiv ⊤ ((i : ι) → β i)) 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
⊢ edist x y ≤
    ↑(↑(Fintype.card ι) ^ (1 / p).toReal) *
      edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) y)