awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsFiniteMeasureOnCompacts μ
K : Set α
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
IsFiniteMeasureOnCompacts.lt_top_of_isCompact hK

Premises used: MeasureTheory.IsFiniteMeasureOnCompacts.lt_top_of_isCompact
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsFiniteMeasureOnCompacts μ
K : Set α
hK : IsCompact K
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
hK.measure_lt_top.ne

Premises used: IsCompact.measure_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
μ : Measure α
inst_2 : IsFiniteMeasureOnCompacts μ
s : Set α
hs : Bornology.IsBounded s
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
calc
    μ s ≤ μ (closure s) := measure_mono subset_closure
    _ < ∞ := (Metric.isCompact_of_isClosed_isBounded isClosed_closure hs.closure).measure_lt_top

Premises used: Trans.trans, subset_closure, Metric.isCompact_of_isClosed_isBounded, IsCompact.measure_lt_top, MeasureTheory.measure_mono, isClosed_closure, Bornology.IsBounded.closure
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
μ : Measure α
inst_2 : IsFiniteMeasureOnCompacts μ
x : α
r : ℝ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
Metric.isBounded_closedBall.measure_lt_top

Premises used: Metric.isBounded_closedBall, Bornology.IsBounded.measure_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
μ : Measure α
inst_2 : IsFiniteMeasureOnCompacts μ
x : α
r : ℝ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Metric.ball x r) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
Metric.isBounded_ball.measure_lt_top.ne

Premises used: Metric.isBounded_ball, Bornology.IsBounded.measure_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
μ : Measure α
inst_2 : IsFiniteMeasureOnCompacts μ
x : α
r : ℝ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Metric.ball x r) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsFiniteMeasureOnCompacts μ
c : ℝ≥0∞
hc : c ≠ ∞
⊢ IsFiniteMeasureOnCompacts (c • μ)

Tactic:
⟨fun _K hK => ENNReal.mul_lt_top hc.lt_top hK.measure_lt_top⟩

Premises used: MeasureTheory.IsFiniteMeasureOnCompacts.mk, ENNReal.mul_lt_top, Ne.lt_top, IsCompact.measure_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s t : Set α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsFiniteMeasureOnCompacts μ
c : ℝ≥0
⊢ IsFiniteMeasureOnCompacts (c • μ)

Tactic:
IsFiniteMeasureOnCompacts.smul μ coe_ne_top

Premises used: MeasureTheory.IsFiniteMeasureOnCompacts.smul, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ_1 ν ν₁ ν₂ : Measure α
s_1 t : Set α
inst : TopologicalSpace α
μ : Measure α
inst_1 : IsFiniteMeasureOnCompacts μ
s : Set α
⊢ IsFiniteMeasureOnCompacts (μ.restrict s)

Tactic:
⟨fun _k hk ↦ (restrict_apply_le _ _).trans_lt hk.measure_lt_top⟩

Premises used: MeasureTheory.IsFiniteMeasureOnCompacts.mk, MeasureTheory.Measure.restrict_apply_le, IsCompact.measure_lt_top, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
μ : Measure β
inst_2 : IsFiniteMeasureOnCompacts μ
f : α → β
f_cont : Continuous[inst, inst_1] f
f_me : MeasurableEmbedding f
K : Set α
hK : IsCompact K
rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' K) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [f_me.comap_apply]

Premises used: MeasurableEmbedding.comap_apply
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
μ : Measure β
inst_2 : IsFiniteMeasureOnCompacts μ
f : α → β
f_cont : Continuous[inst, inst_1] f
f_me : MeasurableEmbedding f
K : Set α
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' K) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
IsFiniteMeasureOnCompacts.lt_top_of_isCompact (hK.image f_cont)

Premises used: MeasureTheory.IsFiniteMeasureOnCompacts.lt_top_of_isCompact, IsCompact.image
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
μ : Measure β
inst_2 : IsFiniteMeasureOnCompacts μ
f : α → β
f_cont : Continuous[inst, inst_1] f
f_me : MeasurableEmbedding f
K : Set α
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' K) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact IsFiniteMeasureOnCompacts.lt_top_of_isCompact (hK.image f_cont)

Premises used: MeasureTheory.IsFiniteMeasureOnCompacts.lt_top_of_isCompact, IsCompact.image
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : IsFiniteMeasureOnCompacts μ
⊢ IsFiniteMeasure μ

Tactic:
⟨IsFiniteMeasureOnCompacts.lt_top_of_isCompact isCompact_univ⟩

Premises used: isCompact_univ, MeasureTheory.IsFiniteMeasure.mk, MeasureTheory.IsFiniteMeasureOnCompacts.lt_top_of_isCompact
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst : TopologicalSpace α
inst_1 : WeaklyLocallyCompactSpace α
inst_2 : IsFiniteMeasureOnCompacts μ
⊢ IsLocallyFiniteMeasure μ

Tactic:
⟨fun x ↦
    let ⟨K, K_compact, K_mem⟩ := exists_compact_mem_nhds x
    ⟨K, K_mem, K_compact.measure_lt_top⟩⟩

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds, nhds, MeasureTheory.Measure.FiniteAtFilter, MeasureTheory.IsLocallyFiniteMeasure.mk, IsCompact.measure_lt_top, And.intro, Exists.intro, _private.0.MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts.match_1
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
U : ι → Set α
hU : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), U i) univ
hμ : μ ≠ 0
contrapose! : ∀ (H : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U i) : ℝ≥0∞) (0 : ℝ≥0∞)), μ = 0
⊢ ∃ (i : ι), LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U i) : ℝ≥0∞)

