awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
h₁ : p = p / q * q⁻¹⁻¹
h₂ : p = p / q * q
h₃ : p = p * q⁻¹ * q
h₄ : p = p * (q⁻¹ * q)
h₅ : p = p * 1
⊢ p = p / q / q⁻¹
have h₆ : p = p
Tactic: rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) 1 μ
have h : 1 = p / p
Tactic: convert! hf.enorm_rpow_div p
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ 1 = p / p
have h : 1 = p * p⁻¹
Tactic: rw [div_eq_mul_inv, ENNReal.mul_inv_cancel hp_ne_zero hp_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
h : 1 = p * p⁻¹
⊢ 1 = p / p
have h₁ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [div_eq_mul_inv, ENNReal.mul_inv_cancel hp_ne_zero hp_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) 1 μ
have h : 1 = p / p
Tactic: convert! hf.norm_rpow_div p
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ 1 = p / p
have h : 1 = p * p⁻¹
Tactic: rw [div_eq_mul_inv, ENNReal.mul_inv_cancel hp_ne_zero hp_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
h : 1 = p * p⁻¹
⊢ 1 = p / p
have h₁ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [div_eq_mul_inv, ENNReal.mul_inv_cancel hp_ne_zero hp_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
β : Type u_7
inst_1 : MeasurableSpace β
μb : Measure β
g : β →ₘ[μb] E
hg : Membership.mem (γ := AddSubgroup (β →ₘ[μb] E)) (Lp E p μb) g
f : α → β
hf : MeasurePreserving f μ μb
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) (g.compMeasurePreserving f hf)
have rw : ∀ (hg : eLpNorm (↑g : β → E) p μb < ∞) {f : α → β} (hf : MeasurePreserving f μ μb),
  eLpNorm (↑(g.compMeasurePreserving f hf) : α → E) p μ < ∞
Tactic: rw [Lp.mem_Lp_iff_eLpNorm_lt_top] at hg ⊢
Cleared hypotheses: hg, f, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
E : Type u_4
p : ℝ≥0∞
inst : NormedAddCommGroup E
β : Type u_7
inst_1 : MeasurableSpace β
μb : Measure β
⊢ Eq (α := ↥(Lp E p μb) →+ ↥(Lp E p μb)) (compMeasurePreserving id ⋯) (AddMonoidHom.id ↥(Lp E p μb))
have h : ∀ (x : ↥(Lp E p μb)),
  EventuallyEq.{u_7, u_4} (β := E) (ae μb)
    (↑(↑((compMeasurePreserving id sorry : (a : ↥(Lp E p μb)) → ↥(Lp E p μb)) x) : β →ₘ[μb] E) : β → E)
    (↑(↑((AddMonoidHom.id ↥(Lp E p μb) : (a : ↥(Lp E p μb)) → ↥(Lp E p μb)) x) : β →ₘ[μb] E) : β → E)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
β : Type u_7
inst_1 : MeasurableSpace β
μb : Measure β
γ : Type u_8
mγ : MeasurableSpace γ
μc : Measure γ
f : β → γ
hf : MeasurePreserving f μb μc
f' : α → β
hf' : MeasurePreserving f' μ μb
⊢ Eq (α := ↥(Lp E p μc) →+ ↥(Lp E p μ)) (compMeasurePreserving (f ∘ f') ⋯)
    (AddMonoidHom.comp (compMeasurePreserving f' hf') (compMeasurePreserving f hf))
have h : ∀ (g : ↥(Lp E p μc)),
  EventuallyEq.{u_1, u_4} (β := E) (ae μ)
    (↑(↑((compMeasurePreserving (f ∘ f') sorry : (a : ↥(Lp E p μc)) → ↥(Lp E p μ)) g) : α →ₘ[μ] E) : α → E)
    (↑(↑((AddMonoidHom.comp (compMeasurePreserving f' hf') (compMeasurePreserving f hf) :
                (a : ↥(Lp E p μc)) → ↥(Lp E p μ))
              g) :
          α →ₘ[μ] E) :
      α → E)
Tactic: ext g
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → α
hf : MeasurePreserving f μ μ
n : ℕ
⊢ Eq (α := ↥(Lp E p μ) → ↥(Lp E p μ)) (⇑(compMeasurePreserving f hf) : (a : ↥(Lp E p μ)) → ↥(Lp E p μ))^[n]
    (⇑(compMeasurePreserving f^[n] ⋯) : (a : ↥(Lp E p μ)) → ↥(Lp E p μ))
have h : ∀ (x : ↥(Lp E p μ)),
  (⇑(compMeasurePreserving f hf) : (a : ↥(Lp E p μ)) → ↥(Lp E p μ))^[n] x =
    (compMeasurePreserving f^[n] sorry : (a : ↥(Lp E p μ)) → ↥(Lp E p μ)) x
Tactic: funext
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → α
hf : MeasurePreserving f μ μ
x : ↥(Lp E p μ)
n : ℕ
h :
  (⇑(compMeasurePreserving f hf) : (a : ↥(Lp E p μ)) → ↥(Lp E p μ))^[n] x =
    (compMeasurePreserving f^[n] ⋯ : (a : ↥(Lp E p μ)) → ↥(Lp E p μ)) x
⊢ (⇑(compMeasurePreserving f hf) : (a : ↥(Lp E p μ)) → ↥(Lp E p μ))^[n + 1] x =
    (compMeasurePreserving f^[n + 1] ⋯ : (a : ↥(Lp E p μ)) → ↥(Lp E p μ)) x
have h₁ : (⇑(compMeasurePreserving f hf) : (a : ↥(Lp E p μ)) → ↥(Lp E p μ))^[1 + n] x =
  (compMeasurePreserving f^[n + 1] sorry : (a : ↥(Lp E p μ)) → ↥(Lp E p μ)) x
Tactic: nth_rewrite 1 [add_comm n 1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → α
hf : MeasurePreserving f μ μ
n : ℕ
x : ↥(Lp E p μ)
⊢ (⇑(compMeasurePreserving f hf) : (a : ↥(Lp E p μ)) → ↥(Lp E p μ))^[n] x =
    (compMeasurePreserving f^[n] ⋯ : (a : ↥(Lp E p μ)) → ↥(Lp E p μ)) x
have h : (⇑(compMeasurePreserving f hf) : (a : ↥(Lp E p μ)) → ↥(Lp E p μ))^[0] x =
  (compMeasurePreserving f^[0] sorry : (a : ↥(Lp E p μ)) → ↥(Lp E p μ)) x
Tactic: induction n with
  | zero => simp
  | succ n h =>
    nth_rewrite 1 [add_comm n 1]
    simp [Function.iterate_add, h, compMeasurePreserving_comp (hf.iterate n) hf]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → α
hf : MeasurePreserving f μ μ
n : ℕ
x : ↥(Lp E p μ)
h :
  (⇑(compMeasurePreserving f hf) : (a : ↥(Lp E p μ)) → ↥(Lp E p μ))^[0] x =
    (compMeasurePreserving f^[0] ⋯ : (a : ↥(Lp E p μ)) → ↥(Lp E p μ)) x
⊢ (⇑(compMeasurePreserving f hf) : (a : ↥(Lp E p μ)) → ↥(Lp E p μ))^[n] x =
    (compMeasurePreserving f^[n] ⋯ : (a : ↥(Lp E p μ)) → ↥(Lp E p μ)) x
have h₁ : ∀ (n : ℕ)
  (h :
    (⇑(compMeasurePreserving f hf) : (a : ↥(Lp E p μ)) → ↥(Lp E p μ))^[n] x =
      (compMeasurePreserving f^[n] sorry : (a : ↥(Lp E p μ)) → ↥(Lp E p μ)) x),
  (⇑(compMeasurePreserving f hf) : (a : ↥(Lp E p μ)) → ↥(Lp E p μ))^[n + 1] x =
    (compMeasurePreserving f^[n + 1] sorry : (a : ↥(Lp E p μ)) → ↥(Lp E p μ)) x
Tactic: induction n with
  | zero => simp
  | succ n h =>
    nth_rewrite 1 [add_comm n 1]
    simp [Function.iterate_add, h, compMeasurePreserving_comp (hf.iterate n) hf]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
ε : Type u_6
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
β : Type u_7
inst_4 : MeasurableSpace β
μb : Measure β
f_1 : α → β
𝕜 : Type u_8
inst_5 : NormedRing 𝕜
inst_6 : Module 𝕜 E
inst_7 : IsBoundedSMul 𝕜 E
f : α → β
hf : MeasurePreserving f μ μb
c : 𝕜
g : ↥(Lp E p μb)
⊢ ZeroHom.toFun (↑(compMeasurePreserving f hf) : ZeroHom ↥(Lp E p μb) ↥(Lp E p μ)) (c • g) =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (ZeroHom.toFun (↑(compMeasurePreserving f hf) : ZeroHom ↥(Lp E p μb) ↥(Lp E p μ)) g)
have mk : ∀ (val : β →ₘ[μb] E) (a : { f : β → E // AEStronglyMeasurable f μb })
  (property :
    Membership.mem (γ := AddSubgroup (β →ₘ[μb] E)) (Lp E p μb)
      (Quot.mk
        (⇑(Measure.aeEqSetoid E μb) :
          { f : β → E // AEStronglyMeasurable f μb } → { f : β → E // AEStronglyMeasurable f μb } → Prop)
        a)),
  ZeroHom.toFun (↑(compMeasurePreserving f hf) : ZeroHom ↥(Lp E p μb) ↥(Lp E p μ))
      (c •
        Subtype.mk (p := fun (x : β →ₘ[μb] E) ↦ Membership.mem (γ := AddSubgroup (β →ₘ[μb] E)) (Lp E p μb) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μb) :
              { f : β → E // AEStronglyMeasurable f μb } → { f : β → E // AEStronglyMeasurable f μb } → Prop)
            a)
          property) =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (ZeroHom.toFun (↑(compMeasurePreserving f hf) : ZeroHom ↥(Lp E p μb) ↥(Lp E p μ))
        (Subtype.mk (p := fun (x : β →ₘ[μb] E) ↦ Membership.mem (γ := AddSubgroup (β →ₘ[μb] E)) (Lp E p μb) x)
          (Quot.mk
            (⇑(Measure.aeEqSetoid E μb) :
              { f : β → E // AEStronglyMeasurable f μb } → { f : β → E // AEStronglyMeasurable f μb } → Prop)
            a)
          property))
Tactic: rcases g with ⟨⟨_⟩, _⟩
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
p : ℝ≥0∞
α : Type u_6
E : Type u_7
F : Type u_8
K' : ℝ≥0
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
f : α → E
g : E → F
hL : MemLp (g ∘ f) p μ
hg : UniformContinuous g
hg' : AntilipschitzWith K' g
g0 : g 0 = 0
x : α
⊢ ‖f x‖ ≤ (↑K' : ℝ) * ‖g (f x)‖
have rw : dist (f x) 0 ≤ (↑K' : ℝ) * dist (g (f x)) (g 0)
Tactic: rw [← dist_zero_right, ← dist_zero_right, ← g0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (hypothesis)
Goal:
p : ℝ≥0∞
α : Type u_6
E : Type u_7
F : Type u_8
K' : ℝ≥0
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
f : α → E
g : E → F
hL : MemLp (g ∘ f) p μ
hg : UniformContinuous g
hg' : AntilipschitzWith K' g
g0 : g 0 = 0
⊢ MemLp f p μ
have A : ∀ (x : α), ‖f x‖ ≤ (↑K' : ℝ) * ‖g (f x)‖
Tactic: have A : ∀ x, ‖f x‖ ≤ K' * ‖g (f x)‖ := by
    intro x
    -- TODO: add `AntilipschitzWith.le_mul_nnnorm_sub` and `AntilipschitzWith.le_mul_norm`
    rw [← dist_zero_right, ← dist_zero_right, ← g0]
    apply hg'.le_mul_dist
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (hypothesis)
Goal:
p : ℝ≥0∞
α : Type u_6
E : Type u_7
F : Type u_8
K' : ℝ≥0
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
f : α → E
g : E → F
hL : MemLp (g ∘ f) p μ
hg : UniformContinuous g
hg' : AntilipschitzWith K' g
g0 : g 0 = 0
A : ∀ (x : α), ‖f x‖ ≤ (↑K' : ℝ) * ‖g (f x)‖
⊢ MemLp f p μ
have B : AEStronglyMeasurable f μ
Tactic: have B : AEStronglyMeasurable f μ :=
    (hg'.isUniformEmbedding hg).isEmbedding.aestronglyMeasurable_comp_iff.1 hL.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
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 μ)
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] F)) (Lp F p μ) (AEEqFun.comp g ⋯ (↑f : α →ₘ[μ] E))
have rw : MemLp (↑(AEEqFun.comp g sorry (↑f : α →ₘ[μ] E)) : α → F) p μ
Tactic: rw [Lp.mem_Lp_iff_memLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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
⊢ Eq (α := ↥(Lp F p μ)) (hg.compLp g0 0) 0
have rw : (↑(↑(hg.compLp g0 0) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] 0
Tactic: rw [Lp.eq_zero_iff_ae_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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
⊢ (↑(↑(hg.compLp g0 0) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] 0
have apply : g ∘ (↑(↑0 : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
Tactic: apply (coeFn_compLp _ _ _).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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
⊢ g ∘ (↑(↑0 : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
have h : ∀ (a : α) (ha : Eq.{u_4 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a)), (g ∘ (↑(↑0 : α →ₘ[μ] E) : α → E)) a = 0 a
Tactic: filter_upwards [Lp.coeFn_zero E p μ] with _ ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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 μ)
⊢ ‖hg.compLp g0 f - hg.compLp g0 f'‖ ≤ (↑c : ℝ) * ‖f - f'‖
have h : ∀ᵐ (x : α) ∂μ,
  ‖(↑(↑(hg.compLp g0 f - hg.compLp g0 f') : α →ₘ[μ] F) : α → F) x‖ ≤ (↑c : ℝ) * ‖(↑(↑(f - f') : α →ₘ[μ] E) : α → E) x‖
Tactic: apply Lp.norm_le_mul_norm_of_ae_le_mul
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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 μ)
⊢ ∀ᵐ (x : α) ∂μ,
    ‖(↑(↑(hg.compLp g0 f - hg.compLp g0 f') : α →ₘ[μ] F) : α → F) x‖ ≤ (↑c : ℝ) * ‖(↑(↑(f - f') : α →ₘ[μ] E) : α → E) x‖
have 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‖
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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
⊢ ‖(↑(↑(hg.compLp g0 f - hg.compLp g0 f') : α →ₘ[μ] F) : α → F) a‖ ≤ (↑c : ℝ) * ‖(↑(↑(f - f') : α →ₘ[μ] E) : α → E) a‖
have h : dist (g ((↑(↑f : α →ₘ[μ] E) : α → E) a)) (g ((↑(↑f' : α →ₘ[μ] E) : α → E) a)) ≤
  (↑c : ℝ) * dist ((↑(↑f : α →ₘ[μ] E) : α → E) a) ((↑(↑f' : α →ₘ[μ] E) : α → E) a)
Tactic: simp only [ha1, ha2, ha3, ha4, ← dist_eq_norm, Pi.sub_apply, Function.comp_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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 μ
have refine : 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⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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 f p μ
have 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)
Tactic: convert! MeasureTheory.MemLp.add (ε := K) hre.ofReal (him.ofReal.const_mul RCLike.I)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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 μ
⊢ 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)
have 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
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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 : α
⊢ 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
have h : f x = (↑((RCLike.re : (a : K) → ℝ) (f x)) : K) + HMul.hMul (α := K) RCLike.I (↑((RCLike.im : (a : K) → ℝ) (f x)) : K)
Tactic: rw [Pi.add_apply, mul_comm, RCLike.re_add_im]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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)
⊢ 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
have h₁ : f x = (↑((RCLike.re : (a : K) → ℝ) (f x)) : K) + HMul.hMul (α := K) (↑((RCLike.im : (a : K) → ℝ) (f x)) : K) RCLike.I
Tactic: rw [Pi.add_apply, mul_comm, RCLike.re_add_im]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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
⊢ 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
have h₂ : f x = f x
Tactic: rw [Pi.add_apply, mul_comm, RCLike.re_add_im]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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 μ)
⊢ (L + L').compLp f = L.compLp f + L'.compLp f
have h : (↑(↑((L + L').compLp f) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(L.compLp f + L'.compLp f) : α →ₘ[μ] F) : α → F)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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 μ)
⊢ (↑(↑((L + L').compLp f) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(L.compLp f + L'.compLp f) : α →ₘ[μ] F) : α → F)
have 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)
Tactic: grw [Lp.coeFn_add, coeFn_compLp', coeFn_compLp', coeFn_compLp']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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 μ)
⊢ (c • L).compLp f = c • L.compLp f
have h : (↑(↑((c • L).compLp f) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(c • L.compLp f) : α →ₘ[μ] F) : α → F)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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 μ)
⊢ (↑(↑((c • L).compLp f) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(c • L.compLp f) : α →ₘ[μ] F) : α → F)
have 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)
Tactic: grw [Lp.coeFn_smul, coeFn_compLp', coeFn_compLp']