awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
pos : ∀ (hp : p = 0), LE.le (α := ℝ) 0 (↑(Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) ⋯).card : ℝ)
⊢ 0 ≤
    if p = 0 then (↑(Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) ⋯).card : ℝ)
    else
      if p = ∞ then ⨆ (i : ι), dist (f.ofLp i) (g.ofLp i)
      else HPow.hPow (α := ℝ) (∑ i : ι, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) (1 / p.toReal)
have pos₁ : ∀ (hp : ¬p = 0), p = ∞ → LE.le (α := ℝ) 0 (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))
Tactic: split_ifs with hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
pos : ∀ (hp : p = 0), LE.le (α := ℝ) 0 (↑(Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) ⋯).card : ℝ)
pos₁ : ∀ (hp : ¬p = 0), p = ∞ → LE.le (α := ℝ) 0 (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))
⊢ 0 ≤
    if p = 0 then (↑(Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) ⋯).card : ℝ)
    else
      if p = ∞ then ⨆ (i : ι), dist (f.ofLp i) (g.ofLp i)
      else HPow.hPow (α := ℝ) (∑ i : ι, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) (1 / p.toReal)
have neg : ∀ (hp : ¬p = 0), ¬p = ∞ → 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) (1 / p.toReal)
Tactic: split_ifs with hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
hp : p = 0
⊢ LE.le (α := ℝ) 0 (↑(Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) ⋯).card : ℝ)
have linarith : LT.lt (α := ℝ) (↑(Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) sorry).card : ℝ) 0 →
  HSub.hSub (α := ℝ) 0 (↑(Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) sorry).card : ℝ) +
      HSub.hSub (α := ℝ) (↑(Finite.toFinset (s := {i : ι | dist (f.ofLp i) (g.ofLp i) ≠ 0}) sorry).card : ℝ) 0 =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
⊢ edist f g = ENNReal.ofReal (dist f g)
have inl : ∀ [inst : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g : PiLp ∞ α), edist f g = ENNReal.ofReal (dist f g)
Tactic: rcases p.dichotomy with (rfl | h)
Cleared hypotheses: p, inst, f, g
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
inl : ∀ [inst : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g : PiLp ∞ α), 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.PiLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : PiLp ∞ α
⊢ edist f g = ENNReal.ofReal (dist f g)
have inl : ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))
Tactic: rw [edist_eq_iSup, dist_eq_iSup]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : PiLp ∞ α
⊢ ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))
have inl : IsEmpty ι → ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : PiLp ∞ α
inl : IsEmpty ι → ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))
⊢ ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))
have inl₁ : Nonempty ι → ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : PiLp ∞ α
h : Nonempty ι
⊢ ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i))
have inl : ∀ (r : ℝ≥0),
  ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) ≤ (↑r : ℝ≥0∞) ↔
    ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i)) ≤ (↑r : ℝ≥0∞)
Tactic: refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : PiLp ∞ α
h : Nonempty ι
r : ℝ≥0
⊢ ⨆ (i : ι), edist (f.ofLp i) (g.ofLp i) ≤ (↑r : ℝ≥0∞) ↔
    ENNReal.ofReal (⨆ (i : ι), dist (f.ofLp i) (g.ofLp i)) ≤ (↑r : ℝ≥0∞)
have this : BddAbove (α := ℝ) (range fun (i : ι) ↦ dist (f.ofLp i) (g.ofLp i))
Tactic: have : BddAbove <| .range fun i ↦ dist (f i) (g i) := Finite.bddAbove_range _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp 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.PiLp (hypothesis)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp 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.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ edist f g = ENNReal.ofReal (dist f g)
have inr : HPow.hPow (α := ℝ≥0∞) (∑ x : ι, ENNReal.ofReal (dist (f.ofLp x) (g.ofLp x)) ^ p.toReal) (1 / p.toReal) =
  ENNReal.ofReal (HPow.hPow (α := ℝ) (∑ i : ι, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) (1 / p.toReal))
