awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
g : Set (Set α)
a : generateFrom (generatePiSystem g) ≤ generateFrom g
a₁ : generateFrom g ≤ generateFrom (generatePiSystem g)
⊢ generateFrom (generatePiSystem g) = generateFrom g

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
g : Set (Set α)
a : ∀ t ∈ generatePiSystem g, MeasurableSet t
⊢ generateFrom (generatePiSystem g) ≤ generateFrom g

Tactic:
apply generateFrom_le

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
g : Set (Set α)
a : ∀ t ∈ g, MeasurableSet t
⊢ generateFrom g ≤ generateFrom (generatePiSystem g)

Tactic:
apply generateFrom_le

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
g : Set (Set α)
⊢ ∀ t ∈ generatePiSystem g, MeasurableSet t

Tactic:
fun t h_t => generateFrom_measurableSet_of_generatePiSystem t h_t

Premises used: generateFrom_measurableSet_of_generatePiSystem
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
g : Set (Set α)
⊢ ∀ t ∈ generatePiSystem g, MeasurableSet t

Tactic:
exact fun t h_t => generateFrom_measurableSet_of_generatePiSystem t h_t

Premises used: generateFrom_measurableSet_of_generatePiSystem
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
g : Set (Set α)
⊢ ∀ t ∈ g, MeasurableSet t

Tactic:
fun t h_t => measurableSet_generateFrom (generatePiSystem.base h_t)

Premises used: MeasurableSpace.measurableSet_generateFrom, generatePiSystem.base
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
g : Set (Set α)
⊢ ∀ t ∈ g, MeasurableSet t

Tactic:
exact fun t h_t => measurableSet_generateFrom (generatePiSystem.base h_t)

Premises used: MeasurableSpace.measurableSet_generateFrom, generatePiSystem.base
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s : Set α
h_s : Membership.mem (γ := Set (Set α)) (⋃ (b : β), g b) s
base :
  ∀ (b : β) (h_s_in_t' : Membership.mem (γ := Set (Set α)) ((fun (b : β) ↦ g b) b) s),
    ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
⊢ ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Tactic:
rcases h_s with ⟨t', ⟨⟨b, rfl⟩, h_s_in_t'⟩⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s : Set α
b : β
h_s_in_t' : Membership.mem (γ := Set (Set α)) ((fun (b : β) ↦ g b) b) s
⊢ ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Tactic:
⟨{b}, fun _ => s, ?_⟩

Premises used: Exists.intro, Singleton.singleton
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s : Set α
b : β
h_s_in_t' : Membership.mem (γ := Set (Set α)) ((fun (b : β) ↦ g b) b) s
base :
  s = ⋂ (b_1 : β), ⋂ (_ : Membership.mem (γ := Finset β) {b} b_1), (fun (x : β) ↦ s) b_1 ∧
    ∀ (b_1 : β), Membership.mem (γ := Finset β) {b} b_1 → (fun (x : β) ↦ s) b_1 ∈ g b_1
⊢ ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Tactic:
refine ⟨{b}, fun _ => s, ?_⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s : Set α
b : β
h_s_in_t' : Membership.mem (γ := Set (Set α)) ((fun (b : β) ↦ g b) b) s
⊢ s = ⋂ (b_1 : β), ⋂ (_ : Membership.mem (γ := Finset β) {b} b_1), (fun (x : β) ↦ s) b_1 ∧
    ∀ (b_1 : β), Membership.mem (γ := Finset β) {b} b_1 → (fun (x : β) ↦ s) b_1 ∈ g b_1

Tactic:
simpa using h_s_in_t'
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s t_1 : Set α
h_gen_s : generatePiSystem (⋃ (b : β), g b) s
h_gen_t' : generatePiSystem (⋃ (b : β), g b) t_1
h_nonempty : (s ∩ t_1).Nonempty
h_s : ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
h_t' : ∃ (T : Finset β) (f : β → Set α), t_1 = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
inter :
  ∀ (T_t' : Finset β) (f_t' : β → Set α) (h_t' : ∀ b ∈ T_t', f_t' b ∈ g b)
    (h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b))
    (h_nonempty : (s ∩ ⋂ b ∈ T_t', f_t' b).Nonempty),
    ∃ (T : Finset β) (f : β → Set α), s ∩ ⋂ b ∈ T_t', f_t' b = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
⊢ ∃ (T : Finset β) (f : β → Set α), s ∩ t_1 = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Tactic:
rcases h_t' with ⟨T_t', ⟨f_t', ⟨rfl, h_t'⟩⟩⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s : Set α
h_gen_s : generatePiSystem (⋃ (b : β), g b) s
h_s : ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
h_nonempty : (s ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
inter :
  ∀ (T_s : Finset β) (f_s : β → Set α) (h_s : ∀ b ∈ T_s, f_s b ∈ g b)
    (h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b))
    (h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)),
    ∃ (T : Finset β) (f : β → Set α),
      Eq.{u_3 + 1} (α := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b) (⋂ b ∈ T, f b) ∧ ∀ b ∈ T, f b ∈ g b
⊢ ∃ (T : Finset β) (f : β → Set α), s ∩ ⋂ b ∈ T_t', f_t' b = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Tactic:
rcases h_s with ⟨T_s, ⟨f_s, ⟨rfl, h_s⟩⟩⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
h :
  Eq.{u_3 + 1} (α := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
      (⋂ b ∈ T_s ∪ T_t',
        (fun (b : β) ↦ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
          b) ∧
    ∀ b ∈ T_s ∪ T_t',
      (fun (b : β) ↦ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) b ∈
        g b
⊢ ∃ (T : Finset β) (f : β → Set α),
    Eq.{u_3 + 1} (α := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b) (⋂ b ∈ T, f b) ∧ ∀ b ∈ T, f b ∈ g b

Tactic:
use T_s ∪ T_t', fun b : β =>
      if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b
      else if b ∈ T_t' then f_t' b else (∅ : Set α)

Premises used: Membership.mem, Inter.inter, EmptyCollection.emptyCollection, ite
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
h :
  Eq.{u_3 + 1} (α := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
    (⋂ b ∈ T_s ∪ T_t', if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
h₁ :
  ∀ b ∈ T_s ∪ T_t',
    (if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∈ g b
⊢ Eq.{u_3 + 1} (α := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
      (⋂ b ∈ T_s ∪ T_t',
        (fun (b : β) ↦ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
          b) ∧
    ∀ b ∈ T_s ∪ T_t',
      (fun (b : β) ↦ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) b ∈
        g b

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b) a ↔
      Membership.mem (γ := Set α)
        (⋂ b ∈ T_s ∪ T_t',
          if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
        a
⊢ Eq.{u_3 + 1} (α := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
    (⋂ b ∈ T_s ∪ T_t', if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)

Tactic:
ext a
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
a : α
h :
  ((∀ (i : β) (i_1 : i ∈ T_s), a ∈ f_s i) ∧ ∀ (i : β) (i_1 : i ∈ T_t'), a ∈ f_t' i) ↔
    ∀ (i : β) (i_1 : i ∈ T_s ∨ i ∈ T_t'),
      a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅
⊢ Membership.mem (γ := Set α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b) a ↔
    Membership.mem (γ := Set α)
      (⋂ b ∈ T_s ∪ T_t', if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
      a

Tactic:
simp_rw [Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union]

Premises used: Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
a : α
⊢ ((∀ (i : β) (i_1 : i ∈ T_s), a ∈ f_s i) ∧ ∀ (i : β) (i_1 : i ∈ T_t'), a ∈ f_t' i) ↔
    ∀ (i : β) (i_1 : i ∈ T_s ∨ i ∈ T_t'),
      a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅

Tactic:
grind
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
pos : ∀ (hbs : b ∈ T_s) (hbt : b ∈ T_t'), f_s b ∩ f_t' b ∈ g b
neg : ∀ (hbs : b ∈ T_s) (hbt : b ∉ T_t'), f_s b ∈ g b
pos₁ : ∀ (hbs : b ∉ T_s) (hbt : b ∈ T_t'), f_t' b ∈ g b
neg₁ : ∀ (hbs : b ∉ T_s) (hbt : b ∉ T_t'), ∅ ∈ g b
⊢ (if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∈ g b

Tactic:
split_ifs with hbs hbt hbt
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∈ T_s
hbt : b ∈ T_t'
⊢ f_s b ∩ f_t' b ∈ g b

Tactic:
h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono ?_ h_nonempty)

Premises used: Set.Nonempty.mono
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∈ T_s
hbt : b ∈ T_t'
pos : (⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b ⊆ f_s b ∩ f_t' b
⊢ f_s b ∩ f_t' b ∈ g b

Tactic:
refine h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono ?_ h_nonempty)

Premises used: Set.Nonempty.mono
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∈ T_s
hbt : b ∈ T_t'
⊢ (⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b ⊆ f_s b ∩ f_t' b

Tactic:
Set.inter_subset_inter (Set.biInter_subset_of_mem hbs) (Set.biInter_subset_of_mem hbt)

Premises used: Set.biInter_subset_of_mem, Set.inter_subset_inter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∈ T_s
hbt : b ∈ T_t'
⊢ (⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b ⊆ f_s b ∩ f_t' b

Tactic:
exact Set.inter_subset_inter (Set.biInter_subset_of_mem hbs) (Set.biInter_subset_of_mem hbt)

Premises used: Set.biInter_subset_of_mem, Set.inter_subset_inter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∈ T_s
hbt : b ∉ T_t'
⊢ f_s b ∈ g b

Tactic:
h_s b hbs
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∈ T_s
hbt : b ∉ T_t'
⊢ f_s b ∈ g b

Tactic:
exact h_s b hbs
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∉ T_s
hbt : b ∈ T_t'
⊢ f_t' b ∈ g b

Tactic:
h_t' b hbt
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∉ T_s
hbt : b ∈ T_t'
⊢ f_t' b ∈ g b

Tactic:
exact h_t' b hbt
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∉ T_s
hbt : b ∉ T_t'
⊢ b ∈ T_s ∨ b ∈ T_t'

Tactic:
rw [Finset.mem_union] at h_b

Premises used: Finset.mem_union
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∉ T_s
hbt : b ∉ T_t'
h_b₁ : b ∈ T_s ∨ b ∈ T_t'
⊢ b ∉ T_s

Tactic:
rw [Finset.mem_union] at h_b

Premises used: Finset.mem_union
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∉ T_s
hbt : b ∉ T_t'
h_b₁ : b ∈ T_s ∨ b ∈ T_t'
hbs₁ : b ∉ T_s
⊢ b ∉ T_t'

Tactic:
rw [Finset.mem_union] at h_b

Premises used: Finset.mem_union
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem.{u_3} (α := α) (⋃ (b : β), g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : Set.Nonempty.{u_3} (α := α) ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b)
b : β
h_b : b ∈ T_s ∨ b ∈ T_t'
hbs : b ∉ T_s
hbt : b ∉ T_t'
⊢ ∅ ∈ g b

Tactic:
apply False.elim (h_b.elim hbs hbt)

Premises used: False.elim, Or.elim
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
h_t : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : β), g b)) t
base :
  ∀ {s : Set α} (h_s : Membership.mem (γ := Set (Set α)) (⋃ (b : β), g b) s),
    ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
inter :
  ∀ {s t : Set α} (h_gen_s : generatePiSystem (⋃ (b : β), g b) s) (h_gen_t' : generatePiSystem (⋃ (b : β), g b) t)
    (h_nonempty : (s ∩ t).Nonempty) (h_s : ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b)
    (h_t' : ∃ (T : Finset β) (f : β → Set α), t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b),
    ∃ (T : Finset β) (f : β → Set α), s ∩ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
⊢ ∃ (T : Finset β) (f : β → Set α), t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Tactic:
induction h_t with
  | @base s h_s =>
    rcases h_s with ⟨t', ⟨⟨b, rfl⟩, h_s_in_t'⟩⟩
    refine ⟨{b}, fun _ => s, ?_⟩
    simpa using h_s_in_t'
  | inter h_gen_s h_gen_t' h_nonempty h_s h_t' =>
    rcases h_t' with ⟨T_t', ⟨f_t', ⟨rfl, h_t'⟩⟩⟩
    rcases h_s with ⟨T_s, ⟨f_s, ⟨rfl, h_s⟩⟩⟩
    use T_s ∪ T_t', fun b : β =>
      if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b
      else if b ∈ T_t' then f_t' b else (∅ : Set α)
    constructor
    · ext a
      simp_rw [Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union]
      grind
    intro b h_b
    split_ifs with hbs hbt hbt
    · refine h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono ?_ h_nonempty)
      exact Set.inter_subset_inter (Set.biInter_subset_of_mem hbs) (Set.biInter_subset_of_mem hbt)
    · exact h_s b hbs
    · exact h_t' b hbt
    · rw [Finset.mem_union] at h_b
      apply False.elim (h_b.elim hbs hbt)

Premises used: Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union, rfl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
h_t : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : β), g b)) t
base :
  ∀ {s : Set α} (h_s : Membership.mem (γ := Set (Set α)) (⋃ (b : β), g b) s),
    ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
inter :
  ∀ {s t : Set α} (h_gen_s : generatePiSystem (⋃ (b : β), g b) s) (h_gen_t' : generatePiSystem (⋃ (b : β), g b) t)
    (h_nonempty : (s ∩ t).Nonempty) (h_s : ∃ (T : Finset β) (f : β → Set α), s = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b)
    (h_t' : ∃ (T : Finset β) (f : β → Set α), t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b),
    ∃ (T : Finset β) (f : β → Set α), s ∩ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
⊢ ∃ (T : Finset β) (f : β → Set α), t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Tactic:
classical
  induction h_t with
  | @base s h_s =>
    rcases h_s with ⟨t', ⟨⟨b, rfl⟩, h_s_in_t'⟩⟩
    refine ⟨{b}, fun _ => s, ?_⟩
    simpa using h_s_in_t'
  | inter h_gen_s h_gen_t' h_nonempty h_s h_t' =>
    rcases h_t' with ⟨T_t', ⟨f_t', ⟨rfl, h_t'⟩⟩⟩
    rcases h_s with ⟨T_s, ⟨f_s, ⟨rfl, h_s⟩⟩⟩
    use T_s ∪ T_t', fun b : β =>
      if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b
      else if b ∈ T_t' then f_t' b else (∅ : Set α)
    constructor
    · ext a
      simp_rw [Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union]
      grind
    intro b h_b
    split_ifs with hbs hbt hbt
    · refine h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono ?_ h_nonempty)
      exact Set.inter_subset_inter (Set.biInter_subset_of_mem hbs) (Set.biInter_subset_of_mem hbt)
    · exact h_s b hbs
    · exact h_t' b hbt
    · rw [Finset.mem_union] at h_b
      apply False.elim (h_b.elim hbs hbt)

Premises used: Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union, rfl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
t : Set α
h_t : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ b ∈ s, g b)) t
h1 : Eq.{u_3 + 1} (α := Set (Set α)) (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b) (⋃ b ∈ s, g b)
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ b ∈ s, g b)) t
⊢ Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b)) t

Tactic:
rwa [h1]