awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
u : Set Prop
⊢ MeasurableSet.{u_1} (α := α) ((fun (x : α) ↦ x ∈ s) ⁻¹' u)

Tactic:
exact (show MeasurableSet s from GenerateMeasurable.basic _ <| mem_singleton s).mem trivial

Premises used: MeasurableSet.mem, Set.mem_singleton, trivial, MeasurableSpace.GenerateMeasurable.basic
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
letI letI₁ letI₂ :
  Eq (α := MeasurableSpace α) (generateFrom {s}) (MeasurableSpace.comap (β := Prop) (fun (x : α) ↦ x ∈ s) ⊤)
letI₃ : LE.le (α := MeasurableSpace α) (MeasurableSpace.comap (β := Prop) (fun (x : α) ↦ x ∈ s) ⊤) (generateFrom {s})
letI₄ : ∀ (u : Set Prop), MeasurableSet.{u_1} (α := α) ((fun (x : α) ↦ x ∈ s) ⁻¹' u)
⊢ Eq (α := MeasurableSpace α) (generateFrom {s}) (MeasurableSpace.comap (β := Prop) (fun (x : α) ↦ x ∈ s) ⊤)

Tactic:
classical
  letI : MeasurableSpace α := generateFrom {s}
  refine le_antisymm (generateFrom_le fun t ht => ⟨{True}, trivial, by simp [ht.symm]⟩) ?_
  rintro _ ⟨u, -, rfl⟩
  exact (show MeasurableSet s from GenerateMeasurable.basic _ <| mem_singleton s).mem trivial

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ generateFrom {s} ≤ m

Tactic:
generateFrom_le (fun _ ht ↦ mem_singleton_iff.1 ht ▸ hs)

Premises used: Eq.rec, Set.mem_singleton_iff, Iff.mp, Eq.symm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s t : Set α
simp_rw : MeasurableSet t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
⊢ MeasurableSet t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Tactic:
simp_rw +instances [MeasurableSpace.generateFrom_singleton]

Premises used: MeasurableSpace.generateFrom_singleton
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s t : Set α
simp_rw : (∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ s) ⁻¹' s' = t) ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
⊢ ({ MeasurableSet' := fun (s_1 : Set α) ↦ ∃ (s' : Set Prop), MeasurableSet s' ∧ (fun (x : α) ↦ x ∈ s) ⁻¹' s' = s_1,
            measurableSet_empty := ⋯, measurableSet_compl := ⋯, measurableSet_iUnion := ⋯ } :
          MeasurableSpace α).1
      t ↔
    t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Tactic:
simp_rw [MeasurableSpace.measurableSet_top, true_and]

Premises used: MeasurableSpace.measurableSet_top, true_and
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s t : Set α
mp : (∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ s) ⁻¹' s' = t) → t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
mpr : t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ → ∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ s) ⁻¹' s' = t
⊢ (∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ s) ⁻¹' s' = t) ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
x : Set Prop
pos :
  ∀ (hT : True ∈ x),
    Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
        (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
neg :
  ∀ (hT : True ∉ x),
    Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
        (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ

Tactic:
by_cases hT : True ∈ x

Premises used: True
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
pos :
  ∀ (hF : False ∈ x),
    Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
        (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
neg :
  ∀ (hF : False ∉ x),
    Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
        (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ

Tactic:
by_cases hF : False ∈ x

Premises used: False
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
this : x = univ
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ

Tactic:
grind
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
pos : x = univ
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ

Tactic:
suffices x = univ by grind
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
⊢ x = univ

Tactic:
grind [univ_eq_true_false]

Premises used: Set.univ_eq_true_false
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∉ x
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ

Tactic:
grind
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
pos :
  ∀ (hF : False ∈ x),
    Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
        (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
neg :
  ∀ (hF : False ∉ x),
    Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
        (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ

Tactic:
by_cases hF : False ∈ x

Premises used: False
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ

Tactic:
grind
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
this : x ⊆ ∅
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ

Tactic:
grind
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
neg : x ⊆ ∅
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) ∅ ∨
    (fun (x : α) ↦ x ∈ s) ⁻¹' x = s ∨
      (fun (x : α) ↦ x ∈ s) ⁻¹' x = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' x) univ

Tactic:
suffices x ⊆ ∅ by grind
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
p : Prop
hp : p ∈ x
neg : ∀ (hp : True ∈ x), Membership.mem (γ := Set Prop) ∅ True
neg₁ : ∀ (hp : False ∈ x), Membership.mem (γ := Set Prop) ∅ False
⊢ Membership.mem (γ := Set Prop) ∅ p

Tactic:
fin_cases p
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
hp : True ∈ x
⊢ Membership.mem (γ := Set Prop) ∅ True

Tactic:
contradiction
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
hp : False ∈ x
⊢ Membership.mem (γ := Set Prop) ∅ False

Tactic:
contradiction
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
h : Eq.{u_1 + 1} (α := Set α) (preimage (β := Prop) (fun (x : α) ↦ x ∈ s) ∅) ∅
⊢ ∃ (s' : Set Prop), Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' s') ∅

Tactic:
use ∅
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
h : Eq.{u_1 + 1} (α := Set α) (preimage (β := Prop) (fun (x : α) ↦ x ∈ s) ∅) ∅
⊢ ∃ (s' : Set Prop), Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' s') ∅

Tactic:
on_goal 1 => use ∅
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
t : Set α
h : preimage (β := Prop) (fun (x : α) ↦ x ∈ t) {True} = t
⊢ ∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ t) ⁻¹' s' = t

Tactic:
use {True}

Premises used: True
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
t : Set α
h : preimage (β := Prop) (fun (x : α) ↦ x ∈ t) {True} = t
⊢ ∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ t) ⁻¹' s' = t

Tactic:
on_goal 2 => use {True}

Premises used: True
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
h : preimage (β := Prop) (fun (x : α) ↦ x ∈ s) {False} = sᶜ
⊢ ∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ s) ⁻¹' s' = sᶜ

Tactic:
use {False}

Premises used: False
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
h : preimage (β := Prop) (fun (x : α) ↦ x ∈ s) {False} = sᶜ
⊢ ∃ (s' : Set Prop), (fun (x : α) ↦ x ∈ s) ⁻¹' s' = sᶜ

Tactic:
on_goal 3 => use {False}

Premises used: False
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
h : Eq.{u_1 + 1} (α := Set α) (preimage (β := Prop) (fun (x : α) ↦ x ∈ s) univ) univ
⊢ ∃ (s' : Set Prop), Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' s') univ

Tactic:
use Set.univ

Premises used: Set.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
h : Eq.{u_1 + 1} (α := Set α) (preimage (β := Prop) (fun (x : α) ↦ x ∈ s) univ) univ
⊢ ∃ (s' : Set Prop), Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ x ∈ s) ⁻¹' s') univ

Tactic:
on_goal 4 => use Set.univ

Premises used: Set.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
⊢ Eq.{u_1 + 1} (α := Set α) (preimage (β := Prop) (fun (x : α) ↦ x ∈ s) ∅) ∅

Tactic:
simp [compl_def]

Premises used: Set.compl_def
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
t : Set α
⊢ preimage (β := Prop) (fun (x : α) ↦ x ∈ t) {True} = t

Tactic:
simp [compl_def]

Premises used: Set.compl_def
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
⊢ preimage (β := Prop) (fun (x : α) ↦ x ∈ s) {False} = sᶜ

Tactic:
simp [compl_def]

Premises used: Set.compl_def
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
⊢ Eq.{u_1 + 1} (α := Set α) (preimage (β := Prop) (fun (x : α) ↦ x ∈ s) univ) univ

Tactic:
simp [compl_def]

Premises used: Set.compl_def
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
⊢ IsMeasurablyGenerated.{u_1} (α := α) ⊥

Tactic:
⟨fun _ _ => ⟨∅, mem_bot, MeasurableSet.empty, empty_subset _⟩⟩

Premises used: MeasurableSet.empty, Filter.mem_bot, And.intro, Set.empty_subset, Exists.intro, Filter.IsMeasurablyGenerated.mk, EmptyCollection.emptyCollection
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
⊢ IsMeasurablyGenerated.{u_1} (α := α) ⊤

Tactic:
⟨fun _s hs => ⟨univ, univ_mem, MeasurableSet.univ, fun x _ => hs x⟩⟩

Premises used: Set.univ, And.intro, Exists.intro, Filter.IsMeasurablyGenerated.mk, Filter.univ_mem, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
f : Filter α
inst_1 : f.IsMeasurablyGenerated
p : α → Prop
h : ∀ᶠ (x : α) in f, p x
⊢ ∃ s ∈ f, MeasurableSet s ∧ ∀ x ∈ s, p x

Tactic:
IsMeasurablyGenerated.exists_measurable_subset h

Premises used: Set.Mem, Set.Subset, Filter.IsMeasurablyGenerated.exists_measurable_subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
f : Filter α
inst_1 : f.IsMeasurablyGenerated
p : Set α → Prop
h : ∀ᶠ (s : Set α) in f.smallSets, p s
⊢ ∃ s ∈ f, MeasurableSet s ∧ p s

Tactic:
let ⟨_s, hsf, hs⟩ := eventually_smallSets.1 h
  let ⟨t, htf, htm, hts⟩ := IsMeasurablyGenerated.exists_measurable_subset hsf
  ⟨t, htf, htm, hs t hts⟩

Premises used: _private.0.Filter.Eventually.exists_measurable_mem_of_smallSets.match_2, MeasurableSet, _private.0.Filter.Eventually.exists_measurable_mem_of_smallSets.match_1, Membership.mem, Exists, Filter.eventually_smallSets, And, And.intro, Exists.intro, Iff.mp, Filter.IsMeasurablyGenerated.exists_measurable_subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f g : Filter α
inst_1 : f.IsMeasurablyGenerated
inst_2 : g.IsMeasurablyGenerated
exists_measurable_subset : ∀ ⦃s : Set α⦄, s ∈ f ⊓ g → ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ s
⊢ (f ⊓ g).IsMeasurablyGenerated

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f g : Filter α
inst_1 : f.IsMeasurablyGenerated
inst_2 : g.IsMeasurablyGenerated
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
exists_measurable_subset :
  ∀ (s'f : Set α) (hs'f : s'f ∈ f) (hmf : MeasurableSet s'f) (hs'sf : s'f ⊆ sf),
    ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ sf ∩ sg
⊢ ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ sf ∩ sg

Tactic:
rcases IsMeasurablyGenerated.exists_measurable_subset hsf with ⟨s'f, hs'f, hmf, hs'sf⟩

Premises used: Filter.IsMeasurablyGenerated.exists_measurable_subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f g : Filter α
inst_1 : f.IsMeasurablyGenerated
inst_2 : g.IsMeasurablyGenerated
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
s'f : Set α
hs'f : s'f ∈ f
hmf : MeasurableSet s'f
hs'sf : s'f ⊆ sf
exists_measurable_subset :
  ∀ (s'g : Set α) (hs'g : s'g ∈ g) (hmg : MeasurableSet s'g) (hs'sg : s'g ⊆ sg),
    ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ sf ∩ sg
⊢ ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ sf ∩ sg

Tactic:
rcases IsMeasurablyGenerated.exists_measurable_subset hsg with ⟨s'g, hs'g, hmg, hs'sg⟩

Premises used: Filter.IsMeasurablyGenerated.exists_measurable_subset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f g : Filter α
inst_1 : f.IsMeasurablyGenerated
inst_2 : g.IsMeasurablyGenerated
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
s'f : Set α
hs'f : s'f ∈ f
hmf : MeasurableSet s'f
hs'sf : s'f ⊆ sf
s'g : Set α
hs'g : s'g ∈ g
hmg : MeasurableSet s'g
hs'sg : s'g ⊆ sg
⊢ ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ sf ∩ sg

Tactic:
⟨s'f ∩ s'g, inter_mem_inf hs'f hs'g, hmf.inter hmg, ?_⟩

Premises used: Filter.inter_mem_inf, Inter.inter, And.intro, Exists.intro, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f g : Filter α
inst_1 : f.IsMeasurablyGenerated
inst_2 : g.IsMeasurablyGenerated
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
s'f : Set α
hs'f : s'f ∈ f
hmf : MeasurableSet s'f
hs'sf : s'f ⊆ sf
s'g : Set α
hs'g : s'g ∈ g
hmg : MeasurableSet s'g
hs'sg : s'g ⊆ sg
exists_measurable_subset : s'f ∩ s'g ⊆ sf ∩ sg
⊢ ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ sf ∩ sg

Tactic:
refine ⟨s'f ∩ s'g, inter_mem_inf hs'f hs'g, hmf.inter hmg, ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f g : Filter α
inst_1 : f.IsMeasurablyGenerated
inst_2 : g.IsMeasurablyGenerated
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
s'f : Set α
hs'f : s'f ∈ f
hmf : MeasurableSet s'f
hs'sf : s'f ⊆ sf
s'g : Set α
hs'g : s'g ∈ g
hmg : MeasurableSet s'g
hs'sg : s'g ⊆ sg
⊢ s'f ∩ s'g ⊆ sf ∩ sg

Tactic:
inter_subset_inter hs'sf hs'sg

Premises used: Set.inter_subset_inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f g : Filter α
inst_1 : f.IsMeasurablyGenerated
inst_2 : g.IsMeasurablyGenerated
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
s'f : Set α
hs'f : s'f ∈ f
hmf : MeasurableSet s'f
hs'sf : s'f ⊆ sf
s'g : Set α
hs'g : s'g ∈ g
hmg : MeasurableSet s'g
hs'sg : s'g ⊆ sg
⊢ s'f ∩ s'g ⊆ sf ∩ sg

Tactic:
exact inter_subset_inter hs'sf hs'sg

Premises used: Set.inter_subset_inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
⊢ (𝓟 s).IsMeasurablyGenerated ↔ MeasurableSet s

Tactic:
⟨?_, fun hs => ⟨fun t ht => ⟨s, mem_principal_self s, hs, ht⟩⟩⟩

Premises used: Filter.mem_principal_self, And.intro, Iff.intro, Exists.intro, Filter.IsMeasurablyGenerated.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
refine : (𝓟 s).IsMeasurablyGenerated → MeasurableSet s
⊢ (𝓟 s).IsMeasurablyGenerated ↔ MeasurableSet s

Tactic:
refine ⟨?_, fun hs => ⟨fun t ht => ⟨s, mem_principal_self s, hs, ht⟩⟩⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1
rcases : ∀ (t : Set α) (ht : t ∈ 𝓟 s) (htm : MeasurableSet t) (hts : t ⊆ s), MeasurableSet s
⊢ MeasurableSet s

Tactic:
rcases hs (mem_principal_self s) with ⟨t, ht, htm, hts⟩

Premises used: Filter.mem_principal_self
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1
t : Set α
ht : t ∈ 𝓟 s
htm : MeasurableSet t
hts : t ⊆ s
⊢ t = s

Tactic:
have : t = s := hts.antisymm ht
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1
t : Set α
ht : t ∈ 𝓟 s
htm : MeasurableSet t
hts : t ⊆ s
this : t = s
rwa rwa₁ rwa₂ rwa₃ : MeasurableSet t
⊢ MeasurableSet s

Tactic:
rwa [← this]
-- 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
⊢ IsMeasurablyGenerated.{u_1} (α := α) (⨅ (i : ι), f i)

Tactic:
⟨fun s hs => ?_⟩

Premises used: Filter.IsMeasurablyGenerated.mk
-- 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
refine :
  ∀ (s : Set α) (hs : Membership.mem (γ := Filter α) (⨅ (i : ι), f i) s),
    ∃ (t : Set α), Membership.mem (γ := Filter α) (⨅ (i : ι), f i) t ∧ MeasurableSet t ∧ t ⊆ s
⊢ IsMeasurablyGenerated.{u_1} (α := α) (⨅ (i : ι), f i)

Tactic:
refine ⟨fun s hs => ?_⟩
-- 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
s : Set α
hs : Membership.mem (γ := Filter α) (⨅ (i : ι), f i) s
⊢ ∃ (I : Set (PLift ι)),
    I.Finite ∧
      ∃ (V : (↑I : Type uι) → Set α),
        (∀ (i : (↑I : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))) ∧
          s = ⋂ (i : (↑I : Type uι)), V i

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

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
s : Set α
hs :
  ∃ (I : Set (PLift ι)),
    I.Finite ∧
      ∃ (V : (↑I : Type uι) → Set α),
        (∀ (i : (↑I : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))) ∧
          s = ⋂ (i : (↑I : Type uι)), V i
rcases :
  ∀ (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 ι))),
    ∃ (t_1 : Set α),
      Membership.mem (γ := Filter α) (⨅ (i : ι), f i) t_1 ∧ MeasurableSet t_1 ∧ t_1 ⊆ ⋂ (i : (↑t : Type uι)), V i
⊢ ∃ (t : Set α), Membership.mem (γ := Filter α) (⨅ (i : ι), f i) t ∧ MeasurableSet t ∧ t ⊆ s

Tactic:
rcases hs with ⟨t, ht, ⟨V, hVf, 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 α
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 ι))
choose :
  ∀ (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),
    ∃ (t_1 : Set α),
      Membership.mem (γ := Filter α) (⨅ (i : ι), f i) t_1 ∧ MeasurableSet t_1 ∧ t_1 ⊆ ⋂ (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:
choose U hUf hU using fun i => IsMeasurablyGenerated.exists_measurable_subset (hVf i)

Premises used: Filter.IsMeasurablyGenerated.exists_measurable_subset
-- 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
⊢ ∃ (t_1 : Set α),
    Membership.mem (γ := Filter α) (⨅ (i : ι), f i) t_1 ∧ MeasurableSet t_1 ∧ t_1 ⊆ ⋂ (i : (↑t : Type uι)), V i

Tactic:
⟨⋂ i : t, U i, ?_, ?_, ?_⟩

Premises used: Set.iInter, And.intro, Exists.intro