awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
inst_3 : OpensMeasurableSpace X
inst_4 : LocallyCompactSpace X
inst_5 : T2Space X
𝕜 : Type u_9
inst_6 : NormedRing 𝕜
inst_7 : SecondCountableTopologyEither X E
inst_8 : Module 𝕜 E
inst_9 : NormSMulClass 𝕜 E
f : X → 𝕜
g : X → E
s : Set X
hs : IsLocallyClosed s
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) k μ

Tactic:
fun k hk_sub hk_c => (hf k hk_sub hk_c).smul_continuousOn (hg.mono hk_sub) hk_c

Premises used: MeasureTheory.IntegrableOn.smul_continuousOn, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
inst_3 : OpensMeasurableSpace X
inst_4 : LocallyCompactSpace X
inst_5 : T2Space X
𝕜 : Type u_9
inst_6 : NormedRing 𝕜
inst_7 : SecondCountableTopologyEither X E
inst_8 : Module 𝕜 E
inst_9 : NormSMulClass 𝕜 E
f : X → 𝕜
g : X → E
s : Set X
hs : IsLocallyClosed s
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ f x • g x) k μ

Tactic:
exact fun k hk_sub hk_c => (hf k hk_sub hk_c).smul_continuousOn (hg.mono hk_sub) hk_c

Premises used: MeasureTheory.IntegrableOn.smul_continuousOn, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f g : ↥(Lp E p μ)
rw : (↑(↑f : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E) ↔ (↑f : α →ₘ[μ] E) ≤ (↑g : α →ₘ[μ] E)
rw₁ rw₂ :
  (↑(↑f : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E) ↔
    (↑(↑f : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E)
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E) : α → E) ↔ f ≤ g

Tactic:
rw [← Subtype.coe_le_coe, ← AEEqFun.coeFn_le]

Premises used: MeasureTheory.AEEqFun.coeFn_le, Subtype.coe_le_coe
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f : ↥(Lp E p μ)
rw : 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) ↔ (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
⊢ 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) ↔ 0 ≤ f

Tactic:
rw [← coeFn_le]

Premises used: MeasureTheory.Lp.coeFn_le
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f : ↥(Lp E p μ)
⊢ Filter.EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E) 0

Tactic:
have h0 := Lp.coeFn_zero E p μ
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f : ↥(Lp E p μ)
h0 : Filter.EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E) 0
mp : 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) → (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
mpr : (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) → 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
⊢ 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) ↔ (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f : ↥(Lp E p μ)
h0 : Filter.EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E) 0
h : 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
a : α
h₁ :
  0 a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a →
    Eq.{u_2 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a) →
      (↑(↑0 : α →ₘ[μ] E) : α → E) a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a
⊢ 0 a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a →
    Eq.{u_2 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a) →
      (↑(↑0 : α →ₘ[μ] E) : α → E) a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f : ↥(Lp E p μ)
h0 : Filter.EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E) 0
h : 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
h₁ :
  ∀ (a : α),
    0 a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a →
      ∀ (h2 : Eq.{u_2 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a)),
        (↑(↑0 : α →ₘ[μ] E) : α → E) a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a
⊢ (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)

Tactic:
filter_upwards [h, h0] with _ _ h2
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f : ↥(Lp E p μ)
h0 : Filter.EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E) 0
h : (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
a : α
h₁ :
  (↑(↑0 : α →ₘ[μ] E) : α → E) a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a →
    Eq.{u_2 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a) → 0 a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a
⊢ (↑(↑0 : α →ₘ[μ] E) : α → E) a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a →
    Eq.{u_2 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a) → 0 a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f : ↥(Lp E p μ)
h0 : Filter.EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E) 0
h : (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
h₁ :
  ∀ (a : α),
    (↑(↑0 : α →ₘ[μ] E) : α → E) a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a →
      ∀ (h2 : Eq.{u_2 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a)), 0 a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a
⊢ 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)

Tactic:
filter_upwards [h, h0] with _ _ h2
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f : ↥(Lp E p μ)
h0 : Filter.EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E) 0
h : 0 ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
a : α
h_1 : 0 a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a
h2 : Eq.{u_2 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a)
h₁ h₂ h₃ h₄ : 0 a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a
⊢ (↑(↑0 : α →ₘ[μ] E) : α → E) a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a

Tactic:
rwa [h2]
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
f : ↥(Lp E p μ)
h0 : Filter.EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑0 : α →ₘ[μ] E) : α → E) 0
h : (↑(↑0 : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E)
a : α
h_1 : (↑(↑0 : α →ₘ[μ] E) : α → E) a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a
h2 : Eq.{u_2 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) a) (0 a)
h₁ h₂ h₃ h₄ : (↑(↑0 : α →ₘ[μ] E) : α → E) a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a
⊢ 0 a ≤ (↑(↑f : α →ₘ[μ] E) : α → E) a

Tactic:
rwa [← h2]
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
⊢ AddLeftMono ↥(Lp E p μ)

Tactic:
⟨fun f g₁ g₂ hg₁₂ => ?_⟩

Premises used: CovariantClass.mk
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
refine : ∀ (f g₁ g₂ : ↥(Lp E p μ)) (hg₁₂ : g₁ ≤ g₂), f + g₁ ≤ f + g₂
⊢ AddLeftMono ↥(Lp E p μ)

Tactic:
refine ⟨fun f g₁ g₂ hg₁₂ => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
f g₁ g₂ : ↥(Lp E p μ)
hg₁₂ : g₁ ≤ g₂
rw :
  ∀ (hg₁₂ : (↑(↑g₁ : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g₂ : α →ₘ[μ] E) : α → E)),
    (↑(↑(f + g₁) : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑(f + g₂) : α →ₘ[μ] E) : α → E)
⊢ f + g₁ ≤ f + g₂

Tactic:
rw [← coeFn_le] at hg₁₂ ⊢

Premises used: MeasureTheory.Lp.coeFn_le
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
f g₁ g₂ : ↥(Lp E p μ)
hg₁₂ : (↑(↑g₁ : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g₂ : α →ₘ[μ] E) : α → E)
h :
  ∀ (a : α) (h1 : (↑(↑(f + g₁) : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g₁ : α →ₘ[μ] E) : α → E)) a)
    (h2 : (↑(↑(f + g₂) : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g₂ : α →ₘ[μ] E) : α → E)) a)
    (h3 : (↑(↑g₁ : α →ₘ[μ] E) : α → E) a ≤ (↑(↑g₂ : α →ₘ[μ] E) : α → E) a),
    (↑(↑(f + g₁) : α →ₘ[μ] E) : α → E) a ≤ (↑(↑(f + g₂) : α →ₘ[μ] E) : α → E) a
⊢ (↑(↑(f + g₁) : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑(f + g₂) : α →ₘ[μ] E) : α → E)

Tactic:
filter_upwards [coeFn_add f g₁, coeFn_add f g₂, hg₁₂] with _ h1 h2 h3

Premises used: MeasureTheory.Lp.coeFn_add
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
f g₁ g₂ : ↥(Lp E p μ)
hg₁₂ : (↑(↑g₁ : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g₂ : α →ₘ[μ] E) : α → E)
a : α
h1 : (↑(↑(f + g₁) : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g₁ : α →ₘ[μ] E) : α → E)) a
h2 : (↑(↑(f + g₂) : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g₂ : α →ₘ[μ] E) : α → E)) a
h3 : (↑(↑g₁ : α →ₘ[μ] E) : α → E) a ≤ (↑(↑g₂ : α →ₘ[μ] E) : α → E) a
h :
  (↑(↑f : α →ₘ[μ] E) : α → E) a + (↑(↑g₁ : α →ₘ[μ] E) : α → E) a ≤
    (↑(↑f : α →ₘ[μ] E) : α → E) a + (↑(↑g₂ : α →ₘ[μ] E) : α → E) a
⊢ (↑(↑(f + g₁) : α →ₘ[μ] E) : α → E) a ≤ (↑(↑(f + g₂) : α →ₘ[μ] E) : α → E) a

