awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hs : s ≠ ⊥
t : Set α
ht : t ∈ P.parts (a := S.sup id)
⊢ ∃ (Q : Finpartition (t \ s)), (↑(Q.parts (a := t \ s)) : Set (Set α)) ⊆ C

Tactic:
exact hC.exists_finpartition_diff (hP ht) hsC

Premises used: MeasureTheory.IsSetSemiring.exists_finpartition_diff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hs : s ≠ ⊥
insert :
  ∀ (Q : (t : Set α) → t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s) → Finpartition t)
    (hQ :
      ∀ (t : Set α) (a : t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)),
        (↑((Q t a).parts (a := t)) : Set (Set α)) ⊆ C),
    ∃ (P : Finpartition (S.sup id ⊔ s)), (↑(P.parts (a := S.sup id ⊔ s)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (S.sup id ⊔ s)), (↑(P.parts (a := S.sup id ⊔ s)) : Set (Set α)) ⊆ C

Tactic:
choose Q hQ using show ∀ t ∈ (P.avoid s).parts, ∃ Q : Finpartition t, ↑Q.parts ⊆ C by
        simp_rw [Finpartition.mem_avoid]
        rintro _ ⟨t, ht, -, rfl⟩
        exact hC.exists_finpartition_diff (hP ht) hsC
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hs : s ≠ ⊥
Q : (t : Set α) → t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s) → Finpartition t
hQ :
  ∀ (t : Set α) (a : t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)),
    (↑((Q t a).parts (a := t)) : Set (Set α)) ⊆ C
insert :
  (↑((((P.avoid (a := S.sup id) s).bind (a := S.sup id \ s) Q).extend (a := S.sup id \ s) (b := s) (c := S.sup id ⊔ s)
              hs ⋯ ⋯).parts
          (a := S.sup id ⊔ s)) :
      Set (Set α)) ⊆
    C
⊢ ∃ (P : Finpartition (S.sup id ⊔ s)), (↑(P.parts (a := S.sup id ⊔ s)) : Set (Set α)) ⊆ C

Tactic:
exists P.avoid s |>.bind Q |>.extend hs disjoint_sdiff_left (sdiff_sup_self _ _)

Premises used: Finpartition.avoid, sdiff_sup_self, Finpartition.extend, Set.disjoint_sdiff_left, Finpartition.bind
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hs : s ≠ ⊥
Q : (t : Set α) → t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s) → Finpartition t
hQ :
  ∀ (t : Set α) (a : t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)),
    (↑((Q t a).parts (a := t)) : Set (Set α)) ⊆ C
insert :
  s ∈ C ∧
    ∀ (a : Set α) (b : a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s))
      (j :
        Subtype.mk (p := fun (a : Set α) ↦ a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)) a b ∈
          (↑(P.avoid (a := S.sup id) s).parts (a := S.sup id \ s).attach : Set ↥(P.avoid s).parts)),
      (↑(Finpartition.parts (a :=
              (↑(Subtype.mk (p := fun (a : Set α) ↦ a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)) a b) :
                Set α))
              (Q
                (↑(Subtype.mk (p := fun (a : Set α) ↦ a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)) a b) :
                  Set α)
                ⋯)) :
          Set (Set α)) ⊆
        C
⊢ (↑((((P.avoid (a := S.sup id) s).bind (a := S.sup id \ s) Q).extend (a := S.sup id \ s) (b := s) (c := S.sup id ⊔ s)
              hs ⋯ ⋯).parts
          (a := S.sup id ⊔ s)) :
      Set (Set α)) ⊆
    C

Tactic:
rw [Finpartition.extend_parts, coe_insert, insert_subset_iff, Finpartition.bind_parts,
        coe_biUnion, iUnion₂_subset_iff, Subtype.forall]

Premises used: Finset.coe_biUnion, Finpartition.extend_parts, Finpartition.bind_parts, Subtype.forall, Set.insert_subset_iff, Set.iUnion₂_subset_iff, Finset.coe_insert
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hs : s ≠ ⊥
Q : (t : Set α) → t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s) → Finpartition t
hQ :
  ∀ (t : Set α) (a : t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)),
    (↑((Q t a).parts (a := t)) : Set (Set α)) ⊆ C
⊢ s ∈ C ∧
    ∀ (a : Set α) (b : a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s))
      (j :
        Subtype.mk (p := fun (a : Set α) ↦ a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)) a b ∈
          (↑(P.avoid (a := S.sup id) s).parts (a := S.sup id \ s).attach : Set ↥(P.avoid s).parts)),
      (↑(Finpartition.parts (a :=
              (↑(Subtype.mk (p := fun (a : Set α) ↦ a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)) a b) :
                Set α))
              (Q
                (↑(Subtype.mk (p := fun (a : Set α) ↦ a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)) a b) :
                  Set α)
                ⋯)) :
          Set (Set α)) ⊆
        C

