awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs :
  Subset.{u_4} (α := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
apply :
  Set.Countable.{u_4} (α := ι)
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
⊢ Set.Countable.{u_4} (α := ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}

Tactic:
apply Countable.mono obs

Premises used: Set.Countable.mono
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs :
  Subset.{u_4} (α := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
⊢ Set.Countable.{u_4} (α := ι)
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})

Tactic:
countable_iUnion fun n ↦ ?_

Premises used: Set.countable_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs :
  Subset.{u_4} (α := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
refine :
  ∀ (n : ℕ),
    Set.Countable.{u_4} (α := ι)
      {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
⊢ Set.Countable.{u_4} (α := ι)
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})

Tactic:
refine countable_iUnion fun n ↦ ?_

Premises used: Set.countable_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs :
  Subset.{u_4} (α := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
n : ℕ
As_mble₁ : ∀ (i : ι), NullMeasurableSet (As i) (sfiniteSeq μ n)
As_disj₁ : Pairwise (AEDisjoint (sfiniteSeq μ n) on As)
Union_As_finite : Ne (α := ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Set.Countable.{u_4} (α := ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}

Tactic:
apply countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀

Premises used: MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs :
  Subset.{u_4} (α := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
n : ℕ
⊢ ∀ (i : ι), NullMeasurableSet (As i) (sfiniteSeq μ n)

Tactic:
fun i ↦ (As_mble i).mono (le_sum _ _)

Premises used: MeasureTheory.Measure.le_sum, MeasureTheory.NullMeasurableSet.mono, MeasureTheory.sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs :
  Subset.{u_4} (α := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
n : ℕ
⊢ ∀ (i : ι), NullMeasurableSet (As i) (sfiniteSeq μ n)

Tactic:
exact fun i ↦ (As_mble i).mono (le_sum _ _)

Premises used: MeasureTheory.Measure.le_sum, MeasureTheory.NullMeasurableSet.mono, MeasureTheory.sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs :
  Subset.{u_4} (α := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
n : ℕ
⊢ Pairwise (AEDisjoint (sfiniteSeq μ n) on As)

Tactic:
fun i j hij ↦ AEDisjoint.of_le (As_disj hij) (le_sum _ _)

Premises used: MeasureTheory.AEDisjoint.of_le, MeasureTheory.Measure.le_sum, Pairwise, MeasureTheory.sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs :
  Subset.{u_4} (α := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
n : ℕ
⊢ Pairwise (AEDisjoint (sfiniteSeq μ n) on As)

Tactic:
exact fun i j hij ↦ AEDisjoint.of_le (As_disj hij) (le_sum _ _)

Premises used: MeasureTheory.AEDisjoint.of_le, MeasureTheory.Measure.le_sum, MeasureTheory.sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs :
  Subset.{u_4} (α := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
n : ℕ
⊢ Ne (α := ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_ne_top _ (⋃ i, As i)

Premises used: MeasureTheory.measure_ne_top, Set.iUnion
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs :
  Subset.{u_4} (α := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
n : ℕ
⊢ Ne (α := ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact measure_ne_top _ (⋃ i, As i)

Premises used: MeasureTheory.measure_ne_top, Set.iUnion
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
⊢ Set.Countable.{u_4} (α := ι) {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}

Tactic:
countable_meas_pos_of_disjoint_iUnion₀ (fun i ↦ (As_mble i).nullMeasurableSet)
    ((fun _ _ h ↦ Disjoint.aedisjoint (As_disj h)))

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion₀, Disjoint.aedisjoint
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_4
β : Type u_5
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass β
g : α → β
g_mble : NullMeasurable g μ
⊢ Pairwise.{u_5} (α := β) (onFun.{u_5 + 1, u_4 + 1, 1} (β := Set α) Disjoint fun (t : β) ↦ {a : α | g a = t})

Tactic:
have level_sets_disjoint : Pairwise (Disjoint on fun t : β => { a : α | g a = t }) :=
    fun s t hst => Disjoint.preimage g (disjoint_singleton.mpr hst)
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_4
β : Type u_5
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass β
g : α → β
g_mble : NullMeasurable g μ
level_sets_disjoint :
  Pairwise.{u_5} (α := β) (onFun.{u_5 + 1, u_4 + 1, 1} (β := Set α) Disjoint fun (t : β) ↦ {a : α | g a = t})
⊢ Set.Countable.{u_5} (α := β)
    {t : β | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | g a = t} : ℝ≥0∞)}

Tactic:
Measure.countable_meas_pos_of_disjoint_iUnion₀
    (fun b => g_mble (‹MeasurableSingletonClass β›.measurableSet_singleton b))
    ((fun _ _ h ↦ Disjoint.aedisjoint (level_sets_disjoint h)))

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion₀, Disjoint.aedisjoint
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_4
β : Type u_5
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass β
g : α → β
g_mble : NullMeasurable g μ
level_sets_disjoint :
  Pairwise.{u_5} (α := β) (onFun.{u_5 + 1, u_4 + 1, 1} (β := Set α) Disjoint fun (t : β) ↦ {a : α | g a = t})
⊢ Set.Countable.{u_5} (α := β)
    {t : β | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | g a = t} : ℝ≥0∞)}

Tactic:
exact Measure.countable_meas_pos_of_disjoint_iUnion₀
    (fun b => g_mble (‹MeasurableSingletonClass β›.measurableSet_singleton b))
    ((fun _ _ h ↦ Disjoint.aedisjoint (level_sets_disjoint h)))

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion₀, Disjoint.aedisjoint
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_4
β : Type u_5
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass β
g : α → β
g_mble : Measurable g
⊢ Set.Countable.{u_5} (α := β)
    {t : β | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | g a = t} : ℝ≥0∞)}

Tactic:
countable_meas_level_set_pos₀ g_mble.nullMeasurable

Premises used: Measurable.nullMeasurable, MeasureTheory.Measure.countable_meas_level_set_pos₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
inl :
  ∀ (hm : m = ⊥),
    ∃ (D : Set (Set α)),
      Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
        (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
inr :
  ∀ (hm : ⊥ < m),
    ∃ (D : Set (Set α)),
      Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
        (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
⊢ ∃ (D : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m

Tactic:
rcases eq_bot_or_bot_lt m with hm | hm

Premises used: eq_bot_or_bot_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : m = ⊥
⊢ Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} ∅

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : m = ⊥
⊢ (μ : (a : Set α) → ℝ≥0∞) (⋃₀ ∅) = m

Tactic:
simp [hm]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : m = ⊥
⊢ ∃ (D : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m

Tactic:
exact ⟨∅, by simp, by simp [hm]⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
⊢ ∃ (u : ℕ → ℝ≥0∞), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo 0 m) ∧ Tendsto u atTop (𝓝 m)

Tactic:
exists_seq_strictMono_tendsto' hm

Premises used: Set.Mem, exists_seq_strictMono_tendsto'
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
inr :
  ∀ (u : ℕ → ℝ≥0∞) (u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m) (u_lim : Tendsto u atTop (𝓝 m)),
    ∃ (D : Set (Set α)),
      Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
        (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
⊢ ∃ (D : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m

Tactic:
obtain ⟨u, -, u_mem, u_lim⟩ :
        ∃ u : ℕ → ℝ≥0∞, StrictMono u ∧ (∀ n, u n ∈ Ioo 0 m) ∧ Tendsto u atTop (𝓝 m) :=
      exists_seq_strictMono_tendsto' hm

Premises used: exists_seq_strictMono_tendsto'
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
⊢ ∀ (n : ℕ),
    ∃ (D : Set (Set α)),
      Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
        u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)

Tactic:
have A n : ∃ D ∈ {D : Set (Set α) | D ⊆ C ∧ D.Countable}, u n < μ (⋃₀ D) :=
      lt_biSup_iff.1 (u_mem n).2
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
A :
  ∀ (n : ℕ),
    ∃ (D : Set (Set α)),
      Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
        u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
inr :
  ∀ (D : (n : ℕ) → Set (Set α))
    (D_mem : ∀ (n : ℕ), Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D n))
    (huD : ∀ (n : ℕ), u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n)),
    ∃ (D : Set (Set α)),
      Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
        (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
⊢ ∃ (D : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m

Tactic:
choose! D D_mem huD using A
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : (n : ℕ) → Set (Set α)
D_mem : ∀ (n : ℕ), Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D n)
huD : ∀ (n : ℕ), u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n)
simp : (∀ (i : ℕ), D i ⊆ C) ∧ ∀ (i : ℕ), (D i).Countable
⊢ Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (⋃ (n : ℕ), D n)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : (n : ℕ) → Set (Set α)
D_mem : ∀ (n : ℕ), Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D n)
huD : ∀ (n : ℕ), u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n)
⊢ (∀ (i : ℕ), D i ⊆ C) ∧ ∀ (i : ℕ), (D i).Countable

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : (n : ℕ) → Set (Set α)
D_mem : ∀ (n : ℕ), Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D n)
huD : ∀ (n : ℕ), u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n)
⊢ Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (⋃ (n : ℕ), D n)

Tactic:
have hD : ⋃ n, D n ∈ {D | D ⊆ C ∧ D.Countable} := by simp; grind
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : (n : ℕ) → Set (Set α)
D_mem : ∀ (n : ℕ), Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D n)
huD : ∀ (n : ℕ), u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n)
hD : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (⋃ (n : ℕ), D n)
⊢ ∃ (D : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m

Tactic:
⟨⋃ n, D n, hD, ?_⟩

Premises used: And.intro, Exists.intro, Set.iUnion
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : (n : ℕ) → Set (Set α)
D_mem : ∀ (n : ℕ), Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D n)
huD : ∀ (n : ℕ), u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n)
hD : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (⋃ (n : ℕ), D n)
inr : (μ : (a : Set α) → ℝ≥0∞) (⋃₀ ⋃ (n : ℕ), D n) = m
⊢ ∃ (D : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m

Tactic:
refine ⟨⋃ n, D n, hD, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : (n : ℕ) → Set (Set α)
D_mem : ∀ (n : ℕ), Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D n)
huD : ∀ (n : ℕ), u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n)
hD : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (⋃ (n : ℕ), D n)
inr :
  LE.le (α := ℝ≥0∞)
    (⨆ (i : Set (Set α)),
      ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} i),
        (fun (D : Set (Set α)) ↦ ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)) i)
    ((fun (D : Set (Set α)) ↦ ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)) (⋃ (n : ℕ), D n))
⊢ (μ : (a : Set α) → ℝ≥0∞) (⋃₀ ⋃ (n : ℕ), D n) = m

Tactic:
apply le_antisymm (le_biSup (f := fun D ↦ μ (⋃₀ D)) hD)

Premises used: Set.sUnion, le_antisymm, le_biSup, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : (n : ℕ) → Set (Set α)
D_mem : ∀ (n : ℕ), Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D n)
huD : ∀ (n : ℕ), u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n)
hD : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (⋃ (n : ℕ), D n)
apply :
  ∀ (n : ℕ),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n) : ℝ≥0∞)
      ((fun (D : Set (Set α)) ↦ ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)) (⋃ (n : ℕ), D n) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (i : Set (Set α)),
      ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} i),
        (fun (D : Set (Set α)) ↦ ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)) i)
    ((fun (D : Set (Set α)) ↦ ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)) (⋃ (n : ℕ), D n))

Tactic:
apply le_of_tendsto' u_lim (fun n ↦ (huD n).le.trans ?_)

Premises used: LT.lt.le, LE.le.trans, le_of_tendsto'