awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → UniformSpace (β i)
⊢ UniformContinuous (α := (i : ι) → β i) (toLp p)

Tactic:
uniformContinuous_comap' uniformContinuous_id

Premises used: uniformContinuous_id, uniformContinuous_comap'
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → UniformSpace (β i)
⊢ Eq (α := PiLp p β ≃ₜ ((i : ι) → β i)) (UniformEquiv.toHomeomorph (uniformEquiv p β)) (homeomorph p β)

Tactic:
rfl

Premises used: WithLp.equiv, PiLp.homeomorph, UniformEquiv.toHomeomorph, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → UniformSpace (β i)
⊢ UniformEquiv.toEquiv (uniformEquiv p β) = WithLp.equiv p ((i : ι) → β i)

Tactic:
rfl

Premises used: WithLp.equiv, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → UniformSpace (β i)
inst_1 : ∀ (i : ι), CompleteSpace.{u_4} (β i)
⊢ CompleteSpace (PiLp p β)

Tactic:
(uniformEquiv p β).completeSpace_iff.2 inferInstance

Premises used: Iff.mpr, PiLp.uniformEquiv, inferInstance, UniformEquiv.completeSpace_iff
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 β
push_cast : dist x y = HPow.hPow (α := ℝ) (∑ x_1 : ι, dist (x.ofLp x_1) (y.ofLp x_1) ^ p.toReal) (1 / p.toReal)
⊢ (↑(nndist x y) : ℝ) = (↑(HPow.hPow (α := ℝ≥0) (∑ i : ι, nndist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal)) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 β
⊢ dist x y = HPow.hPow (α := ℝ) (∑ x_1 : ι, dist (x.ofLp x_1) (y.ofLp x_1) ^ p.toReal) (1 / p.toReal)

Tactic:
dist_eq_sum (p.toReal_pos_iff_ne_top.mpr hp) _ _

Premises used: Iff.mpr, ENNReal.toReal_pos_iff_ne_top, PiLp.dist_eq_sum
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 β
⊢ dist x y = HPow.hPow (α := ℝ) (∑ x_1 : ι, dist (x.ofLp x_1) (y.ofLp x_1) ^ p.toReal) (1 / p.toReal)

Tactic:
exact dist_eq_sum (p.toReal_pos_iff_ne_top.mpr hp) _ _

Premises used: Iff.mpr, ENNReal.toReal_pos_iff_ne_top, PiLp.dist_eq_sum
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
inst : Fintype ι
β : ι → Type u_5
inst_1 : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp ∞ β
push_cast : dist x y = ⨆ (i : ι), dist (x.ofLp i) (y.ofLp i)
⊢ (↑(nndist x y) : ℝ) = (↑(⨆ (i : ι), nndist (x.ofLp i) (y.ofLp i)) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
inst : Fintype ι
β : ι → Type u_5
inst_1 : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp ∞ β
⊢ dist x y = ⨆ (i : ι), dist (x.ofLp i) (y.ofLp i)

Tactic:
dist_eq_iSup _ _

Premises used: PiLp.dist_eq_iSup
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
inst : Fintype ι
β : ι → Type u_5
inst_1 : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp ∞ β
⊢ dist x y = ⨆ (i : ι), dist (x.ofLp i) (y.ofLp i)

Tactic:
exact dist_eq_iSup _ _

Premises used: PiLp.dist_eq_iSup
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
x y : PiLp p β
i : ι
⊢ edist (x.ofLp i) (y.ofLp i) ≤ edist x y

Tactic:
edist_apply_le_edist_aux x y i

Premises used: _private.0.PiLp.edist_apply_le_edist_aux
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp p β
i : ι
⊢ nndist (x.ofLp i) (y.ofLp i) ≤ nndist x y

Tactic:
simpa [← coe_nnreal_ennreal_nndist] using edist_apply_le x y i

Premises used: coe_nnreal_ennreal_nndist, PiLp.edist_apply_le
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp p β
i : ι
⊢ dist (x.ofLp i) (y.ofLp i) ≤ dist x y

Tactic:
nndist_apply_le x y i

Premises used: PiLp.nndist_apply_le
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
⊢ LipschitzWith (α := WithLp p ((i : ι) → β i)) 1 ofLp

Tactic:
lipschitzWith_ofLp_aux p β

Premises used: LipschitzWith, iInf, Set.Mem, setOf, Set.Subset, _private.0.PiLp.lipschitzWith_ofLp_aux, Filter.join, Filter.comap
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
⊢ AntilipschitzWith (α := (i : ι) → β i) 1 (toLp p)

Tactic:
(lipschitzWith_ofLp p β).to_rightInverse (ofLp_toLp p)

Premises used: PiLp.lipschitzWith_ofLp, LipschitzWith.to_rightInverse, WithLp.ofLp_toLp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
⊢ AntilipschitzWith (α := WithLp p ((i : ι) → β i)) (HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal) ofLp

Tactic:
antilipschitzWith_ofLp_aux p β

Premises used: iInf, Set.Mem, setOf, Set.Subset, Filter.join, _private.0.PiLp.antilipschitzWith_ofLp_aux, Filter.comap, AntilipschitzWith
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
⊢ LipschitzWith (α := (i : ι) → β i) (HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal) (toLp p)

Tactic:
(antilipschitzWith_ofLp p β).to_rightInverse (ofLp_toLp p)

Premises used: AntilipschitzWith.to_rightInverse, PiLp.antilipschitzWith_ofLp, WithLp.ofLp_toLp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
x y : WithLp ∞ ((i : ι) → β i)
⊢ edist x.ofLp y.ofLp ≤ edist x y

Tactic:
simpa only [ENNReal.coe_one, one_mul] using lipschitzWith_ofLp ∞ β x y

Premises used: PiLp.lipschitzWith_ofLp, ENNReal.coe_one, Top.top, one_mul
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
x y : WithLp ∞ ((i : ι) → β i)
⊢ edist x y ≤ edist x.ofLp y.ofLp

Tactic:
simpa only [ENNReal.div_top, ENNReal.toReal_zero, NNReal.rpow_zero, ENNReal.coe_one,
      one_mul] using antilipschitzWith_ofLp ∞ β x y

Premises used: ENNReal.div_top, ENNReal.coe_one, PiLp.antilipschitzWith_ofLp, ENNReal.toReal_zero, NNReal.rpow_zero, Top.top, one_mul
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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‖
inr : ∀ (h : 1 ≤ p.toReal), dist x y = ‖-x + y‖
⊢ dist x y = ‖-x + y‖

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

Premises used: ENNReal.dichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
x y : PiLp ∞ β
⊢ dist x y = ‖-x + y‖

Tactic:
simp only [dist_eq_iSup, norm_eq_ciSup, dist_eq_norm, add_apply, neg_apply, norm_neg_add]

Premises used: dist_eq_norm, norm_neg_add, PiLp.dist_eq_iSup, PiLp.norm_eq_ciSup, PiLp.add_apply, PiLp.neg_apply
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 = ∞
⊢ LE.le (α := ℝ) 1 0

Tactic:
rw [hp, ENNReal.toReal_top] at h

Premises used: ENNReal.toReal_top
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 = ∞
h₁ : LE.le (α := ℝ) 1 0
⊢ p = ∞

Tactic:
rw [hp, ENNReal.toReal_top] at h

Premises used: ENNReal.toReal_top
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 = ∞
linarith : -1 + HSub.hSub (α := ℝ) 1 0 = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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
⊢ p ≠ ∞

Tactic:
have : p ≠ ∞ := by
        intro hp
        rw [hp, ENNReal.toReal_top] at h
        linarith
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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
this : p ≠ ∞
⊢ dist x y = ‖-x + y‖

Tactic:
simp only [dist_eq_sum (zero_lt_one.trans_le h), norm_eq_sum (zero_lt_one.trans_le h),
        dist_eq_norm, add_apply, neg_apply, norm_neg_add]

Premises used: dist_eq_norm, norm_neg_add, PiLp.norm_eq_sum, zero_lt_one, PiLp.add_apply, LT.lt.trans_le, PiLp.neg_apply, PiLp.dist_eq_sum
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Finite ι
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
⊢ IsUniformInducing (α := (i : ι) → β i) (toLp p)

Tactic:
have := Fintype.ofFinite ι
  (antilipschitzWith_toLp p β).isUniformInducing
    (lipschitzWith_toLp p β).uniformContinuous

Premises used: PiLp.lipschitzWith_toLp, Fintype.ofFinite, PiLp.antilipschitzWith_toLp, AntilipschitzWith.isUniformInducing, LipschitzWith.uniformContinuous
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp p β
i : ι
⊢ ‖x.ofLp i‖ₑ ≤ ‖x‖ₑ

Tactic:
simpa using edist_apply_le x 0 i

Premises used: PiLp.edist_apply_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp p β
i : ι
⊢ ‖x.ofLp i‖₊ ≤ ‖x‖₊

Tactic:
simpa using nndist_apply_le x 0 i

Premises used: PiLp.nndist_apply_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp p β
i : ι
⊢ ‖x.ofLp i‖ ≤ ‖x‖

Tactic:
simpa using dist_apply_le x 0 i

Premises used: PiLp.dist_apply_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 β
a : (↑‖f‖₊ : ℝ) = (↑(HPow.hPow (α := ℝ≥0) (∑ i : ι, ‖f.ofLp i‖₊ ^ p.toReal) (1 / p.toReal)) : ℝ)
⊢ ‖f‖₊ = HPow.hPow (α := ℝ≥0) (∑ i : ι, ‖f.ofLp i‖₊ ^ p.toReal) (1 / p.toReal)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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)) : ℝ)

