awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp 𝕜 2 μ)
rw :
  inner 𝕜 (E := 𝕜) 1 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ) =
    ∫ (x : α) in s, (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ
⊢ ⟪indicatorConstLp (s := s) 2 hs hμs 1, f⟫ = ∫ (x : α) in s, (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ

Tactic:
rw [L2.inner_indicatorConstLp_eq_inner_setIntegral 𝕜 hs hμs (1 : 𝕜) f]

Premises used: MeasureTheory.L2.inner_indicatorConstLp_eq_inner_setIntegral, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp 𝕜 2 μ)
⊢ inner 𝕜 (E := 𝕜) 1 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ) =
    ∫ (x : α) in s, (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
s t : Set α
inst_4 : CompleteSpace E
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
a b : E
this : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
rw :
  ⟪a, ∫ (x : α) in s, (↑(↑(indicatorConstLp (s := t) 2 ht hμt b) : α →ₘ[μ] E) : α → E) x ∂μ⟫ = μ.real (s ∩ t) • ⟪a, b⟫
rw₁ : ⟪a, μ.real (t ∩ s) • b⟫ = μ.real (s ∩ t) • ⟪a, b⟫
rw₂ : μ.real (t ∩ s) • ⟪a, b⟫ = μ.real (s ∩ t) • ⟪a, b⟫
rw₃ rw₄ : μ.real (s ∩ t) • ⟪a, b⟫ = μ.real (s ∩ t) • ⟪a, b⟫
⊢ inner 𝕜 (E := ↥(Lp E 2 μ)) (indicatorConstLp (s := s) 2 hs hμs a) (indicatorConstLp (s := t) 2 ht hμt b) =
    μ.real (s ∩ t) • ⟪a, b⟫

Tactic:
rw [inner_indicatorConstLp_eq_inner_setIntegral, setIntegral_indicatorConstLp hs,
    inner_smul_right_eq_smul, Set.inter_comm]

Premises used: MeasureTheory.L2.inner_indicatorConstLp_eq_inner_setIntegral, Set.inter_comm, MeasureTheory.setIntegral_indicatorConstLp, inner_smul_right_eq_smul
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1) (indicatorConstLp (s := t) 2 ht hμt 1) =
    (↑(μ.real (s ∩ t)) : 𝕜)

Tactic:
simp [inner_indicatorConstLp_indicatorConstLp, RCLike.ofReal_alg]

Premises used: MeasureTheory.L2.inner_indicatorConstLp_indicatorConstLp, RCLike.ofReal_alg
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ inner ℝ (E := ↥(Lp ℝ 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1) (indicatorConstLp (s := t) 2 ht hμt 1) =
    μ.real (s ∩ t)

Tactic:
simp [inner_indicatorConstLp_indicatorConstLp]

Premises used: MeasureTheory.L2.inner_indicatorConstLp_indicatorConstLp
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
h :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (fun (a : α) ↦
      inner 𝕜 (E := 𝕜)
        ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
        ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a))
    fun (a : α) ↦
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
⊢ inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) ((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f : ↥(Lp 𝕜 2 μ))
      ((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g : ↥(Lp 𝕜 2 μ)) =
    ∫ (x : α),
      HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) x : 𝕜)
        ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) : 𝕜) ∂μ

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)

Tactic:
have hf_ae := f.coeFn_toLp 2 μ 𝕜
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
⊢ EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑g : (a : α) → 𝕜)

Tactic:
have hg_ae := g.coeFn_toLp 2 μ 𝕜
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
hg_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑g : (a : α) → 𝕜)
h :
  ∀ (a : α)
    (hf :
      Eq.{u_2 + 1} (α := 𝕜)
        ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
        ((f : (a : α) → 𝕜) a : 𝕜))
    (hg :
      Eq.{u_2 + 1} (α := 𝕜)
        ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
        ((g : (a : α) → 𝕜) a : 𝕜)),
    inner 𝕜 (E := 𝕜)
        ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
        ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a) =
      HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜)
        ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
⊢ EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (fun (a : α) ↦
      inner 𝕜 (E := 𝕜)
        ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
        ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a))
    fun (a : α) ↦
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)

Tactic:
filter_upwards [hf_ae, hg_ae] with _ hf hg
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
hg_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑g : (a : α) → 𝕜)
a : α
hf :
  Eq.{u_2 + 1} (α := 𝕜)
    ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
    ((f : (a : α) → 𝕜) a : 𝕜)
hg :
  Eq.{u_2 + 1} (α := 𝕜)
    ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
    ((g : (a : α) → 𝕜) a : 𝕜)
h :
  inner 𝕜 (E := 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
⊢ inner 𝕜 (E := 𝕜) ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
      ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)

Tactic:
rw [hf, hg]
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
hg_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑g : (a : α) → 𝕜)
a : α
hf :
  Eq.{u_2 + 1} (α := 𝕜)
    ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
    ((f : (a : α) → 𝕜) a : 𝕜)
hg :
  Eq.{u_2 + 1} (α := 𝕜)
    ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
    ((g : (a : α) → 𝕜) a : 𝕜)
