awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
inr :
  ∀ (hv : v ≤ v'),
    ∃ (I : Finset (Set α)),
      (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
        (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ (↑I : Set (Set α))
inr₁ :
  ∀ (hv : v' < v),
    ∃ (I : Finset (Set α)),
      (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
        (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ (↑I : Set (Set α))
⊢ ∃ (I : Finset (Set α)),
    (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
      (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ (↑I : Set (Set α))

Tactic:
rcases le_or_gt v v' with hv | hv

Premises used: le_or_gt
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v ≤ v'
inr :
  ∀ (u'' v'' : α) (h'' : u'' ≤ v'') (heq : Set.Ioc u (min u' v) = Set.Ioc u'' v''),
    ∃ (I : Finset (Set α)),
      (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
        (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ (↑I : Set (Set α))
⊢ ∃ (I : Finset (Set α)),
    (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
      (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ (↑I : Set (Set α))

Tactic:
rcases Ioc_mem_setOf_Ioc_le u (min u' v) with ⟨u'', v'', h'', heq⟩

Premises used: _private.0.Set.Ioc_mem_setOf_Ioc_le, Min.min
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v ≤ v'
u'' v'' : α
h'' : u'' ≤ v''
heq : Set.Ioc u (min u' v) = Set.Ioc u'' v''
inr :
  (↑{Set.Ioc u'' v''} : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
    (↑{Set.Ioc u'' v''} : Set (Set α)).PairwiseDisjoint id ∧
      Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ (↑{Set.Ioc u'' v''} : Set (Set α))
⊢ ∃ (I : Finset (Set α)),
    (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
      (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ (↑I : Set (Set α))

Tactic:
exists {Set.Ioc u'' v''}

Premises used: Set.Ioc
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v ≤ v'
u'' v'' : α
h'' : u'' ≤ v''
heq : Set.Ioc u (min u' v) = Set.Ioc u'' v''
⊢ (↑{Set.Ioc u'' v''} : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
    (↑{Set.Ioc u'' v''} : Set (Set α)).PairwiseDisjoint id ∧
      Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ (↑{Set.Ioc u'' v''} : Set (Set α))

Tactic:
grind [coe_singleton, pairwiseDisjoint_singleton]

Premises used: Finset.coe_singleton, Set.pairwiseDisjoint_singleton
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
⊢ Set.Ioc u v \ Set.Ioc u' v' = Set.Ioc u u' ∪ Set.Ioc v' v

Tactic:
grind
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
inr :
  ∃ (I : Finset (Set α)),
    (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
      (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u u' ∪ Set.Ioc v' v = ⋃₀ (↑I : Set (Set α))
⊢ ∃ (I : Finset (Set α)),
    (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
      (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ (↑I : Set (Set α))

Tactic:
rw [show Set.Ioc u v \ Set.Ioc u' v' = Set.Ioc u u' ∪ Set.Ioc v' v by grind]
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
⊢ (↑{Set.Ioc u u', Set.Ioc v' v} : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}

Tactic:
grind
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
⊢ Set.Ioc u u' ∪ Set.Ioc v' v = ⋃₀ (↑{Set.Ioc u u', Set.Ioc v' v} : Set (Set α))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
inr : (↑{Set.Ioc u u', Set.Ioc v' v} : Set (Set α)).PairwiseDisjoint id
⊢ ∃ (I : Finset (Set α)),
    (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
      (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u u' ∪ Set.Ioc v' v = ⋃₀ (↑I : Set (Set α))

Tactic:
refine ⟨{Set.Ioc u u', Set.Ioc v' v}, by grind, ?_, by simp⟩
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
a : Set α
ha : a ∈ (↑{Set.Ioc u u', Set.Ioc v' v} : Set (Set α))
b : Set α
hb : b ∈ (↑{Set.Ioc u u', Set.Ioc v' v} : Set (Set α))
hab : a ≠ b
inr : Disjoint a b
⊢ Function.onFun Disjoint id a b

Tactic:
simp [Function.onFun]

Premises used: Function.onFun
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
a : Set α
ha : a ∈ (↑{Set.Ioc u u', Set.Ioc v' v} : Set (Set α))
b : Set α
hb : b ∈ (↑{Set.Ioc u u', Set.Ioc v' v} : Set (Set α))
hab : a ≠ b
⊢ Disjoint a b

Tactic:
grind
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
rw : s \ (s \ t) ∈ C
⊢ s ∩ t ∈ C

Tactic:
rw [← diff_diff_right_self]

Premises used: Set.diff_diff_right_self
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ s \ (s \ t) ∈ C

Tactic:
hC.diff_mem hs (hC.diff_mem hs ht)

Premises used: MeasureTheory.IsSetRing.diff_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ s \ (s \ t) ∈ C

Tactic:
exact hC.diff_mem hs (hC.diff_mem hs ht)

Premises used: MeasureTheory.IsSetRing.diff_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
⊢ ∀ s ∈ C,
    ∀ t ∈ C,
      ∃ (I : Finset (Set α)),
        (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α))

Tactic:
fun s hs t ht => ⟨{s \ t}, ?_, ?_, ?_⟩

Premises used: SDiff.sdiff, And.intro, Exists.intro, Singleton.singleton
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
refine_1 : ∀ (s : Set α) (hs : s ∈ C) (t : Set α) (ht : t ∈ C), (↑{s \ t} : Set (Set α)) ⊆ C
refine_2 : ∀ (s : Set α) (hs : s ∈ C) (t : Set α) (ht : t ∈ C), (↑{s \ t} : Set (Set α)).PairwiseDisjoint id
refine_3 : ∀ (s : Set α) (hs : s ∈ C) (t : Set α) (ht : t ∈ C), s \ t = ⋃₀ (↑{s \ t} : Set (Set α))
⊢ ∀ s ∈ C,
    ∀ t ∈ C,
      ∃ (I : Finset (Set α)),
        (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α))

Tactic:
refine fun s hs t ht => ⟨{s \ t}, ?_, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : Set α
hs : s ∈ C
t : Set α
ht : t ∈ C
refine_1 : s \ t ∈ C
⊢ (↑{s \ t} : Set (Set α)) ⊆ C

Tactic:
simp only [coe_singleton, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Finset.coe_singleton
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : Set α
hs : s ∈ C
t : Set α
ht : t ∈ C
⊢ s \ t ∈ C

Tactic:
hC.diff_mem hs ht

Premises used: MeasureTheory.IsSetRing.diff_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : Set α
hs : s ∈ C
t : Set α
ht : t ∈ C
⊢ s \ t ∈ C

Tactic:
exact hC.diff_mem hs ht

Premises used: MeasureTheory.IsSetRing.diff_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : Set α
hs : s ∈ C
t : Set α
ht : t ∈ C
⊢ (↑{s \ t} : Set (Set α)).PairwiseDisjoint id

Tactic:
simp only [coe_singleton, pairwiseDisjoint_singleton]

Premises used: Finset.coe_singleton, Set.pairwiseDisjoint_singleton
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : Set α
hs : s ∈ C
t : Set α
ht : t ∈ C
⊢ s \ t = ⋃₀ (↑{s \ t} : Set (Set α))

Tactic:
simp only [coe_singleton, sUnion_singleton]

Premises used: Finset.coe_singleton, Set.sUnion_singleton
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
hs : ∀ (n : ι), Membership.mem (γ := Finset ι) ∅ n → s n ∈ C
⊢ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i ∈ C

Tactic:
simp [hC.empty_mem]

Premises used: MeasureTheory.IsSetRing.empty_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
h_1 : i ∉ S
h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋃ i ∈ S, s i ∈ C
hs : ∀ n ∈ Insert.insert i S, s n ∈ C
insert : s i ∪ ⋃ x ∈ (↑S : Set ι), s x ∈ C
⊢ ⋃ i_1 ∈ Insert.insert i S, s i_1 ∈ C

Tactic:
simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]

Premises used: Set.biUnion_insert, Finset.coe_insert, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
h_1 : i ∉ S
h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋃ i ∈ S, s i ∈ C
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ s i ∪ ⋃ x ∈ (↑S : Set ι), s x ∈ C

Tactic:
hC.union_mem (hs i (mem_insert_self i S)) ?_

Premises used: Finset.mem_insert_self, MeasureTheory.IsSetRing.union_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
h_1 : i ∉ S
h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋃ i ∈ S, s i ∈ C
hs : ∀ n ∈ Insert.insert i S, s n ∈ C
insert : ⋃ x ∈ (↑S : Set ι), s x ∈ C
⊢ s i ∪ ⋃ x ∈ (↑S : Set ι), s x ∈ C

Tactic:
refine hC.union_mem (hs i (mem_insert_self i S)) ?_

Premises used: Finset.mem_insert_self, MeasureTheory.IsSetRing.union_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
h_1 : i ∉ S
h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋃ i ∈ S, s i ∈ C
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ ⋃ x ∈ (↑S : Set ι), s x ∈ C

Tactic:
h (fun n hnS ↦ hs n (mem_insert_of_mem hnS))

Premises used: Set.Mem, Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
h_1 : i ∉ S
h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋃ i ∈ S, s i ∈ C
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ ⋃ x ∈ (↑S : Set ι), s x ∈ C

Tactic:
exact h (fun n hnS ↦ hs n (mem_insert_of_mem hnS))

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
empty :
  ∀ (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) ∅ n → s n ∈ C),
    ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i ∈ C
insert :
  ∀ (i : ι) (S : Finset ι),
    i ∉ S →
      ∀ (h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋃ i ∈ S, s i ∈ C) (hs : ∀ n ∈ Insert.insert i S, s n ∈ C),
        ⋃ i_1 ∈ Insert.insert i S, s i_1 ∈ C
⊢ ⋃ i ∈ S, s i ∈ C

Tactic:
induction S using Finset.induction with
  | empty => simp [hC.empty_mem]
  | insert i S _ h =>
    simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
    refine hC.union_mem (hs i (mem_insert_self i S)) ?_
    exact h (fun n hnS ↦ hs n (mem_insert_of_mem hnS))

Premises used: Set.biUnion_insert, Insert.insert, MeasureTheory.IsSetRing.empty_mem, Finset.coe_insert, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
empty :
  ∀ (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) ∅ n → s n ∈ C),
    ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i ∈ C
insert :
  ∀ (i : ι) (S : Finset ι),
    i ∉ S →
      ∀ (h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋃ i ∈ S, s i ∈ C) (hs : ∀ n ∈ Insert.insert i S, s n ∈ C),
        ⋃ i_1 ∈ Insert.insert i S, s i_1 ∈ C
⊢ ⋃ i ∈ S, s i ∈ C

Tactic:
classical
  induction S using Finset.induction with
  | empty => simp [hC.empty_mem]
  | insert i S _ h =>
    simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
    refine hC.union_mem (hs i (mem_insert_self i S)) ?_
    exact h (fun n hnS ↦ hs n (mem_insert_of_mem hnS))

Premises used: Set.biUnion_insert, Insert.insert, MeasureTheory.IsSetRing.empty_mem, Finset.coe_insert, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
a : ι
hs : ∀ (n : ι), Membership.mem (γ := Finset ι) {a} n → s n ∈ C
⊢ ⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {a} i), s i ∈ C

Tactic:
simpa using hs
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S_1 : Finset ι
i : ι
S : Finset ι
hiS : i ∉ S
hs_1 : S.Nonempty
h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋂ i ∈ S, s i ∈ C
hs : ∀ n ∈ Finset.cons i S hiS, s n ∈ C
cons : s i ∩ ⋂ x ∈ (↑S : Set ι), s x ∈ C
⊢ ⋂ i_1 ∈ Finset.cons i S hiS, s i_1 ∈ C

Tactic:
simp_rw [← Finset.mem_coe, Finset.coe_cons, Set.biInter_insert]

Premises used: Set.biInter_insert, Finset.coe_cons, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S_1 : Finset ι
i : ι
S : Finset ι
hiS : i ∉ S
hs_1 : S.Nonempty
h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋂ i ∈ S, s i ∈ C
hs : ∀ n ∈ cons i S hiS, s n ∈ C
⊢ s i ∈ C ∧ ∀ a ∈ S, s a ∈ C

Tactic:
simp only [cons_eq_insert, Finset.mem_insert, forall_eq_or_imp] at hs

Premises used: Finset.mem_insert, forall_eq_or_imp, Finset.cons_eq_insert
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S_1 : Finset ι
i : ι
S : Finset ι
hiS : i ∉ S
hs_1 : S.Nonempty
h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋂ i ∈ S, s i ∈ C
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
⊢ s i ∩ ⋂ x ∈ (↑S : Set ι), s x ∈ C

Tactic:
hC.inter_mem hs.1 ?_

Premises used: MeasureTheory.IsSetRing.inter_mem, And.left
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S_1 : Finset ι
i : ι
S : Finset ι
hiS : i ∉ S
hs_1 : S.Nonempty
h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋂ i ∈ S, s i ∈ C
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
cons : ⋂ x ∈ (↑S : Set ι), s x ∈ C
⊢ s i ∩ ⋂ x ∈ (↑S : Set ι), s x ∈ C

Tactic:
refine hC.inter_mem hs.1 ?_

Premises used: MeasureTheory.IsSetRing.inter_mem, And.left
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S_1 : Finset ι
i : ι
S : Finset ι
hiS : i ∉ S
hs_1 : S.Nonempty
h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋂ i ∈ S, s i ∈ C
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
⊢ ⋂ x ∈ (↑S : Set ι), s x ∈ C

Tactic:
h (fun n hnS ↦ hs.2 n hnS)

Premises used: Set.Mem, And.right
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S_1 : Finset ι
i : ι
S : Finset ι
hiS : i ∉ S
hs_1 : S.Nonempty
h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋂ i ∈ S, s i ∈ C
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
⊢ ⋂ x ∈ (↑S : Set ι), s x ∈ C

Tactic:
exact h (fun n hnS ↦ hs.2 n hnS)

Premises used: And.right
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hS : S.Nonempty
hs : ∀ n ∈ S, s n ∈ C
singleton :
  ∀ (a : ι) (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) {a} n → s n ∈ C),
    ⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {a} i), s i ∈ C
cons :
  ∀ (i : ι) (S : Finset ι) (hiS : i ∉ S),
    S.Nonempty →
      ∀ (h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋂ i ∈ S, s i ∈ C) (hs : ∀ n ∈ Finset.cons i S hiS, s n ∈ C),
        ⋂ i_1 ∈ Finset.cons i S hiS, s i_1 ∈ C
⊢ ⋂ i ∈ S, s i ∈ C

Tactic:
induction hS using Finset.Nonempty.cons_induction with
  | singleton => simpa using hs
  | cons i S hiS _ h =>
    simp_rw [← Finset.mem_coe, Finset.coe_cons, Set.biInter_insert]
    simp only [cons_eq_insert, Finset.mem_insert, forall_eq_or_imp] at hs
    refine hC.inter_mem hs.1 ?_
    exact h (fun n hnS ↦ hs.2 n hnS)

Premises used: Set.biInter_insert, Finset.cons, Finset.coe_cons, Finset.mem_insert, forall_eq_or_imp, Finset.cons_eq_insert, Singleton.singleton, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hS : S.Nonempty
hs : ∀ n ∈ S, s n ∈ C
singleton :
  ∀ (a : ι) (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) {a} n → s n ∈ C),
    ⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {a} i), s i ∈ C
cons :
  ∀ (i : ι) (S : Finset ι) (hiS : i ∉ S),
    S.Nonempty →
      ∀ (h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋂ i ∈ S, s i ∈ C) (hs : ∀ n ∈ Finset.cons i S hiS, s n ∈ C),
        ⋂ i_1 ∈ Finset.cons i S hiS, s i_1 ∈ C
⊢ ⋂ i ∈ S, s i ∈ C

Tactic:
classical
  induction hS using Finset.Nonempty.cons_induction with
  | singleton => simpa using hs
  | cons i S hiS _ h =>
    simp_rw [← Finset.mem_coe, Finset.coe_cons, Set.biInter_insert]
    simp only [cons_eq_insert, Finset.mem_insert, forall_eq_or_imp] at hs
    refine hC.inter_mem hs.1 ?_
    exact h (fun n hnS ↦ hs.2 n hnS)

Premises used: Set.biInter_insert, Finset.cons, Finset.coe_cons, Finset.mem_insert, forall_eq_or_imp, Finset.cons_eq_insert, Singleton.singleton, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
ι : Type u_2
s : ι → Set α
t : Finset ι
hs : ∀ i ∈ t, s i ∈ C
⊢ t.sup s ∈ C

Tactic:
simpa using biUnion_mem hC _ hs

Premises used: MeasureTheory.IsSetRing.biUnion_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
hC : IsSetRing C
s : ι → Set α
hs : ∀ (n : ι), s n ∈ C
n : ι
⊢ Membership.mem (α := Set α) C (((partialSups s : OrderHom.{u_2, u_1} ι (Set α)) : (a : ι) → Set α) n : Set α)

Tactic:
simpa only [partialSups_apply, sup'_eq_sup] using hC.finsetSup_mem (fun i hi ↦ hs i)

Premises used: partialSups_apply, MeasureTheory.IsSetRing.finsetSup_mem, Finset.sup'_eq_sup
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
hC : IsSetRing C
s : ι → Set α
hs : ∀ (j : ι), s j ∈ C
i : ι
⊢ disjointed s i ∈ C

Tactic:
disjointedRec (fun _ j ht ↦ hC.diff_mem ht <| hs j) (hs i)

Premises used: MeasureTheory.IsSetRing.diff_mem, disjointedRec
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
⊢ ⋃ (i : ℕ), ⋃ (_ : i ≤ 0), s i ∈ C

Tactic:
simp [hs 0]

Premises used: OfNat.ofNat
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋃ (i : ℕ), ⋃ (_ : i ≤ n), s i ∈ C
succ : (⋃ (k : ℕ), ⋃ (_ : k ≤ n), s k) ∪ s (n + 1) ∈ C
⊢ ⋃ (i : ℕ), ⋃ (_ : i ≤ n + 1), s i ∈ C

Tactic:
rw [biUnion_le_succ]

Premises used: Set.biUnion_le_succ
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋃ (i : ℕ), ⋃ (_ : i ≤ n), s i ∈ C
⊢ (⋃ (k : ℕ), ⋃ (_ : k ≤ n), s k) ∪ s (n + 1) ∈ C

Tactic:
hC.union_mem hn (hs _)

Premises used: MeasureTheory.IsSetRing.union_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋃ (i : ℕ), ⋃ (_ : i ≤ n), s i ∈ C
⊢ (⋃ (k : ℕ), ⋃ (_ : k ≤ n), s k) ∪ s (n + 1) ∈ C

Tactic:
exact hC.union_mem hn (hs _)

Premises used: MeasureTheory.IsSetRing.union_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
zero : ⋃ (i : ℕ), ⋃ (_ : i ≤ 0), s i ∈ C
succ : ∀ (n : ℕ) (hn : ⋃ (i : ℕ), ⋃ (_ : i ≤ n), s i ∈ C), ⋃ (i : ℕ), ⋃ (_ : i ≤ n + 1), s i ∈ C
⊢ ⋃ (i : ℕ), ⋃ (_ : i ≤ n), s i ∈ C

Tactic:
induction n with
  | zero => simp [hs 0]
  | succ n hn => rw [biUnion_le_succ]; exact hC.union_mem hn (hs _)

Premises used: OfNat.ofNat, Set.biUnion_le_succ
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
⊢ ⋂ (i : ℕ), ⋂ (_ : i ≤ 0), s i ∈ C

Tactic:
simp [hs 0]

Premises used: OfNat.ofNat
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋂ (i : ℕ), ⋂ (_ : i ≤ n), s i ∈ C
succ : (⋂ (k : ℕ), ⋂ (_ : k ≤ n), s k) ∩ s (n + 1) ∈ C
⊢ ⋂ (i : ℕ), ⋂ (_ : i ≤ n + 1), s i ∈ C

Tactic:
rw [biInter_le_succ]

Premises used: Set.biInter_le_succ
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋂ (i : ℕ), ⋂ (_ : i ≤ n), s i ∈ C
⊢ (⋂ (k : ℕ), ⋂ (_ : k ≤ n), s k) ∩ s (n + 1) ∈ C

Tactic:
hC.inter_mem hn (hs _)

Premises used: MeasureTheory.IsSetRing.inter_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋂ (i : ℕ), ⋂ (_ : i ≤ n), s i ∈ C
⊢ (⋂ (k : ℕ), ⋂ (_ : k ≤ n), s k) ∩ s (n + 1) ∈ C

Tactic:
exact hC.inter_mem hn (hs _)

Premises used: MeasureTheory.IsSetRing.inter_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
zero : ⋂ (i : ℕ), ⋂ (_ : i ≤ 0), s i ∈ C
succ : ∀ (n : ℕ) (hn : ⋂ (i : ℕ), ⋂ (_ : i ≤ n), s i ∈ C), ⋂ (i : ℕ), ⋂ (_ : i ≤ n + 1), s i ∈ C
⊢ ⋂ (i : ℕ), ⋂ (_ : i ≤ n), s i ∈ C

Tactic:
induction n with
  | zero => simp [hs 0]
  | succ n hn => rw [biInter_le_succ]; exact hC.inter_mem hn (hs _)

Premises used: Set.biInter_le_succ, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
⊢ accumulate s 0 ∈ C

Tactic:
simp [hs 0]

Premises used: OfNat.ofNat
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : accumulate s n ∈ C
succ : accumulate s n ∪ s (n + 1) ∈ C
⊢ accumulate s (n + 1) ∈ C

Tactic:
rw [accumulate_succ]

Premises used: Set.accumulate_succ
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : accumulate s n ∈ C
⊢ accumulate s n ∪ s (n + 1) ∈ C

Tactic:
hC.union_mem hn (hs _)

Premises used: MeasureTheory.IsSetRing.union_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : accumulate s n ∈ C
⊢ accumulate s n ∪ s (n + 1) ∈ C

Tactic:
exact hC.union_mem hn (hs _)

Premises used: MeasureTheory.IsSetRing.union_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
n : ℕ
zero : accumulate s 0 ∈ C
succ : ∀ (n : ℕ) (hn : accumulate s n ∈ C), accumulate s (n + 1) ∈ C
⊢ accumulate s n ∈ C

Tactic:
induction n with
  | zero => simp [hs 0]
  | succ n hn => rw [accumulate_succ]; exact hC.union_mem hn (hs _)

Premises used: Set.accumulate_succ, OfNat.ofNat