awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
⊢ ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} s →
      ∀ (t : Set α),
        Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} t →
          ∃ (I : Finset (Set α)),
            (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
              (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α))
have rintro : ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : 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 α))
Tactic: classical
    rintro s ⟨u, v, huv, rfl⟩ t ⟨u', v', hu'v', rfl⟩
    rcases le_or_gt u' u with hu | hu
    · rcases Ioc_mem_setOf_Ioc_le (max u v') v with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rcases le_or_gt v v' with hv | hv
    · rcases Ioc_mem_setOf_Ioc_le u (min u' v) with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rw [show Set.Ioc u v \ Set.Ioc u' v' = Set.Ioc u u' ∪ Set.Ioc v' v by grind]
    refine ⟨{Set.Ioc u u', Set.Ioc v' v}, by grind, ?_, by simp⟩
    intro a ha b hb hab
    simp [Function.onFun]
    grind
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
rintro :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : 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 α))
⊢ ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} s →
      ∀ (t : Set α),
        Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} t →
          ∃ (I : Finset (Set α)),
            (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
              (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α))
have inl : ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u' ≤ u),
  ∃ (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: classical
    rintro s ⟨u, v, huv, rfl⟩ t ⟨u', v', hu'v', rfl⟩
    rcases le_or_gt u' u with hu | hu
    · rcases Ioc_mem_setOf_Ioc_le (max u v') v with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rcases le_or_gt v v' with hv | hv
    · rcases Ioc_mem_setOf_Ioc_le u (min u' v) with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rw [show Set.Ioc u v \ Set.Ioc u' v' = Set.Ioc u u' ∪ Set.Ioc v' v by grind]
    refine ⟨{Set.Ioc u u', Set.Ioc v' v}, by grind, ?_, by simp⟩
    intro a ha b hb hab
    simp [Function.onFun]
    grind
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
rintro :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : 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 α))
inl :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u' ≤ u),
    ∃ (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 α))
⊢ ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} s →
      ∀ (t : Set α),
        Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} t →
          ∃ (I : Finset (Set α)),
            (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
              (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α))
have inr : ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u < u'),
  ∃ (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: classical
    rintro s ⟨u, v, huv, rfl⟩ t ⟨u', v', hu'v', rfl⟩
    rcases le_or_gt u' u with hu | hu
    · rcases Ioc_mem_setOf_Ioc_le (max u v') v with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rcases le_or_gt v v' with hv | hv
    · rcases Ioc_mem_setOf_Ioc_le u (min u' v) with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rw [show Set.Ioc u v \ Set.Ioc u' v' = Set.Ioc u u' ∪ Set.Ioc v' v by grind]
    refine ⟨{Set.Ioc u u', Set.Ioc v' v}, by grind, ?_, by simp⟩
    intro a ha b hb hab
    simp [Function.onFun]
    grind
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
rintro :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : 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 α))
inl :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u' ≤ u),
    ∃ (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 inr₁ :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u < u'),
    ∃ (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 α))
⊢ ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} s →
      ∀ (t : Set α),
        Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} t →
          ∃ (I : Finset (Set α)),
            (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
              (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α))
have inr₂ : ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u < u') (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 α))
Tactic: classical
    rintro s ⟨u, v, huv, rfl⟩ t ⟨u', v', hu'v', rfl⟩
    rcases le_or_gt u' u with hu | hu
    · rcases Ioc_mem_setOf_Ioc_le (max u v') v with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rcases le_or_gt v v' with hv | hv
    · rcases Ioc_mem_setOf_Ioc_le u (min u' v) with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rw [show Set.Ioc u v \ Set.Ioc u' v' = Set.Ioc u u' ∪ Set.Ioc v' v by grind]
    refine ⟨{Set.Ioc u u', Set.Ioc v' v}, by grind, ?_, by simp⟩
    intro a ha b hb hab
    simp [Function.onFun]
    grind
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
rintro :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : 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 α))
inl :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u' ≤ u),
    ∃ (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 inr₁ :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u < u'),
    ∃ (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₂ :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u < u') (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 α))
⊢ ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} s →
      ∀ (t : Set α),
        Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} t →
          ∃ (I : Finset (Set α)),
            (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
              (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α))
have inr₃ : ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u < u') (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 α))
Tactic: classical
    rintro s ⟨u, v, huv, rfl⟩ t ⟨u', v', hu'v', rfl⟩
    rcases le_or_gt u' u with hu | hu
    · rcases Ioc_mem_setOf_Ioc_le (max u v') v with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rcases le_or_gt v v' with hv | hv
    · rcases Ioc_mem_setOf_Ioc_le u (min u' v) with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rw [show Set.Ioc u v \ Set.Ioc u' v' = Set.Ioc u u' ∪ Set.Ioc v' v by grind]
    refine ⟨{Set.Ioc u u', Set.Ioc v' v}, by grind, ?_, by simp⟩
    intro a ha b hb hab
    simp [Function.onFun]
    grind
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
rintro :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : 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 α))
inl :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u' ≤ u),
    ∃ (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 inr₁ :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u < u'),
    ∃ (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₂ :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u < u') (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₃ inr₄ :
  ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u < u') (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 α))
⊢ ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} s →
      ∀ (t : Set α),
        Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} t →
          ∃ (I : Finset (Set α)),
            (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
              (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α))
