awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i

Tactic:
have h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i := by
    rw [ht1_eq, ht2_eq]
    simp_rw [← Set.inf_eq_inter]
    ext1 x
    simp only [inf_eq_inter, mem_inter_iff, mem_iInter]
    grind
-- 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_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
⊢ ∃ (_ : ∀ x ∈ p1 ∪ p2, g x ∈ π x), t1 ∩ t2 = ⋂ x ∈ p1 ∪ p2, g x

Tactic:
⟨fun n hn => ?_, h_inter_eq⟩

Premises used: Exists.intro
-- 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_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
h : ∀ (n : ι) (hn : n ∈ p1 ∪ p2), g n ∈ π n
⊢ ∃ (_ : ∀ x ∈ p1 ∪ p2, g x ∈ π x), t1 ∩ t2 = ⋂ x ∈ p1 ∪ p2, g x

Tactic:
refine ⟨fun n hn => ?_, h_inter_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_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
h : ((if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ) ∈ π n
⊢ g n ∈ π n

Tactic:
simp only [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
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
pos : ∀ (hn1 : n ∈ p1) (hn2 : n ∈ p2), f1 n ∩ f2 n ∈ π n
neg : ∀ (hn1 : n ∈ p1) (hn2 : n ∉ p2), f1 n ∩ univ ∈ π n
pos₁ : ∀ (hn1 : n ∉ p1) (h : n ∈ p2), univ ∩ f2 n ∈ π n
neg₁ : ∀ (hn1 : n ∉ p1) (h : n ∉ p2), univ ∩ univ ∈ π n
⊢ ((if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ) ∈ π n

Tactic:
split_ifs with hn1 hn2 h
-- 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_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
⊢ f1 n ∩ f2 n ∈ π n

Tactic:
hpi n (f1 n) (hf1m n hn1) (f2 n) (hf2m n hn2) (Set.nonempty_iff_ne_empty.2 fun h => ?_)

Premises used: Iff.mpr, Set.nonempty_iff_ne_empty
-- 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_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
pos : ∀ (h : f1 n ∩ f2 n = ∅), False
⊢ f1 n ∩ f2 n ∈ π n

Tactic:
refine hpi n (f1 n) (hf1m n hn1) (f2 n) (hf2m n hn2) (Set.nonempty_iff_ne_empty.2 fun h => ?_)

Premises used: Iff.mpr, Set.nonempty_iff_ne_empty
-- 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_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
pos :
  ∀ (h_nonempty : Set.Nonempty.{u_3} (α := α) (⋂ i ∈ p1 ∪ p2, g i)) (hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S)
    (h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i) (n : ι) (hn : n ∈ p1 ∪ p2) (hn1 : n ∈ p1) (hn2 : n ∈ p2)
    (h : f1 n ∩ f2 n = ∅), False
⊢ False

Tactic:
rw [h_inter_eq] at h_nonempty
-- 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
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : Set.Nonempty.{u_3} (α := α) (⋂ i ∈ p1 ∪ p2, g i)
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
pos : Eq.{u_3 + 1} (α := Set α) (⋂ i ∈ p1 ∪ p2, g i) ∅
⊢ False

Tactic:
suffices h_empty : ⋂ i ∈ p1 ∪ p2, g i = ∅ from
      (Set.not_nonempty_iff_eq_empty.mpr h_empty) h_nonempty
-- 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
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : Set.Nonempty.{u_3} (α := α) (⋂ i ∈ p1 ∪ p2, g i)
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ Eq.{u_3 + 1} (α := Set α) (⋂ i ∈ p1 ∪ p2, g i) ∅

Tactic:
le_antisymm (Set.iInter_subset_of_subset n ?_) (Set.empty_subset _)

Premises used: le_antisymm, Set.iInter_subset_of_subset, Set.empty_subset
-- 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
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : Set.Nonempty.{u_3} (α := α) (⋂ i ∈ p1 ∪ p2, g i)
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
pos : Subset.{u_3} (α := Set α) (⋂ (_ : n ∈ p1 ∪ p2), g n) ∅
⊢ Eq.{u_3 + 1} (α := Set α) (⋂ i ∈ p1 ∪ p2, g i) ∅

Tactic:
refine le_antisymm (Set.iInter_subset_of_subset n ?_) (Set.empty_subset _)

Premises used: le_antisymm, Set.iInter_subset_of_subset, Set.empty_subset
-- 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
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : Set.Nonempty.{u_3} (α := α) (⋂ i ∈ p1 ∪ p2, g i)
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ Subset.{u_3} (α := Set α) (⋂ (_ : n ∈ p1 ∪ p2), g n) ∅

Tactic:
Set.iInter_subset_of_subset hn ?_

Premises used: Set.iInter_subset_of_subset
-- 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
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : Set.Nonempty.{u_3} (α := α) (⋂ i ∈ p1 ∪ p2, g i)
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
pos : g n ⊆ ∅
⊢ Subset.{u_3} (α := Set α) (⋂ (_ : n ∈ p1 ∪ p2), g n) ∅

Tactic:
refine Set.iInter_subset_of_subset hn ?_

Premises used: Set.iInter_subset_of_subset
-- 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
g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : Set.Nonempty.{u_3} (α := α) (⋂ i ∈ p1 ∪ p2, g i)
hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ g n ⊆ ∅

Tactic:
grind
-- 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_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∉ p2
⊢ f1 n ∩ univ ∈ π n

Tactic:
simp [hf1m n hn1]
-- 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_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∈ p2
⊢ univ ∩ f2 n ∈ π n

Tactic:
simp [hf2m n h]
-- 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_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∉ p2
⊢ n ∉ p1 ∪ p2

Tactic:
simp [hn1, h]
-- 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_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∉ p2
⊢ univ ∩ univ ∈ π n

Tactic:
exact absurd hn (by simp [hn1, h])

Premises used: absurd
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π π' : ι → Set (Set α)
h_le : ∀ (i : ι), π i ⊆ π' i
S : Set ι
⊢ piiUnionInter π S ⊆ piiUnionInter π' S

Tactic:
fun _ ⟨t, ht_mem, ft, hft_mem_pi, h_eq⟩ =>
  ⟨t, ht_mem, ft, fun x hxt => h_le x (hft_mem_pi x hxt), h_eq⟩

Premises used: piiUnionInter, Membership.mem, _private.0.piiUnionInter_mono_left.match_1, Set.Subset, Exists.intro
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S T : Set ι
hST : S ⊆ T
⊢ piiUnionInter π S ⊆ piiUnionInter π T

Tactic:
fun _ ⟨t, ht_mem, ft, hft_mem_pi, h_eq⟩ =>
  ⟨t, ht_mem.trans hST, ft, hft_mem_pi, h_eq⟩

Premises used: piiUnionInter, Membership.mem, _private.0.piiUnionInter_mono_left.match_1, HasSubset.Subset.trans, Set.Subset, Exists.intro
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
⊢ generateFrom (piiUnionInter π S) ≤ m

Tactic:
generateFrom_le ?_

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
refine : ∀ t ∈ piiUnionInter π S, MeasurableSet t
⊢ generateFrom (piiUnionInter π S) ≤ m

Tactic:
refine generateFrom_le ?_

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
ht_p : Finset ι
w : (↑ht_p : Set ι) ⊆ S
ft : ι → Set α
hft_mem_pi : ∀ x ∈ ht_p, ft x ∈ π x
⊢ MeasurableSet.{u_3} (α := α) (⋂ x ∈ ht_p, ft x)

Tactic:
Finset.measurableSet_biInter _ fun x hx_mem => (h x) _ ?_

Premises used: Finset.measurableSet_biInter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
ht_p : Finset ι
w : (↑ht_p : Set ι) ⊆ S
ft : ι → Set α
hft_mem_pi : ∀ x ∈ ht_p, ft x ∈ π x
refine : ∀ (x : ι) (hx_mem : x ∈ ht_p), MeasurableSet (ft x)
⊢ MeasurableSet.{u_3} (α := α) (⋂ x ∈ ht_p, ft x)

Tactic:
refine Finset.measurableSet_biInter _ fun x hx_mem => (h x) _ ?_

Premises used: Finset.measurableSet_biInter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
ht_p : Finset ι
w : (↑ht_p : Set ι) ⊆ S
ft : ι → Set α
hft_mem_pi : ∀ x ∈ ht_p, ft x ∈ π x
x : ι
hx_mem : x ∈ ht_p
⊢ MeasurableSet (ft x)

Tactic:
measurableSet_generateFrom (hft_mem_pi x hx_mem)

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
ht_p : Finset ι
w : (↑ht_p : Set ι) ⊆ S
ft : ι → Set α
hft_mem_pi : ∀ x ∈ ht_p, ft x ∈ π x
x : ι
hx_mem : x ∈ ht_p
⊢ MeasurableSet (ft x)

Tactic:
exact measurableSet_generateFrom (hft_mem_pi x hx_mem)

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
j : ι
hj : Membership.mem (γ := Set ι) {i} j
⊢ j = i

Tactic:
rw [mem_singleton_iff] at hj

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
j : ι
hj : j = i
rwa rwa₁ rwa₂ rwa₃ : i ∈ S
⊢ j ∈ S

Tactic:
rwa [hj]
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
⊢ {i} ⊆ S

Tactic:
have h_ss : {i} ⊆ S := by
    intro j hj
    rw [mem_singleton_iff] at hj
    rwa [hj]
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π S

Tactic:
Subset.trans ?_ (piiUnionInter_mono_right h_ss)

Premises used: Set.Subset.trans, piiUnionInter_mono_right
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
refine : π i ⊆ piiUnionInter π {i}
⊢ π i ⊆ piiUnionInter π S

Tactic:
refine Subset.trans ?_ (piiUnionInter_mono_right h_ss)

Premises used: Set.Subset.trans, piiUnionInter_mono_right
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
rw : π i ⊆ π i ∪ {univ}
⊢ π i ⊆ piiUnionInter π {i}

Tactic:
rw [piiUnionInter_singleton]

Premises used: piiUnionInter_singleton
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ π i ∪ {univ}

Tactic:
subset_union_left

Premises used: Set.subset_union_left
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ π i ∪ {univ}

Tactic:
exact subset_union_left

Premises used: Set.subset_union_left
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
i : ι
hiS : i ∈ S
s : Set α
hs : MeasurableSet s
⊢ Membership.mem (γ := Set (Set α)) (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S) s

Tactic:
subset_piiUnionInter hiS hs

Premises used: subset_piiUnionInter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
x : ι
hxS : x ∈ S
⊢ generateFrom (π x) ≤ generateFrom (piiUnionInter π S)

Tactic:
generateFrom_mono (subset_piiUnionInter hxS)

Premises used: MeasurableSpace.generateFrom_mono, subset_piiUnionInter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
t : Set α
ht : Membership.mem (γ := Set (Set α)) (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S) t
rcases :
  ∀ (pt : Finset ι) (hpt : (↑pt : Set ι) ⊆ S) (ft : ι → Set α)
    (ht_m :
      ∀ x ∈ pt,
        Membership.mem (γ := Set (Set α)) ((fun (n : ι) ↦ ({s : Set α | MeasurableSet s} : Set (Set α))) x) (ft x)),
    MeasurableSet.{u_3} (α := α) (⋂ x ∈ pt, ft x)
⊢ MeasurableSet t

Tactic:
rcases ht with ⟨pt, hpt, ft, ht_m, rfl⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : (↑pt : Set ι) ⊆ S
ft : ι → Set α
ht_m :
  ∀ x ∈ pt, Membership.mem (γ := Set (Set α)) ((fun (n : ι) ↦ ({s : Set α | MeasurableSet s} : Set (Set α))) x) (ft x)
⊢ MeasurableSet.{u_3} (α := α) (⋂ x ∈ pt, ft x)

Tactic:
pt.measurableSet_biInter fun i hi => ?_

Premises used: Finset.measurableSet_biInter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : (↑pt : Set ι) ⊆ S
ft : ι → Set α
ht_m :
  ∀ x ∈ pt, Membership.mem (γ := Set (Set α)) ((fun (n : ι) ↦ ({s : Set α | MeasurableSet s} : Set (Set α))) x) (ft x)
refine : ∀ (i : ι) (hi : i ∈ pt), MeasurableSet (ft i)
⊢ MeasurableSet.{u_3} (α := α) (⋂ x ∈ pt, ft x)

Tactic:
refine pt.measurableSet_biInter fun i hi => ?_

Premises used: Finset.measurableSet_biInter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : (↑pt : Set ι) ⊆ S
ft : ι → Set α
ht_m :
  ∀ x ∈ pt, Membership.mem (γ := Set (Set α)) ((fun (n : ι) ↦ ({s : Set α | MeasurableSet s} : Set (Set α))) x) (ft x)
i : ι
hi : i ∈ pt
suffices : m i ≤ ⨆ i ∈ S, m i
⊢ MeasurableSet (ft i)

Tactic:
suffices h_le : m i ≤ ⨆ i ∈ S, m i from h_le (ft i) (ht_m i hi)
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : (↑pt : Set ι) ⊆ S
ft : ι → Set α
ht_m :
  ∀ x ∈ pt, Membership.mem (γ := Set (Set α)) ((fun (n : ι) ↦ ({s : Set α | MeasurableSet s} : Set (Set α))) x) (ft x)
i : ι
hi : i ∈ pt
⊢ i ∈ S

Tactic:
have hi' : i ∈ S := hpt hi
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : (↑pt : Set ι) ⊆ S
ft : ι → Set α
ht_m :
  ∀ x ∈ pt, Membership.mem (γ := Set (Set α)) ((fun (n : ι) ↦ ({s : Set α | MeasurableSet s} : Set (Set α))) x) (ft x)
i : ι
hi : i ∈ pt
hi' : i ∈ S
⊢ m i ≤ ⨆ i ∈ S, m i

Tactic:
le_iSup₂ (f := fun i (_ : i ∈ S) => m i) i hi'

Premises used: le_iSup₂
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : (↑pt : Set ι) ⊆ S
ft : ι → Set α
ht_m :
  ∀ x ∈ pt, Membership.mem (γ := Set (Set α)) ((fun (n : ι) ↦ ({s : Set α | MeasurableSet s} : Set (Set α))) x) (ft x)
i : ι
hi : i ∈ pt
hi' : i ∈ S
⊢ m i ≤ ⨆ i ∈ S, m i

Tactic:
exact le_iSup₂ (f := fun i (_ : i ∈ S) => m i) i hi'

Premises used: le_iSup₂
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ Eq.{u_3 + 1} (α := MeasurableSpace α) (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))
    (⨆ i ∈ S, m i)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
refine_1 :
  LE.le.{u_3} (α := MeasurableSpace α) (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))
    (⨆ i ∈ S, m i)
refine_2 :
  LE.le.{u_3} (α := MeasurableSpace α) (⨆ i ∈ S, m i)
    (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))
⊢ Eq.{u_3 + 1} (α := MeasurableSpace α) (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))
    (⨆ i ∈ S, m i)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm