awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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.InnerRegularWRT IsCompact IsOpen

Tactic:
innerRegularWRT_isCompact_isOpen P

Premises used: MeasureTheory.innerRegularWRT_isCompact_isOpen
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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.InnerRegularWRT IsCompact IsOpen

Tactic:
exact innerRegularWRT_isCompact_isOpen P

Premises used: MeasureTheory.innerRegularWRT_isCompact_isOpen
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
⊢ ∀ ⦃s U : Set α⦄, IsCompact s → IsOpen U → IsCompact (s \ U)

Tactic:
fun s t hs_compact ht_open ↦ hs_compact.inter_right ht_open.isClosed_compl

Premises used: Set.Mem, Set.diff, setOf, IsOpen.isClosed_compl, IsCompact.inter_right, Not
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
⊢ ∀ ⦃s U : Set α⦄, IsCompact s → IsOpen U → IsCompact (s \ U)

Tactic:
exact fun s t hs_compact ht_open ↦ hs_compact.inter_right ht_open.isClosed_compl
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
μ : Measure α
innerRegular :
  μ.InnerRegularWRT IsCompact fun (s : Set α) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.InnerRegularCompactLTTop

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
μ : Measure α
A : Set α
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
⊢ (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

Tactic:
⟨hA1, hA2⟩
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have := Fact.mk hA2.lt_top
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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∞))
rwa rwa₁ rwa₂ rwa₃ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [Measure.restrict_apply_self]

Premises used: MeasureTheory.Measure.restrict_apply_self
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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∞))
⊢ Ne (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hA2' : (μ.restrict A) A ≠ ⊤ := by
    rwa [Measure.restrict_apply_self]
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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∞)
rwa rwa₁ rwa₂ rwa₃ : r < (μ : (a : Set α) → ℝ≥0∞) A
⊢ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) A

Tactic:
rwa [Measure.restrict_apply_self]

Premises used: MeasureTheory.Measure.restrict_apply_self
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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∞)
⊢ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) A

Tactic:
have hr' : r < μ.restrict A A := by
    rwa [Measure.restrict_apply_self]
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
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
⊢ ∃ 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'

Premises used: MeasurableSet.exists_lt_isCompact_of_ne_top
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
right : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ A, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
use K, hK1, hK2
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
right right₁ right₂ right₃ : ∀ (hK3 : r < (μ : (a : Set α) → ℝ≥0∞) K), r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
rwa [Measure.restrict_eq_self μ hK1] at hK3