Tactic:
simp [NNReal.coe_sum, norm_eq_sum (p.toReal_pos_iff_ne_top.mpr hp)]

Premises used: Iff.mpr, PiLp.norm_eq_sum, NNReal.coe_sum, ENNReal.toReal_pos_iff_ne_top
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ∞ β
a : (↑‖f‖₊ : ℝ) = (↑(⨆ (i : ι), ‖f.ofLp i‖₊) : ℝ)
⊢ ‖f‖₊ = ⨆ (i : ι), ‖f.ofLp i‖₊

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ∞ β
⊢ (↑‖f‖₊ : ℝ) = (↑(⨆ (i : ι), ‖f.ofLp i‖₊) : ℝ)

Tactic:
simp [NNReal.coe_iSup, norm_eq_ciSup]

Premises used: NNReal.coe_iSup, PiLp.norm_eq_ciSup
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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‖₊)
rw₂ rw₃ : Eq (α := ℝ≥0) (⨆ (i : ι), ‖f.ofLp i‖₊) (⨆ (i : ι), ‖f.ofLp i‖₊)
⊢ ‖f.ofLp‖₊ = ‖f‖₊

Tactic:
rw [nnnorm_eq_ciSup, Pi.nnnorm_def, Finset.sup_univ_eq_ciSup]

Premises used: Finset.sup_univ_eq_ciSup, PiLp.nnnorm_eq_ciSup, Pi.nnnorm_def
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
f : (i : ι) → β i
⊢ nnnorm (E := WithLp ∞ ((i : ι) → β i)) (toLp ∞ f) = ‖f‖₊

Tactic:
(nnnorm_ofLp _).symm

Premises used: Eq.symm, PiLp.nnnorm_ofLp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ∞ β
⊢ ‖f.ofLp‖ = ‖f‖

Tactic:
congr_arg NNReal.toReal <| nnnorm_ofLp f

Premises used: Multiset.foldr, Finset.fold, NNReal.mk, NNReal, congr_arg, Finset.sup, NNReal.toReal, Multiset.fold, PiLp.nnnorm_ofLp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
f : (i : ι) → β i
⊢ Norm.norm (E := WithLp ∞ ((i : ι) → β i)) (toLp ∞ f) = ‖f‖

Tactic:
(norm_ofLp _).symm

Premises used: PiLp.norm_ofLp, Eq.symm
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 β
⊢ 0 < p.toReal

Tactic:
have := p.toReal_pos_iff_ne_top.mpr (ne_of_eq_of_ne h <| ENNReal.natCast_ne_top n)
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 β
this : 0 < p.toReal
⊢ ‖f‖ = HPow.hPow (α := ℝ) (∑ i : ι, ‖f.ofLp i‖ ^ n) (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
simp only [one_div, h, Real.rpow_natCast, ENNReal.toReal_natCast,
    norm_eq_sum this]

Premises used: ENNReal.toReal_natCast, PiLp.norm_eq_sum, one_div, Real.rpow_natCast
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 1 β
⊢ ‖x‖ = ∑ i : ι, ‖x.ofLp i‖

Tactic:
simp [norm_eq_sum]

Premises used: PiLp.norm_eq_sum
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 1 β
push_cast : ‖x‖ = ∑ x_1 : ι, ‖x.ofLp x_1‖
⊢ (↑‖x‖₊ : ℝ) = (↑(∑ i : ι, ‖x.ofLp i‖₊) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 1 β
⊢ ‖x‖ = ∑ x_1 : ι, ‖x.ofLp x_1‖

Tactic:
norm_eq_of_L1 x

Premises used: PiLp.norm_eq_of_L1
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 1 β
⊢ ‖x‖ = ∑ x_1 : ι, ‖x.ofLp x_1‖

Tactic:
exact norm_eq_of_L1 x

Premises used: PiLp.norm_eq_of_L1
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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‖
simp_rw₁ : Eq (α := ℝ) (∑ i : ι, ‖(x - y).ofLp i‖) (∑ x_1 : ι, ‖x.ofLp x_1 - y.ofLp x_1‖)
⊢ dist x y = ∑ i : ι, dist (x.ofLp i) (y.ofLp i)

Tactic:
simp_rw [dist_eq_norm, norm_eq_of_L1, sub_apply]

Premises used: dist_eq_norm, PiLp.sub_apply, PiLp.norm_eq_of_L1
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 1 β
push_cast : dist x y = ∑ x_1 : ι, dist (x.ofLp x_1) (y.ofLp x_1)
⊢ (↑(nndist x y) : ℝ) = (↑(∑ i : ι, nndist (x.ofLp i) (y.ofLp i)) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 1 β
⊢ dist x y = ∑ x_1 : ι, dist (x.ofLp x_1) (y.ofLp x_1)

Tactic:
dist_eq_of_L1 _ _

Premises used: setOf, PiLp.dist_eq_of_L1
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 1 β
⊢ dist x y = ∑ x_1 : ι, dist (x.ofLp x_1) (y.ofLp x_1)

Tactic:
exact dist_eq_of_L1 _ _

Premises used: PiLp.dist_eq_of_L1
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 1 β
⊢ edist x y = ∑ i : ι, edist (x.ofLp i) (y.ofLp i)

Tactic:
simp [PiLp.edist_eq_sum]

Premises used: PiLp.edist_eq_sum
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℕ) 2 2
⊢ Eq (α := ℝ≥0∞) 2 (↑2 : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
rw :
  HPow.hPow (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2) (HDiv.hDiv (α := ℝ) 1 (↑2 : ℝ)) =
    √(∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2)
⊢ ‖x‖ = √(∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2)

Tactic:
rw [norm_eq_of_nat 2 (by norm_cast) _]

Premises used: PiLp.norm_eq_of_nat, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
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)
⊢ HPow.hPow (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2) (HDiv.hDiv (α := ℝ) 1 (↑2 : ℝ)) =
    √(∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2)

Tactic:
rw [Real.sqrt_eq_rpow]

Premises used: Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
norm_cast norm_cast₁ norm_cast₂ 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)
⊢ 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:
norm_cast
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
push_cast : ‖x‖ = √(∑ x_1 : ι, HPow.hPow (β := ℕ) ‖x.ofLp x_1‖ 2)
⊢ (↑‖x‖₊ : ℝ) = (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2)) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ = √(∑ x_1 : ι, HPow.hPow (β := ℕ) ‖x.ofLp x_1‖ 2)

