awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
⊢ P.InnerRegularWRT IsCompact IsClosed
have rw : P.InnerRegularWRT (IsCompact ∘ closure) IsClosed
Tactic: rw [← innerRegularWRT_isCompact_closure_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
⊢ P.InnerRegular
have suffices : P.InnerRegularCompactLTTop
Tactic: suffices P.InnerRegularCompactLTTop from inferInstance
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
⊢ P.InnerRegularCompactLTTop
have refine_1 : P.InnerRegularWRT IsCompact IsOpen
Tactic: refine ⟨Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
refine_1 : P.InnerRegularWRT IsCompact IsOpen
⊢ P.InnerRegularCompactLTTop
have refine_2 : ∀ ⦃s U : Set α⦄, IsCompact s → IsOpen U → IsCompact (s \ U)
Tactic: refine ⟨Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
μ : Measure α
⊢ μ.InnerRegularCompactLTTop
have innerRegular : μ.InnerRegularWRT IsCompact fun (s : Set α) ↦
  MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
μ : Measure α
A : Set α
⊢ (fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) A →
    ∀ r < (μ : (a : Set α) → ℝ≥0∞) A, ∃ K ⊆ A, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have innerRegular : ∀ (hA1 : MeasurableSet A) (hA2 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ∀ r < (μ : (a : Set α) → ℝ≥0∞) A, ∃ K ⊆ A, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: ⟨hA1, hA2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
μ : Measure α
A : Set α
hA1 : MeasurableSet A
hA2 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
⊢ ∃ K ⊆ A, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have := Fact.mk hA2.lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
μ : Measure α
A : Set α
hA1 : MeasurableSet A
hA2 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ ∃ K ⊆ A, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have hA2' : Ne (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hA2' : (μ.restrict A) A ≠ ⊤ := by
    rwa [Measure.restrict_apply_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
μ : Measure α
A : Set α
hA1 : MeasurableSet A
hA2 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞))
hA2' : Ne (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ K ⊆ A, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have hr' : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) A
Tactic: have hr' : r < μ.restrict A A := by
    rwa [Measure.restrict_apply_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
μ : Measure α
A : Set α
hA1 : MeasurableSet A
hA2 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞))
hA2' : Ne (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
hr' : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) A
⊢ ∃ K ⊆ A, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have innerRegular : ∀ (K : Set α) (hK1 : K ⊆ A) (hK2 : IsCompact K) (hK3 : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K),
  ∃ K ⊆ A, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: obtain ⟨K, ⟨hK1, hK2, hK3⟩⟩ := MeasurableSet.exists_lt_isCompact_of_ne_top hA1 hA2' hr'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
μ : Measure α
A : Set α
hA1 : MeasurableSet A
hA2 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞))
hA2' : Ne (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
hr' : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ A, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have right : r < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: use K, hK1, hK2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
μ : Measure α
A : Set α
hA1 : MeasurableSet A
hA2 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞))
hA2' : Ne (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
hr' : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K
⊢ r < (μ : (a : Set α) → ℝ≥0∞) K
have right : ∀ (hK3 : r < (μ : (a : Set α) → ℝ≥0∞) K), r < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: rwa [Measure.restrict_eq_self μ hK1] at hK3
Cleared hypotheses: hK3
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
this :
  P.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) fun (s : Set α) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((P : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ P.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) MeasurableSet
have h : ∀ (x : Set α), MeasurableSet x ↔ MeasurableSet x ∧ Ne (α := ℝ≥0∞) ((P : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: convert! this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
this :
  P.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) fun (s : Set α) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((P : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : Set α
⊢ MeasurableSet x ↔ MeasurableSet x ∧ Ne (α := ℝ≥0∞) ((P : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)
have h : MeasurableSet x → Ne (α := ℝ≥0∞) ((P : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: simp only [iff_self_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
⊢ P.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) MeasurableSet
have suffices : P.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) fun (s : Set α) ↦
  MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((P : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: suffices P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s)
      fun s ↦ MeasurableSet s ∧ P s ≠ ∞ by
    convert! this
    simp only [iff_self_and]
    exact fun _ ↦ measure_ne_top P _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
⊢ P.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) fun (s : Set α) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((P : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_1 : P.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) IsOpen
Tactic: refine Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
refine_1 : P.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) IsOpen
⊢ P.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) fun (s : Set α) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((P : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_2 : ∀ ⦃s U : Set α⦄, IsCompact s ∧ IsClosed s → IsOpen U → IsCompact (s \ U) ∧ IsClosed (s \ U)
Tactic: refine Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
a : A
inst_2 : OpensMeasurableSpace 𝕜
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : CompleteSpace A
inst_6 : MeasurableSpace A
inst_7 : BorelSpace A
⊢ Measurable.{u_1, u_2} (α := 𝕜) (resolvent a)
have h1 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)
Tactic: have h1 : ContinuousOn (resolvent (R := 𝕜) a) (resolventSet 𝕜 a) :=
    HasDerivAt.continuousOn (fun _ hx ↦ hasDerivAt_resolvent_const_left hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
a : A
inst_2 : OpensMeasurableSpace 𝕜
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : CompleteSpace A
inst_6 : MeasurableSpace A
inst_7 : BorelSpace A
h1 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)
⊢ ContinuousOn (resolvent a) (resolventSet 𝕜 a)ᶜ
have rw : Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  ((resolventSet 𝕜 a)ᶜ.restrict (π := fun (a : 𝕜) ↦ A) (resolvent a))
Tactic: rw [continuousOn_iff_continuous_restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
a : A
inst_2 : OpensMeasurableSpace 𝕜
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : CompleteSpace A
inst_6 : MeasurableSpace A
inst_7 : BorelSpace A
h1 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((resolventSet 𝕜 a)ᶜ.restrict (π := fun (a : 𝕜) ↦ A) (resolvent a))
have h : ∀ (x : (↑(resolventSet 𝕜 a)ᶜ : Type u_1)), (resolventSet 𝕜 a)ᶜ.restrict (π := fun (a : 𝕜) ↦ A) (resolvent a) x = 0
Tactic: convert continuous_const (y := (0 : A)) with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
a : A
inst_2 : OpensMeasurableSpace 𝕜
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : CompleteSpace A
inst_6 : MeasurableSpace A
inst_7 : BorelSpace A
h1 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)
⊢ Measurable.{u_1, u_2} (α := 𝕜) (resolvent a)
have h2 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)ᶜ
Tactic: have h2 : ContinuousOn (resolvent (R := 𝕜) a) (resolventSet 𝕜 a)ᶜ := by
    rw [continuousOn_iff_continuous_restrict]
    convert continuous_const (y := (0 : A)) with x
    simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
a : A
inst_2 : OpensMeasurableSpace 𝕜
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : CompleteSpace A
inst_6 : MeasurableSpace A
inst_7 : BorelSpace A
h1 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)
h2 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)ᶜ
⊢ Measurable.{u_1, u_2} (α := 𝕜) (resolvent a)
have h3 : MeasurableSet (resolventSet 𝕜 a)
Tactic: have h3 : MeasurableSet (resolventSet 𝕜 a) := (isOpen_resolventSet a).measurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
a : A
inst_2 : OpensMeasurableSpace 𝕜
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : CompleteSpace A
inst_6 : MeasurableSpace A
inst_7 : BorelSpace A
⊢ Measurable.{u_1, u_2} (α := 𝕜) (resolvent a)
have have : ∀ (h1 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)), Measurable.{u_1, u_2} (α := 𝕜) (resolvent a)
Tactic: classical
  have h1 : ContinuousOn (resolvent (R := 𝕜) a) (resolventSet 𝕜 a) :=
    HasDerivAt.continuousOn (fun _ hx ↦ hasDerivAt_resolvent_const_left hx)
  have h2 : ContinuousOn (resolvent (R := 𝕜) a) (resolventSet 𝕜 a)ᶜ := by
    rw [continuousOn_iff_continuous_restrict]
    convert continuous_const (y := (0 : A)) with x
    simp
  have h3 : MeasurableSet (resolventSet 𝕜 a) := (isOpen_resolventSet a).measurableSet
  simpa using h1.measurable_piecewise h2 h3
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
a : A
inst_2 : OpensMeasurableSpace 𝕜
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : CompleteSpace A
inst_6 : MeasurableSpace A
inst_7 : BorelSpace A
have have₁ have₂ : ∀ (h1 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)), Measurable.{u_1, u_2} (α := 𝕜) (resolvent a)
⊢ Measurable.{u_1, u_2} (α := 𝕜) (resolvent a)
have have₃ : ∀ (h1 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)) (h2 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)ᶜ),
  Measurable.{u_1, u_2} (α := 𝕜) (resolvent a)
Tactic: classical
  have h1 : ContinuousOn (resolvent (R := 𝕜) a) (resolventSet 𝕜 a) :=
    HasDerivAt.continuousOn (fun _ hx ↦ hasDerivAt_resolvent_const_left hx)
  have h2 : ContinuousOn (resolvent (R := 𝕜) a) (resolventSet 𝕜 a)ᶜ := by
    rw [continuousOn_iff_continuous_restrict]
    convert continuous_const (y := (0 : A)) with x
    simp
  have h3 : MeasurableSet (resolventSet 𝕜 a) := (isOpen_resolventSet a).measurableSet
  simpa using h1.measurable_piecewise h2 h3
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
a : A
inst_2 : OpensMeasurableSpace 𝕜
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : CompleteSpace A
inst_6 : MeasurableSpace A
inst_7 : BorelSpace A
have have₁ have₂ : ∀ (h1 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)), Measurable.{u_1, u_2} (α := 𝕜) (resolvent a)
have₃ :
  ∀ (h1 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)) (h2 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)ᶜ),
    Measurable.{u_1, u_2} (α := 𝕜) (resolvent a)
⊢ Measurable.{u_1, u_2} (α := 𝕜) (resolvent a)
have have₄ : ∀ (h1 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)) (h2 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)ᶜ)
  (h3 : MeasurableSet (resolventSet 𝕜 a)), Measurable.{u_1, u_2} (α := 𝕜) (resolvent a)
Tactic: classical
  have h1 : ContinuousOn (resolvent (R := 𝕜) a) (resolventSet 𝕜 a) :=
    HasDerivAt.continuousOn (fun _ hx ↦ hasDerivAt_resolvent_const_left hx)
  have h2 : ContinuousOn (resolvent (R := 𝕜) a) (resolventSet 𝕜 a)ᶜ := by
    rw [continuousOn_iff_continuous_restrict]
    convert continuous_const (y := (0 : A)) with x
    simp
  have h3 : MeasurableSet (resolventSet 𝕜 a) := (isOpen_resolventSet a).measurableSet
  simpa using h1.measurable_piecewise h2 h3
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
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)
have refine : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
Tactic: refine (IsClosed.notMem_iff_infDist_pos ?_ ((Set.nonempty_of_mem hx).image _)).mp hz
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
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)
have refine : Topology.IsClosedEmbedding.{u_1, u_2} (X := 𝕜) (Y := A) (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A)
Tactic: refine (Topology.IsClosedEmbedding.isClosed_iff_image_isClosed ?_).mp isClosed_support
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (hypothesis)
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
⊢ ‖resolvent a x‖ ≤ (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
have this : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
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‖
have grw : Membership.mem.{u_2, u_2} (α := A) (γ := Set A) ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
  ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A)
Tactic: grw [infDist_le_dist_of_mem (y := (algebraMap 𝕜 A) x), ← dist_eq_norm, dist_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (hypothesis)
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)
⊢ ‖resolvent a x‖ ≤ (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
have this₁ : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
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 < ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
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‖
⊢ ‖resolvent a x‖ ≤ (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
have grw : ‖Ring.inverse (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a)‖ ≤
  (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
Tactic: grw [resolvent, Ring.inverse_eq_inv', norm_inv, inv_le_inv₀ (by linarith) (by positivity), this]