awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
ε : Type u_6
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
β : Type u_7
inst_4 : MeasurableSpace β
μb : Measure β
f_1 f : α → β
hf : MeasurePreserving f μ μb
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)
val_1 : β →ₘ[μb] E
a_1 : { f : β → E // AEStronglyMeasurable f μb }
property_1 :
  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_1)
⊢ Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
      ((↑(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 +
                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_1)
                  property_1) :
            β →ₘ[μb] E).compMeasurePreserving
        f hf)
      ⋯ =
    Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
        ((↑(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) :
              β →ₘ[μb] E).compMeasurePreserving
          f hf)
        ⋯ +
      Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
        ((↑(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_1)
                  property_1) :
              β →ₘ[μb] E).compMeasurePreserving
          f hf)
        ⋯

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
β : Type u_7
inst_1 : MeasurableSpace β
μb : Measure β
f : α → β
g : ↥(Lp E p μb)
hf : MeasurePreserving f μ μb
⊢ (↑((compMeasurePreserving f hf : (a : ↥(Lp E p μb)) → ↥(Lp E p μ)) g) : α →ₘ[μ] E) =
    (↑g : β →ₘ[μb] E).compMeasurePreserving f hf

Tactic:
rfl

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.compMeasurePreserving, MeasureTheory.AEEqFun.compQuasiMeasurePreserving, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
β : Type u_7
inst_1 : MeasurableSpace β
μb : Measure β
f : α → β
g : ↥(Lp E p μb)
hf : MeasurePreserving f μ μb
⊢ (↑(↑((compMeasurePreserving f hf : (a : ↥(Lp E p μb)) → ↥(Lp E p μ)) g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑g : β →ₘ[μb] E) : β → E) ∘ f

Tactic:
g.1.coeFn_compMeasurePreserving hf

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.compMeasurePreserving, MeasureTheory.AEEqFun.coeFn_compMeasurePreserving, MeasureTheory.AEEqFun.compQuasiMeasurePreserving, Subtype.val
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
β : Type u_7
inst_1 : MeasurableSpace β
μb : Measure β
f : α → β
g : ↥(Lp E p μb)
hf : MeasurePreserving f μ μb
⊢ norm (E := ↥(Lp E p μ)) ((compMeasurePreserving f hf : (a : ↥(Lp E p μb)) → ↥(Lp E p μ)) g : ↥(Lp E p μ)) = ‖g‖

Tactic:
congr_arg ENNReal.toReal <| g.1.eLpNorm_compMeasurePreserving hf

Premises used: congr_arg, ENNReal.toReal, MeasureTheory.AEEqFun.eLpNorm_compMeasurePreserving, Subtype.val
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
β : Type u_7
inst_1 : MeasurableSpace β
μb : Measure β
f : α → β
inst_2 : Fact (1 ≤ p)
hf : MeasurePreserving f μ μb
⊢ Isometry (α := ↥(Lp E p μb)) (β := ↥(Lp E p μ)) (⇑(compMeasurePreserving f hf) : (a : ↥(Lp E p μb)) → ↥(Lp E p μ))

Tactic:
AddMonoidHomClass.isometry_of_norm _ (norm_compMeasurePreserving · hf)

Premises used: AddMonoidHomClass.isometry_of_norm, MeasureTheory.Lp.norm_compMeasurePreserving
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
β : Type u_7
inst_1 : MeasurableSpace β
μb : Measure β
f : α → β
g : β → E
hg : MemLp g p μb
hf : MeasurePreserving f μ μb
⊢ (compMeasurePreserving f hf : (a : ↥(Lp E p μb)) → ↥(Lp E p μ)) (MemLp.toLp g hg) = MemLp.toLp (g ∘ f) ⋯

Tactic:
rfl

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.compMeasurePreserving, MeasureTheory.MemLp.toLp, MeasureTheory.AEEqFun.compQuasiMeasurePreserving, rfl, MeasureTheory.AEEqFun.mk
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
E : Type u_4
p : ℝ≥0∞
inst : NormedAddCommGroup E
β : Type u_7
inst_1 : MeasurableSpace β
μb : Measure β
h :
  ∀ (x : ↥(Lp E p μb)),
    EventuallyEq.{u_7, u_4} (β := E) (ae μb)
      (↑(↑((compMeasurePreserving id ⋯ : (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)
⊢ Eq (α := ↥(Lp E p μb) →+ ↥(Lp E p μb)) (compMeasurePreserving id ⋯) (AddMonoidHom.id ↥(Lp E p μb))

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
E : Type u_4
p : ℝ≥0∞
inst : NormedAddCommGroup E
β : Type u_7
inst_1 : MeasurableSpace β
μb : Measure β
x : ↥(Lp E p μb)
⊢ EventuallyEq.{u_7, u_4} (β := E) (ae μb)
    (↑(↑((compMeasurePreserving id ⋯ : (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:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
E : Type u_4
p : ℝ≥0∞
inst : NormedAddCommGroup E
β : Type u_7
inst_1 : MeasurableSpace β
μb : Measure β
g : ↥(Lp E p μb)
⊢ (compMeasurePreserving id ⋯ : (a : ↥(Lp E p μb)) → ↥(Lp E p μb)) g = g

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
h :
  ∀ (g : ↥(Lp E p μc)),
    EventuallyEq.{u_1, u_4} (β := E) (ae μ)
      (↑(↑((compMeasurePreserving (f ∘ f') ⋯ : (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)
⊢ Eq (α := ↥(Lp E p μc) →+ ↥(Lp E p μ)) (compMeasurePreserving (f ∘ f') ⋯)
    (AddMonoidHom.comp (compMeasurePreserving f' hf') (compMeasurePreserving f hf))

Tactic:
ext g
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
g : ↥(Lp E p μc)
⊢ EventuallyEq.{u_1, u_4} (β := E) (ae μ)
    (↑(↑((compMeasurePreserving (f ∘ f') ⋯ : (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:
simp [AEEqFun.compMeasurePreserving_comp _ hf hf']

Premises used: MeasureTheory.AEEqFun.compMeasurePreserving_comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 γ
g : ↥(Lp E p μc)
f : β → γ
hf : MeasurePreserving f μb μc
f' : α → β
hf' : MeasurePreserving f' μ μb
⊢ Eq (α := ↥(Lp E p μ)) ((compMeasurePreserving (f ∘ f') ⋯ : (a : ↥(Lp E p μc)) → ↥(Lp E p μ)) g : ↥(Lp E p μ))
    ((compMeasurePreserving f' hf' : (a : ↥(Lp E p μb)) → ↥(Lp E p μ))
        ((compMeasurePreserving f hf : (a : ↥(Lp E p μc)) → ↥(Lp E p μb)) g) :
      ↥(Lp E p μ))

Tactic:
simp [compMeasurePreserving_comp hf hf']

Premises used: MeasureTheory.Lp.compMeasurePreserving_comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → α
hf : MeasurePreserving f μ μ
n : ℕ
h :
  ∀ (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
⊢ 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 μ))

Tactic:
funext
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → α
hf : MeasurePreserving f μ μ
x : ↥(Lp E p μ)
⊢ (⇑(compMeasurePreserving f hf) : (a : ↥(Lp E p μ)) → ↥(Lp E p μ))^[0] x =
    (compMeasurePreserving f^[0] ⋯ : (a : ↥(Lp E p μ)) → ↥(Lp E p μ)) x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
h₁ :
  (⇑(compMeasurePreserving f hf) : (a : ↥(Lp E p μ)) → ↥(Lp E p μ))^[1 + n] x =
    (compMeasurePreserving f^[n + 1] ⋯ : (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

Tactic:
nth_rewrite 1 [add_comm n 1]

Premises used: add_comm, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 μ))^[1 + n] x =
    (compMeasurePreserving f^[n + 1] ⋯ : (a : ↥(Lp E p μ)) → ↥(Lp E p μ)) x

Tactic:
simp [Function.iterate_add, h, compMeasurePreserving_comp (hf.iterate n) hf]

Premises used: MeasureTheory.Lp.compMeasurePreserving_comp, MeasureTheory.MeasurePreserving.iterate, Function.iterate_add
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
h₁ :
  ∀ (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
⊢ (⇑(compMeasurePreserving f hf) : (a : ↥(Lp E p μ)) → ↥(Lp E p μ))^[n] x =
    (compMeasurePreserving f^[n] ⋯ : (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]

Premises used: MeasureTheory.Lp.compMeasurePreserving_comp, MeasureTheory.MeasurePreserving.iterate, Function.iterate_add, add_comm, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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)
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))
⊢ 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)

Tactic:
rcases g with ⟨⟨_⟩, _⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 : 𝕜
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:
rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
hg : LipschitzWith K g
g0 : g 0 = 0
hL : MemLp f p μ
x : α
⊢ ‖g (f x)‖ ≤ (↑K : ℝ) * ‖f x‖

Tactic:
simpa [g0] using hg.norm_sub_le (f x) 0

Premises used: LipschitzWith.norm_sub_le, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 : α
rw : dist (f x) 0 ≤ (↑K' : ℝ) * dist (g (f x)) (g 0)
⊢ ‖f x‖ ≤ (↑K' : ℝ) * ‖g (f x)‖

Tactic:
rw [← dist_zero_right, ← dist_zero_right, ← g0]

Premises used: dist_zero_right
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 : α
⊢ dist (f x) 0 ≤ (↑K' : ℝ) * dist (g (f x)) (g 0)

Tactic:
apply hg'.le_mul_dist

Premises used: AntilipschitzWith.le_mul_dist
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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)‖

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
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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)‖
⊢ AEStronglyMeasurable f μ

Tactic:
have B : AEStronglyMeasurable f μ :=
    (hg'.isUniformEmbedding hg).isEmbedding.aestronglyMeasurable_comp_iff.1 hL.1
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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)‖
B : AEStronglyMeasurable f μ
⊢ MemLp f p μ

Tactic:
hL.of_le_mul B (Filter.Eventually.of_forall A)

Premises used: MeasureTheory.MemLp.of_le_mul, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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)‖
B : AEStronglyMeasurable f μ
⊢ MemLp f p μ

Tactic:
exact hL.of_le_mul B (Filter.Eventually.of_forall A)

Premises used: MeasureTheory.MemLp.of_le_mul, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
h_Lp : MemLp f p μ
L : E →L[𝕜] F
⊢ Eq.{u_5 + 1} (α := F) ((L : (a : E) → F) 0 : F) (0 : F)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
p : ℝ≥0∞
α : Type u_6
E : Type u_7
F : Type u_8
K K' : ℝ≥0
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
f : α → E
g : E → F
hg : LipschitzWith K g
hg' : AntilipschitzWith K' g
g0 : g 0 = 0
⊢ MemLp (g ∘ f) p μ ↔ MemLp f p μ

Tactic:
⟨fun h => h.of_comp_antilipschitzWith hg.uniformContinuous hg' g0, fun h => hg.comp_memLp g0 h⟩

Premises used: MeasureTheory.MemLp.of_comp_antilipschitzWith, LipschitzWith.comp_memLp, LipschitzWith.uniformContinuous, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 μ)
rw : MemLp (↑(AEEqFun.comp g ⋯ (↑f : α →ₘ[μ] E)) : α → F) p μ
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] F)) (Lp F p μ) (AEEqFun.comp g ⋯ (↑f : α →ₘ[μ] E))

Tactic:
rw [Lp.mem_Lp_iff_memLp]

Premises used: MeasureTheory.Lp.mem_Lp_iff_memLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 μ)
⊢ MemLp (↑(AEEqFun.comp g ⋯ (↑f : α →ₘ[μ] E)) : α → F) p μ

Tactic:
(hg.comp_memLp g0 (Lp.memLp f)).ae_eq (AEEqFun.coeFn_comp _ hg.continuous _).symm

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.AEEqFun.coeFn_comp, LipschitzWith.comp_memLp, LipschitzWith.continuous, MeasureTheory.MemLp.ae_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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 μ)
⊢ MemLp (↑(AEEqFun.comp g ⋯ (↑f : α →ₘ[μ] E)) : α → F) p μ

Tactic:
exact (hg.comp_memLp g0 (Lp.memLp f)).ae_eq (AEEqFun.coeFn_comp _ hg.continuous _).symm

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.AEEqFun.coeFn_comp, LipschitzWith.comp_memLp, LipschitzWith.continuous, MeasureTheory.MemLp.ae_eq, Filter.EventuallyEq.symm
-- 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) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] g ∘ (↑(↑f : α →ₘ[μ] E) : α → E)

Tactic:
AEEqFun.coeFn_comp _ hg.continuous _

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.coeFn_comp, LipschitzWith.continuous, MeasureTheory.AEEqFun.comp