awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : (↑t : Type uι) → Set α
hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
U : (i : (↑t : Type uι)) → Set α
hUf : ∀ (i : (↑t : Type uι)), U i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
hU : ∀ (i : (↑t : Type uι)), MeasurableSet (U i) ∧ U i ⊆ V i
refine_1 : Membership.mem (γ := Filter α) (⨅ (i : ι), f i) (⋂ (i : (↑t : Type uι)), U i)
refine_2 : MeasurableSet.{u_1} (α := α) (⋂ (i : (↑t : Type uι)), U i)
refine_3 : Subset.{u_1} (α := Set α) (⋂ (i : (↑t : Type uι)), U i) (⋂ (i : (↑t : Type uι)), V i)
⊢ ∃ (t_1 : Set α),
    Membership.mem (γ := Filter α) (⨅ (i : ι), f i) t_1 ∧ MeasurableSet t_1 ∧ t_1 ⊆ ⋂ (i : (↑t : Type uι)), V i

Tactic:
refine ⟨⋂ i : t, U i, ?_, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : (↑t : Type uι) → Set α
hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
U : (i : (↑t : Type uι)) → Set α
hUf : ∀ (i : (↑t : Type uι)), U i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
hU : ∀ (i : (↑t : Type uι)), MeasurableSet (U i) ∧ U i ⊆ V i
refine_1 :
  ∃ (I : Set (PLift ι)),
    I.Finite ∧
      ∃ (V : (↑I : Type uι) → Set α),
        (∀ (i : (↑I : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))) ∧
          Eq.{u_1 + 1} (α := Set α) (⋂ (i : (↑t : Type uι)), U i) (⋂ (i : (↑I : Type uι)), V i)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), f i) (⋂ (i : (↑t : Type uι)), U i)

Tactic:
rw [← Equiv.plift.surjective.iInf_comp, mem_iInf]

Premises used: Filter.mem_iInf, Equiv.plift, Function.Surjective.iInf_comp, Equiv.surjective
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : (↑t : Type uι) → Set α
hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
U : (i : (↑t : Type uι)) → Set α
hUf : ∀ (i : (↑t : Type uι)), U i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
hU : ∀ (i : (↑t : Type uι)), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ∃ (I : Set (PLift ι)),
    I.Finite ∧
      ∃ (V : (↑I : Type uι) → Set α),
        (∀ (i : (↑I : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))) ∧
          Eq.{u_1 + 1} (α := Set α) (⋂ (i : (↑t : Type uι)), U i) (⋂ (i : (↑I : Type uι)), V i)

Tactic:
⟨t, ht, U, hUf, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : (↑t : Type uι) → Set α
hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
U : (i : (↑t : Type uι)) → Set α
hUf : ∀ (i : (↑t : Type uι)), U i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
hU : ∀ (i : (↑t : Type uι)), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ∃ (I : Set (PLift ι)),
    I.Finite ∧
      ∃ (V : (↑I : Type uι) → Set α),
        (∀ (i : (↑I : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))) ∧
          Eq.{u_1 + 1} (α := Set α) (⋂ (i : (↑t : Type uι)), U i) (⋂ (i : (↑I : Type uι)), V i)

Tactic:
exact ⟨t, ht, U, hUf, rfl⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : (↑t : Type uι) → Set α
hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
U : (i : (↑t : Type uι)) → Set α
hUf : ∀ (i : (↑t : Type uι)), U i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
hU : ∀ (i : (↑t : Type uι)), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ Countable.{uι + 1} (↑t : Type uι)

Tactic:
haveI := ht.countable.toEncodable.countable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : (↑t : Type uι) → Set α
hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
U : (i : (↑t : Type uι)) → Set α
hUf : ∀ (i : (↑t : Type uι)), U i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
hU : ∀ (i : (↑t : Type uι)), MeasurableSet (U i) ∧ U i ⊆ V i
this : Countable.{uι + 1} (↑t : Type uι)
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : (↑t : Type uι)), U i)

Tactic:
MeasurableSet.iInter fun i => (hU i).1

Premises used: And.left, MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : (↑t : Type uι) → Set α
hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
U : (i : (↑t : Type uι)) → Set α
hUf : ∀ (i : (↑t : Type uι)), U i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
hU : ∀ (i : (↑t : Type uι)), MeasurableSet (U i) ∧ U i ⊆ V i
this : Countable.{uι + 1} (↑t : Type uι)
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : (↑t : Type uι)), U i)

Tactic:
exact MeasurableSet.iInter fun i => (hU i).1

Premises used: And.left, MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : (↑t : Type uι) → Set α
hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
U : (i : (↑t : Type uι)) → Set α
hUf : ∀ (i : (↑t : Type uι)), U i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
hU : ∀ (i : (↑t : Type uι)), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ Subset.{u_1} (α := Set α) (⋂ (i : (↑t : Type uι)), U i) (⋂ (i : (↑t : Type uι)), V i)

Tactic:
iInter_mono fun i => (hU i).2

Premises used: And.right, Set.iInter_mono
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : (↑t : Type uι) → Set α
hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
U : (i : (↑t : Type uι)) → Set α
hUf : ∀ (i : (↑t : Type uι)), U i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
hU : ∀ (i : (↑t : Type uι)), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ Subset.{u_1} (α := Set α) (⋂ (i : (↑t : Type uι)), U i) (⋂ (i : (↑t : Type uι)), V i)

Tactic:
exact iInter_mono fun i => (hU i).2

Premises used: And.right, Set.iInter_mono
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
x : MeasurableSpace β
inst : MeasurableSpace γ
inst_1 : Countable δ
l : Filter δ
inst_2 : l.IsCountablyGenerated
l' : Filter γ
inst_3 : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
rcases :
  ∀ (u : ℕ → Set δ) (hu : l.HasAntitoneBasis u),
    MeasurableSet.{u_2} (α := β) {x : β | Tendsto (fun (n : δ) ↦ f n x) l l'}
⊢ MeasurableSet.{u_2} (α := β) {x : β | Tendsto (fun (n : δ) ↦ f n x) l l'}

Tactic:
rcases l.exists_antitone_basis with ⟨u, hu⟩

Premises used: Filter.exists_antitone_basis
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
x : MeasurableSpace β
inst : MeasurableSpace γ
inst_1 : Countable δ
l : Filter δ
inst_2 : l.IsCountablyGenerated
l' : Filter γ
inst_3 : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
u : ℕ → Set δ
hu : l.HasAntitoneBasis u
rcases :
  ∀ (v : ℕ → Set γ) (v_meas : ∀ (i : ℕ), v i ∈ l' ∧ MeasurableSet (v i))
    (hv : l'.HasAntitoneBasis fun (i : ℕ) ↦ id (v i)),
    MeasurableSet.{u_2} (α := β) {x : β | Tendsto (fun (n : δ) ↦ f n x) l l'}
⊢ MeasurableSet.{u_2} (α := β) {x : β | Tendsto (fun (n : δ) ↦ f n x) l l'}

Tactic:
rcases (Filter.hasBasis_self.mpr hl'.exists_measurable_subset).exists_antitone_subbasis with
    ⟨v, v_meas, hv⟩

Premises used: Iff.mpr, Filter.HasBasis.exists_antitone_subbasis, Filter.hasBasis_self, Filter.IsMeasurablyGenerated.exists_measurable_subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
x : MeasurableSpace β
inst : MeasurableSpace γ
inst_1 : Countable δ
l : Filter δ
inst_2 : l.IsCountablyGenerated
l' : Filter γ
inst_3 : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
u : ℕ → Set δ
hu : l.HasAntitoneBasis u
v : ℕ → Set γ
v_meas : ∀ (i : ℕ), v i ∈ l' ∧ MeasurableSet (v i)
hv : l'.HasAntitoneBasis fun (i : ℕ) ↦ id (v i)
simp : MeasurableSet.{u_2} (α := β) (⋂ (i : ℕ), ⋃ (i_1 : ℕ), ⋂ i_2 ∈ u i_1, {x : β | f i_2 x ∈ id (v i)})
⊢ MeasurableSet.{u_2} (α := β) {x : β | Tendsto (fun (n : δ) ↦ f n x) l l'}

Tactic:
simp only [hu.tendsto_iff hv.toHasBasis, true_imp_iff, true_and, setOf_forall, setOf_exists]

Premises used: Filter.HasAntitoneBasis.toHasBasis, Filter.HasBasis.tendsto_iff, Set.setOf_exists, true_imp_iff, Set.setOf_forall, true_and
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
x : MeasurableSpace β
inst : MeasurableSpace γ
inst_1 : Countable δ
l : Filter δ
inst_2 : l.IsCountablyGenerated
l' : Filter γ
inst_3 : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
u : ℕ → Set δ
hu : l.HasAntitoneBasis u
v : ℕ → Set γ
v_meas : ∀ (i : ℕ), v i ∈ l' ∧ MeasurableSet (v i)
hv : l'.HasAntitoneBasis fun (i : ℕ) ↦ id (v i)
⊢ MeasurableSet.{u_2} (α := β) (⋂ (i : ℕ), ⋃ (i_1 : ℕ), ⋂ i_2 ∈ u i_1, {x : β | f i_2 x ∈ id (v i)})

Tactic:
.iInter fun n ↦ .iUnion fun _ ↦ .biInter (to_countable _) fun i _ ↦
    (v_meas n).2.preimage (hf i)

Premises used: MeasurableSet.preimage, And.right, MeasurableSet.biInter, Set.to_countable, MeasurableSet.iUnion, MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
x : MeasurableSpace β
inst : MeasurableSpace γ
inst_1 : Countable δ
l : Filter δ
inst_2 : l.IsCountablyGenerated
l' : Filter γ
inst_3 : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
u : ℕ → Set δ
hu : l.HasAntitoneBasis u
v : ℕ → Set γ
v_meas : ∀ (i : ℕ), v i ∈ l' ∧ MeasurableSet (v i)
hv : l'.HasAntitoneBasis fun (i : ℕ) ↦ id (v i)
⊢ MeasurableSet.{u_2} (α := β) (⋂ (i : ℕ), ⋃ (i_1 : ℕ), ⋂ i_2 ∈ u i_1, {x : β | f i_2 x ∈ id (v i)})

Tactic:
exact .iInter fun n ↦ .iUnion fun _ ↦ .biInter (to_countable _) fun i _ ↦
    (v_meas n).2.preimage (hf i)
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Monotone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
rcases :
  ∀ (x : ℕ → ι) (hx : Tendsto x atTop atTop) (hxm : ∀ (n : ℕ), MeasurableSet (s (x n))),
    MeasurableSet.{u_1} (α := α) (⋃ (i : ι), s i)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), s i)

Tactic:
rcases exists_seq_forall_of_frequently hs with ⟨x, hx, hxm⟩

Premises used: Filter.exists_seq_forall_of_frequently
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Monotone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
x : ℕ → ι
hx : Tendsto x atTop atTop
hxm : ∀ (n : ℕ), MeasurableSet (s (x n))
rw : MeasurableSet.{u_1} (α := α) (⋃ (a : ℕ), s (x a))
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), s i)

Tactic:
rw [← hsm.iUnion_comp_tendsto_atTop hx]

Premises used: Monotone.iUnion_comp_tendsto_atTop
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Monotone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
x : ℕ → ι
hx : Tendsto x atTop atTop
hxm : ∀ (n : ℕ), MeasurableSet (s (x n))
⊢ MeasurableSet.{u_1} (α := α) (⋃ (a : ℕ), s (x a))

Tactic:
.iUnion hxm

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Monotone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
x : ℕ → ι
hx : Tendsto x atTop atTop
hxm : ∀ (n : ℕ), MeasurableSet (s (x n))
⊢ MeasurableSet.{u_1} (α := α) (⋃ (a : ℕ), s (x a))

Tactic:
exact .iUnion hxm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Antitone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
rw : MeasurableSet.{u_1} (α := α) (⋃ (i : ι), (s i)ᶜ)
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ι), s i)

Tactic:
rw [← compl_iff, compl_iInter]

Premises used: Set.compl_iInter, MeasurableSet.compl_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Antitone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), (s i)ᶜ)