⊢ inner 𝕜 (E := 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
inst_5 : CompactSpace α
f g : C(α, 𝕜)
h :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (fun (a : α) ↦
      inner 𝕜 (E := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
        ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a))
    fun (a : α) ↦
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
⊢ inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) ((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f : ↥(Lp 𝕜 2 μ))
      ((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g : ↥(Lp 𝕜 2 μ)) =
    ∫ (x : α),
      HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) x : 𝕜)
        ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) : 𝕜) ∂μ

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
inst_5 : CompactSpace α
f g : C(α, 𝕜)
⊢ EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)

Tactic:
have hf_ae := f.coeFn_toLp (p := 2) (𝕜 := 𝕜) μ
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
inst_5 : CompactSpace α
f g : C(α, 𝕜)
hf_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
⊢ EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑g : (a : α) → 𝕜)

Tactic:
have hg_ae := g.coeFn_toLp (p := 2) (𝕜 := 𝕜) μ
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
inst_5 : CompactSpace α
f g : C(α, 𝕜)
hf_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
hg_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑g : (a : α) → 𝕜)
h :
  ∀ (a : α)
    (hf :
      Eq.{u_2 + 1} (α := 𝕜)
        ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
        ((f : (a : α) → 𝕜) a : 𝕜))
    (hg :
      Eq.{u_2 + 1} (α := 𝕜)
        ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
        ((g : (a : α) → 𝕜) a : 𝕜)),
    inner 𝕜 (E := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
        ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a) =
      HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜)
        ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
⊢ EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (fun (a : α) ↦
      inner 𝕜 (E := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
        ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a))
    fun (a : α) ↦
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)

