awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → 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
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
refine : Topology.IsClosedEmbedding.{u_1, u_2} (X := 𝕜) (Y := A) (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A)
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → 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
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
⊢ Topology.IsClosedEmbedding.{u_1, u_2} (X := 𝕜) (Y := A) (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A)

Tactic:
(algebraMap_isometry 𝕜 A).isClosedEmbedding

Premises used: algebraMap_isometry, Isometry.isClosedEmbedding
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
⊢ Topology.IsClosedEmbedding.{u_1, u_2} (X := 𝕜) (Y := A) (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A)

Tactic:
exact (algebraMap_isometry 𝕜 A).isClosedEmbedding

Premises used: algebraMap_isometry, Isometry.isClosedEmbedding
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
⊢ 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)

Tactic:
have : 0 < infDist a (algebraMap 𝕜 A '' μ.support) := by
    refine (IsClosed.notMem_iff_infDist_pos ?_ ((Set.nonempty_of_mem hx).image _)).mp hz
    refine (Topology.IsClosedEmbedding.isClosed_iff_image_isClosed ?_).mp isClosed_support
    exact (algebraMap_isometry 𝕜 A).isClosedEmbedding
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
grw :
  Membership.mem.{u_2, u_2} (α := A) (γ := Set A) ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
    ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A)
⊢ infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖

Tactic:
grw [infDist_le_dist_of_mem (y := (algebraMap 𝕜 A) x), ← dist_eq_norm, dist_comm]

Premises used: Metric.infDist_le_dist_of_mem, dist_eq_norm, dist_comm
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
⊢ Membership.mem.{u_2, u_2} (α := A) (γ := Set A) ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
    ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A)

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
⊢ infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖

Tactic:
have : infDist a (algebraMap 𝕜 A '' μ.support) ≤ ‖(algebraMap 𝕜 A) x - a‖ := by
    grw [infDist_le_dist_of_mem (y := (algebraMap 𝕜 A) x), ← dist_eq_norm, dist_comm]
    simp [hx]
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
this_1 : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
this :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
linarith :
  ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖ ≤ 0 →
    0 - infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) +
          (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) -
            ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖) +
        (‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖ - 0) =
      0