Tactic:
.iUnion_of_monotone_of_frequently (compl_anti.comp hsm) <| hs.mono fun _ ↦ .compl

Premises used: compl_anti, Antitone.comp, MeasurableSet.compl, Filter.Frequently.mono, MeasurableSet.iUnion_of_monotone_of_frequently
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Antitone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), (s i)ᶜ)

Tactic:
exact .iUnion_of_monotone_of_frequently (compl_anti.comp hsm) <| hs.mono fun _ ↦ .compl

Premises used: Filter.Frequently.mono
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Monotone s
hs : ∀ (i : ι), MeasurableSet (s i)
h : IsEmpty ι
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), s i)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Monotone s
hs : ∀ (i : ι), MeasurableSet (s i)
h : Nonempty ι
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), s i)

Tactic:
.iUnion_of_monotone_of_frequently hsm <| .of_forall hs

Premises used: Filter.Frequently.of_forall, MeasurableSet.iUnion_of_monotone_of_frequently
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Monotone s
hs : ∀ (i : ι), MeasurableSet (s i)
h : Nonempty ι
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), s i)

Tactic:
exact .iUnion_of_monotone_of_frequently hsm <| .of_forall hs
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Monotone s
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ IsEmpty ι ∨ Nonempty ι

Tactic:
cases isEmpty_or_nonempty ι with
  | inl _ => simp
  | inr _ => exact .iUnion_of_monotone_of_frequently hsm <| .of_forall hs

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Antitone s
hs : ∀ (i : ι), MeasurableSet (s i)
rw : MeasurableSet.{u_1} (α := α) (⋃ (i : ι), (s i)ᶜ)
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ι), s i)

Tactic:
rw [← compl_iff, compl_iInter]

Premises used: Set.compl_iInter, MeasurableSet.compl_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Antitone s
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), (s i)ᶜ)

Tactic:
.iUnion_of_monotone (compl_anti.comp hsm) fun i ↦ (hs i).compl

Premises used: compl_anti, Antitone.comp, MeasurableSet.compl, MeasurableSet.iUnion_of_monotone
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Antitone s
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), (s i)ᶜ)

Tactic:
exact .iUnion_of_monotone (compl_anti.comp hsm) fun i ↦ (hs i).compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
s : Subtype (α := Set α) MeasurableSet
⊢ a ∈ (↑s : Set α) ↔ a ∈ s

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := Set α) (↑∅ : Set α) ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
s : Subtype (α := Set α) MeasurableSet
⊢ (↑(insert a s) : Set α) = insert a (↑s : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
⊢ Eq (α := Set α) (↑{a} : Set α) {a}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
⊢ LawfulSingleton α (Subtype (α := Set α) MeasurableSet)

Tactic:
⟨fun _ => Subtype.ext <| insert_empty_eq _⟩

Premises used: LawfulSingleton.mk, LawfulSingleton.insert_empty_eq, Subtype.ext
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Subtype (α := Set α) MeasurableSet
⊢ (↑sᶜ : Set α) = (↑s : Set α)ᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : Subtype (α := Set α) MeasurableSet
⊢ (↑(s ∪ t) : Set α) = (↑s : Set α) ∪ (↑t : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : { s : Set α // MeasurableSet s }
⊢ s ⊔ t = s ∪ t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : Subtype (α := Set α) MeasurableSet
⊢ (↑(s ∩ t) : Set α) = (↑s : Set α) ∩ (↑t : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : { s : Set α // MeasurableSet s }
⊢ s ⊓ t = s ∩ t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : Subtype (α := Set α) MeasurableSet
⊢ (↑(s \ t) : Set α) = (↑s : Set α) \ (↑t : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : Subtype (α := Set α) MeasurableSet
⊢ (↑(s ⇨ t) : Set α) = (↑s : Set α) ⇨ (↑t : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := Set α) (↑⊥ : Set α) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := Subtype (α := Set α) MeasurableSet) (Subtype.mk (p := MeasurableSet) ∅ ⋯) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := Set α) (↑⊤ : Set α) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
simp : MeasurableSet.{u_1} (α := α) (⋂ (i : ℕ), ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), s j)
⊢ MeasurableSet (blimsup s atTop p)

Tactic:
simp only [blimsup_eq_iInf_biSup_of_nat, iSup_eq_iUnion, iInf_eq_iInter]

Premises used: Set.iInf_eq_iInter, Set.iSup_eq_iUnion, Filter.blimsup_eq_iInf_biSup_of_nat
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ℕ), ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), s j)

Tactic:
.iInter fun _ => .iUnion fun m => .iUnion fun hm => h m hm.1

Premises used: And.left, MeasurableSet.iUnion, MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ℕ), ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), s j)

Tactic:
exact .iInter fun _ => .iUnion fun m => .iUnion fun hm => h m hm.1
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
simp : MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), ⋂ (j : ℕ), ⋂ (_ : p j ∧ i ≤ j), s j)
⊢ MeasurableSet (bliminf s atTop p)

Tactic:
simp only [Filter.bliminf_eq_iSup_biInf_of_nat, iInf_eq_iInter, iSup_eq_iUnion]

Premises used: Set.iInf_eq_iInter, Filter.bliminf_eq_iSup_biInf_of_nat, Set.iSup_eq_iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), ⋂ (j : ℕ), ⋂ (_ : p j ∧ i ≤ j), s j)

Tactic:
.iUnion fun n => .iInter fun m => .iInter fun hm => h m hm.1

Premises used: And.left, MeasurableSet.iUnion, MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), ⋂ (j : ℕ), ⋂ (_ : p j ∧ i ≤ j), s j)

Tactic:
exact .iUnion fun n => .iInter fun m => .iInter fun hm => h m hm.1