awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
    (generateFrom {s : Set α | MeasurableSet s})
⊢ LE.le.{u_3} (α := MeasurableSpace α) (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))
    (⨆ i ∈ S, m i)

Tactic:
rw [← @generateFrom_measurableSet α (⨆ i ∈ S, m i)]

Premises used: MeasurableSpace.generateFrom_measurableSet
-- Module: Mathlib.MeasureTheory.PiSystem
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))
    (generateFrom {s : Set α | MeasurableSet s})

Tactic:
generateFrom_mono (measurableSet_iSup_of_mem_piiUnionInter m S)

Premises used: MeasurableSpace.generateFrom_mono, measurableSet_iSup_of_mem_piiUnionInter
-- Module: Mathlib.MeasureTheory.PiSystem
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))
    (generateFrom {s : Set α | MeasurableSet s})

Tactic:
exact generateFrom_mono (measurableSet_iSup_of_mem_piiUnionInter m S)

Premises used: MeasurableSpace.generateFrom_mono, measurableSet_iSup_of_mem_piiUnionInter
-- Module: Mathlib.MeasureTheory.PiSystem
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))

Tactic:
iSup₂_le fun i hi => ?_

Premises used: iSup₂_le
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
refine_2 : ∀ (i : ι) (hi : i ∈ S), m i ≤ generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S)
⊢ LE.le.{u_3} (α := MeasurableSpace α) (⨆ i ∈ S, m i)
    (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))

Tactic:
refine iSup₂_le fun i hi => ?_

Premises used: iSup₂_le
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
refine_2 :
  LE.le.{u_3} (α := MeasurableSpace α) (generateFrom {s : Set α | MeasurableSet s})
    (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))
⊢ m i ≤ generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S)

Tactic:
rw [← @generateFrom_measurableSet α (m i)]

Premises used: MeasurableSpace.generateFrom_measurableSet
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
⊢ LE.le.{u_3} (α := MeasurableSpace α) (generateFrom {s : Set α | MeasurableSet s})
    (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))

Tactic:
generateFrom_mono (mem_piiUnionInter_of_measurableSet m hi)

Premises used: MeasurableSpace.generateFrom_mono, mem_piiUnionInter_of_measurableSet
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
⊢ LE.le.{u_3} (α := MeasurableSpace α) (generateFrom {s : Set α | MeasurableSet s})
    (generateFrom (piiUnionInter (fun (n : ι) ↦ {s : Set α | MeasurableSet s}) S))

Tactic:
exact generateFrom_mono (mem_piiUnionInter_of_measurableSet m hi)

Premises used: MeasurableSpace.generateFrom_mono, mem_piiUnionInter_of_measurableSet
-- Module: Mathlib.MeasureTheory.PiSystem
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
⊢ s₁ = s₂

Tactic:
have : s₁ = s₂ := funext fun x => propext <| h x
-- Module: Mathlib.MeasureTheory.PiSystem
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₂
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 }
⊢ { 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 }

Tactic:
subst this
-- Module: Mathlib.MeasureTheory.PiSystem
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)
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 }

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
d : DynkinSystem α
a : Set α
h : d.Has aᶜ
⊢ d.Has a

Tactic:
simpa using d.has_compl h

Premises used: MeasurableSpace.DynkinSystem.has_compl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
d : DynkinSystem α
⊢ d.Has univ

Tactic:
simpa using d.has_compl d.has_empty

Premises used: MeasurableSpace.DynkinSystem.has_compl, MeasurableSpace.DynkinSystem.has_empty
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
d : DynkinSystem α
β : Type u_4
inst : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
h : ∀ (i : β), d.Has (f i)
intro : ∀ (val : Encodable β), d.Has (⋃ (i : β), f i)
⊢ d.Has (⋃ (i : β), f i)

Tactic:
cases nonempty_encodable β

Premises used: nonempty_encodable
-- Module: Mathlib.MeasureTheory.PiSystem
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 β
intro : d.Has (⋃ (i : ℕ), ⋃ b ∈ Encodable.decode₂ β i, f b)
⊢ d.Has (⋃ (i : β), f i)

Tactic:
rw [← Encodable.iUnion_decode₂]

Premises used: Encodable.iUnion_decode₂
-- Module: Mathlib.MeasureTheory.PiSystem
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 : ℕ), ⋃ b ∈ Encodable.decode₂ β i, f b)

Tactic:
d.has_iUnion_nat (Encodable.iUnion_decode₂_disjoint_on hd) fun n =>
      Encodable.iUnion_decode₂_cases d.has_empty h

