-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem MeasureTheory.MemLp.of_comp_antilipschitzWith {α E F} {K'} [MeasurableSpace α]
    {μ : Measure α} [NormedAddCommGroup E] [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 μ

Proof state:
p : ℝ≥0∞
α : Type u_7
E : Type u_8
F : Type u_9
K' : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : 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 μ

Tactic:
have A : ∀ x, ‖f x‖ ≤ K' * ‖g (f x)‖ := by
  intro x
  rw [← dist_zero_right, ← dist_zero_right, ← g0]
  apply hg'.le_mul_dist

Result:
p : ℝ≥0∞
α : Type u_7
E : Type u_8
F : Type u_9
K' : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : 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 μ

Proof state:
p : ℝ≥0∞
α : Type u_7
E : Type u_8
F : Type u_9
K' : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : 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 μ

Tactic:
have B : AEStronglyMeasurable f μ :=
  (hg'.isUniformEmbedding hg).isEmbedding.aestronglyMeasurable_comp_iff.1 hL.1

Result:
p : ℝ≥0∞
α : Type u_7
E : Type u_8
F : Type u_9
K' : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : 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 μ

Proof state:
p : ℝ≥0∞
α : Type u_7
E : Type u_8
F : Type u_9
K' : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : 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:
rw [← dist_zero_right, ← dist_zero_right, ← g0]

Result:
p : ℝ≥0∞
α : Type u_7
E : Type u_8
F : Type u_9
K' : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : 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)

Proof state:
p : ℝ≥0∞
α : Type u_7
E : Type u_8
F : Type u_9
K' : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : 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:
intro x

Result:
p : ℝ≥0∞
α : Type u_7
E : Type u_8
F : Type u_9
K' : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : 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)‖

Proof state:
p : ℝ≥0∞
α : Type u_7
E : Type u_8
F : Type u_9
K' : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : 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

Result:
no goals

Proof state:
p : ℝ≥0∞
α : Type u_7
E : Type u_8
F : Type u_9
K' : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : 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)

Result:
no goals