awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
refine :
  ∀ (ε : ℝ) (hε : 0 < ε),
    ∃ (y : ↥(Lp F p μ)),
      Membership.mem (γ := Set ↥(Lp F p μ))
          {f : ↥(Lp F p μ) |
            ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}
          y ∧
        y ∈ Metric.closedBall f ε
⊢ Membership.mem (γ := Set ↥(Lp F p μ))
    (closure
      {f : ↥(Lp F p μ) | ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g})
    f

Tactic:
refine (mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall).2 fun ε hε ↦ ?_

Premises used: Iff.mpr, Metric.nhds_basis_closedBall, mem_closure_iff_nhds_basis
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
obtain :
  ∀ (g : E → F) (hg₁ : HasCompactSupport g) (hg₂ : ContDiff ℝ ∞ g)
    (hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε),
    ∃ (y : ↥(Lp F p μ)),
      Membership.mem (γ := Set ↥(Lp F p μ))
          {f : ↥(Lp F p μ) |
            ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}
          y ∧
        y ∈ Metric.closedBall f ε
⊢ ∃ (y : ↥(Lp F p μ)),
    Membership.mem (γ := Set ↥(Lp F p μ))
        {f : ↥(Lp F p μ) | ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}
        y ∧
      y ∈ Metric.closedBall f ε

Tactic:
obtain ⟨g, hg₁, hg₂, hg₃⟩ := exist_eLpNorm_sub_le hp hp₂.out (Lp.memLp f) hε

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.MemLp.exist_eLpNorm_sub_le, Fact.out
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
⊢ MemLp g p μ

Tactic:
have hg₄ : MemLp g p μ := hg₂.continuous.memLp_of_hasCompactSupport hg₁
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
hg₄ : MemLp g p μ
h :
  Membership.mem (γ := Set ↥(Lp F p μ))
      {f : ↥(Lp F p μ) | ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}
      (toLp g hg₄) ∧
    toLp g hg₄ ∈ Metric.closedBall f ε
⊢ ∃ (y : ↥(Lp F p μ)),
    Membership.mem (γ := Set ↥(Lp F p μ))
        {f : ↥(Lp F p μ) | ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}
        y ∧
      y ∈ Metric.closedBall f ε

Tactic:
use hg₄.toLp

Premises used: MeasureTheory.MemLp.toLp
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
hg₄ : MemLp g p μ
right : toLp g hg₄ ∈ Metric.closedBall f ε
⊢ Membership.mem (γ := Set ↥(Lp F p μ))
      {f : ↥(Lp F p μ) | ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}
      (toLp g hg₄) ∧
    toLp g hg₄ ∈ Metric.closedBall f ε

Tactic:
use ⟨g, hg₄.coeFn_toLp, hg₁, hg₂⟩
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
hg₄ : MemLp g p μ
right : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F)) p μ ≤ ENNReal.ofReal ε
⊢ toLp g hg₄ ∈ Metric.closedBall f ε

Tactic:
rw [Metric.mem_closedBall, dist_comm, Lp.dist_def,
    ← le_ofReal_iff_toReal_le ((Lp.memLp f).sub (Lp.memLp hg₄.toLp)).eLpNorm_ne_top hε.le]

Premises used: MeasureTheory.Lp.dist_def, MeasureTheory.Lp.memLp, LT.lt.le, dist_comm, ENNReal.le_ofReal_iff_toReal_le, MeasureTheory.MemLp.toLp, Metric.mem_closedBall, MeasureTheory.MemLp.sub, MeasureTheory.MemLp.eLpNorm_ne_top
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
hg₄ : MemLp g p μ
⊢ eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε

Tactic:
hg₃
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
hg₄ : MemLp g p μ
h :
  eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F)) p μ =
    eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ
⊢ eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F)) p μ ≤ ENNReal.ofReal ε

Tactic:
convert! hg₃ using 1
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
hg₄ : MemLp g p μ
h : (↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] (↑(↑f : E →ₘ[μ] F) : E → F) - g
⊢ eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F)) p μ =
    eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ

Tactic:
apply eLpNorm_congr_ae