Premises used: Encodable.iUnion_decode₂_cases, MeasurableSpace.DynkinSystem.has_iUnion_nat, Encodable.iUnion_decode₂_disjoint_on
-- Module: Mathlib.MeasureTheory.PiSystem
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 : ℕ), ⋃ b ∈ Encodable.decode₂ β i, f b)

Tactic:
exact
    d.has_iUnion_nat (Encodable.iUnion_decode₂_disjoint_on hd) fun n =>
      Encodable.iUnion_decode₂_cases d.has_empty h

Premises used: Encodable.iUnion_decode₂_cases, MeasurableSpace.DynkinSystem.has_iUnion_nat, Encodable.iUnion_decode₂_disjoint_on
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : Disjoint s₁ s₂
rw : d.Has (⋃ (b : Bool), bif b then s₁ else s₂)
⊢ d.Has (s₁ ∪ s₂)

Tactic:
rw [union_eq_iUnion]

Premises used: Set.union_eq_iUnion
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : Disjoint s₁ s₂
⊢ d.Has (⋃ (b : Bool), bif b then s₁ else s₂)

Tactic:
d.has_iUnion (pairwise_disjoint_on_bool.2 h) (Bool.forall_bool.2 ⟨h₂, h₁⟩)

Premises used: Iff.mpr, Bool.forall_bool, And.intro, pairwise_disjoint_on_bool, MeasurableSpace.DynkinSystem.has_iUnion
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : Disjoint s₁ s₂
⊢ d.Has (⋃ (b : Bool), bif b then s₁ else s₂)

Tactic:
exact d.has_iUnion (pairwise_disjoint_on_bool.2 h) (Bool.forall_bool.2 ⟨h₂, h₁⟩)

Premises used: Iff.mpr, Bool.forall_bool, And.intro, pairwise_disjoint_on_bool, MeasurableSpace.DynkinSystem.has_iUnion
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
apply : d.Has (s₁ \ s₂)ᶜ
⊢ d.Has (s₁ \ s₂)

Tactic:
apply d.has_compl_iff.1

Premises used: MeasurableSpace.DynkinSystem.has_compl_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
simp : d.Has (s₁ᶜ ∪ s₂)
⊢ d.Has (s₁ \ s₂)ᶜ

Tactic:
simp only [diff_eq, compl_inter, compl_compl]

Premises used: compl_compl, Set.compl_inter, Set.diff_eq
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
⊢ d.Has (s₁ᶜ ∪ s₂)

Tactic:
d.has_union (d.has_compl h₁) h₂ (disjoint_compl_left.mono_right h)

Premises used: MeasurableSpace.DynkinSystem.has_compl, disjoint_compl_left, MeasurableSpace.DynkinSystem.has_union, Disjoint.mono_right
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
⊢ d.Has (s₁ᶜ ∪ s₂)

Tactic:
exact d.has_union (d.has_compl h₁) h₂ (disjoint_compl_left.mono_right h)

Premises used: MeasurableSpace.DynkinSystem.has_compl, disjoint_compl_left, MeasurableSpace.DynkinSystem.has_union, Disjoint.mono_right
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
a b : DynkinSystem α
⊢ a ≤ b ↔ a.Has ≤ b.Has

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
m₁ m₂ : MeasurableSpace α
⊢ ofMeasurableSpace m₁ ≤ ofMeasurableSpace m₂ ↔ m₁ ≤ m₂

Tactic:
Iff.rfl

Premises used: MeasurableSet, Iff.rfl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
C : Set (Set α)
s : Set α
⊢ GenerateHas C sᶜ ↔ GenerateHas C s

Tactic:
⟨?_, GenerateHas.compl⟩

Premises used: Iff.intro, MeasurableSpace.DynkinSystem.GenerateHas.compl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
C : Set (Set α)
s : Set α
refine : GenerateHas C sᶜ → GenerateHas C s
⊢ GenerateHas C sᶜ ↔ GenerateHas C s

Tactic:
refine ⟨?_, GenerateHas.compl⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
C : Set (Set α)
s : Set α
h : GenerateHas C sᶜ
⊢ GenerateHas C sᶜᶜ

Tactic:
GenerateHas.compl h

Premises used: MeasurableSpace.DynkinSystem.GenerateHas.compl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
C : Set (Set α)
s : Set α
h : GenerateHas C sᶜ
h₁ : s = sᶜᶜ
⊢ GenerateHas C s

Tactic:
convert! GenerateHas.compl h