Premises used: MeasureTheory.Measure.restrict_eq_self
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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) fun (s : Set α) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((P : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
this
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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∞)
h : ∀ (x : Set α), MeasurableSet x ↔ MeasurableSet x ∧ Ne (α := ℝ≥0∞) ((P : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ P.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) MeasurableSet

Tactic:
convert! this
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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 α
h : MeasurableSet x → Ne (α := ℝ≥0∞) ((P : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ MeasurableSet x ↔ MeasurableSet x ∧ Ne (α := ℝ≥0∞) ((P : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [iff_self_and]

Premises used: iff_self_and
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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 → Ne (α := ℝ≥0∞) ((P : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
fun _ ↦ measure_ne_top P _

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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 → Ne (α := ℝ≥0∞) ((P : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact fun _ ↦ measure_ne_top P _

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
suffices :
  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

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 _
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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∞)

Tactic:
Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_

Premises used: MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
refine_2 : ∀ ⦃s U : Set α⦄, IsCompact s ∧ IsClosed s → IsOpen U → IsCompact (s \ U) ∧ IsClosed (s \ U)
⊢ P.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) fun (s : Set α) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((P : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_

Premises used: MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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) IsOpen

Tactic:
innerRegularWRT_isCompact_isClosed_isOpen P

Premises used: MeasureTheory.innerRegularWRT_isCompact_isClosed_isOpen
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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) IsOpen

Tactic:
exact innerRegularWRT_isCompact_isClosed_isOpen P

Premises used: MeasureTheory.innerRegularWRT_isCompact_isClosed_isOpen
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
s t : Set α
hs_compact : IsCompact s
hs_closed : IsClosed s
ht_open : IsOpen t
⊢ IsCompact (s ∩ tᶜ) ∧ IsClosed (s ∩ tᶜ)

Tactic:
⟨hs_compact.inter_right ht_open.isClosed_compl,
      hs_closed.inter (isClosed_compl_iff.mpr ht_open)⟩

Premises used: Iff.mpr, IsOpen.isClosed_compl, And.intro, IsCompact.inter_right, IsClosed.inter, isClosed_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
s t : Set α
hs_compact : IsCompact s
hs_closed : IsClosed s
ht_open : IsOpen t
⊢ IsCompact (s ∩ tᶜ) ∧ IsClosed (s ∩ tᶜ)

Tactic:
exact ⟨hs_compact.inter_right ht_open.isClosed_compl,
      hs_closed.inter (isClosed_compl_iff.mpr ht_open)⟩
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
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
⊢ ContinuousOn (resolvent a) (resolventSet 𝕜 a)

Tactic:
have h1 : ContinuousOn (resolvent (R := 𝕜) a) (resolventSet 𝕜 a) :=
    HasDerivAt.continuousOn (fun _ hx ↦ hasDerivAt_resolvent_const_left hx)
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
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)
rw :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((resolventSet 𝕜 a)ᶜ.restrict (π := fun (a : 𝕜) ↦ A) (resolvent a))
⊢ ContinuousOn (resolvent a) (resolventSet 𝕜 a)ᶜ

Tactic:
rw [continuousOn_iff_continuous_restrict]

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
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]
    fun (x : (↑(resolventSet 𝕜 a)ᶜ : Type u_1)) ↦ 0

Tactic:
continuous_const (y := (0 : A))

Premises used: continuous_const
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
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)
h : ∀ (x : (↑(resolventSet 𝕜 a)ᶜ : Type u_1)), (resolventSet 𝕜 a)ᶜ.restrict (π := fun (a : 𝕜) ↦ A) (resolvent a) x = 0
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((resolventSet 𝕜 a)ᶜ.restrict (π := fun (a : 𝕜) ↦ A) (resolvent a))

Tactic:
convert continuous_const (y := (0 : A)) with x

Premises used: continuous_const
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
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)
x : (↑(resolventSet 𝕜 a)ᶜ : Type u_1)
⊢ (resolventSet 𝕜 a)ᶜ.restrict (π := fun (a : 𝕜) ↦ A) (resolvent a) x = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
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)ᶜ

Tactic:
have h2 : ContinuousOn (resolvent (R := 𝕜) a) (resolventSet 𝕜 a)ᶜ := by
    rw [continuousOn_iff_continuous_restrict]
    convert continuous_const (y := (0 : A)) with x
    simp
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
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)ᶜ
⊢ MeasurableSet (resolventSet 𝕜 a)

Tactic:
have h3 : MeasurableSet (resolventSet 𝕜 a) := (isOpen_resolventSet a).measurableSet
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
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)ᶜ
h3 : MeasurableSet (resolventSet 𝕜 a)
⊢ Measurable.{u_1, u_2} (α := 𝕜) (resolvent a)

Tactic:
simpa using h1.measurable_piecewise h2 h3

Premises used: ContinuousOn.measurable_piecewise
-- Module: Mathlib.MeasureTheory.Measure.ResolventTransform
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)
have₄ :
  ∀ (h1 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)) (h2 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)ᶜ)
    (h3 : MeasurableSet (resolventSet 𝕜 a)), Measurable.{u_1, u_2} (α := 𝕜) (resolvent 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
-- 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:
(IsClosed.notMem_iff_infDist_pos ?_ ((Set.nonempty_of_mem hx).image _)).mp hz

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

Tactic:
refine (IsClosed.notMem_iff_infDist_pos ?_ ((Set.nonempty_of_mem hx).image _)).mp hz

Premises used: Set.Nonempty.image, Iff.mp, Set.nonempty_of_mem, IsClosed.notMem_iff_infDist_pos