Tactic:
contrapose! hμ with H
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
U : ι → Set α
hU : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), U i) univ
H : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U i) : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), U i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ = 0

Tactic:
rw [← measure_univ_eq_zero, ← hU]

Premises used: MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
U : ι → Set α
hU : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), U i) univ
H : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), U i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_iUnion_null fun i => nonpos_iff_eq_zero.1 (H i)

Premises used: MeasureTheory.measure_iUnion_null, Iff.mp, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
U : ι → Set α
hU : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), U i) univ
H : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), U i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_iUnion_null fun i => nonpos_iff_eq_zero.1 (H i)

Premises used: MeasureTheory.measure_iUnion_null, Iff.mp, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
δ : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace δ
f : α → δ
x : δ
hμ : μ ≠ 0
rw : f ⁻¹' ⋃ (i : ℕ), Metric.ball x (↑i : ℝ) = univ
rw₁ : f ⁻¹' univ = univ
rw₂ rw₃ : Eq.{u_1 + 1} (α := Set α) univ univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f ⁻¹' Metric.ball x (↑i : ℝ)) univ

Tactic:
rw [← preimage_iUnion, Metric.iUnion_ball_nat, preimage_univ]

Premises used: Metric.iUnion_ball_nat, Set.preimage_univ, Set.preimage_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace α
x : α
hμ : μ ≠ 0
⊢ ∃ (n : ℕ), LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Metric.ball x (↑n : ℝ)) : ℝ≥0∞)

Tactic:
exists_pos_preimage_ball id x hμ

Premises used: MeasureTheory.exists_pos_preimage_ball, Set.Mem, setOf, id, Metric.ball, Set.preimage
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
h : ∀ (b : β), ∃ᵐ (x : α) ∂μ, f x ≠ b
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
⊢ ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
replace h : ∀ b : β, m {b}ᶜ ≠ 0 := fun b => not_eventually.mpr (h b)
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
h : ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
inhabit :
  ∀ (inhabited_h : Inhabited β),
    ∃ (a : β) (b : β),
      a ≠ b ∧
        (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
          ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
⊢ ∃ (a : β) (b : β),
    a ≠ b ∧
      (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
        ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)

Tactic:
inhabit β
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
h : ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
inhabited_h : Inhabited β
⊢ Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have : m univ ≠ 0 := ne_bot_of_le_ne_bot (h default) (measure_mono <| subset_univ _)
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
h : ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
inhabited_h : Inhabited β
this : Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
rcases :
  ∀ (b : β) (hb : ∀ t ∈ 𝓝[univ] b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)),
    ∃ (a : β) (b : β),
      a ≠ b ∧
        (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
          ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
⊢ ∃ (a : β) (b : β),
    a ≠ b ∧
      (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
        ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)

Tactic:
rcases exists_mem_forall_mem_nhdsWithin_pos_measure this with ⟨b, -, hb⟩

Premises used: MeasureTheory.exists_mem_forall_mem_nhdsWithin_pos_measure
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
h : ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
inhabited_h : Inhabited β
this : Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
b : β
hb : ∀ t ∈ 𝓝[univ] b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp only [nhdsWithin_univ] at hb

Premises used: nhdsWithin_univ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
h : ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
inhabited_h : Inhabited β
this : Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
b : β
hb : ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
rcases :
  ∀ (a : β) (hab : a ≠ b) (ha : ∀ t ∈ 𝓝[{b}ᶜ] a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)),
    ∃ (a : β) (b : β),
      a ≠ b ∧
        (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
          ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
⊢ ∃ (a : β) (b : β),
    a ≠ b ∧
      (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
        ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)

Tactic:
rcases exists_mem_forall_mem_nhdsWithin_pos_measure (h b) with ⟨a, hab : a ≠ b, ha⟩

Premises used: MeasureTheory.exists_mem_forall_mem_nhdsWithin_pos_measure
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
h : ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
inhabited_h : Inhabited β
this : Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
b : β
hb : ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
a : β
hab : a ≠ b
ha : ∀ t ∈ 𝓝[{b}ᶜ] a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∀ t ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp only [isOpen_compl_singleton.nhdsWithin_eq hab] at ha

Premises used: IsOpen.nhdsWithin_eq, isOpen_compl_singleton
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
h : ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
inhabited_h : Inhabited β
this : Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
b : β
hb : ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
a : β
hab : a ≠ b
ha : ∀ t ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∃ (a : β) (b : β),
    a ≠ b ∧
      (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
        ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)

Tactic:
⟨a, b, hab, ha, hb⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
h : ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
inhabited_h : Inhabited β
this : Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
b : β
hb : ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
a : β
hab : a ≠ b
ha : ∀ t ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∃ (a : β) (b : β),
    a ≠ b ∧
      (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
        ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)

Tactic:
exact ⟨a, b, hab, ha, hb⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
measure_univ_lt_top : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasure ν

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
measure_univ_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← h_univ]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
apply IsFiniteMeasure.measure_univ_lt_top

Premises used: MeasureTheory.IsFiniteMeasure.measure_univ_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
⊢ IsFiniteMeasure ν

Tactic:
haveI : IsFiniteMeasure ν := by
    constructor
    rw [← h_univ]
    apply IsFiniteMeasure.measure_univ_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
this : IsFiniteMeasure ν
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
this : IsFiniteMeasure ν
t : Set α
ht : t ∈ C
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
hμν t ht
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
this : IsFiniteMeasure ν
t : Set α
ht : t ∈ C
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact hμν t ht
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
this : IsFiniteMeasure ν
t : Set α
htm : MeasurableSet t
iht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
this : IsFiniteMeasure ν
t : Set α
htm : MeasurableSet t
iht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness