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)ᶜ
a_1 : A
⊢ AEStronglyMeasurable (resolvent a_1) μ

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)ᶜ
h₁ : ∀ (a : A), Membership.mem (γ := Set A) {x : A | (fun (w : A) ↦ AEStronglyMeasurable (resolvent w) μ) x} a
h₂ h₃ : ∀ (a : A), AEStronglyMeasurable (resolvent a) μ
⊢ ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ

Tactic:
filter_upwards with _ using by 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)ᶜ
⊢ ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ

Tactic:
have resolvent_meas : ∀ᶠ w in nhds a, AEStronglyMeasurable (resolvent w) μ := by
    filter_upwards with _ using by 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) μ
h₁ :
  ∀ (x : 𝕜) (hx : x ∈ μ.support) (w : A) (hw : w ∈ s),
    ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
      HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
⊢ ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2

Tactic:
filter_upwards [support_mem_ae] with x hx w hw

Premises used: MeasureTheory.Measure.support_mem_ae
-- 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) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
h₁ :
  HPow.hPow (β := ℕ) ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖⁻¹ 2 ≤
    HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
⊢ ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
    HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2

Tactic:
grw [resolvent, Ring.inverse_eq_inv, norm_pow, norm_inv]

Premises used: norm_pow, Ring.inverse_eq_inv, norm_inv, resolvent
-- 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) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
h₁ :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖
⊢ HPow.hPow (β := ℕ) ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖⁻¹ 2 ≤
    HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2

Tactic:
gcongr
-- 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) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
    infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) -
      infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2

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
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
hab :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
hcd : ‖a - w‖ ≤ infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2
⊢ infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) -
      infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖ - ‖a - w‖

Tactic:
gcongr
-- 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) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ 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 : 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) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
hab : dist a ((algebraMap 𝕜 A : (a : 𝕜) → A) x) ≤ ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
hab₁ : dist ((algebraMap 𝕜 A : (a : 𝕜) → A) x) a ≤ ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
hab₂ hab₃ :
  ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖ ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) 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) (by simp [hx]), dist_comm,
            dist_eq_norm]

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 : 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) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
hcd : ‖a - w‖ < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2
⊢ ‖a - w‖ ≤ infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2

Tactic:
apply le_of_lt

Premises used: le_of_lt
-- 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) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ ‖a - w‖ < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2

Tactic:
simpa [s, ← dist_eq_norm, dist_comm w a] using hw

Premises used: dist_eq_norm, dist_comm
-- 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) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
grw :
  ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a + (a - w)‖ ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖
⊢ ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖ - ‖a - w‖ ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖

Tactic:
grw [norm_sub_le_norm_add]

Premises used: norm_sub_le_norm_add
-- 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) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a + (a - w)‖ ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖

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
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
calc :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
    infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) -
      infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2
calc₁ :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) -
      infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖ - ‖a - w‖
calc₂ :
  ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖ - ‖a - w‖ ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖
⊢ infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖

Tactic:
calc infDist a (algebraMap 𝕜 A '' μ.support) / 2
      _ ≤ infDist a (algebraMap 𝕜 A '' μ.support)
        - infDist a (algebraMap 𝕜 A '' μ.support) / 2 := by grind
      _ ≤ ‖(algebraMap 𝕜 A) x - a‖ - ‖a - w‖ := by
        gcongr
        · grw [infDist_le_dist_of_mem (y := (algebraMap 𝕜 A) x) (by simp [hx]), dist_comm,
            dist_eq_norm]
        · apply le_of_lt
          simpa [s, ← dist_eq_norm, dist_comm w a] using hw
      _ ≤ ‖(algebraMap 𝕜 A) x - w‖ := by grw [norm_sub_le_norm_add]; grind

Premises used: Algebra.algebraMap, Metric.infDist, MeasureTheory.Measure.support, Set.image, DFunLike.coe
-- 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) μ
⊢ ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2

Tactic:
have resolvent'_bound : ∀ᵐ x ∂μ, ∀ w ∈ s,
      ‖(resolvent w x) ^ 2‖ ≤ ((infDist a (algebraMap 𝕜 A '' μ.support)) / 2)⁻¹ ^ 2 := by
    filter_upwards [support_mem_ae] with x hx w hw
    grw [resolvent, Ring.inverse_eq_inv, norm_pow, norm_inv]
    gcongr
    calc infDist a (algebraMap 𝕜 A '' μ.support) / 2
      _ ≤ infDist a (algebraMap 𝕜 A '' μ.support)
        - infDist a (algebraMap 𝕜 A '' μ.support) / 2 := by grind
      _ ≤ ‖(algebraMap 𝕜 A) x - a‖ - ‖a - w‖ := by
        gcongr
        · grw [infDist_le_dist_of_mem (y := (algebraMap 𝕜 A) x) (by simp [hx]), dist_comm,
            dist_eq_norm]
        · apply le_of_lt
          simpa [s, ← dist_eq_norm, dist_comm w a] using hw
      _ ≤ ‖(algebraMap 𝕜 A) x - w‖ := by grw [norm_sub_le_norm_add]; 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
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₁ :
  ∀ (x : 𝕜) (hx : x ∈ μ.support) (w : A) (hw : w ∈ s),
    HasDerivAt (fun (w : A) ↦ resolvent w x) (HPow.hPow (β := ℕ) (resolvent w x) 2) w
⊢ ∀ᵐ (x : 𝕜) ∂μ, ∀ w ∈ s, HasDerivAt (fun (w : A) ↦ resolvent w x) (HPow.hPow (β := ℕ) (resolvent w x) 2) w

Tactic:
filter_upwards [support_mem_ae] with x hx w hw

Premises used: MeasureTheory.Measure.support_mem_ae
-- 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 : w ∈ s
h₁ : x ∈ resolventSet 𝕜 w
⊢ HasDerivAt (fun (w : A) ↦ resolvent w x) (HPow.hPow (β := ℕ) (resolvent w x) 2) w

Tactic:
apply hasDerivAt_resolvent_const_right

Premises used: spectrum.hasDerivAt_resolvent_const_right
-- 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 : w ∈ s
⊢ Membership.mem (γ := Set A) ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ w

Tactic:
replace hw := hs_μ 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
x : 𝕜
hx : x ∈ μ.support
w : A
hw : Membership.mem (γ := Set A) ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ w
h₁ : ∀ (hw : ¬x ∈ resolventSet 𝕜 w), w ∉ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
⊢ x ∈ resolventSet 𝕜 w

Tactic:
contrapose! 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
x : 𝕜
hx : x ∈ μ.support
w : A
hw : ¬x ∈ resolventSet 𝕜 w
h₁ : Membership.mem (γ := Set A) ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) w
⊢ w ∉ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ

Tactic:
rw [Set.notMem_compl_iff]

Premises used: Set.notMem_compl_iff