awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound :
  ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
x : 𝕜
hx : x ∈ μ.support
w : A
hw : ¬x ∈ resolventSet 𝕜 w
right : (algebraMap 𝕜 A : (a : 𝕜) → A) x = w
⊢ Membership.mem (γ := Set A) ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) w

Tactic:
use x, hx
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound :
  ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
x : 𝕜
hx : x ∈ μ.support
w : A
hw : ¬x ∈ resolventSet 𝕜 w
⊢ (algebraMap 𝕜 A : (a : 𝕜) → A) x = w

Tactic:
simpa [resolventSet, sub_eq_zero] using hw

Premises used: sub_eq_zero, resolventSet
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound :
  ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
⊢ ∀ᵐ (x : 𝕜) ∂μ, ∀ w ∈ s, HasDerivAt (fun (w : A) ↦ resolvent w x) (HPow.hPow (β := ℕ) (resolvent w x) 2) w

Tactic:
have h_deriv : ∀ᵐ x ∂μ, ∀ w ∈ s, HasDerivAt (fun w ↦ resolvent w x) (resolvent w x ^ 2) w := by
    filter_upwards [support_mem_ae] with x hx w hw
    apply hasDerivAt_resolvent_const_right
    replace hw := hs_μ hw
    contrapose! hw
    rw [Set.notMem_compl_iff]
    use x, hx
    simpa [resolventSet, sub_eq_zero] using hw
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound :
  ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
h_deriv : ∀ᵐ (x : 𝕜) ∂μ, ∀ w ∈ s, HasDerivAt (fun (w : A) ↦ resolvent w x) (HPow.hPow (β := ℕ) (resolvent w x) 2) w
⊢ a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support

Tactic:
simp [ha]
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound :
  ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
h_deriv : ∀ᵐ (x : 𝕜) ∂μ, ∀ w ∈ s, HasDerivAt (fun (w : A) ↦ resolvent w x) (HPow.hPow (β := ℕ) (resolvent w x) 2) w
⊢ AEStronglyMeasurable.{u_1, u_2} (β := A) (fun (a_1 : 𝕜) ↦ HPow.hPow (β := ℕ) (resolvent a a_1) 2) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound :
  ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