have inr₅ : ∀ (u v : α) (huv : u ≤ v) (u' v' : α) (hu'v' : u' ≤ v') (hu : u < u') (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 u' ∪ Set.Ioc v' v = ⋃₀ (↑I : Set (Set α))
Tactic: classical
    rintro s ⟨u, v, huv, rfl⟩ t ⟨u', v', hu'v', rfl⟩
    rcases le_or_gt u' u with hu | hu
    · rcases Ioc_mem_setOf_Ioc_le (max u v') v with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rcases le_or_gt v v' with hv | hv
    · rcases Ioc_mem_setOf_Ioc_le u (min u' v) with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rw [show Set.Ioc u v \ Set.Ioc u' v' = Set.Ioc u u' ∪ Set.Ioc v' v by grind]
    refine ⟨{Set.Ioc u u', Set.Ioc v' v}, by grind, ?_, by simp⟩
    intro a ha b hb hab
    simp [Function.onFun]
    grind
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ s ∩ t ∈ C
have rw : s \ (s \ t) ∈ C
Tactic: rw [← diff_diff_right_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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 α))
have refine_1 : ∀ (s : Set α) (hs : s ∈ C) (t : Set α) (ht : t ∈ C), (↑{s \ t} : Set (Set α)) ⊆ C
Tactic: refine fun s hs t ht => ⟨{s \ t}, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ ∀ s ∈ C,
    ∀ t ∈ C,
      ∃ (I : Finset (Set α)),
        (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α))
have refine_2 : ∀ (s : Set α) (hs : s ∈ C) (t : Set α) (ht : t ∈ C), (↑{s \ t} : Set (Set α)).PairwiseDisjoint id
Tactic: refine fun s hs t ht => ⟨{s \ t}, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ ∀ s ∈ C,
    ∀ t ∈ C,
      ∃ (I : Finset (Set α)),
        (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α))
have refine_3 : ∀ (s : Set α) (hs : s ∈ C) (t : Set α) (ht : t ∈ C), s \ t = ⋃₀ (↑{s \ t} : Set (Set α))
Tactic: refine fun s hs t ht => ⟨{s \ t}, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : Set α
hs : s ∈ C
t : Set α
ht : t ∈ C
⊢ (↑{s \ t} : Set (Set α)) ⊆ C
have refine_1 : s \ t ∈ C
Tactic: simp only [coe_singleton, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ ⋃ i_1 ∈ insert i S, s i_1 ∈ C
have insert : s i ∪ ⋃ x ∈ (↑S : Set ι), s x ∈ C
Tactic: simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
have insert : ⋃ x ∈ (↑S : Set ι), s x ∈ C
Tactic: refine hC.union_mem (hs i (mem_insert_self i S)) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
⊢ ⋃ i ∈ S, s i ∈ C
have empty : ∀ (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) ∅ n → s n ∈ C),
  ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), 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))
Cleared hypotheses: S, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ ⋃ i ∈ S, s i ∈ C
have insert : ∀ (i : ι) (S : Finset ι),
  i ∉ S →
    ∀ (h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋃ i ∈ S, s i ∈ C) (hs : ∀ n ∈ insert i S, s n ∈ C), ⋃ i_1 ∈ insert i S, s i_1 ∈ 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))
Cleared hypotheses: S, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
⊢ ⋃ i ∈ S, s i ∈ C
have empty : ∀ (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) ∅ n → s n ∈ C),
  ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), 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))
Cleared hypotheses: S, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ ⋃ i ∈ S, s i ∈ C
have insert : ∀ (i : ι) (S : Finset ι),
  i ∉ S →
    ∀ (h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋃ i ∈ S, s i ∈ C) (hs : ∀ n ∈ insert i S, s n ∈ C), ⋃ i_1 ∈ insert i S, s i_1 ∈ 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))
Cleared hypotheses: S, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ ⋂ i_1 ∈ cons i S hiS, s i_1 ∈ C
have cons : s i ∩ ⋂ x ∈ (↑S : Set ι), s x ∈ C
Tactic: simp_rw [← Finset.mem_coe, Finset.coe_cons, Set.biInter_insert]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
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 ∩ ⋂ x ∈ (↑S : Set ι), s x ∈ C
have hs₁ : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
Tactic: simp only [cons_eq_insert, Finset.mem_insert, forall_eq_or_imp] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
have cons : ⋂ x ∈ (↑S : Set ι), s x ∈ C
Tactic: refine hC.inter_mem hs.1 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ ⋂ i ∈ S, s i ∈ C
have singleton : ∀ (a : ι) (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) {a} n → s n ∈ C),
  ⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {a} i), 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)
Cleared hypotheses: hS, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ ⋂ i ∈ S, s i ∈ C
have cons : ∀ (i : ι) (S : Finset ι) (hiS : i ∉ S),
  S.Nonempty →
    ∀ (h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋂ i ∈ S, s i ∈ C) (hs : ∀ n ∈ cons i S hiS, s n ∈ C),
      ⋂ i_1 ∈ cons i S hiS, s i_1 ∈ 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)
Cleared hypotheses: hS, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ ⋂ i ∈ S, s i ∈ C
have singleton : ∀ (a : ι) (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) {a} n → s n ∈ C),
  ⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {a} i), 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)
Cleared hypotheses: hS, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ ⋂ i ∈ S, s i ∈ C
have cons : ∀ (i : ι) (S : Finset ι) (hiS : i ∉ S),
  S.Nonempty →
    ∀ (h : ∀ (hs : ∀ n ∈ S, s n ∈ C), ⋂ i ∈ S, s i ∈ C) (hs : ∀ n ∈ cons i S hiS, s n ∈ C),
      ⋂ i_1 ∈ cons i S hiS, s i_1 ∈ 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)
Cleared hypotheses: hS, hs