awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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
⊢ ((if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ) ∈ π n
have neg : ∀ (hn1 : n ∈ p1) (hn2 : n ∉ p2), f1 n ∩ univ ∈ π n
Tactic: split_ifs with hn1 hn2 h
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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
⊢ ((if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ) ∈ π n
have pos₁ : ∀ (hn1 : n ∉ p1) (h : n ∈ p2), univ ∩ f2 n ∈ π n
Tactic: split_ifs with hn1 hn2 h
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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
⊢ ((if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ) ∈ π n
have neg₁ : ∀ (hn1 : n ∉ p1) (h : n ∉ p2), univ ∩ univ ∈ π n
Tactic: split_ifs with hn1 hn2 h
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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
have pos : ∀ (h : f1 n ∩ f2 n = ∅), False
Tactic: refine hpi n (f1 n) (hf1m n hn1) (f2 n) (hf2m n hn2) (Set.nonempty_iff_ne_empty.2 fun h => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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 = ∅
⊢ False
have 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
Tactic: rw [h_inter_eq] at h_nonempty
Cleared hypotheses: h_nonempty, hp_union_ss, h_inter_eq, n, hn, hn1, hn2, h
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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 = ∅
⊢ False
have pos : Eq.{u_3 + 1} (α := Set α) (⋂ i ∈ p1 ∪ p2, g i) ∅
Tactic: suffices h_empty : ⋂ i ∈ p1 ∪ p2, g i = ∅ from
      (Set.not_nonempty_iff_eq_empty.mpr h_empty) h_nonempty
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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) ∅
have pos : Subset.{u_3} (α := Set α) (⋂ (_ : n ∈ p1 ∪ p2), g n) ∅
Tactic: refine le_antisymm (Set.iInter_subset_of_subset n ?_) (Set.empty_subset _)
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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) ∅
have pos : g n ⊆ ∅
Tactic: refine Set.iInter_subset_of_subset hn ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
⊢ IsPiSystem (piiUnionInter π S)
have rintro : ∀ (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),
  t1 ∩ t2 ∈ piiUnionInter π S
Tactic: classical
  rintro t1 ⟨p1, hp1S, f1, hf1m, ht1_eq⟩ t2 ⟨p2, hp2S, f2, hf2m, ht2_eq⟩ h_nonempty
  simp_rw [piiUnionInter, Set.mem_setOf_eq]
  let g n := ite (n ∈ p1) (f1 n) Set.univ ∩ ite (n ∈ p2) (f2 n) Set.univ
  have hp_union_ss : ↑(p1 ∪ p2) ⊆ S := by
    simp only [hp1S, hp2S, Finset.coe_union, union_subset_iff, and_self_iff]
  use p1 ∪ p2, hp_union_ss, g
  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
  refine ⟨fun n hn => ?_, h_inter_eq⟩
  simp only [g]
  split_ifs with hn1 hn2 h
  · refine hpi n (f1 n) (hf1m n hn1) (f2 n) (hf2m n hn2) (Set.nonempty_iff_ne_empty.2 fun h => ?_)
    rw [h_inter_eq] at h_nonempty
    suffices h_empty : ⋂ i ∈ p1 ∪ p2, g i = ∅ from
      (Set.not_nonempty_iff_eq_empty.mpr h_empty) h_nonempty
    refine le_antisymm (Set.iInter_subset_of_subset n ?_) (Set.empty_subset _)
    refine Set.iInter_subset_of_subset hn ?_
    grind
  · simp [hf1m n hn1]
  · simp [hf2m n h]
  · exact absurd hn (by simp [hn1, h])
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
rintro :
  ∀ (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),
    t1 ∩ t2 ∈ piiUnionInter π S
⊢ IsPiSystem (piiUnionInter π S)
have rintro₁ : ∀ (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),
  ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S) (f : ι → Set α) (_ : ∀ x ∈ t, f x ∈ π x), t1 ∩ t2 = ⋂ x ∈ t, f x
Tactic: classical
  rintro t1 ⟨p1, hp1S, f1, hf1m, ht1_eq⟩ t2 ⟨p2, hp2S, f2, hf2m, ht2_eq⟩ h_nonempty
  simp_rw [piiUnionInter, Set.mem_setOf_eq]
  let g n := ite (n ∈ p1) (f1 n) Set.univ ∩ ite (n ∈ p2) (f2 n) Set.univ
  have hp_union_ss : ↑(p1 ∪ p2) ⊆ S := by
    simp only [hp1S, hp2S, Finset.coe_union, union_subset_iff, and_self_iff]
  use p1 ∪ p2, hp_union_ss, g
  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
  refine ⟨fun n hn => ?_, h_inter_eq⟩
  simp only [g]
  split_ifs with hn1 hn2 h
  · refine hpi n (f1 n) (hf1m n hn1) (f2 n) (hf2m n hn2) (Set.nonempty_iff_ne_empty.2 fun h => ?_)
    rw [h_inter_eq] at h_nonempty
    suffices h_empty : ⋂ i ∈ p1 ∪ p2, g i = ∅ from
      (Set.not_nonempty_iff_eq_empty.mpr h_empty) h_nonempty
    refine le_antisymm (Set.iInter_subset_of_subset n ?_) (Set.empty_subset _)
    refine Set.iInter_subset_of_subset hn ?_
    grind
  · simp [hf1m n hn1]
  · simp [hf2m n h]
  · exact absurd hn (by simp [hn1, h])
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
rintro :
  ∀ (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),
    t1 ∩ t2 ∈ piiUnionInter π S
rintro₁ :
  ∀ (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),
    ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S) (f : ι → Set α) (_ : ∀ x ∈ t, f x ∈ π x), t1 ∩ t2 = ⋂ x ∈ t, f x