Tactic:
rw [h1, h2, Pi.add_apply, Pi.add_apply]

Premises used: Pi.add_apply
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
f g₁ g₂ : ↥(Lp E p μ)
hg₁₂ : (↑(↑g₁ : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g₂ : α →ₘ[μ] E) : α → E)
a : α
h1 : (↑(↑(f + g₁) : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g₁ : α →ₘ[μ] E) : α → E)) a
h2 : (↑(↑(f + g₂) : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g₂ : α →ₘ[μ] E) : α → E)) a
h3 : (↑(↑g₁ : α →ₘ[μ] E) : α → E) a ≤ (↑(↑g₂ : α →ₘ[μ] E) : α → E) a
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) a + (↑(↑g₁ : α →ₘ[μ] E) : α → E) a ≤
    (↑(↑f : α →ₘ[μ] E) : α → E) a + (↑(↑g₂ : α →ₘ[μ] E) : α → E) a

Tactic:
add_le_add le_rfl h3

Premises used: le_rfl, add_le_add
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
f g₁ g₂ : ↥(Lp E p μ)
hg₁₂ : (↑(↑g₁ : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑g₂ : α →ₘ[μ] E) : α → E)
a : α
h1 : (↑(↑(f + g₁) : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g₁ : α →ₘ[μ] E) : α → E)) a
h2 : (↑(↑(f + g₂) : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g₂ : α →ₘ[μ] E) : α → E)) a
h3 : (↑(↑g₁ : α →ₘ[μ] E) : α → E) a ≤ (↑(↑g₂ : α →ₘ[μ] E) : α → E) a
⊢ (↑(↑f : α →ₘ[μ] E) : α → E) a + (↑(↑g₁ : α →ₘ[μ] E) : α → E) a ≤
    (↑(↑f : α →ₘ[μ] E) : α → E) a + (↑(↑g₂ : α →ₘ[μ] E) : α → E) a

Tactic:
exact add_le_add le_rfl h3

Premises used: le_rfl, add_le_add
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
⊢ IsOrderedAddMonoid ↥(Lp E p μ)

Tactic:
{ add_le_add_left := fun _ _ => add_le_add_left }

Premises used: Membership.mem, Subtype, add_le_add_left, MeasureTheory.Lp, IsOrderedAddMonoid._proof_1, IsOrderedAddMonoid.mk
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
inst_3 : Fact (1 ≤ p)
inst_4 : ClosedIciTopology E
f : ℕ → ↥(Lp E p μ)
f₀ : ↥(Lp E p μ)
hf : ∀ (n : ℕ), 0 ≤ f n
h_tendsto : Filter.Tendsto f Filter.atTop (nhds f₀)
simp :
  ∀ (hf : ∀ (n : ℕ), 0 ≤ᶠ[ae μ] (↑(↑(f n) : α →ₘ[μ] E) : α → E)),
    Membership.mem (γ := Set ↥(Lp E p μ)) {x : ↥(Lp E p μ) | 0 ≤ᶠ[ae μ] (↑(↑x : α →ₘ[μ] E) : α → E)} f₀
⊢ Membership.mem (γ := Set ↥(Lp E p μ)) {x : ↥(Lp E p μ) | 0 ≤ x} f₀

Tactic:
simp only [← coeFn_nonneg] at hf ⊢

Premises used: MeasureTheory.Lp.coeFn_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
inst_3 : Fact (1 ≤ p)
inst_4 : ClosedIciTopology E
f : ℕ → ↥(Lp E p μ)
f₀ : ↥(Lp E p μ)
h_tendsto : Filter.Tendsto f Filter.atTop (nhds f₀)
hf : ∀ (n : ℕ), 0 ≤ᶠ[ae μ] (↑(↑(f n) : α →ₘ[μ] E) : α → E)
obtain :
  ∀ (φ : ℕ → ℕ)
    (hφ :
      ∀ᵐ (x : α) ∂μ,
        Filter.Tendsto (fun (i : ℕ) ↦ (↑(↑(f (φ i)) : α →ₘ[μ] E) : α → E) x) Filter.atTop
          (nhds ((↑(↑f₀ : α →ₘ[μ] E) : α → E) x))),
    Membership.mem (γ := Set ↥(Lp E p μ)) {x : ↥(Lp E p μ) | 0 ≤ᶠ[ae μ] (↑(↑x : α →ₘ[μ] E) : α → E)} f₀
