awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  HPow.hPow (α := ℝ≥0∞) (∑ i : ι, EDist.edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ _i : ι, EDist.edist x.ofLp y.ofLp ^ p.toReal) (1 / p.toReal)
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i : ι, EDist.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.edist (x.ofLp b) (y.ofLp b)
have edist₁ : HPow.hPow (α := ℝ≥0∞) (∑ _i : ι, EDist.edist x.ofLp y.ofLp ^ p.toReal) (1 / p.toReal) =
  (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal)) : ℝ≥0∞) * EDist.edist x.ofLp y.ofLp
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]
-- 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 ι
⊢ Eq (α := Filter (PiLp p β × PiLp p β)) (𝓤 (PiLp p β)) (𝓤 (WithLp p ((i : ι) → β i)))
have rw : Eq (α := Filter (PiLp p β × PiLp p β))
  (comap (β := ((i : ι) → β i) × ((i : ι) → β i))
    (fun (x : WithLp p ((i : ι) → β i) × WithLp p ((i : ι) → β i)) ↦ (x.1.ofLp, x.2.ofLp)) (𝓤 ((i : ι) → β i)))
  (𝓤 (WithLp p ((i : ι) → β i)))
Tactic: rw [← (isUniformInducing_ofLp_aux p β).comap_uniformity]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
inst : Fintype ι
p : ℝ≥0∞
inst_1 : Fact (1 ≤ p)
β : ι → Type u_5
inst_2 : (i : ι) → PseudoMetricSpace (β i)
hp : p ≠ ∞
x y : PiLp p β
⊢ (↑(nndist x y) : ℝ) = (↑(HPow.hPow (α := ℝ≥0) (∑ i : ι, nndist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal)) : ℝ)
have push_cast : dist x y = HPow.hPow (α := ℝ) (∑ x_1 : ι, dist (x.ofLp x_1) (y.ofLp x_1) ^ p.toReal) (1 / p.toReal)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
inst : Fintype ι
β : ι → Type u_5
inst_1 : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp ∞ β
⊢ (↑(nndist x y) : ℝ) = (↑(⨆ (i : ι), nndist (x.ofLp i) (y.ofLp i)) : ℝ)
have push_cast : dist x y = ⨆ (i : ι), dist (x.ofLp i) (y.ofLp i)
Tactic: push_cast
-- 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
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp p β
⊢ dist x y = ‖-x + y‖
have inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : PiLp ∞ β), dist x y = ‖-x + y‖
Tactic: rcases p.dichotomy with (rfl | h)
Cleared hypotheses: p, hp, x, y
-- 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
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp p β
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : PiLp ∞ β), dist x y = ‖-x + y‖
⊢ dist x y = ‖-x + y‖
have inr : ∀ (h : 1 ≤ p.toReal), dist x y = ‖-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_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp p β
h : 1 ≤ p.toReal
hp : p = ∞
⊢ False
have h₁ : LE.le (α := ℝ) 1 0
Tactic: rw [hp, ENNReal.toReal_top] at h
Cleared hypotheses: h, 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
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp p β
h : LE.le (α := ℝ) 1 0
hp : p = ∞
⊢ False
have linarith : -1 + HSub.hSub (α := ℝ) 1 0 = 0
Tactic: linarith
-- 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
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp p β
h : 1 ≤ p.toReal
⊢ dist x y = ‖-x + y‖
have this : p ≠ ∞
Tactic: have : p ≠ ∞ := by
        intro hp
        rw [hp, ENNReal.toReal_top] at h
        linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
inst : Fintype ι
p : ℝ≥0∞
inst_1 : Fact (1 ≤ p)
β : ι → Type u_5
hp : p ≠ ∞
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp p β
⊢ ‖f‖₊ = HPow.hPow (α := ℝ≥0) (∑ i : ι, ‖f.ofLp i‖₊ ^ p.toReal) (1 / p.toReal)
have a : (↑‖f‖₊ : ℝ) = (↑(HPow.hPow (α := ℝ≥0) (∑ i : ι, ‖f.ofLp i‖₊ ^ p.toReal) (1 / p.toReal)) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ∞ β
⊢ ‖f‖₊ = ⨆ (i : ι), ‖f.ofLp i‖₊
have a : (↑‖f‖₊ : ℝ) = (↑(⨆ (i : ι), ‖f.ofLp i‖₊) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ∞ β
⊢ ‖f.ofLp‖₊ = ‖f‖₊
have rw : ‖f.ofLp‖₊ = ⨆ (i : ι), ‖f.ofLp i‖₊
Tactic: rw [nnnorm_eq_ciSup, Pi.nnnorm_def, Finset.sup_univ_eq_ciSup]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ∞ β
rw : ‖f.ofLp‖₊ = ⨆ (i : ι), ‖f.ofLp i‖₊
⊢ ‖f.ofLp‖₊ = ‖f‖₊
have rw₁ : Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (b : ι) ↦ ‖f.ofLp b‖₊) (⨆ (i : ι), ‖f.ofLp i‖₊)
Tactic: rw [nnnorm_eq_ciSup, Pi.nnnorm_def, Finset.sup_univ_eq_ciSup]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ∞ β
rw : ‖f.ofLp‖₊ = ⨆ (i : ι), ‖f.ofLp i‖₊
rw₁ : Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (b : ι) ↦ ‖f.ofLp b‖₊) (⨆ (i : ι), ‖f.ofLp i‖₊)
⊢ ‖f.ofLp‖₊ = ‖f‖₊
have rw₂ : Eq (α := ℝ≥0) (⨆ (i : ι), ‖f.ofLp i‖₊) (⨆ (i : ι), ‖f.ofLp i‖₊)
Tactic: rw [nnnorm_eq_ciSup, Pi.nnnorm_def, Finset.sup_univ_eq_ciSup]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
Goal:
ι : Type u_2
inst : Fintype ι
p : ℝ≥0∞
inst_1 : Fact (1 ≤ p)
β : ι → Type u_5
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
n : ℕ
h : p = (↑n : ℝ≥0∞)
f : PiLp p β
⊢ ‖f‖ = HPow.hPow (α := ℝ) (∑ i : ι, ‖f.ofLp i‖ ^ n) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have this : 0 < p.toReal
Tactic: have := p.toReal_pos_iff_ne_top.mpr (ne_of_eq_of_ne h <| ENNReal.natCast_ne_top n)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 1 β
⊢ (↑‖x‖₊ : ℝ) = (↑(∑ i : ι, ‖x.ofLp i‖₊) : ℝ)
have push_cast : ‖x‖ = ∑ x_1 : ι, ‖x.ofLp x_1‖
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 1 β
⊢ dist x y = ∑ i : ι, dist (x.ofLp i) (y.ofLp i)
have simp_rw : ‖x - y‖ = ∑ x_1 : ι, ‖x.ofLp x_1 - y.ofLp x_1‖
Tactic: simp_rw [dist_eq_norm, norm_eq_of_L1, sub_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 1 β
simp_rw : ‖x - y‖ = ∑ x_1 : ι, ‖x.ofLp x_1 - y.ofLp x_1‖
⊢ dist x y = ∑ i : ι, dist (x.ofLp i) (y.ofLp i)
have simp_rw₁ : Eq (α := ℝ) (∑ i : ι, ‖(x - y).ofLp i‖) (∑ x_1 : ι, ‖x.ofLp x_1 - y.ofLp x_1‖)
Tactic: simp_rw [dist_eq_norm, norm_eq_of_L1, sub_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 1 β
⊢ (↑(nndist x y) : ℝ) = (↑(∑ i : ι, nndist (x.ofLp i) (y.ofLp i)) : ℝ)
have push_cast : dist x y = ∑ x_1 : ι, dist (x.ofLp x_1) (y.ofLp x_1)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ Eq (α := ℝ≥0∞) 2 (↑2 : ℝ≥0∞)
have norm_cast : Eq (α := ℕ) 2 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ = √(∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2)
have rw : HPow.hPow (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2) (HDiv.hDiv (α := ℝ) 1 (↑2 : ℝ)) =
  √(∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2)
Tactic: rw [norm_eq_of_nat 2 (by norm_cast) _]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ HPow.hPow (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2) (HDiv.hDiv (α := ℝ) 1 (↑2 : ℝ)) =
    √(∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2)
have rw : HPow.hPow (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2) (HDiv.hDiv (α := ℝ) 1 (↑2 : ℝ)) =
  HPow.hPow (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2) (1 / 2)
Tactic: rw [Real.sqrt_eq_rpow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ HPow.hPow (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2) (HDiv.hDiv (α := ℝ) 1 (↑2 : ℝ)) =
    HPow.hPow (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2) (1 / 2)
have norm_cast : HPow.hPow (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2) (HDiv.hDiv (α := ℝ) 1 2) =
  HPow.hPow (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2) (HDiv.hDiv (α := ℝ) 1 2)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (↑‖x‖₊ : ℝ) = (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2)) : ℝ)
have push_cast : ‖x‖ = √(∑ x_1 : ι, HPow.hPow (β := ℕ) ‖x.ofLp x_1‖ 2)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
inst : Fintype ι
β : ι → Type u_5
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = ∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2
have suffices : HPow.hPow (β := ℕ) ‖x‖₊ 2 = ∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2
Tactic: suffices ‖x‖₊ ^ 2 = ∑ i : ι, ‖x i‖₊ ^ 2 by
    simpa only [NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
inst : Fintype ι
β : ι → Type u_5
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ HPow.hPow (β := ℕ) ‖x‖₊ 2 = ∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2
have rw : HPow.hPow (α := ℝ≥0) (β := ℕ) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2)) 2 =
  ∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2