Premises used: MeasurableSpace.DynkinSystem.GenerateHas.compl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
C : Set (Set α)
s : Set α
h : GenerateHas C sᶜ
⊢ s = sᶜᶜ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
C : Set (Set α)
⊢ (generate C).Has = GenerateHas C

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
h_inter : ∀ (s₁ s₂ : Set α), d.Has s₁ → d.Has s₂ → d.Has (s₁ ∩ s₂)
f : ℕ → Set α
hf : ∀ (i : ℕ), d.Has (f i)
rw : d.Has (⋃ (i : ℕ), disjointed f i)
⊢ d.Has (⋃ (i : ℕ), f i)

Tactic:
rw [← iUnion_disjointed]

Premises used: iUnion_disjointed
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
h_inter : ∀ (s₁ s₂ : Set α), d.Has s₁ → d.Has s₂ → d.Has (s₁ ∩ s₂)
f : ℕ → Set α
hf : ∀ (i : ℕ), d.Has (f i)
⊢ d.Has (⋃ (i : ℕ), disjointed f i)

Tactic:
d.has_iUnion (disjoint_disjointed _) fun n =>
        disjointedRec (fun (t : Set α) i h => h_inter _ _ h <| d.has_compl <| hf i) (hf n)

Premises used: MeasurableSpace.DynkinSystem.has_compl, MeasurableSpace.DynkinSystem.has_iUnion, disjoint_disjointed, disjointedRec
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
h_inter : ∀ (s₁ s₂ : Set α), d.Has s₁ → d.Has s₂ → d.Has (s₁ ∩ s₂)
f : ℕ → Set α
hf : ∀ (i : ℕ), d.Has (f i)
⊢ d.Has (⋃ (i : ℕ), disjointed f i)

Tactic:
exact
      d.has_iUnion (disjoint_disjointed _) fun n =>
        disjointedRec (fun (t : Set α) i h => h_inter _ _ h <| d.has_compl <| hf i) (hf n)

Premises used: MeasurableSpace.DynkinSystem.has_compl, MeasurableSpace.DynkinSystem.has_iUnion, disjoint_disjointed, disjointedRec
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
d : DynkinSystem α
h_inter : ∀ (s₁ s₂ : Set α), d.Has s₁ → d.Has s₂ → d.Has (s₁ ∩ s₂)
⊢ ofMeasurableSpace (d.toMeasurableSpace h_inter) = d

Tactic:
ext fun _ => Iff.rfl

Premises used: Iff.rfl, MeasurableSpace.DynkinSystem.ext
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
⊢ d.Has (∅ ∩ s)

Tactic:
simp [d.has_empty]

Premises used: MeasurableSpace.DynkinSystem.has_empty
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
t : Set α
hts : d.Has (t ∩ s)
x : α
pos : ∀ (h : x ∈ s), x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ
neg : ∀ (h : x ∉ s), x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ
⊢ x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ

Tactic:
by_cases h : x ∈ s
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h_1 : d.Has s
t : Set α
hts : d.Has (t ∩ s)
x : α
h : x ∈ s
⊢ x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h_1 : d.Has s
t : Set α
hts : d.Has (t ∩ s)
x : α
h : x ∉ s
⊢ x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
t : Set α
hts : d.Has (t ∩ s)
⊢ tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ

Tactic:
have : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ := Set.ext fun x => by by_cases h : x ∈ s <;> simp [h]
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
t : Set α
hts : d.Has (t ∩ s)
this : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ
simp_rw : d.Has ((t ∩ s)ᶜ \ sᶜ)
⊢ d.Has (tᶜ ∩ s)

Tactic:
simp_rw [this]
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
t : Set α
hts : d.Has (t ∩ s)
this : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ
⊢ d.Has ((t ∩ s)ᶜ \ sᶜ)

Tactic:
d.has_diff (d.has_compl hts) (d.has_compl h)
        (compl_subset_compl.mpr inter_subset_right)

Premises used: Iff.mpr, MeasurableSpace.DynkinSystem.has_compl, Set.compl_subset_compl, MeasurableSpace.DynkinSystem.has_diff, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
t : Set α
hts : d.Has (t ∩ s)
this : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ
⊢ d.Has ((t ∩ s)ᶜ \ sᶜ)

Tactic:
exact
      d.has_diff (d.has_compl hts) (d.has_compl h)
        (compl_subset_compl.mpr inter_subset_right)

Premises used: Iff.mpr, MeasurableSpace.DynkinSystem.has_compl, Set.compl_subset_compl, MeasurableSpace.DynkinSystem.has_diff, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), d.Has (f i ∩ s)
rw : d.Has (⋃ (i : ℕ), f i ∩ s)
⊢ d.Has ((⋃ (i : ℕ), f i) ∩ s)

Tactic:
rw [iUnion_inter]