⊢ Membership.mem (γ := Set ↥(Lp E p μ)) {x : ↥(Lp E p μ) | 0 ≤ᶠ[ae μ] (↑(↑x : α →ₘ[μ] E) : α → E)} f₀

Tactic:
obtain ⟨φ, -, hφ⟩ := tendstoInMeasure_of_tendsto_Lp h_tendsto |>.exists_seq_tendsto_ae

Premises used: MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae, MeasureTheory.tendstoInMeasure_of_tendsto_Lp
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
inst_3 : Fact (1 ≤ p)
inst_4 : ClosedIciTopology E
f : ℕ → ↥(Lp E p μ)
f₀ : ↥(Lp E p μ)
h_tendsto : Filter.Tendsto f Filter.atTop (nhds f₀)
hf : ∀ (n : ℕ), 0 ≤ᶠ[ae μ] (↑(↑(f n) : α →ₘ[μ] E) : α → E)
φ : ℕ → ℕ
hφ :
  ∀ᵐ (x : α) ∂μ,
    Filter.Tendsto (fun (i : ℕ) ↦ (↑(↑(f (φ i)) : α →ₘ[μ] E) : α → E) x) Filter.atTop
      (nhds ((↑(↑f₀ : α →ₘ[μ] E) : α → E) x))
h :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) (⋂ (i : ℕ), {x : α | 0 x ≤ (↑(↑(f i) : α →ₘ[μ] E) : α → E) x}) x)
    (hφx :
      Filter.Tendsto (fun (i : ℕ) ↦ (↑(↑(f (φ i)) : α →ₘ[μ] E) : α → E) x) Filter.atTop
        (nhds ((↑(↑f₀ : α →ₘ[μ] E) : α → E) x))),
    0 x ≤ (↑(↑f₀ : α →ₘ[μ] E) : α → E) x
⊢ Membership.mem (γ := Set ↥(Lp E p μ)) {x : ↥(Lp E p μ) | 0 ≤ᶠ[ae μ] (↑(↑x : α →ₘ[μ] E) : α → E)} f₀

Tactic:
filter_upwards [countable_iInter_mem.mpr hf, hφ] with x hx hφx

Premises used: Iff.mpr, countable_iInter_mem
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
inst_3 : Fact (1 ≤ p)
inst_4 : ClosedIciTopology E
f : ℕ → ↥(Lp E p μ)
f₀ : ↥(Lp E p μ)
h_tendsto : Filter.Tendsto f Filter.atTop (nhds f₀)
hf : ∀ (n : ℕ), 0 ≤ᶠ[ae μ] (↑(↑(f n) : α →ₘ[μ] E) : α → E)
φ : ℕ → ℕ
hφ :
  ∀ᵐ (x : α) ∂μ,
    Filter.Tendsto (fun (i : ℕ) ↦ (↑(↑(f (φ i)) : α →ₘ[μ] E) : α → E) x) Filter.atTop
      (nhds ((↑(↑f₀ : α →ₘ[μ] E) : α → E) x))
x : α
hx : Membership.mem (γ := Set α) (⋂ (i : ℕ), {x : α | 0 x ≤ (↑(↑(f i) : α →ₘ[μ] E) : α → E) x}) x
hφx :
  Filter.Tendsto (fun (i : ℕ) ↦ (↑(↑(f (φ i)) : α →ₘ[μ] E) : α → E) x) Filter.atTop
    (nhds ((↑(↑f₀ : α →ₘ[μ] E) : α → E) x))
⊢ 0 x ≤ (↑(↑f₀ : α →ₘ[μ] E) : α → E) x