Tactic:
⟨hsC, fun t ht _ => hQ t ht⟩

Premises used: And.intro
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
h : s ∉ S
ih : ∀ (hSC : (↑S : Set (Set α)) ⊆ C), ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hsC : s ∈ C
hSC : (↑S : Set (Set α)) ⊆ C
P : Finpartition (S.sup id)
hP : (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
hs : s ≠ ⊥
Q : (t : Set α) → t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s) → Finpartition t
hQ :
  ∀ (t : Set α) (a : t ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)),
    (↑((Q t a).parts (a := t)) : Set (Set α)) ⊆ C
⊢ s ∈ C ∧
    ∀ (a : Set α) (b : a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s))
      (j :
        Subtype.mk (p := fun (a : Set α) ↦ a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)) a b ∈
          (↑(P.avoid (a := S.sup id) s).parts (a := S.sup id \ s).attach : Set ↥(P.avoid s).parts)),
      (↑(Finpartition.parts (a :=
              (↑(Subtype.mk (p := fun (a : Set α) ↦ a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)) a b) :
                Set α))
              (Q
                (↑(Subtype.mk (p := fun (a : Set α) ↦ a ∈ (P.avoid (a := S.sup id) s).parts (a := S.sup id \ s)) a b) :
                  Set α)
                ⋯)) :
          Set (Set α)) ⊆
        C

Tactic:
exact ⟨hsC, fun t ht _ => hQ t ht⟩
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
S : Finset (Set α)
hSC : (↑S : Set (Set α)) ⊆ C
empty :
  ∀ (hSC : (↑∅ : Set (Set α)) ⊆ C),
    ∃ (P : Finpartition (α := Set α) (sup ∅ id)), (↑(P.parts (a := sup ∅ id)) : Set (Set α)) ⊆ C
insert :
  ∀ (s : Set α) (S : Finset (Set α)),
    s ∉ S →
      ∀
        (ih :
          ∀ (hSC : (↑S : Set (Set α)) ⊆ C),
            ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C)
        (hSC : (↑(Insert.insert s S) : Set (Set α)) ⊆ C),
        ∃ (P : Finpartition ((Insert.insert s S).sup id)),
          (↑(P.parts (a := (Insert.insert s S).sup id)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C

Tactic:
induction S using Finset.induction with
    | empty =>
      rw [sup_empty]
      exact ⟨.empty _, hSC⟩
    | insert s S _ ih =>
      rw [coe_insert, insert_subset_iff] at hSC
      obtain ⟨hsC, hSC⟩ := hSC
      obtain ⟨P, hP⟩ := ih hSC
      rw [sup_insert, sup_comm, id]
      rcases eq_or_ne s ⊥ with rfl | hs
      · rw [sup_bot_eq]; exact ⟨P, hP⟩
      choose Q hQ using show ∀ t ∈ (P.avoid s).parts, ∃ Q : Finpartition t, ↑Q.parts ⊆ C by
        simp_rw [Finpartition.mem_avoid]
        rintro _ ⟨t, ht, -, rfl⟩
        exact hC.exists_finpartition_diff (hP ht) hsC
      exists P.avoid s |>.bind Q |>.extend hs disjoint_sdiff_left (sdiff_sup_self _ _)
      rw [Finpartition.extend_parts, coe_insert, insert_subset_iff, Finpartition.bind_parts,
        coe_biUnion, iUnion₂_subset_iff, Subtype.forall]
      exact ⟨hsC, fun t ht _ => hQ t ht⟩

Premises used: Finset.coe_biUnion, Finset.sup_insert, Finpartition.extend_parts, Finpartition.bind_parts, Finset.sup_empty, id, Subtype.forall, Insert.insert, sup_bot_eq, Set.insert_subset_iff, sup_comm, Set.iUnion₂_subset_iff, Finset.coe_insert, rfl
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
rintro :
  ∀ (S : Finset (Set α)) (hS : S.Nonempty) (hSC : (↑S : Set (Set α)) ⊆ C),
    ∃ (P : Finpartition (S.sup' hS id)), (↑(P.parts (a := S.sup' hS id)) : Set (Set α)) ⊆ C
rintro₁ :
  ∀ (S : Finset (Set α)) (hS : S.Nonempty) (hSC : (↑S : Set (Set α)) ⊆ C),
    ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
rintro₂ :
  ∀ (S : Finset (Set α)) (hSC : (↑S : Set (Set α)) ⊆ C),
    ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s →
    ∃ (P : Finpartition s), (↑(P.parts (a := s)) : Set (Set α)) ⊆ C

Tactic:
classical
    rintro ⟨S, hS, hSC, rfl⟩
    rw [sup'_eq_sup]
    clear hS
    induction S using Finset.induction with
    | empty =>
      rw [sup_empty]
      exact ⟨.empty _, hSC⟩
    | insert s S _ ih =>
      rw [coe_insert, insert_subset_iff] at hSC
      obtain ⟨hsC, hSC⟩ := hSC
      obtain ⟨P, hP⟩ := ih hSC
      rw [sup_insert, sup_comm, id]
      rcases eq_or_ne s ⊥ with rfl | hs
      · rw [sup_bot_eq]; exact ⟨P, hP⟩
      choose Q hQ using show ∀ t ∈ (P.avoid s).parts, ∃ Q : Finpartition t, ↑Q.parts ⊆ C by
        simp_rw [Finpartition.mem_avoid]
        rintro _ ⟨t, ht, -, rfl⟩
        exact hC.exists_finpartition_diff (hP ht) hsC
      exists P.avoid s |>.bind Q |>.extend hs disjoint_sdiff_left (sdiff_sup_self _ _)
      rw [Finpartition.extend_parts, coe_insert, insert_subset_iff, Finpartition.bind_parts,
        coe_biUnion, iUnion₂_subset_iff, Subtype.forall]
      exact ⟨hsC, fun t ht _ => hQ t ht⟩

Premises used: Finset.coe_biUnion, Finset.sup_insert, Finpartition.extend_parts, Finpartition.bind_parts, Finset.sup_empty, id, Subtype.forall, Insert.insert, Bot.bot, sup_bot_eq, Set.insert_subset_iff, sup_comm, eq_or_ne, Set.iUnion₂_subset_iff, Finset.coe_insert, Finset.sup'_eq_sup, rfl
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
P : Finpartition s
hP : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
rw :
  Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑(P.parts (a := s)) : Set (Set α)))
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s

