awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
R : Type u_2
inst : Semiring R
inst_1 : Module R ℝ
inst_2 : ContinuousConstSMul R ℝ
inst_3 : ContinuousConstSMul R ℂ
r : R
c : ComplexMeasure α
i : Set α
h : MeasurableSet i
⊢ (↑(mapRange (r • c) Complex.reLm.toAddMonoidHom Complex.continuous_re,
              mapRange (r • c) Complex.imLm.toAddMonoidHom Complex.continuous_im).2 :
        Set α → ℝ)
      i =
    (↑(r • mapRange c Complex.reLm.toAddMonoidHom Complex.continuous_re,
              r • mapRange c Complex.imLm.toAddMonoidHom Complex.continuous_im).2 :
        Set α → ℝ)
      i

Tactic:
simp [Complex.smul_im]

Premises used: Complex.smul_im
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
mp :
  c ≪ᵥ μ →
    AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
      AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
mpr :
  AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
      AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ →
    c ≪ᵥ μ
⊢ c ≪ᵥ μ ↔
    AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
      AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
mp : AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ
mp₁ : AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
⊢ AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
    AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
i : Set α
hi : (↑μ : Set α → ℝ≥0∞) i = 0
⊢ Eq (α := ℝ) ((↑((re : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i) 0

Tactic:
simp [h hi]
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
i : Set α
hi : (↑μ : Set α → ℝ≥0∞) i = 0
⊢ Eq (α := ℝ) ((↑((im : (a : ComplexMeasure α) → SignedMeasure α) c) : Set α → ℝ) i) 0

Tactic:
simp [h hi]
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h :
  AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
    AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
i : Set α
hi : (↑μ : Set α → ℝ≥0∞) i = 0
mpr : (↑0 : ℂ) + (↑0 : ℂ) * Complex.I = 0
rw : ((↑c : Set α → ℂ) i).im = 0
rw₁ : ((↑c : Set α → ℂ) i).re = 0
⊢ (↑c : Set α → ℂ) i = 0

Tactic:
rw [← Complex.re_add_im (c i), (_ : (c i).re = 0), (_ : (c i).im = 0)]

Premises used: MeasureTheory.VectorMeasure.measureOf', Complex.re_add_im
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h :
  AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
    AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
i : Set α
hi : (↑μ : Set α → ℝ≥0∞) i = 0
⊢ (↑0 : ℂ) + (↑0 : ℂ) * Complex.I = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h :
  AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
    AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
i : Set α
hi : (↑μ : Set α → ℝ≥0∞) i = 0
⊢ ((↑c : Set α → ℂ) i).im = 0

Tactic:
h.2 hi

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.Complex
Goal:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h :
  AbsolutelyContinuous (M := ℝ) ((re : (a : ComplexMeasure α) → SignedMeasure α) c) μ ∧
    AbsolutelyContinuous (M := ℝ) ((im : (a : ComplexMeasure α) → SignedMeasure α) c) μ
i : Set α
hi : (↑μ : Set α → ℝ≥0∞) i = 0
⊢ ((↑c : Set α → ℂ) i).re = 0

Tactic:
h.1 hi

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
⊢ ∀ (K₁ K₂ : Compacts G), (↑K₁ : Set G) ⊆ (↑K₂ : Set G) → LE.le (α := ℝ≥0) 0 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
⊢ ∀ (K₁ K₂ : Compacts G),
    Disjoint (↑K₁ : Set G) (↑K₂ : Set G) →
      IsClosed (↑K₁ : Set G) → IsClosed (↑K₂ : Set G) → 0 = HAdd.hAdd (α := ℝ≥0) 0 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
⊢ ∀ (K₁ K₂ : Compacts G), 0 ≤ HAdd.hAdd (α := ℝ≥0) 0 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Compacts G → ℝ≥0
mono' : ∀ (K₁ K₂ : Compacts G), (↑K₁ : Set G) ⊆ (↑K₂ : Set G) → μ K₁ ≤ μ K₂
sup_disjoint' :
  ∀ (K₁ K₂ : Compacts G),
    Disjoint (↑K₁ : Set G) (↑K₂ : Set G) → IsClosed (↑K₁ : Set G) → IsClosed (↑K₂ : Set G) → μ (K₁ ⊔ K₂) = μ K₁ + μ K₂
sup_le' : ∀ (K₁ K₂ : Compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂
v : Compacts G → ℝ≥0
mono'_1 : ∀ (K₁ K₂ : Compacts G), (↑K₁ : Set G) ⊆ (↑K₂ : Set G) → v K₁ ≤ v K₂
sup_disjoint'_1 :
  ∀ (K₁ K₂ : Compacts G),
    Disjoint (↑K₁ : Set G) (↑K₂ : Set G) → IsClosed (↑K₁ : Set G) → IsClosed (↑K₂ : Set G) → v (K₁ ⊔ K₂) = v K₁ + v K₂
sup_le'_1 : ∀ (K₁ K₂ : Compacts G), v (K₁ ⊔ K₂) ≤ v K₁ + v K₂
h :
  Eq.{max (w + 1) 1} (α := (a : Compacts G) → ℝ≥0∞)
    ((fun (μ : Content G) (s : Compacts G) ↦ (↑(μ.toFun s) : ℝ≥0∞))
      { toFun := μ, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' })
    ((fun (μ : Content G) (s : Compacts G) ↦ (↑(μ.toFun s) : ℝ≥0∞))
      { toFun := v, mono' := mono'_1, sup_disjoint' := sup_disjoint'_1, sup_le' := sup_le'_1 })
h₁ : μ = v
⊢ { toFun := μ, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' : Content G } =
    { toFun := v, mono' := mono'_1, sup_disjoint' := sup_disjoint'_1, sup_le' := sup_le'_1 }

Tactic:
congr!
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Compacts G → ℝ≥0
mono' : ∀ (K₁ K₂ : Compacts G), (↑K₁ : Set G) ⊆ (↑K₂ : Set G) → μ K₁ ≤ μ K₂
sup_disjoint' :
  ∀ (K₁ K₂ : Compacts G),
    Disjoint (↑K₁ : Set G) (↑K₂ : Set G) → IsClosed (↑K₁ : Set G) → IsClosed (↑K₂ : Set G) → μ (K₁ ⊔ K₂) = μ K₁ + μ K₂
sup_le' : ∀ (K₁ K₂ : Compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂
v : Compacts G → ℝ≥0
mono'_1 : ∀ (K₁ K₂ : Compacts G), (↑K₁ : Set G) ⊆ (↑K₂ : Set G) → v K₁ ≤ v K₂
sup_disjoint'_1 :
  ∀ (K₁ K₂ : Compacts G),
    Disjoint (↑K₁ : Set G) (↑K₂ : Set G) → IsClosed (↑K₁ : Set G) → IsClosed (↑K₂ : Set G) → v (K₁ ⊔ K₂) = v K₁ + v K₂
sup_le'_1 : ∀ (K₁ K₂ : Compacts G), v (K₁ ⊔ K₂) ≤ v K₁ + v K₂
h :
  Eq.{max (w + 1) 1} (α := (a : Compacts G) → ℝ≥0∞)
    ((fun (μ : Content G) (s : Compacts G) ↦ (↑(μ.toFun s) : ℝ≥0∞))
      { toFun := μ, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' })
    ((fun (μ : Content G) (s : Compacts G) ↦ (↑(μ.toFun s) : ℝ≥0∞))
      { toFun := v, mono' := mono'_1, sup_disjoint' := sup_disjoint'_1, sup_le' := sup_le'_1 })
h₁ : ∀ (s : Compacts G), μ s = v s
⊢ μ = v

Tactic:
ext s : 1
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Compacts G → ℝ≥0
mono' : ∀ (K₁ K₂ : Compacts G), (↑K₁ : Set G) ⊆ (↑K₂ : Set G) → μ K₁ ≤ μ K₂
sup_disjoint' :
  ∀ (K₁ K₂ : Compacts G),
    Disjoint (↑K₁ : Set G) (↑K₂ : Set G) → IsClosed (↑K₁ : Set G) → IsClosed (↑K₂ : Set G) → μ (K₁ ⊔ K₂) = μ K₁ + μ K₂
sup_le' : ∀ (K₁ K₂ : Compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂
v : Compacts G → ℝ≥0
mono'_1 : ∀ (K₁ K₂ : Compacts G), (↑K₁ : Set G) ⊆ (↑K₂ : Set G) → v K₁ ≤ v K₂
sup_disjoint'_1 :
  ∀ (K₁ K₂ : Compacts G),
    Disjoint (↑K₁ : Set G) (↑K₂ : Set G) → IsClosed (↑K₁ : Set G) → IsClosed (↑K₂ : Set G) → v (K₁ ⊔ K₂) = v K₁ + v K₂
sup_le'_1 : ∀ (K₁ K₂ : Compacts G), v (K₁ ⊔ K₂) ≤ v K₁ + v K₂
h :
  Eq.{max (w + 1) 1} (α := (a : Compacts G) → ℝ≥0∞)
    ((fun (μ : Content G) (s : Compacts G) ↦ (↑(μ.toFun s) : ℝ≥0∞))
      { toFun := μ, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' })
    ((fun (μ : Content G) (s : Compacts G) ↦ (↑(μ.toFun s) : ℝ≥0∞))
      { toFun := v, mono' := mono'_1, sup_disjoint' := sup_disjoint'_1, sup_le' := sup_le'_1 })
s : Compacts G
⊢ μ s = v s

Tactic:
ENNReal.coe_injective <| congr_fun h s

Premises used: congr_fun, ENNReal.coe_injective
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Compacts G → ℝ≥0
mono' : ∀ (K₁ K₂ : Compacts G), (↑K₁ : Set G) ⊆ (↑K₂ : Set G) → μ K₁ ≤ μ K₂
sup_disjoint' :
  ∀ (K₁ K₂ : Compacts G),
    Disjoint (↑K₁ : Set G) (↑K₂ : Set G) → IsClosed (↑K₁ : Set G) → IsClosed (↑K₂ : Set G) → μ (K₁ ⊔ K₂) = μ K₁ + μ K₂
sup_le' : ∀ (K₁ K₂ : Compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂
v : Compacts G → ℝ≥0
mono'_1 : ∀ (K₁ K₂ : Compacts G), (↑K₁ : Set G) ⊆ (↑K₂ : Set G) → v K₁ ≤ v K₂
sup_disjoint'_1 :
  ∀ (K₁ K₂ : Compacts G),
    Disjoint (↑K₁ : Set G) (↑K₂ : Set G) → IsClosed (↑K₁ : Set G) → IsClosed (↑K₂ : Set G) → v (K₁ ⊔ K₂) = v K₁ + v K₂
sup_le'_1 : ∀ (K₁ K₂ : Compacts G), v (K₁ ⊔ K₂) ≤ v K₁ + v K₂
h :
  Eq.{max (w + 1) 1} (α := (a : Compacts G) → ℝ≥0∞)
    ((fun (μ : Content G) (s : Compacts G) ↦ (↑(μ.toFun s) : ℝ≥0∞))
      { toFun := μ, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' })
    ((fun (μ : Content G) (s : Compacts G) ↦ (↑(μ.toFun s) : ℝ≥0∞))
      { toFun := v, mono' := mono'_1, sup_disjoint' := sup_disjoint'_1, sup_le' := sup_le'_1 })
s : Compacts G
⊢ μ s = v s

Tactic:
exact ENNReal.coe_injective <| congr_fun h s

Premises used: congr_fun, ENNReal.coe_injective
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K : Compacts G
⊢ μ.toFun K = ENNReal.toNNReal ((μ : (a : Compacts G) → ℝ≥0∞) K)

Tactic:
rfl

Premises used: ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
toFun : Compacts G → ℝ≥0
mono' : ∀ (K₁ K₂ : Compacts G), (↑K₁ : Set G) ⊆ (↑K₂ : Set G) → toFun K₁ ≤ toFun K₂
sup_disjoint' :
  ∀ (K₁ K₂ : Compacts G),
    Disjoint (↑K₁ : Set G) (↑K₂ : Set G) →
      IsClosed (↑K₁ : Set G) → IsClosed (↑K₂ : Set G) → toFun (K₁ ⊔ K₂) = toFun K₁ + toFun K₂
sup_le' : ∀ (K₁ K₂ : Compacts G), toFun (K₁ ⊔ K₂) ≤ toFun K₁ + toFun K₂
K : Compacts G
⊢ ({ toFun := toFun, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' : Content G } :
        (a : Compacts G) → ℝ≥0∞)
      K =
    (↑(toFun K) : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K : Compacts G
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
coe_ne_top

Premises used: ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
h : (↑K₁ : Set G) ⊆ (↑K₂ : Set G)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K₁ : ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K₂ : ℝ≥0∞)

Tactic:
simpa using μ.mono' _ _ h

Premises used: MeasureTheory.Content.mono'
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
h : Disjoint (↑K₁ : Set G) (↑K₂ : Set G)
h₁ : IsClosed (↑K₁ : Set G)
h₂ : IsClosed (↑K₂ : Set G)
⊢ (μ : (a : Compacts G) → ℝ≥0∞) (K₁ ⊔ K₂) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K₁ : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K₂ : ℝ≥0∞)

Tactic:
simpa [toNNReal_eq_toNNReal_iff, ← toNNReal_add] using μ.sup_disjoint' _ _ h h₁ h₂

Premises used: ENNReal.toNNReal_eq_toNNReal_iff, ENNReal.toNNReal_add, MeasureTheory.Content.sup_disjoint'
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
⊢ (μ : (a : Compacts G) → ℝ≥0∞) (K₁ ⊔ K₂) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K₁ : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K₂ : ℝ≥0∞)

Tactic:
simpa [← toNNReal_add] using μ.sup_le' _ _

Premises used: ENNReal.toNNReal_add, MeasureTheory.Content.sup_le'
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K : Compacts G
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ENNReal.coe_lt_top

Premises used: ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) ⊥ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa [toNNReal_eq_zero_iff] using μ.sup_disjoint' ⊥ ⊥

Premises used: ENNReal.toNNReal_eq_zero_iff, MeasureTheory.Content.sup_disjoint', Bot.bot
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K : Compacts G
U : Opens G
h2 : (↑K : Set G) ⊆ (↑U : Set G)
⊢ (μ : (a : Compacts G) → ℝ≥0∞) K ≤ μ.innerContent U

Tactic:
le_iSup_of_le K <| le_iSup (fun _ ↦ (μ.toFun K : ℝ≥0∞)) h2

Premises used: ENNReal.ofNNReal, le_iSup, le_iSup_of_le, MeasureTheory.Content.toFun, MeasureTheory.Content.innerContent
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U : Opens G
K : Compacts G
h2 : (↑U : Set G) ⊆ (↑K : Set G)
⊢ μ.innerContent U ≤ (μ : (a : Compacts G) → ℝ≥0∞) K

Tactic:
iSup₂_le fun _ hK' => μ.mono _ _ (Subset.trans hK' h2)

Premises used: iSup₂_le, Set.Subset.trans, MeasureTheory.Content.mono, MeasureTheory.Content.innerContent
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K : Set G
h1K : IsCompact K
h2K : IsOpen K
⊢ μ.innerContent { carrier := K, is_open' := h2K : Opens G } =
    (μ : (a : Compacts G) → ℝ≥0∞) { carrier := K, isCompact' := h1K }

Tactic:
le_antisymm (iSup₂_le fun _ hK' => μ.mono _ ⟨K, h1K⟩ hK') (μ.le_innerContent _ _ Subset.rfl)

Premises used: iSup₂_le, MeasureTheory.Content.le_innerContent, MeasureTheory.Content.mono, TopologicalSpace.Compacts.mk, le_antisymm, Set.Subset.rfl
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
rw : μ.innerContent ⊥ ≤ (μ : (a : Compacts G) → ℝ≥0∞) ⊥
⊢ μ.innerContent ⊥ = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← μ.empty]

Premises used: MeasureTheory.Content.empty, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
⊢ μ.innerContent ⊥ ≤ (μ : (a : Compacts G) → ℝ≥0∞) ⊥

Tactic:
iSup₂_le fun K hK => ?_

Premises used: iSup₂_le, MeasureTheory.Content.innerContent
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
refine :
  ∀ (K : Compacts G) (hK : (↑K : Set G) ⊆ (↑⊥ : Set G)),
    LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) ⊥ : ℝ≥0∞)
⊢ μ.innerContent ⊥ ≤ (μ : (a : Compacts G) → ℝ≥0∞) ⊥

Tactic:
refine iSup₂_le fun K hK => ?_

Premises used: iSup₂_le
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K : Compacts G
hK : (↑K : Set G) ⊆ (↑⊥ : Set G)
h : (↑K : Set G) = (↑⊥ : Set G)
⊢ K = ⊥

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K : Compacts G
hK : (↑K : Set G) ⊆ (↑⊥ : Set G)
h : ∅ = (↑⊥ : Set G)
h₁ h₂ : Eq.{w + 1} (α := Set G) ∅ ∅
⊢ (↑K : Set G) = (↑⊥ : Set G)

Tactic:
rw [subset_empty_iff.mp hK, Compacts.coe_bot]

Premises used: TopologicalSpace.Compacts.coe_bot, Iff.mp, Set.subset_empty_iff
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K : Compacts G
hK : (↑K : Set G) ⊆ (↑⊥ : Set G)
⊢ K = ⊥

Tactic:
have : K = ⊥ := by
    ext1
    rw [subset_empty_iff.mp hK, Compacts.coe_bot]
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
K : Compacts G
hK : (↑K : Set G) ⊆ (↑⊥ : Set G)
this : K = ⊥
rw rw₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) ⊥ : ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) ⊥ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) ⊥ : ℝ≥0∞)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U V : Set G
hU : IsOpen U
hV : IsOpen V
h2 : U ⊆ V
⊢ μ.innerContent { carrier := U, is_open' := hU : Opens G } ≤ μ.innerContent { carrier := V, is_open' := hV }

Tactic:
biSup_mono fun _ hK => hK.trans h2

Premises used: biSup_mono, HasSubset.Subset.trans, MeasureTheory.Content.innerContent
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ (↑ε : ℝ≥0∞) ≠ 0

Tactic:
have h'ε := ENNReal.coe_ne_zero.2 hε
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : (↑ε : ℝ≥0∞) ≠ 0
inl :
  ∀ (h : μ.innerContent U ≤ (↑ε : ℝ≥0∞)),
    ∃ (K : Compacts G),
      (↑K : Set G) ⊆ (↑U : Set G) ∧
        μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
inr :
  ∀ (h : (↑ε : ℝ≥0∞) < μ.innerContent U),
    ∃ (K : Compacts G),
      (↑K : Set G) ⊆ (↑U : Set G) ∧
        μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ ∃ (K : Compacts G),
    (↑K : Set G) ⊆ (↑U : Set G) ∧
      μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
rcases le_or_gt (μ.innerContent U) ε with h | h

Premises used: ENNReal.ofNNReal, le_or_gt, MeasureTheory.Content.innerContent
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : (↑ε : ℝ≥0∞) ≠ 0
h : μ.innerContent U ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (K : Compacts G),
    (↑K : Set G) ⊆ (↑U : Set G) ∧
      μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
⟨⊥, empty_subset _, le_add_left h⟩

Premises used: Bot.bot, And.intro, Set.empty_subset, Exists.intro, le_add_left
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : (↑ε : ℝ≥0∞) ≠ 0
h : μ.innerContent U ≤ (↑ε : ℝ≥0∞)
⊢ ∃ (K : Compacts G),
    (↑K : Set G) ⊆ (↑U : Set G) ∧
      μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
exact ⟨⊥, empty_subset _, le_add_left h⟩
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : (↑ε : ℝ≥0∞) ≠ 0
h : (↑ε : ℝ≥0∞) < μ.innerContent U
⊢ μ.innerContent U - (↑ε : ℝ≥0∞) < μ.innerContent U

Tactic:
have h₂ := ENNReal.sub_lt_self hU h.ne_bot h'ε
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : (↑ε : ℝ≥0∞) ≠ 0
h : (↑ε : ℝ≥0∞) < μ.innerContent U
h₂ : μ.innerContent U - (↑ε : ℝ≥0∞) < μ.innerContent U
rhs : μ.innerContent U
| μ.innerContent U - (↑ε : ℝ≥0∞) < μ.innerContent U

Tactic:
rhs
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : (↑ε : ℝ≥0∞) ≠ 0
h : (↑ε : ℝ≥0∞) < μ.innerContent U
h₂ : μ.innerContent U - (↑ε : ℝ≥0∞) < μ.innerContent U
rw : ⨆ (K : Compacts G), ⨆ (_ : (↑K : Set G) ⊆ (↑U : Set G)), (μ : (a : Compacts G) → ℝ≥0∞) K
| μ.innerContent U - (↑ε : ℝ≥0∞) < μ.innerContent U

Tactic:
rhs; rw [innerContent]

Premises used: MeasureTheory.Content.innerContent
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : (↑ε : ℝ≥0∞) ≠ 0
h : (↑ε : ℝ≥0∞) < μ.innerContent U
h₂ : μ.innerContent U - (↑ε : ℝ≥0∞) < μ.innerContent U
⊢ μ.innerContent U - (↑ε : ℝ≥0∞) <
    ⨆ (K : Compacts G), ⨆ (_ : (↑K : Set G) ⊆ (↑U : Set G)), (μ : (a : Compacts G) → ℝ≥0∞) K

Tactic:
conv at h₂ => rhs; rw [innerContent]

Premises used: MeasureTheory.Content.innerContent
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : (↑ε : ℝ≥0∞) ≠ 0
h : (↑ε : ℝ≥0∞) < μ.innerContent U
h₂ :
  μ.innerContent U - (↑ε : ℝ≥0∞) <
    ⨆ (K : Compacts G), ⨆ (_ : (↑K : Set G) ⊆ (↑U : Set G)), (μ : (a : Compacts G) → ℝ≥0∞) K
⊢ ∃ (i : Compacts G) (_ : (↑i : Set G) ⊆ (↑U : Set G)), μ.innerContent U - (↑ε : ℝ≥0∞) < (μ : (a : Compacts G) → ℝ≥0∞) i

Tactic:
simp only [lt_iSup_iff] at h₂

Premises used: lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : (↑ε : ℝ≥0∞) ≠ 0
h : (↑ε : ℝ≥0∞) < μ.innerContent U
h₂ :
  ∃ (i : Compacts G) (_ : (↑i : Set G) ⊆ (↑U : Set G)), μ.innerContent U - (↑ε : ℝ≥0∞) < (μ : (a : Compacts G) → ℝ≥0∞) i
inr :
  ∀ (U_1 : Compacts G) (h1U : (↑U_1 : Set G) ⊆ (↑U : Set G))
    (h2U : μ.innerContent U - (↑ε : ℝ≥0∞) < (μ : (a : Compacts G) → ℝ≥0∞) U_1),
    ∃ (K : Compacts G),
      (↑K : Set G) ⊆ (↑U : Set G) ∧
        μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ ∃ (K : Compacts G),
    (↑K : Set G) ⊆ (↑U : Set G) ∧
      μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
rcases h₂ with ⟨U, h1U, h2U⟩
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U_1 : Opens G
hU : μ.innerContent U_1 ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : (↑ε : ℝ≥0∞) ≠ 0
h : (↑ε : ℝ≥0∞) < μ.innerContent U_1
U : Compacts G
h1U : (↑U : Set G) ⊆ (↑U_1 : Set G)
h2U : μ.innerContent U_1 - (↑ε : ℝ≥0∞) < (μ : (a : Compacts G) → ℝ≥0∞) U
⊢ ∃ (K : Compacts G),
    (↑K : Set G) ⊆ (↑U_1 : Set G) ∧
      μ.innerContent U_1 ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
⟨U, h1U, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U_1 : Opens G
hU : μ.innerContent U_1 ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : (↑ε : ℝ≥0∞) ≠ 0
h : (↑ε : ℝ≥0∞) < μ.innerContent U_1
U : Compacts G
h1U : (↑U : Set G) ⊆ (↑U_1 : Set G)
h2U : μ.innerContent U_1 - (↑ε : ℝ≥0∞) < (μ : (a : Compacts G) → ℝ≥0∞) U
inr : μ.innerContent U_1 ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) U : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ ∃ (K : Compacts G),
    (↑K : Set G) ⊆ (↑U_1 : Set G) ∧
      μ.innerContent U_1 ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
refine ⟨U, h1U, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
U_1 : Opens G
hU : μ.innerContent U_1 ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : (↑ε : ℝ≥0∞) ≠ 0
h : (↑ε : ℝ≥0∞) < μ.innerContent U_1
U : Compacts G
h1U : (↑U : Set G) ⊆ (↑U_1 : Set G)
h2U : μ.innerContent U_1 - (↑ε : ℝ≥0∞) < (μ : (a : Compacts G) → ℝ≥0∞) U
inr : μ.innerContent U_1 - (↑ε : ℝ≥0∞) ≤ (μ : (a : Compacts G) → ℝ≥0∞) U
⊢ μ.innerContent U_1 ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) U : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
rw [← tsub_le_iff_right]

Premises used: tsub_le_iff_right