Tactic:
ge_of_tendsto' hφx fun _ ↦ Set.mem_iInter.mp hx _

Premises used: Set.mem_iInter, ge_of_tendsto', Iff.mp
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : IsOrderedAddMonoid E
inst_3 : Fact (1 ≤ p)
inst_4 : ClosedIciTopology E
f : ℕ → ↥(Lp E p μ)
f₀ : ↥(Lp E p μ)
h_tendsto : Filter.Tendsto f Filter.atTop (nhds f₀)
hf : ∀ (n : ℕ), 0 ≤ᶠ[ae μ] (↑(↑(f n) : α →ₘ[μ] E) : α → E)
φ : ℕ → ℕ
hφ :
  ∀ᵐ (x : α) ∂μ,
    Filter.Tendsto (fun (i : ℕ) ↦ (↑(↑(f (φ i)) : α →ₘ[μ] E) : α → E) x) Filter.atTop
      (nhds ((↑(↑f₀ : α →ₘ[μ] E) : α → E) x))
x : α
hx : Membership.mem (γ := Set α) (⋂ (i : ℕ), {x : α | 0 x ≤ (↑(↑(f i) : α →ₘ[μ] E) : α → E) x}) x
hφx :
  Filter.Tendsto (fun (i : ℕ) ↦ (↑(↑(f (φ i)) : α →ₘ[μ] E) : α → E) x) Filter.atTop
    (nhds ((↑(↑f₀ : α →ₘ[μ] E) : α → E) x))
⊢ 0 x ≤ (↑(↑f₀ : α →ₘ[μ] E) : α → E) x

Tactic:
exact ge_of_tendsto' hφx fun _ ↦ Set.mem_iInter.mp hx _

Premises used: Set.mem_iInter, ge_of_tendsto', Iff.mp
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ MemLp (f ⊔ g) p μ

Tactic:
MemLp.mono' (hf.norm.add hg.norm) (hf.1.sup hg.1)
    (Filter.Eventually.of_forall fun x => norm_sup_le_add (f x) (g x))

Premises used: MeasureTheory.MemLp.mono', MeasureTheory.MemLp.add, Filter.Eventually.of_forall, norm_sup_le_add, MeasureTheory.MemLp.norm, And.left, MeasureTheory.AEStronglyMeasurable.sup
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ MemLp (f ⊓ g) p μ

Tactic:
MemLp.mono' (hf.norm.add hg.norm) (hf.1.inf hg.1)
    (Filter.Eventually.of_forall fun x => norm_inf_le_add (f x) (g x))

Premises used: MeasureTheory.MemLp.mono', MeasureTheory.MemLp.add, Filter.Eventually.of_forall, MeasureTheory.MemLp.norm, And.left, norm_inf_le_add, MeasureTheory.AEStronglyMeasurable.inf
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
f : α → E
hf : MemLp f p μ
⊢ MemLp |f| p μ

Tactic:
hf.sup hf.neg

Premises used: MeasureTheory.MemLp.sup, abs, MeasureTheory.MemLp.neg
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
f g : α →ₘ[μ] E
hf : Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) f
hg : Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) g
rw : ∀ (hf : MemLp (↑f : α → E) p μ) (hg : MemLp (↑g : α → E) p μ), MemLp (↑(f ⊔ g) : α → E) p μ
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) (f ⊔ g)

Tactic:
rw [mem_Lp_iff_memLp] at *

Premises used: MeasureTheory.Lp.mem_Lp_iff_memLp
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
f g : α →ₘ[μ] E
hf : MemLp (↑f : α → E) p μ
hg : MemLp (↑g : α → E) p μ
⊢ MemLp (↑(f ⊔ g) : α → E) p μ

Tactic:
(memLp_congr_ae (AEEqFun.coeFn_sup _ _)).mpr (hf.sup hg)

Premises used: Iff.mpr, MeasureTheory.memLp_congr_ae, MeasureTheory.MemLp.sup, MeasureTheory.AEEqFun.coeFn_sup
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
f g : α →ₘ[μ] E
hf : MemLp (↑f : α → E) p μ
hg : MemLp (↑g : α → E) p μ
⊢ MemLp (↑(f ⊔ g) : α → E) p μ