Tactic:
rw [← P.sup_parts, sup_id_set_eq_sUnion]

Premises used: Finpartition.sup_parts, Finset.sup_id_set_eq_sUnion
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
P : Finpartition s
hP : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑(P.parts (a := s)) : Set (Set α)))

Tactic:
supClosed_supClosure.sSup_mem
      (Finset.finite_toSet _)
      (subset_supClosure hC.empty_mem)
      (hP.trans subset_supClosure)

Premises used: Set.Mem, setOf, Set.sUnion, HasSubset.Subset.trans, SupClosed.sSup_mem, MeasureTheory.IsSetSemiring.empty_mem, Finset.finite_toSet, subset_supClosure, supClosed_supClosure
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
P : Finpartition s
hP : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑(P.parts (a := s)) : Set (Set α)))

Tactic:
exact supClosed_supClosure.sSup_mem
      (Finset.finite_toSet _)
      (subset_supClosure hC.empty_mem)
      (hP.trans subset_supClosure)

Premises used: HasSubset.Subset.trans, SupClosed.sSup_mem, MeasureTheory.IsSetSemiring.empty_mem, Finset.finite_toSet, subset_supClosure, supClosed_supClosure
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ t)

Tactic:
hC.mem_supClosure_iff.mpr <| hC.exists_finpartition_diff hs ht

Premises used: Iff.mpr, MeasureTheory.IsSetSemiring.mem_supClosure_iff, MeasureTheory.IsSetSemiring.exists_finpartition_diff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s
T : Finset (Set α)
hT : T.Nonempty
hTC : (↑T : Set (Set α)) ⊆ C
rw : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup' hT id)