Premises used: Set.iUnion_inter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), d.Has (f i ∩ s)
⊢ d.Has (⋃ (i : ℕ), f i ∩ s)

Tactic:
d.has_iUnion_nat ?_ hf

Premises used: MeasurableSpace.DynkinSystem.has_iUnion_nat
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), d.Has (f i ∩ s)
refine : Pairwise (α := ℕ) (Function.onFun.{1, u_3 + 1, 1} (β := Set α) Disjoint fun (i : ℕ) ↦ f i ∩ s)
⊢ d.Has (⋃ (i : ℕ), f i ∩ s)

Tactic:
refine d.has_iUnion_nat ?_ hf

Premises used: MeasurableSpace.DynkinSystem.has_iUnion_nat
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), d.Has (f i ∩ s)
⊢ Pairwise (α := ℕ) (Function.onFun.{1, u_3 + 1, 1} (β := Set α) Disjoint fun (i : ℕ) ↦ f i ∩ s)

Tactic:
hd.mono fun i j => Disjoint.mono inter_subset_left inter_subset_left

Premises used: Set.inter_subset_left, Disjoint.mono, Pairwise.mono
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), d.Has (f i ∩ s)
⊢ Pairwise (α := ℕ) (Function.onFun.{1, u_3 + 1, 1} (β := Set α) Disjoint fun (i : ℕ) ↦ f i ∩ s)

Tactic:
exact hd.mono fun i j => Disjoint.mono inter_subset_left inter_subset_left

Premises used: Set.inter_subset_left, Disjoint.mono, Pairwise.mono
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
d : DynkinSystem α
s : Set (Set α)
h : ∀ t ∈ s, d.Has t
⊢ generate s ≤ d

Tactic:
fun _ ht =>
  ht.recOn h d.has_empty (fun {_} _ h => d.has_compl h) fun {_} hd _ hf => d.has_iUnion hd hf

Premises used: MeasurableSpace.DynkinSystem.GenerateHas.recOn
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
C : Set (Set α)
s : Set α
hs : (generate C).Has s
⊢ MeasurableSet s

Tactic:
generate_le (ofMeasurableSpace (generateFrom C)) (fun _ => measurableSet_generateFrom) s hs

Premises used: MeasurableSet, MeasurableSpace.measurableSet_generateFrom, MeasurableSpace.DynkinSystem.ofMeasurableSpace, MeasurableSpace.generateFrom, MeasurableSpace.DynkinSystem.generate_le
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
t₁ t₂ : Set α
ht₁ : (generate s).Has t₁
ht₂ : (generate s).Has t₂
s₁ : Set α
hs₁ : s₁ ∈ s
this_1 : (generate s).Has s₁
this_2 : generate s ≤ (generate s).restrictOn (s := s₁) this_1
this rwa rwa₁ rwa₂ rwa₃ : (generate s).Has (t₂ ∩ s₁)
⊢ (generate s).Has (s₁ ∩ t₂)

Tactic:
rwa [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
⊢ generate s ≤ ofMeasurableSpace (generateFrom s)

Tactic:
generate_le _ fun t ht => measurableSet_generateFrom ht

Premises used: MeasurableSpace.measurableSet_generateFrom, MeasurableSpace.DynkinSystem.generate_le
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
⊢ generate s ≤ ofMeasurableSpace (generateFrom s)

Tactic:
exact generate_le _ fun t ht => measurableSet_generateFrom ht

Premises used: MeasurableSpace.DynkinSystem.generate_le
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯
rw : MeasurableSet = DynkinSystem.GenerateHas s
⊢ MeasurableSet = DynkinSystem.GenerateHas s

Tactic:
rw [h_eq, DynkinSystem.generateFrom_eq h_inter]

Premises used: MeasurableSpace.DynkinSystem.generateFrom_eq
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯
⊢ MeasurableSet = DynkinSystem.GenerateHas s

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯
⊢ MeasurableSet = DynkinSystem.GenerateHas s

Tactic:
have eq : MeasurableSet = DynkinSystem.GenerateHas s := by
    rw [h_eq, DynkinSystem.generateFrom_eq h_inter]
    rfl
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
suffices : ∀ (t : Set α) (ht : DynkinSystem.GenerateHas s t), C t ⋯
⊢ ∀ (t : Set α) (ht : MeasurableSet t), C t ht

Tactic:
suffices ∀ t (ht : DynkinSystem.GenerateHas s t), C t (eq ▸ ht) from
    fun t ht ↦ this t (eq ▸ ht)
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
t u : Set α
hu : u ∈ s
⊢ C u ⋯

Tactic:
basic u hu