awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
S : Finset (Set α)
hSC : (↑S : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
have empty : ∀ (hSC : (↑∅ : Set (Set α)) ⊆ C),
  ∃ (P : Finpartition (α := Set α) (sup ∅ id)), (↑(P.parts (a := 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⟩
Cleared hypotheses: S, hSC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : Set (Set α)) ⊆ C
have 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 s S) : Set (Set α)) ⊆ C),
      ∃ (P : Finpartition ((insert s S).sup id)), (↑(P.parts (a := (insert s 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⟩
Cleared hypotheses: S, hSC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring 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
have 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
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⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s →
    ∃ (P : Finpartition s), (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
have 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
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⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s →
    ∃ (P : Finpartition s), (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
have rintro₂ : ∀ (S : Finset (Set α)) (hSC : (↑S : Set (Set α)) ⊆ C),
  ∃ (P : Finpartition (S.sup id)), (↑(P.parts (a := S.sup id)) : 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⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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 α)) s
have rw : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
  (⋃₀ (↑(P.parts (a := s)) : Set (Set α)))
Tactic: rw [← P.sup_parts, sup_id_set_eq_sUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup' hT id)
have rw : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
Tactic: rw [sup'_eq_sup]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (s \ (insert t T).sup id)
have insert : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) ((s \ t) \ T.sup id)
Tactic: simp_rw [sup_insert, id, sup_eq_union, ← diff_diff]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
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
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    ((s \ t) \ T.sup id)
have hTC₁ : t ∈ C ∧ (↑T : Set (Set α)) ⊆ C
Tactic: rw [coe_insert, insert_subset_iff] at hTC
Cleared hypotheses: hTC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
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
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    ((s \ t) \ T.sup id)
have htC : t ∈ C
Tactic: obtain ⟨htC, hTC⟩ := hTC
Cleared hypotheses: hTC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
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
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    ((s \ t) \ T.sup id)
have hTC₁ : (↑T : Set (Set α)) ⊆ C
Tactic: obtain ⟨htC, hTC⟩ := hTC
Cleared hypotheses: hTC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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)
have insert : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ t)
Tactic: refine ih ?_ hTC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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)
have 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)
Tactic: obtain ⟨S, hS, hSC, rfl⟩ := hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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' hS id \ t)
have insert : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
  (S.sup fun (b : Set α) ↦ id b \ t)
Tactic: rw [sup'_eq_sup, ← Finset.sup_sdiff_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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)
have insert : ∀ (s : Set α) (hs : s ∈ S),
  Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (id s \ t)
Tactic: refine supClosed_supClosure.finsetSup_mem hS fun s hs => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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 α)
hTC : (↑T : Set (Set α)) ⊆ C
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
have empty : ∀ ⦃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: induction T using Finset.induction generalizing s with
    | empty => simpa
    | insert t T _ ih =>
      simp_rw [sup_insert, id, sup_eq_union, ← diff_diff]
      rw [coe_insert, insert_subset_iff] at hTC
      obtain ⟨htC, hTC⟩ := hTC
      refine ih ?_ hTC
      obtain ⟨S, hS, hSC, rfl⟩ := hs
      rw [sup'_eq_sup, ← Finset.sup_sdiff_right]
      refine supClosed_supClosure.finsetSup_mem hS fun s hs => ?_
      exact hC.diff_mem_supClosure (hSC hs) htC
Cleared hypotheses: s, hs, T, hTC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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 α)
hTC : (↑T : Set (Set α)) ⊆ C
empty :
  ∀ ⦃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)
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
have insert : ∀ (t : Set α) (T : Finset (Set α)),
  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),
      Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
        (s \ (insert t T).sup id)
Tactic: induction T using Finset.induction generalizing s with
    | empty => simpa
    | insert t T _ ih =>
      simp_rw [sup_insert, id, sup_eq_union, ← diff_diff]
      rw [coe_insert, insert_subset_iff] at hTC
      obtain ⟨htC, hTC⟩ := hTC
      refine ih ?_ hTC
      obtain ⟨S, hS, hSC, rfl⟩ := hs
      rw [sup'_eq_sup, ← Finset.sup_sdiff_right]
      refine supClosed_supClosure.finsetSup_mem hS fun s hs => ?_
      exact hC.diff_mem_supClosure (hSC hs) htC
Cleared hypotheses: s, hs, T, hTC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
⊢ ∀ ⦃s t : Set α⦄,
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s →
      Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t →
        Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ t)
have rintro : ∀ ⦃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),
  Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup' hT id)
Tactic: classical
    rintro s _ hs ⟨T, hT, hTC, rfl⟩
    rw [sup'_eq_sup]
    clear hT
    induction T using Finset.induction generalizing s with
    | empty => simpa
    | insert t T _ ih =>
      simp_rw [sup_insert, id, sup_eq_union, ← diff_diff]
      rw [coe_insert, insert_subset_iff] at hTC
      obtain ⟨htC, hTC⟩ := hTC
      refine ih ?_ hTC
      obtain ⟨S, hS, hSC, rfl⟩ := hs
      rw [sup'_eq_sup, ← Finset.sup_sdiff_right]
      refine supClosed_supClosure.finsetSup_mem hS fun s hs => ?_
      exact hC.diff_mem_supClosure (hSC hs) htC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
rintro :
  ∀ ⦃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),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
      (s \ T.sup' hT id)
⊢ ∀ ⦃s t : Set α⦄,
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s →
      Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t →
        Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ t)
have rintro₁ : ∀ ⦃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),
  Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
Tactic: classical
    rintro s _ hs ⟨T, hT, hTC, rfl⟩
    rw [sup'_eq_sup]
    clear hT
    induction T using Finset.induction generalizing s with
    | empty => simpa
    | insert t T _ ih =>
      simp_rw [sup_insert, id, sup_eq_union, ← diff_diff]
      rw [coe_insert, insert_subset_iff] at hTC
      obtain ⟨htC, hTC⟩ := hTC
      refine ih ?_ hTC
      obtain ⟨S, hS, hSC, rfl⟩ := hs
      rw [sup'_eq_sup, ← Finset.sup_sdiff_right]
      refine supClosed_supClosure.finsetSup_mem hS fun s hs => ?_
      exact hC.diff_mem_supClosure (hSC hs) htC
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
rintro :
  ∀ ⦃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),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
      (s \ T.sup' hT id)
rintro₁ :
  ∀ ⦃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),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
⊢ ∀ ⦃s t : Set α⦄,
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s →
      Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t →
        Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ t)
have rintro₂ : ∀ ⦃s : Set α⦄
  (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
  (T : Finset (Set α)) (hTC : (↑T : Set (Set α)) ⊆ C),
  Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
Tactic: classical
    rintro s _ hs ⟨T, hT, hTC, rfl⟩
    rw [sup'_eq_sup]
    clear hT
    induction T using Finset.induction generalizing s with
    | empty => simpa
    | insert t T _ ih =>
      simp_rw [sup_insert, id, sup_eq_union, ← diff_diff]
      rw [coe_insert, insert_subset_iff] at hTC
      obtain ⟨htC, hTC⟩ := hTC
      refine ih ?_ hTC
      obtain ⟨S, hS, hSC, rfl⟩ := hs
      rw [sup'_eq_sup, ← Finset.sup_sdiff_right]
      refine supClosed_supClosure.finsetSup_mem hS fun s hs => ?_
      exact hC.diff_mem_supClosure (hSC hs) htC