rintro₂ :
  ∀ (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),
    ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S) (f : ι → Set α) (_ : ∀ x ∈ t, f x ∈ π x), t1 ∩ t2 = ⋂ x ∈ t, f x
⊢ IsPiSystem (piiUnionInter π S)
have rintro₃ : ∀ (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)
  (hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S),
  ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S) (f : ι → Set α) (_ : ∀ x ∈ t, f x ∈ π x), t1 ∩ t2 = ⋂ x ∈ t, f x
Tactic: classical
  rintro t1 ⟨p1, hp1S, f1, hf1m, ht1_eq⟩ t2 ⟨p2, hp2S, f2, hf2m, ht2_eq⟩ h_nonempty
  simp_rw [piiUnionInter, Set.mem_setOf_eq]
  let g n := ite (n ∈ p1) (f1 n) Set.univ ∩ ite (n ∈ p2) (f2 n) Set.univ
  have hp_union_ss : ↑(p1 ∪ p2) ⊆ S := by
    simp only [hp1S, hp2S, Finset.coe_union, union_subset_iff, and_self_iff]
  use p1 ∪ p2, hp_union_ss, g
  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
  refine ⟨fun n hn => ?_, h_inter_eq⟩
  simp only [g]
  split_ifs with hn1 hn2 h
  · refine hpi n (f1 n) (hf1m n hn1) (f2 n) (hf2m n hn2) (Set.nonempty_iff_ne_empty.2 fun h => ?_)
    rw [h_inter_eq] at h_nonempty
    suffices h_empty : ⋂ i ∈ p1 ∪ p2, g i = ∅ from
      (Set.not_nonempty_iff_eq_empty.mpr h_empty) h_nonempty
    refine le_antisymm (Set.iInter_subset_of_subset n ?_) (Set.empty_subset _)
    refine Set.iInter_subset_of_subset hn ?_
    grind
  · simp [hf1m n hn1]
  · simp [hf2m n h]
  · exact absurd hn (by simp [hn1, h])
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
⊢ generateFrom (piiUnionInter π S) ≤ m
have refine : ∀ t ∈ piiUnionInter π S, MeasurableSet t
Tactic: refine generateFrom_le ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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)
have refine : ∀ (x : ι) (hx_mem : x ∈ ht_p), MeasurableSet (ft x)
Tactic: refine Finset.measurableSet_biInter _ fun x hx_mem => (h x) _ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
j : ι
hj : Membership.mem (γ := Set ι) {i} j
⊢ j ∈ S
have hj₁ : j = i
Tactic: rw [mem_singleton_iff] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
⊢ π i ⊆ piiUnionInter π S
have h_ss : {i} ⊆ S
Tactic: have h_ss : {i} ⊆ S := by
    intro j hj
    rw [mem_singleton_iff] at hj
    rwa [hj]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π S
have refine : π i ⊆ piiUnionInter π {i}
Tactic: refine Subset.trans ?_ (piiUnionInter_mono_right h_ss)
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π {i}
have rw : π i ⊆ π i ∪ {univ}
Tactic: rw [piiUnionInter_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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
⊢ MeasurableSet t
have 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)
Tactic: rcases ht with ⟨pt, hpt, ft, ht_m, rfl⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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)
have refine : ∀ (i : ι) (hi : i ∈ pt), MeasurableSet (ft i)
Tactic: refine pt.measurableSet_biInter fun i hi => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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
⊢ MeasurableSet (ft i)
have suffices : m i ≤ ⨆ i ∈ S, m i
Tactic: suffices h_le : m i ≤ ⨆ i ∈ S, m i from h_le (ft i) (ht_m i hi)
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
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
⊢ m i ≤ ⨆ i ∈ S, m i
have hi' : i ∈ S
Tactic: have hi' : i ∈ S := hpt hi
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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)
have refine_1 : LE.le.{u_3} (α := MeasurableSpace α) (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))
  (⨆ i ∈ S, m i)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
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)
⊢ Eq.{u_3 + 1} (α := MeasurableSpace α) (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))
    (⨆ i ∈ S, m i)
have refine_2 : LE.le.{u_3} (α := MeasurableSpace α) (⨆ i ∈ S, m i)
  (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ LE.le.{u_3} (α := MeasurableSpace α) (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))
    (⨆ i ∈ S, m i)
have refine_1 : LE.le.{u_3} (α := MeasurableSpace α) (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))
  (generateFrom {s : Set α | MeasurableSet s})
Tactic: rw [← @generateFrom_measurableSet α (⨆ i ∈ S, m i)]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ LE.le.{u_3} (α := MeasurableSpace α) (⨆ i ∈ S, m i)
    (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))
have refine_2 : ∀ (i : ι) (hi : i ∈ S), m i ≤ generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S)
Tactic: refine iSup₂_le fun i hi => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
⊢ m i ≤ generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S)
have refine_2 : LE.le.{u_3} (α := MeasurableSpace α) (generateFrom {s : Set α | MeasurableSet s})
  (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))
Tactic: rw [← @generateFrom_measurableSet α (m i)]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
Goal:
α : Type u_3
s₁ : Set α → Prop
has_empty : s₁ ∅
has_compl : ∀ {a : Set α}, s₁ a → s₁ aᶜ
has_iUnion_nat : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₁ (f i)) → s₁ (⋃ (i : ℕ), f i)
s₂ : Set α → Prop
has_empty_1 : s₂ ∅
has_compl_1 : ∀ {a : Set α}, s₂ a → s₂ aᶜ
has_iUnion_nat_1 : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₂ (f i)) → s₂ (⋃ (i : ℕ), f i)
h :
  ∀ (s : Set α),
    { Has := s₁, has_empty := has_empty, has_compl := @has_compl, has_iUnion_nat := @has_iUnion_nat :
            DynkinSystem α }.Has
        s ↔
      { Has := s₂, has_empty := has_empty_1, has_compl := @has_compl_1, has_iUnion_nat := @has_iUnion_nat_1 :
            DynkinSystem α }.Has
        s
⊢ { Has := s₁, has_empty := has_empty, has_compl := @has_compl, has_iUnion_nat := @has_iUnion_nat : DynkinSystem α } =
    { Has := s₂, has_empty := has_empty_1, has_compl := @has_compl_1, has_iUnion_nat := @has_iUnion_nat_1 }
have this : s₁ = s₂
Tactic: have : s₁ = s₂ := funext fun x => propext <| h x
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
s₁ : Set α → Prop
has_empty : s₁ ∅
has_compl : ∀ {a : Set α}, s₁ a → s₁ aᶜ
has_iUnion_nat : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₁ (f i)) → s₁ (⋃ (i : ℕ), f i)
s₂ : Set α → Prop
has_empty_1 : s₂ ∅
has_compl_1 : ∀ {a : Set α}, s₂ a → s₂ aᶜ
has_iUnion_nat_1 : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₂ (f i)) → s₂ (⋃ (i : ℕ), f i)
h :
  ∀ (s : Set α),
    { Has := s₁, has_empty := has_empty, has_compl := @has_compl, has_iUnion_nat := @has_iUnion_nat :
            DynkinSystem α }.Has
        s ↔
      { Has := s₂, has_empty := has_empty_1, has_compl := @has_compl_1, has_iUnion_nat := @has_iUnion_nat_1 :
            DynkinSystem α }.Has
        s
this : s₁ = s₂
⊢ { Has := s₁, has_empty := has_empty, has_compl := @has_compl, has_iUnion_nat := @has_iUnion_nat : DynkinSystem α } =
    { Has := s₂, has_empty := has_empty_1, has_compl := @has_compl_1, has_iUnion_nat := @has_iUnion_nat_1 }
have subst : ∀ (has_empty_2 : s₁ ∅) (has_compl_2 : ∀ {a : Set α}, s₁ a → s₁ aᶜ)
  (has_iUnion_nat_2 : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₁ (f i)) → s₁ (⋃ (i : ℕ), f i))
  (h :
    ∀ (s : Set α),
      { Has := s₁, has_empty := has_empty, has_compl := @has_compl, has_iUnion_nat := @has_iUnion_nat :
              DynkinSystem α }.Has
          s ↔
        { Has := s₁, has_empty := has_empty_2, has_compl := @has_compl_2, has_iUnion_nat := @has_iUnion_nat_2 :
              DynkinSystem α }.Has
          s),
  { Has := s₁, has_empty := has_empty, has_compl := @has_compl, has_iUnion_nat := @has_iUnion_nat : DynkinSystem α } =
    { Has := s₁, has_empty := has_empty_2, has_compl := @has_compl_2, has_iUnion_nat := @has_iUnion_nat_2 }
Tactic: subst this
Cleared hypotheses: s₂, has_empty_1, has_compl_1, has_iUnion_nat_1, h, this
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
d : DynkinSystem α
β : Type u_4
inst : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
h : ∀ (i : β), d.Has (f i)
⊢ d.Has (⋃ (i : β), f i)
have intro : ∀ (val : Encodable β), d.Has (⋃ (i : β), f i)
Tactic: cases nonempty_encodable β
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
d : DynkinSystem α
β : Type u_4
inst : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
h : ∀ (i : β), d.Has (f i)
val : Encodable β
⊢ d.Has (⋃ (i : β), f i)
have intro : d.Has (⋃ (i : ℕ), ⋃ b ∈ Encodable.decode₂ β i, f b)
Tactic: rw [← Encodable.iUnion_decode₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : Disjoint s₁ s₂
⊢ d.Has (s₁ ∪ s₂)
have rw : d.Has (⋃ (b : Bool), bif b then s₁ else s₂)
Tactic: rw [union_eq_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
⊢ d.Has (s₁ \ s₂)
have apply : d.Has (s₁ \ s₂)ᶜ
Tactic: apply d.has_compl_iff.1