Tactic: rw [nnnorm_eq_of_L2, NNReal.sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
inst : Fintype ι
β : ι → Type u_5
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
rw :
  HPow.hPow (α := ℝ≥0) (β := ℕ) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2)) 2 =
    ∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2
⊢ HPow.hPow (β := ℕ) ‖x‖₊ 2 = ∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2
have rw₁ : Eq (α := ℝ≥0) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2)
Tactic: rw [nnnorm_eq_of_L2, NNReal.sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ dist x y = √(∑ i : ι, HPow.hPow (β := ℕ) (dist (x.ofLp i) (y.ofLp i)) 2)
have simp_rw : ‖x - y‖ = √(∑ x_1 : ι, HPow.hPow (β := ℕ) ‖x.ofLp x_1 - y.ofLp x_1‖ 2)
Tactic: simp_rw [dist_eq_norm, norm_eq_of_L2, sub_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
simp_rw : ‖x - y‖ = √(∑ x_1 : ι, HPow.hPow (β := ℕ) ‖x.ofLp x_1 - y.ofLp x_1‖ 2)
⊢ dist x y = √(∑ i : ι, HPow.hPow (β := ℕ) (dist (x.ofLp i) (y.ofLp i)) 2)
have simp_rw₁ : √(∑ i : ι, HPow.hPow (β := ℕ) ‖(x - y).ofLp i‖ 2) = √(∑ x_1 : ι, HPow.hPow (β := ℕ) ‖x.ofLp x_1 - y.ofLp x_1‖ 2)
Tactic: simp_rw [dist_eq_norm, norm_eq_of_L2, sub_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ HPow.hPow (β := ℕ) (dist x y) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (dist (x.ofLp i) (y.ofLp i)) 2
have simp_rw : HPow.hPow (β := ℕ) ‖x - y‖ 2 = ∑ x_1 : ι, HPow.hPow (β := ℕ) ‖x.ofLp x_1 - y.ofLp x_1‖ 2
Tactic: simp_rw [dist_eq_norm, norm_sq_eq_of_L2, sub_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
simp_rw : HPow.hPow (β := ℕ) ‖x - y‖ 2 = ∑ x_1 : ι, HPow.hPow (β := ℕ) ‖x.ofLp x_1 - y.ofLp x_1‖ 2
⊢ HPow.hPow (β := ℕ) (dist x y) 2 = ∑ i : ι, HPow.hPow (β := ℕ) (dist (x.ofLp i) (y.ofLp i)) 2
have simp_rw₁ : Eq (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ‖(x - y).ofLp i‖ 2) (∑ x_1 : ι, HPow.hPow (β := ℕ) ‖x.ofLp x_1 - y.ofLp x_1‖ 2)
Tactic: simp_rw [dist_eq_norm, norm_sq_eq_of_L2, sub_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ (↑(nndist x y) : ℝ) =
    (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ i : ι, HPow.hPow (β := ℕ) (nndist (x.ofLp i) (y.ofLp i)) 2)) : ℝ)
have push_cast : dist x y = √(∑ x_1 : ι, HPow.hPow (β := ℕ) (dist (x.ofLp x_1) (y.ofLp x_1)) 2)
Tactic: push_cast
-- 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
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
have inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f : PiLp ∞ β), ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
Tactic: rcases p.dichotomy with (rfl | hp)
Cleared hypotheses: p, hp, f
-- 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
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f : PiLp ∞ β), ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
have inr : ∀ (hp_1 : 1 ≤ p.toReal), ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
Tactic: rcases p.dichotomy with (rfl | hp)
-- 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 : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f : PiLp ∞ β
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
have inl : ‖c • f.ofLp‖₊ ≤ ‖c‖₊ * ‖f.ofLp‖₊
Tactic: rw [← nnnorm_ofLp, ← nnnorm_ofLp, ofLp_smul]
-- 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
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
have hp0 : 0 < p.toReal
Tactic: have hp0 : 0 < p.toReal := zero_lt_one.trans_le hp
-- 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
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
have hpt : p ≠ ∞
Tactic: have hpt : p ≠ ⊤ := p.toReal_pos_iff_ne_top.mp hp0
-- 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
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
have inr : LE.le (α := ℝ≥0) (∑ i : ι, ‖(c • f).ofLp i‖₊ ^ p.toReal) (∑ i : ι, ‖c‖₊ ^ p.toReal * ‖f.ofLp i‖₊ ^ p.toReal)
Tactic: rw [nnnorm_eq_sum hpt, nnnorm_eq_sum hpt, one_div, NNReal.rpow_inv_le_iff hp0,
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one,
        Finset.mul_sum]
-- 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
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ LE.le (α := ℝ≥0) (∑ i : ι, ‖(c • f).ofLp i‖₊ ^ p.toReal) (∑ i : ι, ‖c‖₊ ^ p.toReal * ‖f.ofLp i‖₊ ^ p.toReal)
have inr : LE.le (α := ℝ≥0) (∑ x : ι, ‖c • f.ofLp x‖₊ ^ p.toReal) (∑ x : ι, (‖c‖₊ * ‖f.ofLp x‖₊) ^ p.toReal)
Tactic: simp_rw [← NNReal.mul_rpow, smul_apply]
-- 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
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), IsBoundedSMul.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ LE.le (α := ℝ≥0) (∑ x : ι, ‖c • f.ofLp x‖₊ ^ p.toReal) (∑ x : ι, (‖c‖₊ * ‖f.ofLp x‖₊) ^ p.toReal)
have inr : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → ‖c • f.ofLp i‖₊ ≤ ‖c‖₊ * ‖f.ofLp i‖₊
Tactic: gcongr
-- 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
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), NormSMulClass.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f : PiLp ∞ β), ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
Tactic: rcases p.dichotomy with (rfl | hp)
Cleared hypotheses: p, hp, f
-- 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
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), NormSMulClass.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f : PiLp ∞ β), ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inr : ∀ (hp_1 : 1 ≤ p.toReal), ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
Tactic: rcases p.dichotomy with (rfl | hp)
-- 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 : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), NormSMulClass.{u_1, u_4} 𝕜 (β i)
c : 𝕜
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f : PiLp ∞ β
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inl : ‖(c • f).ofLp‖₊ = ‖c‖₊ * ‖f‖₊
Tactic: rw [← nnnorm_ofLp, ← nnnorm_ofLp, WithLp.ofLp_smul, nnnorm_smul]
-- 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 : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), NormSMulClass.{u_1, u_4} 𝕜 (β i)
c : 𝕜
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f : PiLp ∞ β
inl : ‖(c • f).ofLp‖₊ = ‖c‖₊ * ‖f‖₊
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inl₁ : ‖(c • f).ofLp‖₊ = ‖c‖₊ * ‖f.ofLp‖₊
Tactic: rw [← nnnorm_ofLp, ← nnnorm_ofLp, WithLp.ofLp_smul, nnnorm_smul]
-- 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 : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), NormSMulClass.{u_1, u_4} 𝕜 (β i)
c : 𝕜
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f : PiLp ∞ β
inl : ‖(c • f).ofLp‖₊ = ‖c‖₊ * ‖f‖₊
inl₁ : ‖(c • f).ofLp‖₊ = ‖c‖₊ * ‖f.ofLp‖₊
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inl₂ : ‖c • f.ofLp‖₊ = ‖c‖₊ * ‖f.ofLp‖₊
Tactic: rw [← nnnorm_ofLp, ← nnnorm_ofLp, WithLp.ofLp_smul, nnnorm_smul]
-- 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 : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), NormSMulClass.{u_1, u_4} 𝕜 (β i)
c : 𝕜
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f : PiLp ∞ β
inl : ‖(c • f).ofLp‖₊ = ‖c‖₊ * ‖f‖₊
inl₁ : ‖(c • f).ofLp‖₊ = ‖c‖₊ * ‖f.ofLp‖₊
inl₂ : ‖c • f.ofLp‖₊ = ‖c‖₊ * ‖f.ofLp‖₊
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have inl₃ : ‖c‖₊ * ‖f.ofLp‖₊ = ‖c‖₊ * ‖f.ofLp‖₊
Tactic: rw [← nnnorm_ofLp, ← nnnorm_ofLp, WithLp.ofLp_smul, nnnorm_smul]
-- 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
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), NormSMulClass.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have hp0 : 0 < p.toReal
Tactic: have hp0 : 0 < p.toReal := zero_lt_one.trans_le hp
-- 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
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : SeminormedRing 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (β i)
inst_3 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
inst_4 : ∀ (i : ι), NormSMulClass.{u_1, u_4} 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
have hpt : p ≠ ∞
Tactic: have hpt : p ≠ ⊤ := p.toReal_pos_iff_ne_top.mp hp0