Tactic:
rw [sup'_eq_sup]

Premises used: Finset.sup'_eq_sup
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s
hTC : (↑∅ : Set (Set α)) ⊆ C
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ sup ∅ id)

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
h : t ∉ T
ih :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (hTC : (↑T : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
s : Set α
hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s
hTC : (↑(Insert.insert t T) : Set (Set α)) ⊆ C
insert :
  Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    ((s \ t) \ T.sup id)
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (s \ (Insert.insert t T).sup id)

Tactic:
simp_rw [sup_insert, id, sup_eq_union, ← diff_diff]

Premises used: Finset.sup_insert, Set.sup_eq_union, id, Set.diff_diff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
h : t ∉ T
ih :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (hTC : (↑T : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
s : Set α
hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s
hTC : (↑(insert t T) : Set (Set α)) ⊆ C
⊢ t ∈ C ∧ (↑T : Set (Set α)) ⊆ C

Tactic:
rw [coe_insert, insert_subset_iff] at hTC

Premises used: Set.insert_subset_iff, Finset.coe_insert
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
h : t ∉ T
ih :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (hTC : (↑T : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
s : Set α
hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s
hTC : t ∈ C ∧ (↑T : Set (Set α)) ⊆ C
⊢ t ∈ C

Tactic:
obtain ⟨htC, hTC⟩ := hTC
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
h : t ∉ T
ih :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (hTC : (↑T : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
s : Set α
hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s
hTC : t ∈ C ∧ (↑T : Set (Set α)) ⊆ C
htC : t ∈ C
⊢ (↑T : Set (Set α)) ⊆ C

Tactic:
obtain ⟨htC, hTC⟩ := hTC
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
h : t ∉ T
ih :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (hTC : (↑T : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
s : Set α
hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s
htC : t ∈ C
hTC : (↑T : Set (Set α)) ⊆ C
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    ((s \ t) \ T.sup id)

Tactic:
ih ?_ hTC
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
h : t ∉ T
ih :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (hTC : (↑T : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
s : Set α
hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s
htC : t ∈ C
hTC : (↑T : Set (Set α)) ⊆ C
insert : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ t)
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    ((s \ t) \ T.sup id)

Tactic:
refine ih ?_ hTC
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
h : t ∉ T
ih :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (hTC : (↑T : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
s : Set α
hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s
htC : t ∈ C
hTC : (↑T : Set (Set α)) ⊆ C
insert :
  ∀ (S : Finset (Set α)) (hS : S.Nonempty) (hSC : (↑S : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
      (S.sup' hS id \ t)
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ t)

Tactic:
obtain ⟨S, hS, hSC, rfl⟩ := hs

Premises used: rfl
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
h : t ∉ T
ih :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (hTC : (↑T : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
htC : t ∈ C
hTC : (↑T : Set (Set α)) ⊆ C
S : Finset (Set α)
hS : S.Nonempty
hSC : (↑S : Set (Set α)) ⊆ C
insert :
  Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (S.sup fun (b : Set α) ↦ id b \ t)
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (S.sup' hS id \ t)

Tactic:
rw [sup'_eq_sup, ← Finset.sup_sdiff_right]

Premises used: Finset.sup_sdiff_right, Finset.sup'_eq_sup
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
h : t ∉ T
ih :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (hTC : (↑T : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
htC : t ∈ C
hTC : (↑T : Set (Set α)) ⊆ C
S : Finset (Set α)
hS : S.Nonempty
hSC : (↑S : Set (Set α)) ⊆ C
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (S.sup fun (b : Set α) ↦ id b \ t)

Tactic:
supClosed_supClosure.finsetSup_mem hS fun s hs => ?_

Premises used: Set.Mem, setOf, SupClosed.finsetSup_mem, supClosed_supClosure
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
h : t ∉ T
ih :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (hTC : (↑T : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
htC : t ∈ C
hTC : (↑T : Set (Set α)) ⊆ C
S : Finset (Set α)
hS : S.Nonempty
hSC : (↑S : Set (Set α)) ⊆ C
insert :
  ∀ (s : Set α) (hs : s ∈ S),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (id s \ t)
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (S.sup fun (b : Set α) ↦ id b \ t)

Tactic:
refine supClosed_supClosure.finsetSup_mem hS fun s hs => ?_

Premises used: SupClosed.finsetSup_mem, supClosed_supClosure
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
h : t ∉ T
ih :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (hTC : (↑T : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
htC : t ∈ C
hTC : (↑T : Set (Set α)) ⊆ C
S : Finset (Set α)
hS : S.Nonempty
hSC : (↑S : Set (Set α)) ⊆ C
s : Set α
hs : s ∈ S
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (id s \ t)

Tactic:
hC.diff_mem_supClosure (hSC hs) htC

Premises used: Set.Mem, setOf, MeasureTheory.IsSetSemiring.diff_mem_supClosure
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
t : Set α
T : Finset (Set α)
h : t ∉ T
ih :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (hTC : (↑T : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
htC : t ∈ C
hTC : (↑T : Set (Set α)) ⊆ C
S : Finset (Set α)
hS : S.Nonempty
hSC : (↑S : Set (Set α)) ⊆ C
s : Set α
hs : s ∈ S
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (id s \ t)

Tactic:
exact hC.diff_mem_supClosure (hSC hs) htC

Premises used: MeasureTheory.IsSetSemiring.diff_mem_supClosure