awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
⊢ Membership.mem (γ := Set (Set α))
      {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}
      s ↔
    s ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} s

Tactic:
⟨?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
h :
  Membership.mem (γ := Set (Set α))
      {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}
      s →
    s ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} s
h₁ :
  ∀ (h : s ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} s),
    Membership.mem (γ := Set (Set α))
      {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s
⊢ Membership.mem (γ := Set (Set α))
      {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}
      s ↔
    s ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} s

Tactic:
refine ⟨?_, fun h => ?_⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
hti : (↑t : Set ι) ⊆ {i}
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
⊢ ∀ y ∈ t, y = i

Tactic:
simp only [subset_singleton_iff, Finset.mem_coe] at hti

Premises used: Set.subset_singleton_iff, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
pos : ∀ (hi : i ∈ t), ⋂ x ∈ t, f x ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (⋂ x ∈ t, f x)
neg : ∀ (hi : i ∉ t), ⋂ x ∈ t, f x ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (⋂ x ∈ t, f x)
⊢ ⋂ x ∈ t, f x ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (⋂ x ∈ t, f x)

Tactic:
by_cases hi : i ∈ t
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
h : ∀ (x : ι), x ∈ t ↔ Membership.mem (γ := Finset ι) {i} x
⊢ t = {i}

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
x : ι
h : x ∈ t ↔ x = i
⊢ x ∈ t ↔ Membership.mem (γ := Finset ι) {i} x

Tactic:
rw [Finset.mem_singleton]

Premises used: Finset.mem_singleton
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
x : ι
⊢ x ∈ t ↔ x = i

Tactic:
⟨fun h => hti x h, fun h => h.symm ▸ hi⟩

Premises used: Eq.rec, Iff.intro, Eq.symm
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
x : ι
⊢ x ∈ t ↔ x = i

Tactic:
exact ⟨fun h => hti x h, fun h => h.symm ▸ hi⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
⊢ t = {i}

Tactic:
have ht_eq_i : t = {i} := by
        ext1 x
        rw [Finset.mem_singleton]
        exact ⟨fun h => hti x h, fun h => h.symm ▸ hi⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
ht_eq_i : t = {i}
pos : f i ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (f i)
⊢ ⋂ x ∈ t, f x ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (⋂ x ∈ t, f x)

Tactic:
simp only [ht_eq_i, Finset.mem_singleton, iInter_iInter_eq_left]

Premises used: Finset.mem_singleton, Set.iInter_iInter_eq_left
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
ht_eq_i : t = {i}
⊢ f i ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (f i)

Tactic:
Or.inl (hfπ i hi)

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∈ t
ht_eq_i : t = {i}
⊢ f i ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (f i)

Tactic:
exact Or.inl (hfπ i hi)

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
h : ∀ (x : ι), x ∈ t ↔ Membership.mem (γ := Finset ι) ∅ x
⊢ t = ∅

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
x : ι
h : x ∉ t
⊢ x ∈ t ↔ Membership.mem (γ := Finset ι) ∅ x

Tactic:
simp only [Finset.notMem_empty, iff_false]

Premises used: iff_false, Finset.notMem_empty
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
x : ι
⊢ x ∉ t

Tactic:
fun hx => hi (hti x hx ▸ hx)

Premises used: Eq.rec, Not
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
x : ι
⊢ x ∉ t

Tactic:
exact fun hx => hi (hti x hx ▸ hx)

Premises used: Eq.rec
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
⊢ t = ∅

Tactic:
have ht_empty : t = ∅ := by
        ext1 x
        simp only [Finset.notMem_empty, iff_false]
        exact fun hx => hi (hti x hx ▸ hx)
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
ht_empty : t = ∅
⊢ ⋂ x ∈ t, f x ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} (⋂ x ∈ t, f x)

Tactic:
simp [ht_empty, iInter_univ, Set.mem_singleton univ]