Tactic:
norm_eq_of_L2 x

Premises used: PiLp.norm_eq_of_L2
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ = √(∑ x_1 : ι, HPow.hPow (β := ℕ) ‖x.ofLp x_1‖ 2)

Tactic:
exact norm_eq_of_L2 x

Premises used: PiLp.norm_eq_of_L2
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
inst : Fintype ι
β : ι → Type u_5
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
this : HPow.hPow (β := ℕ) ‖x‖₊ 2 = ∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = ∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2

Tactic:
simpa only [NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) this

Premises used: NNReal.coe_sum, congr_arg, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
inst : Fintype ι
β : ι → Type u_5
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
suffices : HPow.hPow (β := ℕ) ‖x‖₊ 2 = ∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2
⊢ 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
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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
rw₁ rw₂ : Eq (α := ℝ≥0) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2) (∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2)
⊢ HPow.hPow (β := ℕ) ‖x‖₊ 2 = ∑ i : ι, HPow.hPow (β := ℕ) ‖x.ofLp i‖₊ 2

Tactic:
rw [nnnorm_eq_of_L2, NNReal.sq_sqrt]

Premises used: PiLp.nnnorm_eq_of_L2, NNReal.sq_sqrt
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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)
simp_rw₁ :
  √(∑ i : ι, HPow.hPow (β := ℕ) ‖(x - y).ofLp i‖ 2) = √(∑ 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)

