-- 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 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)

Tactic:
have pos : 0 < p.toReal := 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
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)

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
⊢ ↑(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:
have : (Fintype.card ι : ℝ≥0∞) = (Fintype.card ι : ℝ≥0) :=
  (ENNReal.coe_natCast (Fintype.card ι)).symm

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)
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)

Proof state:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
⊢ AntilipschitzWith (↑(Fintype.card ι) ^ (1 / p).toReal) ⇑(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 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
⊢ (∑ i : ι, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) ≤
    (∑ _i : ?m.87346, edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) y) ^ p.toReal) ^
      (1 / p.toReal)

Tactic:
gcongr with i

Result:
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)

Proof state:
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)

Tactic:
simp only [edist_eq_iSup, ENNReal.div_top, ENNReal.zero_toReal, NNReal.rpow_zero,
  ENNReal.coe_one, one_mul, iSup_le_iff]

Result:
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)

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

Tactic:
simp only [nsmul_eq_mul, Finset.card_univ, ENNReal.rpow_one, Finset.sum_const,
  ENNReal.mul_rpow_of_nonneg _ _ nonneg, ← ENNReal.rpow_mul, cancel]

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)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ ↑(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)