Premises used: Set.mem_singleton, Set.univ, Set.iInter_univ
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
h : s ∈ π i ∨ Membership.mem (γ := Set (Set α)) {univ} s
h₁ :
  ∀ (hs : s ∈ π i),
    Membership.mem (γ := Set (Set α))
      {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s
h₂ :
  ∀ (hs : Membership.mem (γ := Set (Set α)) {univ} s),
    Membership.mem (γ := Set (Set α))
      {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s
⊢ Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s

Tactic:
rcases h with hs | hs
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s

Tactic:
⟨{i}, ?_, fun _ => s, ⟨fun x hx => ?_, ?_⟩⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Singleton.singleton
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
h : (↑{i} : Set ι) ⊆ {i}
h₁ : ∀ (x : ι) (hx : Membership.mem (γ := Finset ι) {i} x), (fun (x : ι) ↦ s) x ∈ π x
h₂ : s = ⋂ (x : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {i} x), (fun (x : ι) ↦ s) x
⊢ Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s

Tactic:
refine ⟨{i}, ?_, fun _ => s, ⟨fun x hx => ?_, ?_⟩⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
h h₁ : Subset (α := Set ι) {i} {i}
⊢ (↑{i} : Set ι) ⊆ {i}

Tactic:
rw [Finset.coe_singleton]

Premises used: Finset.coe_singleton
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : Membership.mem (γ := Finset ι) {i} x
⊢ x = i

Tactic:
rw [Finset.mem_singleton] at hx

Premises used: Finset.mem_singleton
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : x = i
h h₁ h₂ h₃ : (fun (x : ι) ↦ s) i ∈ π i
⊢ (fun (x : ι) ↦ s) x ∈ π x

Tactic:
rwa [hx]
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s = ⋂ (x : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {i} x), (fun (x : ι) ↦ s) x

Tactic:
simp only [Finset.mem_singleton, iInter_iInter_eq_left]

Premises used: Finset.mem_singleton, Set.iInter_iInter_eq_left
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : Membership.mem (γ := Set (Set α)) {univ} s
⊢ Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s

Tactic:
⟨∅, ?_⟩

Premises used: Set.Mem, setOf, Exists.intro, EmptyCollection.emptyCollection
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : Membership.mem (γ := Set (Set α)) {univ} s
h :
  (↑∅ : Set ι) ⊆ {i} ∧
    ∃ (f : ι → Set α),
      (∀ (x : ι), Membership.mem (γ := Finset ι) ∅ x → f x ∈ π x) ∧
        s = ⋂ (x : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ x), f x
⊢ Membership.mem (γ := Set (Set α))
    {s : Set α | ∃ (t : Finset ι), (↑t : Set ι) ⊆ {i} ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} s

Tactic:
refine ⟨∅, ?_⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : Membership.mem (γ := Set (Set α)) {univ} s
⊢ (↑∅ : Set ι) ⊆ {i} ∧
    ∃ (f : ι → Set α),
      (∀ (x : ι), Membership.mem (γ := Finset ι) ∅ x → f x ∈ π x) ∧
        s = ⋂ (x : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ x), f x

Tactic:
simpa only [Finset.coe_empty, subset_singleton_iff, mem_empty_iff_false, IsEmpty.forall_iff,
        imp_true_iff, Finset.notMem_empty, iInter_false, iInter_univ, true_and,
        exists_const] using hs

Premises used: Finset.coe_empty, Set.subset_singleton_iff, Set.iInter_univ, imp_true_iff, Finset.notMem_empty, exists_const, Set.iInter_false, Set.mem_empty_iff_false, true_and, IsEmpty.forall_iff
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
h :
  ∀ (s' : Set α),
    Membership.mem (γ := Set (Set α)) (piiUnionInter (fun (i : ι) ↦ {s i}) S) s' ↔
      Membership.mem (γ := Set (Set α)) {s' : Set α | ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S), s' = ⋂ i ∈ t, s i} s'
⊢ Eq.{u_3 + 1} (α := Set (Set α)) (piiUnionInter (fun (i : ι) ↦ {s i}) S)
    {s' : Set α | ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S), s' = ⋂ i ∈ t, s i}

Tactic:
ext1 s'
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
h :
  (∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x = s x) ∧ s' = ⋂ x ∈ t, f x) ↔
    ∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ s' = ⋂ i ∈ t, s i
⊢ Membership.mem (γ := Set (Set α)) (piiUnionInter (fun (i : ι) ↦ {s i}) S) s' ↔
    Membership.mem (γ := Set (Set α)) {s' : Set α | ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S), s' = ⋂ i ∈ t, s i} s'

Tactic:
simp_rw [piiUnionInter, Set.mem_singleton_iff, exists_prop, Set.mem_setOf_eq]

Premises used: piiUnionInter, Set.mem_setOf_eq, exists_prop, Set.mem_singleton_iff
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
⊢ (∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x = s x) ∧ s' = ⋂ x ∈ t, f x) ↔
    ∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ s' = ⋂ i ∈ t, s i

Tactic:
⟨fun h => ?_, fun ⟨t, htS, h_eq⟩ => ⟨t, htS, s, fun _ _ => rfl, h_eq⟩⟩

Premises used: Set.iInter, Exists, HasSubset.Subset, And, SetLike.coe, And.intro, Iff.intro, _private.0.piiUnionInter_singleton_left.match_1, Exists.intro, Eq, rfl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
h :
  ∀ (h : ∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x = s x) ∧ s' = ⋂ x ∈ t, f x),
    ∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ s' = ⋂ i ∈ t, s i
⊢ (∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x = s x) ∧ s' = ⋂ x ∈ t, f x) ↔
    ∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ s' = ⋂ i ∈ t, s i

Tactic:
refine ⟨fun h => ?_, fun ⟨t, htS, h_eq⟩ => ⟨t, htS, s, fun _ _ => rfl, h_eq⟩⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
h : ∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ ∃ (f : ι → Set α), (∀ x ∈ t, f x = s x) ∧ s' = ⋂ x ∈ t, f x
⊢ ∃ (t : Finset ι), (↑t : Set ι) ⊆ S ∧ s' = ⋂ i ∈ t, s i

Tactic:
grind
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ Eq.{u_3 + 1} (α := MeasurableSpace α) (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) S))
    (generateFrom {t : Set α | ∃ k ∈ S, s k = t})

Tactic:
le_antisymm (generateFrom_le ?_) (generateFrom_mono ?_)

Premises used: MeasurableSpace.generateFrom_mono, le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
refine_1 : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (piiUnionInter (fun (k : ι) ↦ {s k}) S) t → MeasurableSet t
refine_2 : Subset.{u_3} (α := Set (Set α)) {t : Set α | ∃ k ∈ S, s k = t} (piiUnionInter (fun (k : ι) ↦ {s k}) S)
⊢ Eq.{u_3 + 1} (α := MeasurableSpace α) (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) S))
    (generateFrom {t : Set α | ∃ k ∈ S, s k = t})

Tactic:
refine le_antisymm (generateFrom_le ?_) (generateFrom_mono ?_)

Premises used: MeasurableSpace.generateFrom_mono, le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
I : Finset ι
hI : (↑I : Set ι) ⊆ S
f : ι → Set α
hf : ∀ x ∈ I, Membership.mem (γ := Set (Set α)) ((fun (k : ι) ↦ ({s k} : Set (Set α))) x) (f x)
⊢ MeasurableSet.{u_3} (α := α) (⋂ x ∈ I, f x)

Tactic:
Finset.measurableSet_biInter _ fun m hm => measurableSet_generateFrom ?_

Premises used: MeasurableSpace.measurableSet_generateFrom, Finset.measurableSet_biInter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
I : Finset ι
hI : (↑I : Set ι) ⊆ S
f : ι → Set α
hf : ∀ x ∈ I, Membership.mem (γ := Set (Set α)) ((fun (k : ι) ↦ ({s k} : Set (Set α))) x) (f x)
refine_1 : ∀ (m : ι) (hm : m ∈ I), Membership.mem (γ := Set (Set α)) {t : Set α | ∃ k ∈ S, s k = t} (f m)
⊢ MeasurableSet.{u_3} (α := α) (⋂ x ∈ I, f x)

Tactic:
refine Finset.measurableSet_biInter _ fun m hm => measurableSet_generateFrom ?_

Premises used: MeasurableSpace.measurableSet_generateFrom, Finset.measurableSet_biInter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
I : Finset ι
hI : (↑I : Set ι) ⊆ S
f : ι → Set α
hf : ∀ x ∈ I, Membership.mem (γ := Set (Set α)) ((fun (k : ι) ↦ ({s k} : Set (Set α))) x) (f x)
m : ι
hm : m ∈ I
⊢ Membership.mem (γ := Set (Set α)) {t : Set α | ∃ k ∈ S, s k = t} (f m)

Tactic:
⟨m, hI hm, (hf m hm).symm⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
I : Finset ι
hI : (↑I : Set ι) ⊆ S
f : ι → Set α
hf : ∀ x ∈ I, Membership.mem (γ := Set (Set α)) ((fun (k : ι) ↦ ({s k} : Set (Set α))) x) (f x)
m : ι
hm : m ∈ I
⊢ Membership.mem (γ := Set (Set α)) {t : Set α | ∃ k ∈ S, s k = t} (f m)

Tactic:
exact ⟨m, hI hm, (hf m hm).symm⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ Membership.mem (γ := Set (Set α)) (piiUnionInter (fun (k : ι) ↦ {s k}) S) (s k)

Tactic:
⟨{k}, fun m hm => ?_, s, fun i _ => ?_, ?_⟩

Premises used: piiUnionInter, Set.Mem, setOf, Exists.intro, Singleton.singleton
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
refine_2 : ∀ (m : ι) (hm : m ∈ (↑{k} : Set ι)), m ∈ S
refine_2₁ :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) {k} i →
      Membership.mem (γ := Set (Set α)) ((fun (k : ι) ↦ ({s k} : Set (Set α))) i) (s i)
refine_2₂ : s k = ⋂ (x : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {k} x), s x
⊢ Membership.mem (γ := Set (Set α)) (piiUnionInter (fun (k : ι) ↦ {s k}) S) (s k)

Tactic:
refine ⟨{k}, fun m hm => ?_, s, fun i _ => ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m ∈ (↑{k} : Set ι)
⊢ m = k

Tactic:
rw [Finset.mem_coe, Finset.mem_singleton] at hm

Premises used: Finset.mem_singleton, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m = k
refine_2 refine_2₁ refine_2₂ refine_2₃ : k ∈ S
⊢ m ∈ S

Tactic:
rwa [hm]
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
i : ι
h : Membership.mem (γ := Finset ι) {k} i
⊢ Membership.mem (γ := Set (Set α)) ((fun (k : ι) ↦ ({s k} : Set (Set α))) i) (s i)

Tactic:
Set.mem_singleton _

Premises used: Set.mem_singleton, Set.Mem
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
i : ι
h : Membership.mem (γ := Finset ι) {k} i
⊢ Membership.mem (γ := Set (Set α)) ((fun (k : ι) ↦ ({s k} : Set (Set α))) i) (s i)

Tactic:
exact Set.mem_singleton _

Premises used: Set.mem_singleton
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k = ⋂ (x : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {k} x), s x

Tactic:
simp only [Finset.mem_singleton, Set.iInter_iInter_eq_left]

Premises used: Finset.mem_singleton, Set.iInter_iInter_eq_left
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : (↑p1 : Set ι) ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : (↑p2 : Set ι) ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
⊢ (↑(p1 ∪ p2) : Set ι) ⊆ S

Tactic:
simp only [hp1S, hp2S, Finset.coe_union, union_subset_iff, and_self_iff]

Premises used: Set.union_subset_iff, and_self_iff, Finset.coe_union
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : (↑p1 : Set ι) ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : (↑p2 : Set ι) ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
⊢ (↑(p1 ∪ p2) : Set ι) ⊆ S

Tactic:
have hp_union_ss : ↑(p1 ∪ p2) ⊆ S := by
    simp only [hp1S, hp2S, Finset.coe_union, union_subset_iff, and_self_iff]
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : (↑p1 : Set ι) ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : (↑p2 : Set ι) ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
h : ∃ (_ : ∀ x ∈ p1 ∪ p2, g x ∈ π x), t1 ∩ t2 = ⋂ x ∈ p1 ∪ p2, g x
⊢ ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S) (f : ι → Set α) (_ : ∀ x ∈ t, f x ∈ π x), t1 ∩ t2 = ⋂ x ∈ t, f x

Tactic:
use p1 ∪ p2, hp_union_ss, g
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : (↑p1 : Set ι) ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : (↑p2 : Set ι) ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
rw : Eq.{u_3 + 1} (α := Set α) ((⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x) (⋂ i ∈ p1 ∪ p2, g i)
⊢ t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i

Tactic:
rw [ht1_eq, ht2_eq]
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : (↑p1 : Set ι) ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : (↑p2 : Set ι) ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((⋂ x ∈ p1, f1 x) ⊓ ⋂ x ∈ p2, f2 x) x ↔
      Membership.mem (γ := Set α) (⋂ i ∈ p1 ∪ p2, g i) x
⊢ Eq.{u_3 + 1} (α := Set α) ((⋂ x ∈ p1, f1 x) ⊓ ⋂ x ∈ p2, f2 x) (⋂ i ∈ p1 ∪ p2, g i)

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : (↑p1 : Set ι) ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : (↑p2 : Set ι) ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
x : α
h : ((∀ (i : ι) (i_1 : i ∈ p1), x ∈ f1 i) ∧ ∀ (i : ι) (i_1 : i ∈ p2), x ∈ f2 i) ↔ ∀ (i : ι) (i_1 : i ∈ p1 ∪ p2), x ∈ g i
⊢ Membership.mem (γ := Set α) ((⋂ x ∈ p1, f1 x) ⊓ ⋂ x ∈ p2, f2 x) x ↔ Membership.mem (γ := Set α) (⋂ i ∈ p1 ∪ p2, g i) x

Tactic:
simp only [inf_eq_inter, mem_inter_iff, mem_iInter]

Premises used: Set.mem_inter_iff, Set.mem_iInter, Set.inf_eq_inter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : (↑p1 : Set ι) ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : (↑p2 : Set ι) ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
x : α
⊢ ((∀ (i : ι) (i_1 : i ∈ p1), x ∈ f1 i) ∧ ∀ (i : ι) (i_1 : i ∈ p2), x ∈ f2 i) ↔ ∀ (i : ι) (i_1 : i ∈ p1 ∪ p2), x ∈ g i

Tactic:
grind