Premises used: MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
hg₄ : MemLp g p μ
h : (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g
⊢ (↑(↑f : E →ₘ[μ] F) : E → F) - (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] (↑(↑f : E →ₘ[μ] F) : E → F) - g

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
hg₄ : MemLp g p μ
⊢ (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g

Tactic:
hg₄.coeFn_toLp

Premises used: MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm ((↑(↑f : E →ₘ[μ] F) : E → F) - g) p μ ≤ ENNReal.ofReal ε
hg₄ : MemLp g p μ
⊢ (↑(↑(toLp g hg₄) : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g

Tactic:
exact hg₄.coeFn_toLp

Premises used: MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
⊢ Eq (α := (a : V) → WithLp p V) (⇑(WithLp.equiv p V).symm : (a : V) → WithLp p V) (toLp p)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
K' : Type u_2
K'' : Type u_3
V : Type u_4
V' : Type u_5
V'' : Type u_6
inst : Nontrivial V
⊢ Nontrivial.{u_4} (WithLp p V)

Tactic:
(WithLp.equiv p V).nontrivial

Premises used: WithLp.equiv, Equiv.nontrivial
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
x : V
⊢ (toLp p x).ofLp = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
x : WithLp p V
⊢ toLp p x.ofLp = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
⊢ Function.Surjective.{u_4 + 1, u_4 + 1} (α := WithLp p V) ofLp

Tactic:
Function.RightInverse.surjective <| ofLp_toLp _

Premises used: Function.RightInverse.surjective, WithLp.ofLp_toLp
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
⊢ Function.Surjective.{u_4 + 1, u_4 + 1} (α := V) (toLp p)

Tactic:
Function.RightInverse.surjective <| toLp_ofLp _

Premises used: WithLp.toLp_ofLp, Function.RightInverse.surjective
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
⊢ Function.Injective.{u_4 + 1, u_4 + 1} (α := WithLp p V) ofLp

Tactic:
Function.LeftInverse.injective <| toLp_ofLp _

Premises used: Function.LeftInverse.injective, WithLp.toLp_ofLp
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
⊢ Function.Injective.{u_4 + 1, u_4 + 1} (α := V) (toLp p)

Tactic:
Function.LeftInverse.injective <| ofLp_toLp _

Premises used: Function.LeftInverse.injective, WithLp.ofLp_toLp
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
⊢ Function.Bijective.{u_4 + 1, u_4 + 1} (α := WithLp p V) ofLp

Tactic:
⟨ofLp_injective p, ofLp_surjective p⟩

Premises used: WithLp.ofLp_injective, WithLp.ofLp_surjective, And.intro, Function.Bijective
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
⊢ Function.Bijective.{u_4 + 1, u_4 + 1} (α := V) (toLp p)

Tactic:
⟨toLp_injective p, toLp_surjective p⟩

Premises used: And.intro, WithLp.toLp_surjective, WithLp.toLp_injective, Function.Bijective
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
⊢ Eq.{u_4 + 1} (α := (x : WithLp p V) → WithLp p V) (WithLp.map p id) id

Tactic:
rfl

Premises used: WithLp.map, rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
V' : Type u_5
V'' : Type u_6
f : V' → V''
g : V → V'
⊢ WithLp.map p (f ∘ g) = WithLp.map p f ∘ WithLp.map p g

Tactic:
rfl

Premises used: WithLp.map, rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
V' : Type u_5
f : V ≃ V'
⊢ Eq (α := (a : WithLp p V) → WithLp p V') (⇑(WithLp.congr p f) : (a : WithLp p V) → WithLp p V')
    (WithLp.map p (⇑f : (a : V) → V'))

Tactic:
rfl

Premises used: WithLp.map, rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
⊢ WithLp.congr p (Equiv.refl V) = Equiv.refl (WithLp p V)

Tactic:
rfl

Premises used: WithLp.congr, Equiv.refl, rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
V' : Type u_5
f : V ≃ V'
⊢ (WithLp.congr p f).symm = WithLp.congr p f.symm

Tactic:
rfl

Premises used: Equiv.trans, WithLp.congr, Equiv.symm, rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
V' : Type u_5
V'' : Type u_6
f : V ≃ V'
g : V' ≃ V''
⊢ WithLp.congr p (f.trans g) = (WithLp.congr p f).trans (WithLp.congr p g)

Tactic:
rfl

Premises used: WithLp.equiv, Equiv.trans, WithLp.congr, rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
⊢ Eq.{u_4 + 1} (α := WithLp p V) (toLp p 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
⊢ Eq.{u_4 + 1} (α := V) (ofLp (p := p) 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
x y : V
⊢ toLp p (x + y) = toLp p x + toLp p y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
x y : WithLp p V
⊢ (x + y).ofLp = x.ofLp + y.ofLp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
x y : V
⊢ toLp p (x - y) = toLp p x - toLp p y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
x y : WithLp p V
⊢ (x - y).ofLp = x.ofLp - y.ofLp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
x : V
⊢ toLp p (-x) = -toLp p x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
x : WithLp p V
⊢ (-x).ofLp = -x.ofLp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
x : V
⊢ toLp p x = 0 ↔ x = 0

Tactic:
(toLp_injective p).eq_iff

Premises used: Function.Injective.eq_iff, WithLp.toLp_injective
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
x : WithLp p V
⊢ x.ofLp = 0 ↔ x = 0

Tactic:
(ofLp_injective p).eq_iff

Premises used: Function.Injective.eq_iff, WithLp.ofLp_injective
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
V : Type u_4
inst : SMul K V
c : K
x : V
⊢ toLp p (c • x) = c • toLp p x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
V : Type u_4
inst : SMul K V
c : K
x : WithLp p V
⊢ (c • x).ofLp = c • x.ofLp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
K' : Type u_2
K'' : Type u_3
V : Type u_4
V' : Type u_5
V'' : Type u_6
inst : SMul K K'
inst_1 : SMul K V
inst_2 : SMul K' V
inst_3 : IsScalarTower K K' V
x : K
y : K'
z : WithLp p V
change : toLp p ((x • y) • z.ofLp) = toLp p (x • y • z.ofLp)
⊢ (x • y) • z = x • y • z

Tactic:
change toLp p ((x • y) • (ofLp z)) = toLp p (x • y • ofLp z)

Premises used: WithLp.toLp, HSMul.hSMul, WithLp.ofLp
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
K' : Type u_2
K'' : Type u_3
V : Type u_4
V' : Type u_5
V'' : Type u_6
inst : SMul K K'
inst_1 : SMul K V
inst_2 : SMul K' V
inst_3 : IsScalarTower K K' V
x : K
y : K'
z : WithLp p V
⊢ toLp p ((x • y) • z.ofLp) = toLp p (x • y • z.ofLp)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
K' : Type u_2
K'' : Type u_3
V : Type u_4
V' : Type u_5
V'' : Type u_6
inst : SMul K V
inst_1 : SMul K' V
inst_2 : SMulCommClass K K' V
x : K
y : K'
z : WithLp p V
change : toLp p (x • y • z.ofLp) = toLp p (y • x • z.ofLp)
⊢ x • y • z = y • x • z

Tactic:
change toLp p (x • y • ofLp z) = toLp p (y • x • ofLp z)

Premises used: WithLp.toLp, HSMul.hSMul, WithLp.ofLp
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
K' : Type u_2
K'' : Type u_3
V : Type u_4
V' : Type u_5
V'' : Type u_6
inst : SMul K V
inst_1 : SMul K' V
inst_2 : SMulCommClass K K' V
x : K
y : K'
z : WithLp p V
rw rw₁ : toLp p (y • x • z.ofLp) = toLp p (y • x • z.ofLp)
⊢ toLp p (x • y • z.ofLp) = toLp p (y • x • z.ofLp)

Tactic:
rw [smul_comm]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
⊢ Eq (α := (a : WithLp p V) → V) (⇑(WithLp.addEquiv p V) : (a : WithLp p V) → V) ofLp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
⊢ Eq (α := (a : V) → WithLp p V) (⇑(AddEquiv.symm (WithLp.addEquiv p V)) : (a : V) → WithLp p V) (toLp p)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
ι : Type u_7
s : Finset ι
f : ι → WithLp p V
⊢ Eq.{u_4 + 1} (α := V) (ofLp (p := p) (∑ i ∈ s, f i)) (∑ i ∈ s, (f i).ofLp)

Tactic:
map_sum (WithLp.addEquiv _ _) _ _

Premises used: map_sum, WithLp.addEquiv
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
ι : Type u_7
s : Finset ι
f : ι → V
⊢ Eq.{u_4 + 1} (α := WithLp p V) (toLp p (∑ i ∈ s, f i)) (∑ i ∈ s, toLp p (f i))

Tactic:
map_sum (WithLp.addEquiv _ _).symm _ _

Premises used: map_sum, WithLp.addEquiv, AddEquiv.symm
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
l : List (WithLp p V)
⊢ l.sum.ofLp = (List.map ofLp l).sum

Tactic:
map_list_sum (WithLp.addEquiv _ _) _

Premises used: map_list_sum, WithLp.addEquiv
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
l : List V
⊢ toLp p l.sum = (List.map (toLp p) l).sum

Tactic:
map_list_sum (WithLp.addEquiv _ _).symm _

Premises used: map_list_sum, WithLp.addEquiv, AddEquiv.symm
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
s : Multiset (WithLp p V)
⊢ s.sum.ofLp = (Multiset.map ofLp s).sum

Tactic:
map_multiset_sum (WithLp.addEquiv _ _) _

Premises used: map_multiset_sum, WithLp.addEquiv
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
V : Type u_4
inst : AddCommGroup V
s : Multiset V
⊢ toLp p s.sum = (Multiset.map (toLp p) s).sum

Tactic:
map_multiset_sum (WithLp.addEquiv _ _).symm _

Premises used: map_multiset_sum, WithLp.addEquiv, AddEquiv.symm
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
V : Type u_4
inst : Semiring K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ Eq (α := (a : WithLp p V) → V) (⇑(WithLp.linearEquiv p K V) : (a : WithLp p V) → V) ofLp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
V : Type u_4
inst : Semiring K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ Eq (α := (a : V) → WithLp p V) (⇑(LinearEquiv.symm (WithLp.linearEquiv p K V)) : (a : V) → WithLp p V) (toLp p)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
V : Type u_4
inst : Semiring K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ Eq (α := WithLp p V ≃+ V) (LinearEquiv.toAddEquiv (WithLp.linearEquiv p K V)) (WithLp.addEquiv p V)

Tactic:
rfl

Premises used: WithLp.addEquiv, rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
K' : Type u_2
K'' : Type u_3
V : Type u_4
V' : Type u_5
V'' : Type u_6
inst : Semiring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
⊢ Module.Finite.{u_1, u_4} K (WithLp p V)

Tactic:
Module.Finite.equiv (WithLp.linearEquiv p K V).symm

Premises used: LinearEquiv.symm, Module.Finite.equiv, WithLp.linearEquiv
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
K' : Type u_2
V : Type u_4
V' : Type u_5
inst : Semiring K
inst_1 : Semiring K'
σ : K →+* K'
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : AddCommGroup V'
inst_5 : Module K' V'
f : V →ₛₗ[σ] V'
⊢ Eq (α := (a : WithLp p V) → WithLp p V') (⇑(withLpMap p f) : (a : WithLp p V) → WithLp p V')
    (WithLp.map p (⇑f : (a : V) → V'))

Tactic:
rfl

Premises used: WithLp.map, rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
V : Type u_4
inst : Semiring K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ Eq.{u_4 + 1} (α := WithLp p V →ₗ[K] WithLp p V) (withLpMap p id) id

Tactic:
rfl

Premises used: LinearMap.withLpMap, rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
K' : Type u_2
K'' : Type u_3
V : Type u_4
V' : Type u_5
V'' : Type u_6
inst : Semiring K
inst_1 : Semiring K'
inst_2 : Semiring K''
σ : K →+* K'
τ : K' →+* K''
ρ : K →+* K''
inst_3 : RingHomCompTriple σ τ ρ
inst_4 : AddCommGroup V
inst_5 : Module K V
inst_6 : AddCommGroup V'
inst_7 : Module K' V'
inst_8 : AddCommGroup V''
inst_9 : Module K'' V''
f : V' →ₛₗ[τ] V''
g : V →ₛₗ[σ] V'
⊢ withLpMap p (f ∘ₛₗ g) = withLpMap p f ∘ₛₗ withLpMap p g

Tactic:
rfl

Premises used: LinearMap.withLpMap, rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
K' : Type u_2
V : Type u_4
V' : Type u_5
inst : Semiring K
inst_1 : Semiring K'
σ : K →+* K'
σ' : K' →+* K
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
inst_4 : AddCommGroup V
inst_5 : Module K V
inst_6 : AddCommGroup V'
inst_7 : Module K' V'
f : V ≃ₛₗ[σ] V'
⊢ Eq (α := (a : WithLp p V) → WithLp p V') (⇑(withLpCongr p f) : (a : WithLp p V) → WithLp p V')
    (WithLp.map p (⇑f : (a : V) → V'))

Tactic:
rfl

Premises used: WithLp.map, rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
K' : Type u_2
V : Type u_4
V' : Type u_5
inst : Semiring K
inst_1 : Semiring K'
σ : K →+* K'
σ' : K' →+* K
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
inst_4 : AddCommGroup V
inst_5 : Module K V
inst_6 : AddCommGroup V'
inst_7 : Module K' V'
f : V ≃ₛₗ[σ] V'
⊢ (withLpCongr p f).symm = withLpCongr p f.symm

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.withLpCongr, LinearEquiv.trans, rfl
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
V : Type u_4
inst : Semiring K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ Eq (α := WithLp p V ≃ₗ[K] WithLp p V) (withLpCongr p (refl K V)) (refl K (WithLp p V))

Tactic:
rfl

Premises used: LinearEquiv.withLpCongr, LinearEquiv.refl, LinearEquiv.trans, rfl