h_deriv : ∀ᵐ (x : 𝕜) ∂μ, ∀ w ∈ s, HasDerivAt (fun (w : A) ↦ resolvent w x) (HPow.hPow (β := ℕ) (resolvent w x) 2) w
funProp : ‖HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2‖ₑ ≠ ⊤
⊢ Integrable (ε := ℝ)
    (fun (a_1 : 𝕜) ↦ HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound :
  ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
h_deriv : ∀ᵐ (x : 𝕜) ∂μ, ∀ w ∈ s, HasDerivAt (fun (w : A) ↦ resolvent w x) (HPow.hPow (β := ℕ) (resolvent w x) 2) w
⊢ HasDerivAt (F := A) (fun (a : A) ↦ ∫ (x : 𝕜), resolvent a x ∂μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a

Tactic:
exact hasDerivAt_integral_of_dominated_loc_of_deriv_le hs_z resolvent_meas
    (integrable_resolvent (by simp [ha])) (by fun_prop) resolvent'_bound (by fun_prop) h_deriv |>.2

Premises used: MeasureTheory.integrable_resolvent, hasDerivAt_integral_of_dominated_loc_of_deriv_le, And.right
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : NormedAlgebra 𝕜 ℂ
μ : Measure 𝕜
inst_6 : IsFiniteMeasure μ
rw : DifferentiableOn ℂ (E := ℂ) (resolventTransform μ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)ᶜ
rw₁ : IsOpen (X := ℂ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)ᶜ
⊢ AnalyticOn ℂ (E := ℂ) (resolventTransform μ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)ᶜ

Tactic:
rw [analyticOn_iff_differentiableOn]

Premises used: Complex.analyticOn_iff_differentiableOn
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : NormedAlgebra 𝕜 ℂ
μ : Measure 𝕜
inst_6 : IsFiniteMeasure μ
z : ℂ
hz : Membership.mem (γ := Set ℂ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)ᶜ z
⊢ DifferentiableWithinAt ℂ (resolventTransform μ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)ᶜ z

Tactic:
(hasDerivAt_resolventTransform z hz).differentiableAt.differentiableWithinAt

Premises used: MeasureTheory.hasDerivAt_resolventTransform, HasDerivAt.differentiableAt, DifferentiableAt.differentiableWithinAt
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : NormedAlgebra 𝕜 ℂ
μ : Measure 𝕜
inst_6 : IsFiniteMeasure μ
z : ℂ
hz : Membership.mem (γ := Set ℂ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)ᶜ z
⊢ DifferentiableWithinAt ℂ (resolventTransform μ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)ᶜ z

Tactic:
exact (hasDerivAt_resolventTransform z hz).differentiableAt.differentiableWithinAt

Premises used: MeasureTheory.hasDerivAt_resolventTransform, HasDerivAt.differentiableAt, DifferentiableAt.differentiableWithinAt
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : NormedAlgebra 𝕜 ℂ
μ : Measure 𝕜
inst_6 : IsFiniteMeasure μ
apply : IsClosed (X := ℂ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)
⊢ IsOpen (X := ℂ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)ᶜ

Tactic:
apply isOpen_compl_iff.mpr

Premises used: Iff.mpr, isOpen_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : NormedAlgebra 𝕜 ℂ
μ : Measure 𝕜
inst_6 : IsFiniteMeasure μ
⊢ IsClosed (X := ℂ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)

Tactic:
(Topology.IsClosedEmbedding.isClosed_iff_image_isClosed ?_).mp isClosed_support

Premises used: Topology.IsClosedEmbedding.isClosed_iff_image_isClosed, Iff.mp, MeasureTheory.Measure.isClosed_support
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : NormedAlgebra 𝕜 ℂ
μ : Measure 𝕜
inst_6 : IsFiniteMeasure μ
refine : Topology.IsClosedEmbedding (X := 𝕜) (Y := ℂ) (⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ)
⊢ IsClosed (X := ℂ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)

Tactic:
refine (Topology.IsClosedEmbedding.isClosed_iff_image_isClosed ?_).mp isClosed_support

Premises used: Topology.IsClosedEmbedding.isClosed_iff_image_isClosed, Iff.mp, MeasureTheory.Measure.isClosed_support
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : NormedAlgebra 𝕜 ℂ
μ : Measure 𝕜
inst_6 : IsFiniteMeasure μ
⊢ Topology.IsClosedEmbedding (X := 𝕜) (Y := ℂ) (⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ)

Tactic:
(algebraMap_isometry 𝕜 ℂ).isClosedEmbedding

Premises used: algebraMap_isometry, Isometry.isClosedEmbedding, Complex
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : NormedAlgebra 𝕜 ℂ
μ : Measure 𝕜
inst_6 : IsFiniteMeasure μ
⊢ Topology.IsClosedEmbedding (X := 𝕜) (Y := ℂ) (⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ)

Tactic:
exact (algebraMap_isometry 𝕜 ℂ).isClosedEmbedding

Premises used: algebraMap_isometry, Isometry.isClosedEmbedding, Complex
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
δ : Type u_4
γ : Type u_5
ι : Type u_6
m0_1 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ_1 μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s'_1 t_1 : Set α
m0 : MeasurableSpace α
s : Set α
μ : Measure α
s' : Set α
hs' : MeasurableSet s'
t : Set α
this :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∩ s') : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((s ∩ t) \ s') : ℝ≥0∞)
⊢ (((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
        (a : Set α) → ℝ≥0∞)
      t =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
            (a : Set α) → ℝ≥0∞)
          (t ∩ s') :
        ℝ≥0∞)
      ((((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
            (a : Set α) → ℝ≥0∞)
          (t \ s') :
        ℝ≥0∞)

Tactic:
simpa [← Set.inter_assoc, Set.inter_comm _ s, ← inter_diff_assoc]

Premises used: Set.inter_comm, Set.inter_diff_assoc, Set.inter_assoc
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
δ : Type u_4
γ : Type u_5
ι : Type u_6
m0_1 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ_1 μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s'_1 t_1 : Set α
m0 : MeasurableSpace α
s : Set α
μ : Measure α
s' : Set α
hs' : MeasurableSet s'
t : Set α
suffices :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∩ s') : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((s ∩ t) \ s') : ℝ≥0∞)
⊢ (((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
        (a : Set α) → ℝ≥0∞)
      t =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
            (a : Set α) → ℝ≥0∞)
          (t ∩ s') :
        ℝ≥0∞)
      ((((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
            (a : Set α) → ℝ≥0∞)
          (t \ s') :
        ℝ≥0∞)

Tactic:
suffices μ (s ∩ t) = μ (s ∩ t ∩ s') + μ ((s ∩ t) \ s') by
      simpa [← Set.inter_assoc, Set.inter_comm _ s, ← inter_diff_assoc]
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
δ : Type u_4
γ : Type u_5
ι : Type u_6
m0_1 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ_1 μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s'_1 t_1 : Set α
m0 : MeasurableSpace α
s : Set α
μ : Measure α
s' : Set α
hs' : MeasurableSet s'
t : Set α
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∩ s') : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((s ∩ t) \ s') : ℝ≥0∞)

Tactic:
le_toOuterMeasure_caratheodory _ _ hs' _

Premises used: MeasureTheory.le_toOuterMeasure_caratheodory
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
δ : Type u_4
γ : Type u_5
ι : Type u_6
m0_1 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ_1 μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s'_1 t_1 : Set α
m0 : MeasurableSpace α
s : Set α
μ : Measure α
s' : Set α
hs' : MeasurableSet s'
t : Set α
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∩ s') : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((s ∩ t) \ s') : ℝ≥0∞)

Tactic:
exact le_toOuterMeasure_caratheodory _ _ hs' _

Premises used: MeasureTheory.le_toOuterMeasure_caratheodory
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
_m0 : MeasurableSpace α
s : Set α
μ : Measure α
⊢ (restrictₗ s : (a : Measure α) → Measure α) μ = μ.restrict s

Tactic:
rfl

Premises used: MeasureTheory.Measure.restrict, rfl
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
simp_rw :
  Eq.{u_2 + 1} (α := OuterMeasure α) (toOuterMeasure ((restrictₗ s : (a : Measure α) → Measure α) μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₁ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure ((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₂ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure
      (({
            toFun := fun (μ : Measure α) ↦
              OuterMeasure.toMeasure
                ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure) ⋯,
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : Measure α) → Measure α)
        μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₃ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure
      (({
            toFun := fun (μ : Measure α) ↦
              OuterMeasure.toMeasure
                ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure) ⋯,
            map_add' := ⋯ } :
          (a : Measure α) → Measure α)
        μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₄ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure
      (OuterMeasure.toMeasure ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure) ⋯))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₅ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (OuterMeasure.trim ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₆ :
  Eq (α := OuterMeasure α) ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.trim : OuterMeasure α)
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α)
⊢ (μ.restrict s).toOuterMeasure = (OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure

Tactic:
simp_rw [restrict, restrictₗ, liftLinear, LinearMap.coe_mk, AddHom.coe_mk,
    toMeasure_toOuterMeasure, OuterMeasure.restrict_trim h, μ.trimmed]

Premises used: LinearMap.coe_mk, MeasureTheory.OuterMeasure.restrict_trim, MeasureTheory.Measure.restrict, MeasureTheory.Measure.trimmed, MeasureTheory.Measure.liftLinear, MeasureTheory.toMeasure_toOuterMeasure, AddHom.coe_mk, MeasureTheory.Measure.restrictₗ
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t (μ.restrict s)
⊢ NullMeasurableSet t ((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ)

Tactic:
rw [restrict, restrictₗ] at ht

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.Measure.restrictₗ
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t ((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ)
rw :
  Eq (α := ℝ≥0∞) ((((restrictₗ s : (a : Measure α) → Measure α) μ : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ : Measure α) : (a : Set α) → ℝ≥0∞) t :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞)
    ((((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₃ : Eq (α := ℝ≥0∞) ((μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₄ rw₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
rw [← restrictₗ_apply, restrictₗ, liftLinear_apply₀ _ ht, OuterMeasure.restrict_apply,
    coe_toOuterMeasure]

Premises used: MeasureTheory.Measure.coe_toOuterMeasure, MeasureTheory.Measure.liftLinear_apply₀, MeasureTheory.OuterMeasure.restrict_apply, MeasureTheory.Measure.restrictₗ_apply, MeasureTheory.Measure.restrictₗ
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
restrict_apply₀ ht.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.restrict_apply₀
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
_m0 : MeasurableSpace α
s s' : Set α
μ ν : Measure α
hs : s ≤ᶠ[ae μ] s'
hμν : μ ≤ ν
⊢ μ.restrict s ≤ ν.restrict s'

Tactic:
Measure.le_iff.2 fun t ht => calc
    μ.restrict s t = μ (t ∩ s) := restrict_apply ht
    _ ≤ μ (t ∩ s') := (measure_mono_ae <| hs.mono fun _x hx ⟨hxt, hxs⟩ => ⟨hxt, hx hxs⟩)
    _ ≤ ν (t ∩ s') := le_iff'.1 hμν (t ∩ s')
    _ = ν.restrict s' t := (restrict_apply ht).symm

Premises used: Iff.mpr, Trans.trans, MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.le_iff', MeasureTheory.measure_mono_ae, Inter.inter, Filter.Eventually.mono, MeasureTheory.Measure.le_iff, And.intro, Iff.mp, _private.0.MeasureTheory.Measure.restrict_mono'.match_1, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
_m0 : MeasurableSpace α
s s' : Set α
hs : s ⊆ s'
μ ν : Measure α
hμν : μ ≤ ν
⊢ μ.restrict s ≤ ν.restrict s'

Tactic:
restrict_mono' (ae_of_all _ hs) hμν

Premises used: MeasureTheory.Measure.restrict_mono', MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
x : MeasurableSpace α
μ ν : Measure α
h : μ ≤ ν
s : Set α
⊢ μ.restrict s ≤ ν.restrict s

Tactic:
restrict_mono subset_rfl h

Premises used: MeasureTheory.Measure.restrict_mono, subset_rfl
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
x : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
⊢ μ.restrict s ≤ μ.restrict t

Tactic:
restrict_mono h le_rfl

Premises used: le_rfl, MeasureTheory.Measure.restrict_mono
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ≤ᶠ[ae μ] t
⊢ μ.restrict s ≤ μ.restrict t

Tactic:
restrict_mono' h (le_refl μ)

Premises used: MeasureTheory.Measure.restrict_mono', le_refl
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s =ᶠ[ae μ] t
⊢ μ.restrict s = μ.restrict t

Tactic:
le_antisymm (restrict_mono_ae h.le) (restrict_mono_ae h.symm.le)

Premises used: Filter.EventuallyEq.le, le_antisymm, MeasureTheory.Measure.restrict_mono_ae, Filter.EventuallyEq.symm