Tactic:
simp_rw [dist_eq_norm, norm_eq_of_L2, sub_apply]

Premises used: dist_eq_norm, PiLp.sub_apply, PiLp.norm_eq_of_L2
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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
simp_rw₁ :
  Eq (α := ℝ) (∑ i : ι, HPow.hPow (β := ℕ) ‖(x - y).ofLp i‖ 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

Tactic:
simp_rw [dist_eq_norm, norm_sq_eq_of_L2, sub_apply]

Premises used: dist_eq_norm, PiLp.sub_apply, PiLp.norm_sq_eq_of_L2
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
push_cast : dist x y = √(∑ x_1 : ι, HPow.hPow (β := ℕ) (dist (x.ofLp x_1) (y.ofLp x_1)) 2)
⊢ (↑(nndist x y) : ℝ) =
    (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ i : ι, HPow.hPow (β := ℕ) (nndist (x.ofLp i) (y.ofLp i)) 2)) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ dist x y = √(∑ x_1 : ι, HPow.hPow (β := ℕ) (dist (x.ofLp x_1) (y.ofLp x_1)) 2)

Tactic:
dist_eq_of_L2 _ _

Premises used: setOf, PiLp.dist_eq_of_L2
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ dist x y = √(∑ x_1 : ι, HPow.hPow (β := ℕ) (dist (x.ofLp x_1) (y.ofLp x_1)) 2)

Tactic:
exact dist_eq_of_L2 _ _

Premises used: PiLp.dist_eq_of_L2
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ edist x y = HPow.hPow (α := ℝ≥0∞) (∑ i : ι, HPow.hPow (β := ℕ) (edist (x.ofLp i) (y.ofLp i)) 2) (1 / 2)

Tactic:
simp [PiLp.edist_eq_sum]

Premises used: PiLp.edist_eq_sum