awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
rw : (↑(↑(hg.compLp g0 0) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] 0
⊢ Eq (α := ↥(Lp F p μ)) (hg.compLp g0 0) 0

Tactic:
rw [Lp.eq_zero_iff_ae_eq_zero]

Premises used: MeasureTheory.Lp.eq_zero_iff_ae_eq_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
apply : g ∘ (↑(↑0 : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
⊢ (↑(↑(hg.compLp g0 0) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] 0

Tactic:
apply (coeFn_compLp _ _ _).trans

Premises used: Filter.EventuallyEq.trans, LipschitzWith.coeFn_compLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
h :
  ∀ (a : α) (ha : Eq.{u_4 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a)),
    (g ∘ (↑(↑0 : α →ₘ[μ] E) : α → E)) a = 0 a
⊢ g ∘ (↑(↑0 : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0

Tactic:
filter_upwards [Lp.coeFn_zero E p μ] with _ ha

Premises used: MeasureTheory.Lp.coeFn_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
a : α
ha : Eq.{u_4 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a)
⊢ (g ∘ (↑(↑0 : α →ₘ[μ] E) : α → E)) a = 0 a

Tactic:
simp only [ha, g0, Function.comp_apply, Pi.zero_apply]

Premises used: Pi.zero_apply, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : ↥(Lp E p μ)
h :
  ∀ᵐ (x : α) ∂μ,
    ‖(↑(↑(hg.compLp g0 f - hg.compLp g0 f') : α →ₘ[μ] F) : α → F) x‖ ≤ (↑c : ℝ) * ‖(↑(↑(f - f') : α →ₘ[μ] E) : α → E) x‖
⊢ ‖hg.compLp g0 f - hg.compLp g0 f'‖ ≤ (↑c : ℝ) * ‖f - f'‖

Tactic:
apply Lp.norm_le_mul_norm_of_ae_le_mul

Premises used: MeasureTheory.Lp.norm_le_mul_norm_of_ae_le_mul
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : ↥(Lp E p μ)
h :
  ∀ (a : α) (ha1 : (↑(↑(hg.compLp g0 f) : α →ₘ[μ] F) : α → F) a = (g ∘ (↑(↑f : α →ₘ[μ] E) : α → E)) a)
    (ha2 : (↑(↑(hg.compLp g0 f') : α →ₘ[μ] F) : α → F) a = (g ∘ (↑(↑f' : α →ₘ[μ] E) : α → E)) a)
    (ha3 :
      (↑(↑(hg.compLp g0 f - hg.compLp g0 f') : α →ₘ[μ] F) : α → F) a =
        ((↑(↑(hg.compLp g0 f) : α →ₘ[μ] F) : α → F) - (↑(↑(hg.compLp g0 f') : α →ₘ[μ] F) : α → F)) a)
    (ha4 : (↑(↑(f - f') : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑f' : α →ₘ[μ] E) : α → E)) a),
    ‖(↑(↑(hg.compLp g0 f - hg.compLp g0 f') : α →ₘ[μ] F) : α → F) a‖ ≤ (↑c : ℝ) * ‖(↑(↑(f - f') : α →ₘ[μ] E) : α → E) a‖
⊢ ∀ᵐ (x : α) ∂μ,
    ‖(↑(↑(hg.compLp g0 f - hg.compLp g0 f') : α →ₘ[μ] F) : α → F) x‖ ≤ (↑c : ℝ) * ‖(↑(↑(f - f') : α →ₘ[μ] E) : α → E) x‖

Tactic:
filter_upwards [hg.coeFn_compLp g0 f, hg.coeFn_compLp g0 f',
    Lp.coeFn_sub (hg.compLp g0 f) (hg.compLp g0 f'), Lp.coeFn_sub f f'] with a ha1 ha2 ha3 ha4

Premises used: LipschitzWith.coeFn_compLp, MeasureTheory.Lp.coeFn_sub, LipschitzWith.compLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : ↥(Lp E p μ)
a : α
ha1 : (↑(↑(hg.compLp g0 f) : α →ₘ[μ] F) : α → F) a = (g ∘ (↑(↑f : α →ₘ[μ] E) : α → E)) a
ha2 : (↑(↑(hg.compLp g0 f') : α →ₘ[μ] F) : α → F) a = (g ∘ (↑(↑f' : α →ₘ[μ] E) : α → E)) a
ha3 :
  (↑(↑(hg.compLp g0 f - hg.compLp g0 f') : α →ₘ[μ] F) : α → F) a =
    ((↑(↑(hg.compLp g0 f) : α →ₘ[μ] F) : α → F) - (↑(↑(hg.compLp g0 f') : α →ₘ[μ] F) : α → F)) a
ha4 : (↑(↑(f - f') : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑f' : α →ₘ[μ] E) : α → E)) a
h :
  dist (g ((↑(↑f : α →ₘ[μ] E) : α → E) a)) (g ((↑(↑f' : α →ₘ[μ] E) : α → E) a)) ≤
    (↑c : ℝ) * dist ((↑(↑f : α →ₘ[μ] E) : α → E) a) ((↑(↑f' : α →ₘ[μ] E) : α → E) a)
⊢ ‖(↑(↑(hg.compLp g0 f - hg.compLp g0 f') : α →ₘ[μ] F) : α → F) a‖ ≤ (↑c : ℝ) * ‖(↑(↑(f - f') : α →ₘ[μ] E) : α → E) a‖

Tactic:
simp only [ha1, ha2, ha3, ha4, ← dist_eq_norm, Pi.sub_apply, Function.comp_apply]

Premises used: dist_eq_norm, Function.comp_apply, Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : ↥(Lp E p μ)
a : α
ha1 : (↑(↑(hg.compLp g0 f) : α →ₘ[μ] F) : α → F) a = (g ∘ (↑(↑f : α →ₘ[μ] E) : α → E)) a
ha2 : (↑(↑(hg.compLp g0 f') : α →ₘ[μ] F) : α → F) a = (g ∘ (↑(↑f' : α →ₘ[μ] E) : α → E)) a
ha3 :
  (↑(↑(hg.compLp g0 f - hg.compLp g0 f') : α →ₘ[μ] F) : α → F) a =
    ((↑(↑(hg.compLp g0 f) : α →ₘ[μ] F) : α → F) - (↑(↑(hg.compLp g0 f') : α →ₘ[μ] F) : α → F)) a
ha4 : (↑(↑(f - f') : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑f' : α →ₘ[μ] E) : α → E)) a
⊢ dist (g ((↑(↑f : α →ₘ[μ] E) : α → E) a)) (g ((↑(↑f' : α →ₘ[μ] E) : α → E) a)) ≤
    (↑c : ℝ) * dist ((↑(↑f : α →ₘ[μ] E) : α → E) a) ((↑(↑f' : α →ₘ[μ] E) : α → E) a)

Tactic:
hg.dist_le_mul (f a) (f' a)

Premises used: LipschitzWith.dist_le_mul, MeasureTheory.AEEqFun.cast, Subtype.val
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : ↥(Lp E p μ)
a : α
ha1 : (↑(↑(hg.compLp g0 f) : α →ₘ[μ] F) : α → F) a = (g ∘ (↑(↑f : α →ₘ[μ] E) : α → E)) a
ha2 : (↑(↑(hg.compLp g0 f') : α →ₘ[μ] F) : α → F) a = (g ∘ (↑(↑f' : α →ₘ[μ] E) : α → E)) a
ha3 :
  (↑(↑(hg.compLp g0 f - hg.compLp g0 f') : α →ₘ[μ] F) : α → F) a =
    ((↑(↑(hg.compLp g0 f) : α →ₘ[μ] F) : α → F) - (↑(↑(hg.compLp g0 f') : α →ₘ[μ] F) : α → F)) a
ha4 : (↑(↑(f - f') : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) - (↑(↑f' : α →ₘ[μ] E) : α → E)) a
⊢ dist (g ((↑(↑f : α →ₘ[μ] E) : α → E) a)) (g ((↑(↑f' : α →ₘ[μ] E) : α → E) a)) ≤
    (↑c : ℝ) * dist ((↑(↑f : α →ₘ[μ] E) : α → E) a) ((↑(↑f' : α →ₘ[μ] E) : α → E) a)

Tactic:
exact hg.dist_le_mul (f a) (f' a)

Premises used: LipschitzWith.dist_le_mul, MeasureTheory.AEEqFun.cast, Subtype.val
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f : ↥(Lp E p μ)
⊢ ‖hg.compLp g0 f‖ ≤ (↑c : ℝ) * ‖f‖

Tactic:
simpa only [compLp_zero, sub_zero] using hg.norm_compLp_sub_le g0 f 0

Premises used: sub_zero, LipschitzWith.compLp_zero, OfNat.ofNat, LipschitzWith.norm_compLp_sub_le
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g_1 : E → F
c : ℝ≥0
inst_2 : Fact (1 ≤ p)
hg : LipschitzWith c g_1
g0 : g_1 0 = 0
f g : ↥(Lp E p μ)
⊢ dist (hg.compLp g0 f) (hg.compLp g0 g) ≤ (↑c : ℝ) * dist f g

Tactic:
simp only [dist_eq_norm, norm_compLp_sub_le]

Premises used: dist_eq_norm, LipschitzWith.norm_compLp_sub_le
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c : ℝ≥0
inst_2 : Fact (1 ≤ p)
hg : LipschitzWith c g
g0 : g 0 = 0
⊢ Continuous (X := ↥(Lp E p μ)) (hg.compLp g0)

Tactic:
(lipschitzWith_compLp hg g0).continuous

Premises used: LipschitzWith.lipschitzWith_compLp, LipschitzWith.continuous
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ ∀ᵐ (a : α) ∂μ, (↑(↑(L.compLp f) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a)

Tactic:
LipschitzWith.coeFn_compLp _ _ _

Premises used: Filter.EventuallyEq, LipschitzWith.coeFn_compLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ (↑(↑(L.compLp f) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] fun (a : α) ↦ (L : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a)

Tactic:
L.coeFn_compLp f

Premises used: Filter.EventuallyEq, ContinuousLinearMap.coeFn_compLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ MemLp.{u_1, u_5} (ε := F) ((⇑L : (a : E) → F) ∘ (↑(↑f : α →ₘ[μ] E) : α → E)) p μ

Tactic:
(Lp.memLp (L.compLp f)).ae_eq (L.coeFn_compLp' f)

Premises used: MeasureTheory.Lp.memLp, ContinuousLinearMap.compLp, MeasureTheory.MemLp.ae_eq, ContinuousLinearMap.coeFn_compLp'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L : E →SL[σ] F
f : α → E
hf : MemLp f p μ
⊢ MemLp.{u_1, u_5} (ε := F) ((⇑L : (a : E) → F) ∘ f) p μ

Tactic:
(L.comp_memLp (hf.toLp f)).ae_eq (EventuallyEq.fun_comp hf.coeFn_toLp _)

Premises used: ContinuousLinearMap.comp_memLp, MeasureTheory.MemLp.toLp, MeasureTheory.MemLp.coeFn_toLp, MeasureTheory.MemLp.ae_eq, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst : RCLike K
f : α → ℝ
hf : MemLp f p μ
⊢ MemLp.{u_1, u_8} (ε := K) (fun (x : α) ↦ (↑(f x) : K)) p μ

Tactic:
(@RCLike.ofRealCLM K _).comp_memLp' hf

Premises used: RCLike.ofRealCLM, ContinuousLinearMap.comp_memLp'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst : RCLike K
f : α → K
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : K) → ℝ) (f x)) p μ ∧
      MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : K) → ℝ) (f x)) p μ ↔
    MemLp f p μ

Tactic:
⟨?_, fun hf => ⟨hf.re, hf.im⟩⟩

Premises used: MeasureTheory.MemLp.re, And.intro, Iff.intro, MeasureTheory.MemLp.im
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst : RCLike K
f : α → K
refine :
  MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : K) → ℝ) (f x)) p μ ∧
      MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : K) → ℝ) (f x)) p μ →
    MemLp f p μ
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : K) → ℝ) (f x)) p μ ∧
      MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : K) → ℝ) (f x)) p μ ↔
    MemLp f p μ

Tactic:
refine ⟨?_, fun hf => ⟨hf.re, hf.im⟩⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst : RCLike K
f : α → K
hre : MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : K) → ℝ) (f x)) p μ
him : MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : K) → ℝ) (f x)) p μ
⊢ MemLp
    (HAdd.hAdd (α := α → K) (fun (x : α) ↦ (↑((RCLike.re : (a : K) → ℝ) (f x)) : K)) fun (x : α) ↦
      HMul.hMul (α := K) RCLike.I (↑((RCLike.im : (a : K) → ℝ) (f x)) : K))
    p μ

Tactic:
MeasureTheory.MemLp.add (ε := K) hre.ofReal (him.ofReal.const_mul RCLike.I)

Premises used: MeasureTheory.MemLp.const_mul, MeasureTheory.MemLp.add, RCLike.I, MeasureTheory.MemLp.ofReal
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst : RCLike K
f : α → K
hre : MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : K) → ℝ) (f x)) p μ
him : MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : K) → ℝ) (f x)) p μ
h :
  f =
    HAdd.hAdd (α := α → K) (fun (x : α) ↦ (↑((RCLike.re : (a : K) → ℝ) (f x)) : K)) fun (x : α) ↦
      HMul.hMul (α := K) RCLike.I (↑((RCLike.im : (a : K) → ℝ) (f x)) : K)
⊢ MemLp f p μ

Tactic:
convert! MeasureTheory.MemLp.add (ε := K) hre.ofReal (him.ofReal.const_mul RCLike.I)

Premises used: MeasureTheory.MemLp.const_mul, MeasureTheory.MemLp.add, RCLike.I, MeasureTheory.MemLp.ofReal
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst : RCLike K
f : α → K
hre : MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : K) → ℝ) (f x)) p μ
him : MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : K) → ℝ) (f x)) p μ
h :
  ∀ (x : α),
    f x =
      HAdd.hAdd (α := α → K) (β := α → K) (fun (x : α) ↦ (↑((RCLike.re : (a : K) → ℝ) (f x)) : K))
        (fun (x : α) ↦ HMul.hMul (α := K) RCLike.I (↑((RCLike.im : (a : K) → ℝ) (f x)) : K)) x
⊢ f =
    HAdd.hAdd (α := α → K) (fun (x : α) ↦ (↑((RCLike.re : (a : K) → ℝ) (f x)) : K)) fun (x : α) ↦
      HMul.hMul (α := K) RCLike.I (↑((RCLike.im : (a : K) → ℝ) (f x)) : K)

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst : RCLike K
f : α → K
hre : MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : K) → ℝ) (f x)) p μ
him : MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : K) → ℝ) (f x)) p μ
x : α
h :
  f x = (↑((RCLike.re : (a : K) → ℝ) (f x)) : K) + HMul.hMul (α := K) RCLike.I (↑((RCLike.im : (a : K) → ℝ) (f x)) : K)
h₁ :
  f x = (↑((RCLike.re : (a : K) → ℝ) (f x)) : K) + HMul.hMul (α := K) (↑((RCLike.im : (a : K) → ℝ) (f x)) : K) RCLike.I
h₂ h₃ : f x = f x
⊢ f x =
    HAdd.hAdd (α := α → K) (β := α → K) (fun (x : α) ↦ (↑((RCLike.re : (a : K) → ℝ) (f x)) : K))
      (fun (x : α) ↦ HMul.hMul (α := K) RCLike.I (↑((RCLike.im : (a : K) → ℝ) (f x)) : K)) x

Tactic:
rw [Pi.add_apply, mul_comm, RCLike.re_add_im]

Premises used: RCLike.re_add_im, Pi.add_apply, mul_comm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L L' : E →SL[σ] F
f : ↥(Lp E p μ)
h : (↑(↑((L + L').compLp f) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(L.compLp f + L'.compLp f) : α →ₘ[μ] F) : α → F)
⊢ (L + L').compLp f = L.compLp f + L'.compLp f

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L L' : E →SL[σ] F
f : ↥(Lp E p μ)
h :
  EventuallyEq.{u_1, u_5} (β := F) (ae μ) (fun (a : α) ↦ (L + L' : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a))
    fun (a : α) ↦ (L + L' : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a)
⊢ (↑(↑((L + L').compLp f) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(L.compLp f + L'.compLp f) : α →ₘ[μ] F) : α → F)

Tactic:
grw [Lp.coeFn_add, coeFn_compLp', coeFn_compLp', coeFn_compLp']

Premises used: MeasureTheory.Lp.coeFn_add, ContinuousLinearMap.coeFn_compLp'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L L' : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ EventuallyEq.{u_1, u_5} (β := F) (ae μ) (fun (a : α) ↦ (L + L' : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a))
    fun (a : α) ↦ (L + L' : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
𝕜'' : Type u_8
inst_7 : NormedRing 𝕜''
inst_8 : Module 𝕜'' F
inst_9 : IsBoundedSMul 𝕜'' F
inst_10 : SMulCommClass 𝕜' 𝕜'' F
c : 𝕜''
L : E →SL[σ] F
f : ↥(Lp E p μ)
h : (↑(↑((c • L).compLp f) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(c • L.compLp f) : α →ₘ[μ] F) : α → F)
⊢ (c • L).compLp f = c • L.compLp f

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
𝕜'' : Type u_8
inst_7 : NormedRing 𝕜''
inst_8 : Module 𝕜'' F
inst_9 : IsBoundedSMul 𝕜'' F
inst_10 : SMulCommClass 𝕜' 𝕜'' F
c : 𝕜''
L : E →SL[σ] F
f : ↥(Lp E p μ)
h :
  EventuallyEq.{u_1, u_5} (β := F) (ae μ) (fun (a : α) ↦ (c • L : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a))
    fun (a : α) ↦ (c • L : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a)
⊢ (↑(↑((c • L).compLp f) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(c • L.compLp f) : α →ₘ[μ] F) : α → F)

Tactic:
grw [Lp.coeFn_smul, coeFn_compLp', coeFn_compLp']

Premises used: MeasureTheory.Lp.coeFn_smul, ContinuousLinearMap.coeFn_compLp'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
𝕜'' : Type u_8
inst_7 : NormedRing 𝕜''
inst_8 : Module 𝕜'' F
inst_9 : IsBoundedSMul 𝕜'' F
inst_10 : SMulCommClass 𝕜' 𝕜'' F
c : 𝕜''
L : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ EventuallyEq.{u_1, u_5} (β := F) (ae μ) (fun (a : α) ↦ (c • L : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a))
    fun (a : α) ↦ (c • L : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ ‖L.compLp f‖ ≤ ‖L‖ * ‖f‖

Tactic:
LipschitzWith.norm_compLp_le _ _ _

Premises used: LipschitzWith.norm_compLp_le, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g_1 : E → F
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L : E →SL[σ] F
f g : ↥(Lp E p μ)
h : (↑(↑(L.compLp (f + g)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(L.compLp f + L.compLp g) : α →ₘ[μ] F) : α → F)
⊢ L.compLp (f + g) = L.compLp f + L.compLp g

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g_1 : E → F
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L : E →SL[σ] F
f g : ↥(Lp E p μ)
h :
  ∀ (a : α),
    (↑(↑(f + g) : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) a →
      (↑(↑(L.compLp (f + g)) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑(f + g) : α →ₘ[μ] E) : α → E) a) →
        (↑(↑(L.compLp f) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a) →
          (↑(↑(L.compLp g) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑g : α →ₘ[μ] E) : α → E) a) →
            (↑(↑(L.compLp f + L.compLp g) : α →ₘ[μ] F) : α → F) a =
                ((↑(↑(L.compLp f) : α →ₘ[μ] F) : α → F) + (↑(↑(L.compLp g) : α →ₘ[μ] F) : α → F)) a →
              (↑(↑(L.compLp (f + g)) : α →ₘ[μ] F) : α → F) a = (↑(↑(L.compLp f + L.compLp g) : α →ₘ[μ] F) : α → F) a
⊢ (↑(↑(L.compLp (f + g)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(L.compLp f + L.compLp g) : α →ₘ[μ] F) : α → F)

Tactic:
filter_upwards [Lp.coeFn_add f g, coeFn_compLp L (f + g), coeFn_compLp L f,
      coeFn_compLp L g, Lp.coeFn_add (L.compLp f) (L.compLp g)]

Premises used: MeasureTheory.Lp.coeFn_add, ContinuousLinearMap.compLp, HAdd.hAdd, ContinuousLinearMap.coeFn_compLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g_1 : E → F
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L : E →SL[σ] F
f g : ↥(Lp E p μ)
a : α
ha1 : (↑(↑(f + g) : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) a
ha2 : (↑(↑(L.compLp (f + g)) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑(f + g) : α →ₘ[μ] E) : α → E) a)
ha3 : (↑(↑(L.compLp f) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a)
ha4 : (↑(↑(L.compLp g) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑g : α →ₘ[μ] E) : α → E) a)
ha5 :
  (↑(↑(L.compLp f + L.compLp g) : α →ₘ[μ] F) : α → F) a =
    ((↑(↑(L.compLp f) : α →ₘ[μ] F) : α → F) + (↑(↑(L.compLp g) : α →ₘ[μ] F) : α → F)) a
⊢ (↑(↑(L.compLp (f + g)) : α →ₘ[μ] F) : α → F) a = (↑(↑(L.compLp f + L.compLp g) : α →ₘ[μ] F) : α → F) a

Tactic:
simp only [ha1, ha2, ha3, ha4, ha5, map_add, Pi.add_apply]

Premises used: map_add, Pi.add_apply