Tactic:
exact (memLp_congr_ae (AEEqFun.coeFn_sup _ _)).mpr (hf.sup hg)

Premises used: Iff.mpr, MeasureTheory.memLp_congr_ae, MeasureTheory.MemLp.sup, MeasureTheory.AEEqFun.coeFn_sup
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
f g : α →ₘ[μ] E
hf : Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) f
hg : Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) g
rw : ∀ (hf : MemLp (↑f : α → E) p μ) (hg : MemLp (↑g : α → E) p μ), MemLp (↑(f ⊓ g) : α → E) p μ
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) (f ⊓ g)

Tactic:
rw [mem_Lp_iff_memLp] at *

Premises used: MeasureTheory.Lp.mem_Lp_iff_memLp
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
f g : α →ₘ[μ] E
hf : MemLp (↑f : α → E) p μ
hg : MemLp (↑g : α → E) p μ
⊢ MemLp (↑(f ⊓ g) : α → E) p μ

Tactic:
(memLp_congr_ae (AEEqFun.coeFn_inf _ _)).mpr (hf.inf hg)

Premises used: Iff.mpr, MeasureTheory.memLp_congr_ae, MeasureTheory.AEEqFun.coeFn_inf, MeasureTheory.MemLp.inf
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
f g : α →ₘ[μ] E
hf : MemLp (↑f : α → E) p μ
hg : MemLp (↑g : α → E) p μ
⊢ MemLp (↑(f ⊓ g) : α → E) p μ

Tactic:
exact (memLp_congr_ae (AEEqFun.coeFn_inf _ _)).mpr (hf.inf hg)

Premises used: Iff.mpr, MeasureTheory.memLp_congr_ae, MeasureTheory.AEEqFun.coeFn_inf, MeasureTheory.MemLp.inf
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
f g : ↥(Lp E p μ)
⊢ (↑(↑(f ⊔ g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) ⊔ (↑(↑g : α →ₘ[μ] E) : α → E)

Tactic:
AEEqFun.coeFn_sup _ _

Premises used: MeasureTheory.AEEqFun.coeFn_sup
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
f g : ↥(Lp E p μ)
⊢ (↑(↑(f ⊓ g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑f : α →ₘ[μ] E) : α → E) ⊓ (↑(↑g : α →ₘ[μ] E) : α → E)

Tactic:
AEEqFun.coeFn_inf _ _

Premises used: MeasureTheory.AEEqFun.coeFn_inf
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
f : ↥(Lp E p μ)
⊢ (↑(↑|f| : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] fun (x : α) ↦ |(↑(↑f : α →ₘ[μ] E) : α → E) x|

Tactic:
AEEqFun.coeFn_abs _

Premises used: abs, MeasureTheory.AEEqFun.coeFn_abs
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
inst_4 : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : |f| ≤ |g|
⊢ (↑(↑|f| : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑|g| : α →ₘ[μ] E) : α → E)

Tactic:
rw [← coeFn_le] at hfg

Premises used: MeasureTheory.Lp.coeFn_le
-- Module: Mathlib.MeasureTheory.Function.LpOrder
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
inst_1 : Lattice E
inst_2 : HasSolidNorm E
inst_3 : IsOrderedAddMonoid E
inst_4 : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : (↑(↑|f| : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑|g| : α →ₘ[μ] E) : α → E)
simp_rw : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ ≤ eLpNorm (↑(↑g : α →ₘ[μ] E) : α → E) p μ
⊢ ‖f‖ ≤ ‖g‖

Tactic:
simp_rw [Lp.norm_def, ENNReal.toReal_le_toReal (Lp.eLpNorm_ne_top f) (Lp.eLpNorm_ne_top g)]

Premises used: ENNReal.toReal_le_toReal, MeasureTheory.Lp.eLpNorm_ne_top, MeasureTheory.Lp.norm_def