Tactic: simp only [edist_eq_sum, edist_dist, dist_eq_sum, this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ HPow.hPow (α := ℝ≥0∞) (∑ x : ι, ENNReal.ofReal (dist (f.ofLp x) (g.ofLp x)) ^ p.toReal) (1 / p.toReal) =
    ENNReal.ofReal (HPow.hPow (α := ℝ) (∑ i : ι, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) (1 / p.toReal))
have inr : HPow.hPow (α := ℝ≥0∞) (∑ x : ι, ENNReal.ofReal (dist (f.ofLp x) (g.ofLp x)) ^ p.toReal) (1 / p.toReal) =
  ENNReal.ofReal (∑ i : ι, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) ^ (1 / p.toReal)
Tactic: rw [← ENNReal.ofReal_rpow_of_nonneg (by simp [Finset.sum_nonneg, Real.rpow_nonneg]) (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : PiLp p β
i : ι
⊢ edist (x.ofLp i) (y.ofLp i) ≤ edist x y
have inl : ∀ [Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : PiLp ∞ β), edist (x.ofLp i) (y.ofLp i) ≤ edist x y
Tactic: rcases p.dichotomy with (rfl | h)
Cleared hypotheses: p, inst, x, y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : PiLp p β
i : ι
inl : ∀ [Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : PiLp ∞ β), edist (x.ofLp i) (y.ofLp i) ≤ edist x y
⊢ edist (x.ofLp i) (y.ofLp i) ≤ edist x y
have inr : ∀ (h : 1 ≤ p.toReal), edist (x.ofLp i) (y.ofLp i) ≤ edist x y
Tactic: rcases p.dichotomy with (rfl | h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : PiLp p β
i : ι
h : 1 ≤ p.toReal
⊢ edist (x.ofLp i) (y.ofLp i) ≤ edist x y
have cancel : p.toReal * (1 / p.toReal) = 1
Tactic: have cancel : p.toReal * (1 / p.toReal) = 1 := mul_div_cancel₀ 1 (zero_lt_one.trans_le h).ne'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : PiLp p β
i : ι
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist (x.ofLp i) (y.ofLp i) ≤ edist x y
have inr : edist (x.ofLp i) (y.ofLp i) ≤ HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal)
Tactic: rw [edist_eq_sum (zero_lt_one.trans_le h)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : PiLp p β
i : ι
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (edist (x.ofLp i) (y.ofLp i) ^ p.toReal) ^ (1 / p.toReal) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal)
have h₁ : edist (x.ofLp i) (y.ofLp i) ^ p.toReal ≤ ∑ i : ι, edist (x.ofLp i) (y.ofLp i) ^ p.toReal
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : PiLp p β
i : ι
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist (x.ofLp i) (y.ofLp i) ≤ HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal)
have edist : edist (x.ofLp i) (y.ofLp i) = (edist (x.ofLp i) (y.ofLp 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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : PiLp p β
i : ι
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
edist : EDist.edist (x.ofLp i) (y.ofLp i) = (EDist.edist (x.ofLp i) (y.ofLp i) ^ p.toReal) ^ (1 / p.toReal)
⊢ EDist.edist (x.ofLp i) (y.ofLp i) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i : ι, EDist.edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal)
have edist₁ : (EDist.edist (x.ofLp i) (y.ofLp i) ^ p.toReal) ^ (1 / p.toReal) ≤
  HPow.hPow (α := ℝ≥0∞) (∑ i : ι, EDist.edist (x.ofLp i) (y.ofLp 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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
⊢ edist x.ofLp y.ofLp ≤ edist x y
have simp_rw : ∀ (b : ι), edist (x.ofLp b) (y.ofLp b) ≤ edist x y
Tactic: simp_rw [edist_pi_def, Finset.sup_le_iff, Finset.mem_univ, forall_true_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
⊢ edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
have inl : ∀ [inst : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : WithLp ∞ ((i : ι) → β i)),
  edist x y ≤
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (HDiv.hDiv (α := ℝ≥0∞) 1 ∞).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
Tactic: rcases p.dichotomy with (rfl | h)
Cleared hypotheses: p, inst, x, y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
inl :
  ∀ [inst : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : WithLp ∞ ((i : ι) → β i)),
    edist x y ≤
      (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (HDiv.hDiv (α := ℝ≥0∞) 1 ∞).toReal) : ℝ≥0∞) *
        edist x.ofLp y.ofLp
⊢ edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
have inr : ∀ (h : 1 ≤ p.toReal),
  edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
Tactic: rcases p.dichotomy with (rfl | h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → PseudoEMetricSpace (β i)
inst_1 : Fintype ι
inst_2 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
x y : WithLp ∞ ((i : ι) → β i)
⊢ edist x y ≤
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (HDiv.hDiv (α := ℝ≥0∞) 1 ∞).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
have inl : ∀ (i : ι), edist (x.ofLp i) (y.ofLp i) ≤ edist x.ofLp y.ofLp
Tactic: simp only [edist_eq_iSup, ENNReal.div_top, ENNReal.toReal_zero, NNReal.rpow_zero,
      ENNReal.coe_one, one_mul, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
⊢ edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
have pos : 0 < p.toReal
Tactic: have pos : 0 < p.toReal := zero_lt_one.trans_le h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
⊢ edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
have nonneg : 0 ≤ 1 / p.toReal
Tactic: have nonneg : 0 ≤ 1 / p.toReal := one_div_nonneg.2 (le_of_lt pos)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
⊢ edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
have cancel : p.toReal * (1 / p.toReal) = 1
Tactic: have cancel : p.toReal * (1 / p.toReal) = 1 := mul_div_cancel₀ 1 (ne_of_gt pos)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : 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 ≤ (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
have inr : HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal) ≤
  (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (ENNReal.toReal 1 / p.toReal)) : ℝ≥0∞) * edist x.ofLp y.ofLp
Tactic: rw [edist_eq_sum pos, ENNReal.toReal_div 1 p]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : 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
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ _i : ι, edist x.ofLp y.ofLp ^ p.toReal) (1 / p.toReal)
have h₁ : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → edist (x.ofLp i) (y.ofLp i) ≤ edist x.ofLp y.ofLp
Tactic: gcongr with i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : 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
⊢ HPow.hPow (α := ℝ≥0∞) (∑ _i : ι, edist x.ofLp y.ofLp ^ p.toReal) (1 / p.toReal) =
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal)) : ℝ≥0∞) * edist x.ofLp y.ofLp
have simp : HPow.hPow (α := ℝ≥0∞) (↑(Fintype.card ι) : ℝ≥0∞) (1 / p.toReal) * edist x.ofLp y.ofLp =
  (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal)) : ℝ≥0∞) * edist x.ofLp y.ofLp
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : 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
⊢ HPow.hPow (α := ℝ≥0∞) (↑(Fintype.card ι) : ℝ≥0∞) (1 / p.toReal) * edist x.ofLp y.ofLp =
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal)) : ℝ≥0∞) * edist x.ofLp y.ofLp
have this : (↑(Fintype.card ι) : ℝ≥0∞) = (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞)
Tactic: have : (Fintype.card ι : ℝ≥0∞) = (Fintype.card ι : ℝ≥0) :=
          (ENNReal.coe_natCast (Fintype.card ι)).symm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : 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 ι) : ℝ≥0∞) = (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞)