⊢ 0 < ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
this_1 : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
this :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
⊢ 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
this_1 : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
this :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
grw :
  ‖Ring.inverse (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a)‖ ≤
    (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
grw₁ :
  ‖(HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a)⁻¹‖ ≤
    (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
grw₂ :
  ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖⁻¹ ≤
    (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
grw₃ :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
grw₄ grw₅ :
  ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖ ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
⊢ ‖resolvent a x‖ ≤ (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹

Tactic:
grw [resolvent, Ring.inverse_eq_inv', norm_inv, inv_le_inv₀ (by linarith) (by positivity), this]

Premises used: Ring.inverse_eq_inv', norm_inv, resolvent, inv_le_inv₀
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : HereditarilyLindelofSpace 𝕜
inst_6 : OpensMeasurableSpace 𝕜
inst_7 : CompleteSpace A
inst_8 : SecondCountableTopology A
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μ : Measure 𝕜
inst_11 : IsFiniteMeasure μ
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
⊢ AEStronglyMeasurable (resolvent a) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : HereditarilyLindelofSpace 𝕜
inst_6 : OpensMeasurableSpace 𝕜
inst_7 : CompleteSpace A
inst_8 : SecondCountableTopology A
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μ : Measure 𝕜
inst_11 : IsFiniteMeasure μ
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
refine : HasFiniteIntegral (resolvent a) μ
⊢ Integrable (resolvent a) μ

Tactic:
refine ⟨by fun_prop, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : HereditarilyLindelofSpace 𝕜
inst_6 : OpensMeasurableSpace 𝕜
inst_7 : CompleteSpace A
inst_8 : SecondCountableTopology A
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μ : Measure 𝕜
inst_11 : IsFiniteMeasure μ
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
hC : ∀ᵐ (a_1 : 𝕜) ∂μ, ‖resolvent a a_1‖ ≤ (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
C : ℝ
⊢ HasFiniteIntegral (resolvent a) μ

Tactic:
apply HasFiniteIntegral.of_bounded

Premises used: MeasureTheory.HasFiniteIntegral.of_bounded
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : HereditarilyLindelofSpace 𝕜
inst_6 : OpensMeasurableSpace 𝕜
inst_7 : CompleteSpace A
inst_8 : SecondCountableTopology A
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μ : Measure 𝕜
inst_11 : IsFiniteMeasure μ
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
⊢ ‖resolvent a x‖ ≤ (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹

Tactic:
norm_resolvent_le_inv_infDist_support hz hx

Premises used: MeasureTheory.norm_resolvent_le_inv_infDist_support
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : NormedAlgebra 𝕜 A
m𝕜 : MeasurableSpace 𝕜
μ : Measure 𝕜
⊢ Eq.{u_2 + 1} (α := (a : A) → A) (resolventTransform μ) fun (a : A) ↦ ∫ (x : 𝕜), resolvent a x ∂μ

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : NormedAlgebra 𝕜 A
m𝕜 : MeasurableSpace 𝕜
μ : Measure 𝕜
a : A
⊢ resolventTransform μ a = ∫ (x : 𝕜), resolvent a x ∂μ

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : NormedAlgebra 𝕜 A
m𝕜 : MeasurableSpace 𝕜
h : ∀ (x : A), resolventTransform.{u_1, u_2} (𝕜 := 𝕜) (m𝕜 := m𝕜) 0 x = 0 x
⊢ Eq.{u_2 + 1} (α := (a : A) → A) (resolventTransform.{u_1, u_2} (𝕜 := 𝕜) (m𝕜 := m𝕜) 0) 0

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : NormedAlgebra 𝕜 A
m𝕜 : MeasurableSpace 𝕜
x : A
⊢ resolventTransform.{u_1, u_2} (𝕜 := 𝕜) (m𝕜 := m𝕜) 0 x = 0 x

Tactic:
simp [resolventTransform_def]

Premises used: MeasureTheory.resolventTransform_def
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : NormedAlgebra 𝕜 A
m𝕜 : MeasurableSpace 𝕜
inst_4 : MeasurableSingletonClass 𝕜
inst_5 : CompleteSpace A
x : 𝕜
a : A
⊢ resolventTransform (m𝕜 := m𝕜) (dirac x) a = resolvent a x

Tactic:
simp [resolventTransform_def]

Premises used: MeasureTheory.resolventTransform_def
-- 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
pos :
  ∀ (h : μ.support.Nonempty), HasDerivAt (resolventTransform μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a
neg : ∀ (h : μ.support = ∅), HasDerivAt (resolventTransform μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a
⊢ HasDerivAt (resolventTransform μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a

Tactic:
by_cases! h : μ.support.Nonempty

Premises used: MeasureTheory.Measure.support, Set.Nonempty
-- 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 = ∅
⊢ HasDerivAt (resolventTransform μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a

Tactic:
simp [support_eq_empty_iff.mp h]

Premises used: MeasureTheory.Measure.support_eq_empty_iff, Iff.mp
-- 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
⊢ 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)

Tactic:
(IsClosed.notMem_iff_infDist_pos ?_ (h.image _)).mp ha

Premises used: Set.Nonempty.image, Iff.mp, IsClosed.notMem_iff_infDist_pos
-- 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
refine : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
⊢ 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)

Tactic:
refine (IsClosed.notMem_iff_infDist_pos ?_ (h.image _)).mp ha

Premises used: Set.Nonempty.image, Iff.mp, IsClosed.notMem_iff_infDist_pos
-- 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
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → 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
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
refine : Topology.IsClosedEmbedding.{u_1, u_2} (X := 𝕜) (Y := A) (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A)
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → 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
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
⊢ Topology.IsClosedEmbedding.{u_1, u_2} (X := 𝕜) (Y := A) (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A)

Tactic:
(algebraMap_isometry 𝕜 A).isClosedEmbedding

Premises used: algebraMap_isometry, Isometry.isClosedEmbedding
-- 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
⊢ Topology.IsClosedEmbedding.{u_1, u_2} (X := 𝕜) (Y := A) (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A)

Tactic:
exact (algebraMap_isometry 𝕜 A).isClosedEmbedding

Premises used: algebraMap_isometry, Isometry.isClosedEmbedding
-- 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
⊢ 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)

Tactic:
have : 0 < infDist a (algebraMap 𝕜 A '' μ.support) := by
    refine (IsClosed.notMem_iff_infDist_pos ?_ (h.image _)).mp ha
    refine (Topology.IsClosedEmbedding.isClosed_iff_image_isClosed ?_).mp isClosed_support
    exact (algebraMap_isometry 𝕜 A).isClosedEmbedding
-- 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)
⊢ 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2

Tactic:
positivity
-- 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)
⊢ s ∈ 𝓝 a

Tactic:
have hs_z : s ∈ 𝓝 a := ball_mem_nhds _ (by positivity)
-- 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
unfold :
  ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2) ⊆
    ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
⊢ s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ

Tactic:
unfold s
-- 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
grw :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
    infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
⊢ ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2) ⊆
    ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ

Tactic:
grw [ball_subset_ball, ball_infDist_subset_compl]

Premises used: Metric.ball_infDist_subset_compl, Metric.ball_subset_ball
-- 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
⊢ infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
    infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)

Tactic:
grind
-- 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
⊢ s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ

Tactic:
have hs_μ : s ⊆ (algebraMap 𝕜 A '' μ.support)ᶜ := by
    unfold s
    grw [ball_subset_ball, ball_infDist_subset_compl]
    grind