Tactic:
filter_upwards [hf_ae, hg_ae] with _ hf hg
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
inst_5 : CompactSpace α
f g : C(α, 𝕜)
hf_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
hg_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑g : (a : α) → 𝕜)
a : α
hf :
  Eq.{u_2 + 1} (α := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
    ((f : (a : α) → 𝕜) a : 𝕜)
hg :
  Eq.{u_2 + 1} (α := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
    ((g : (a : α) → 𝕜) a : 𝕜)
h :
  inner 𝕜 (E := 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
⊢ inner 𝕜 (E := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
      ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)

Tactic:
rw [hf, hg]
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
inst_5 : CompactSpace α
f g : C(α, 𝕜)
hf_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
hg_ae :
  EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑g : (a : α) → 𝕜)
a : α
hf :
  Eq.{u_2 + 1} (α := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
    ((f : (a : α) → 𝕜) a : 𝕜)
hg :
  Eq.{u_2 + 1} (α := 𝕜) ((↑(↑((ContinuousMap.toLp 2 μ 𝕜 : (a : C(α, 𝕜)) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a : 𝕜)
    ((g : (a : α) → 𝕜) a : 𝕜)
⊢ inner 𝕜 (E := 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
hf : LocallyIntegrableOn f s μ
t : Set X
hst : t ⊆ s
⊢ LocallyIntegrableOn f t μ

Tactic:
fun x hx =>
  (hf x <| hst hx).filter_mono (nhdsWithin_mono x hst)

Premises used: MeasureTheory.LocallyIntegrableOn, MeasureTheory.IntegrableAtFilter.filter_mono, nhdsWithin_mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
hf : LocallyIntegrableOn f s μ
⊢ LocallyIntegrableOn (ε := ℝ≥0∞) (fun (x : X) ↦ ‖f x‖ₑ) s μ

Tactic:
fun t ht ↦
  let ⟨U, hU_nhd, hU_int⟩ := hf t ht
  ⟨U, hU_nhd, hU_int.enorm⟩

Premises used: _private.0.MeasureTheory.LocallyIntegrableOn.enorm.match_1, nhdsWithin, MeasureTheory.IntegrableAtFilter, ENorm.enorm, MeasureTheory.Integrable.enorm, And.intro, Exists.intro, MeasureTheory.LocallyIntegrableOn
-- 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
s : Set X
f : X → E
hf : LocallyIntegrableOn f s μ
⊢ LocallyIntegrableOn (ε := ℝ) (fun (x : X) ↦ ‖f x‖) s μ

Tactic:
fun t ht =>
  let ⟨U, hU_nhd, hU_int⟩ := hf t ht
  ⟨U, hU_nhd, hU_int.norm⟩

Premises used: Norm.norm, nhdsWithin, MeasureTheory.IntegrableAtFilter, _private.0.MeasureTheory.LocallyIntegrableOn.norm.match_1, And.intro, Exists.intro, MeasureTheory.LocallyIntegrableOn, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
ε' : Type u_4
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
inst_4 : TopologicalSpace ε'
inst_5 : ContinuousENorm ε'
f : X → ε
μ : Measure X
s : Set X
hf : LocallyIntegrableOn f s μ
g : X → ε'
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ
x : X
hx : x ∈ s
rcases : ∀ (t : Set X) (t_mem : t ∈ 𝓝[s] x) (ht : IntegrableOn f t μ), IntegrableAtFilter g (𝓝[s] x) μ
⊢ IntegrableAtFilter g (𝓝[s] x) μ

Tactic:
rcases hf x hx with ⟨t, t_mem, ht⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
ε' : Type u_4
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
inst_4 : TopologicalSpace ε'
inst_5 : ContinuousENorm ε'
f : X → ε
μ : Measure X
s : Set X
hf : LocallyIntegrableOn f s μ
g : X → ε'
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ
x : X
hx : x ∈ s
t : Set X
t_mem : t ∈ 𝓝[s] x
ht : IntegrableOn f t μ
⊢ IntegrableAtFilter g (𝓝[s] x) μ

Tactic:
⟨t, t_mem, ht.mono_enorm hg.restrict (ae_restrict_of_ae h)⟩

Premises used: MeasureTheory.AEStronglyMeasurable.restrict, MeasureTheory.Integrable.mono_enorm, MeasureTheory.ae_restrict_of_ae, MeasureTheory.IntegrableAtFilter, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
ε' : Type u_4
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
inst_4 : TopologicalSpace ε'
inst_5 : ContinuousENorm ε'
f : X → ε
μ : Measure X
s : Set X
hf : LocallyIntegrableOn f s μ
g : X → ε'
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ
x : X
hx : x ∈ s
t : Set X
t_mem : t ∈ 𝓝[s] x
ht : IntegrableOn f t μ
⊢ IntegrableAtFilter g (𝓝[s] x) μ

Tactic:
exact ⟨t, t_mem, ht.mono_enorm hg.restrict (ae_restrict_of_ae h)⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
F : Type u_7
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
μ : Measure X
s : Set X
f : X → E
hf : LocallyIntegrableOn f s μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
x : X
hx : x ∈ s
rcases : ∀ (t : Set X) (t_mem : t ∈ 𝓝[s] x) (ht : IntegrableOn f t μ), IntegrableAtFilter g (𝓝[s] x) μ
⊢ IntegrableAtFilter g (𝓝[s] x) μ

Tactic:
rcases hf x hx with ⟨t, t_mem, ht⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
F : Type u_7
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
μ : Measure X
s : Set X
f : X → E
hf : LocallyIntegrableOn f s μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
x : X
hx : x ∈ s
t : Set X
t_mem : t ∈ 𝓝[s] x
ht : IntegrableOn f t μ
⊢ IntegrableAtFilter g (𝓝[s] x) μ

Tactic:
⟨t, t_mem, Integrable.mono ht hg.restrict (ae_restrict_of_ae h)⟩

Premises used: MeasureTheory.Integrable.mono, MeasureTheory.AEStronglyMeasurable.restrict, MeasureTheory.ae_restrict_of_ae, MeasureTheory.IntegrableAtFilter, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
F : Type u_7
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
μ : Measure X
s : Set X
f : X → E
hf : LocallyIntegrableOn f s μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
x : X
hx : x ∈ s
t : Set X
t_mem : t ∈ 𝓝[s] x
ht : IntegrableOn f t μ
⊢ IntegrableAtFilter g (𝓝[s] x) μ

Tactic:
exact ⟨t, t_mem, Integrable.mono ht hg.restrict (ae_restrict_of_ae h)⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ ν : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf : LocallyIntegrableOn f s μ
h : ν.restrict s ≤ μ.restrict s
x : X
hx : x ∈ s
obtain : ∀ (t : Set X) (ht : t ∈ 𝓝[s] x) (hf : IntegrableOn f t μ), IntegrableAtFilter f (𝓝[s] x) ν
⊢ IntegrableAtFilter f (𝓝[s] x) ν

Tactic:
obtain ⟨t, ht, hf⟩ := hf x hx
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ ν : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf_1 : LocallyIntegrableOn f s μ
h : ν.restrict s ≤ μ.restrict s
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hf : IntegrableOn f t μ
obtain : ∀ (u : Set X) (hu : IsOpen[inst_1] u) (hxu : x ∈ u) (hut : u ∩ s ⊆ t), IntegrableAtFilter f (𝓝[s] x) ν
⊢ IntegrableAtFilter f (𝓝[s] x) ν

Tactic:
obtain ⟨u, hu, hxu, hut⟩ := mem_nhdsWithin.mp ht

Premises used: mem_nhdsWithin, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ ν : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf_1 : LocallyIntegrableOn f s μ
h : ν.restrict s ≤ μ.restrict s
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hf : IntegrableOn f t μ
u : Set X
hu : IsOpen[inst_1] u
hxu : x ∈ u
hut : u ∩ s ⊆ t
⊢ IntegrableAtFilter f (𝓝[s] x) ν

Tactic:
⟨u ∩ s, inter_mem (mem_nhdsWithin.mpr ⟨u, hu, hxu, inter_subset_left⟩) self_mem_nhdsWithin,
    ?_⟩

Premises used: Iff.mpr, Filter.inter_mem, Set.inter_subset_left, mem_nhdsWithin, Inter.inter, MeasureTheory.IntegrableAtFilter, self_mem_nhdsWithin, And.intro, Exists.intro