⊢ HPow.hPow (α := ℝ≥0∞) (↑(Fintype.card ι) : ℝ≥0∞) (1 / p.toReal) * edist x.ofLp y.ofLp =
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal)) : ℝ≥0∞) * edist x.ofLp y.ofLp
have rw : (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞) ^ (1 / p.toReal) * edist x.ofLp y.ofLp =
  (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal)) : ℝ≥0∞) * edist x.ofLp y.ofLp
Tactic: rw [this, ENNReal.coe_rpow_of_nonneg _ nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : 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 ι) : ℝ≥0∞) = (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞)
rw :
  (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞) ^ (1 / p.toReal) * edist x.ofLp y.ofLp =
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal)) : ℝ≥0∞) * edist x.ofLp y.ofLp
⊢ HPow.hPow (α := ℝ≥0∞) (↑(Fintype.card ι) : ℝ≥0∞) (1 / p.toReal) * edist x.ofLp y.ofLp =
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal)) : ℝ≥0∞) * edist x.ofLp y.ofLp
have rw₁ : (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞) ^ (1 / p.toReal) * edist x.ofLp y.ofLp =
  (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞) ^ (1 / p.toReal) * edist x.ofLp y.ofLp
Tactic: rw [this, ENNReal.coe_rpow_of_nonneg _ nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : 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
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal) ≤
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal)) : ℝ≥0∞) *
      Finset.sup Finset.univ fun (b : ι) ↦ edist (x.ofLp b) (y.ofLp b)
have edist : HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal) ≤
  HPow.hPow (α := ℝ≥0∞) (∑ _i : ι, edist x.ofLp y.ofLp ^ p.toReal) (1 / p.toReal)
Tactic: calc
      (∑ i, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) ≤
          (∑ _i, edist (ofLp x) (ofLp 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 (ofLp x) (ofLp 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]