awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) ⊆ C
have simp : (↑(sorry.choose (p := fun (I : Finset (Set α)) ↦
        (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
    Set (Set α)) ⊆
  insert ∅ C
Tactic: simp only [disjointOfDiff, coe_sdiff, coe_singleton, diff_singleton_subset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) ⊆ C
have simp : (↑(sorry.choose (p := fun (I : Finset (Set α)) ↦
        (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
    Set (Set α)) ⊆
  insert ∅ C
Tactic: classical
  simp only [disjointOfDiff, coe_sdiff, coe_singleton, diff_singleton_subset_iff]
  exact (hC.diff_eq_sUnion' s hs t ht).choose_spec.1.trans (Set.subset_insert _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id
have simp : ((↑(sorry.choose (p := fun (I : Finset (Set α)) ↦
            (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
        Set (Set α)) \
      {∅}).PairwiseDisjoint
  id
Tactic: simp only [disjointOfDiff, coe_sdiff, coe_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id
have simp : ((↑(sorry.choose (p := fun (I : Finset (Set α)) ↦
            (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
        Set (Set α)) \
      {∅}).PairwiseDisjoint
  id
Tactic: classical
  simp only [disjointOfDiff, coe_sdiff, coe_singleton]
  exact Set.PairwiseDisjoint.subset (hC.diff_eq_sUnion' s hs t ht).choose_spec.2.1
      diff_subset
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) = s \ t
have rw : ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) =
  ⋃₀
    (↑(sorry.choose (p := fun (I : Finset (Set α)) ↦
          (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
      Set (Set α))
Tactic: rw [(hC.diff_eq_sUnion' s hs t ht).choose_spec.2.2]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) =
    ⋃₀
      (↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
            (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
        Set (Set α))
have simp : ⋃₀
    ((↑(sorry.choose (p := fun (I : Finset (Set α)) ↦
            (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
        Set (Set α)) \
      {∅}) =
  ⋃₀
    (↑(sorry.choose (p := fun (I : Finset (Set α)) ↦
          (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
      Set (Set α))
Tactic: simp only [disjointOfDiff, coe_sdiff, coe_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ⋃₀
      ((↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
              (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
          Set (Set α)) \
        {∅}) =
    ⋃₀
      (↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
            (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
        Set (Set α))
have rw : ⋃₀
    (↑(sorry.choose (p := fun (I : Finset (Set α)) ↦
          (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
      Set (Set α)) =
  ⋃₀
    (↑(sorry.choose (p := fun (I : Finset (Set α)) ↦
          (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
      Set (Set α))
Tactic: rw [sUnion_diff_singleton_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) = s \ t
have rw : ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) =
  ⋃₀
    (↑(sorry.choose (p := fun (I : Finset (Set α)) ↦
          (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
      Set (Set α))
Tactic: classical
  rw [(hC.diff_eq_sUnion' s hs t ht).choose_spec.2.2]
  simp only [disjointOfDiff, coe_sdiff, coe_singleton]
  rw [sUnion_diff_singleton_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
rw rw₁ rw₂ :
  ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) =
    ⋃₀
      (↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
            (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
        Set (Set α))
⊢ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) = s \ t
have rw₃ : ⋃₀
    ((↑(sorry.choose (p := fun (I : Finset (Set α)) ↦
            (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
        Set (Set α)) \
      {∅}) =
  ⋃₀
    (↑(sorry.choose (p := fun (I : Finset (Set α)) ↦
          (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
      Set (Set α))
Tactic: classical
  rw [(hC.diff_eq_sUnion' s hs t ht).choose_spec.2.2]
  simp only [disjointOfDiff, coe_sdiff, coe_singleton]
  rw [sUnion_diff_singleton_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
this : t ⊆ s \ t
⊢ False
have h : Disjoint t (s \ t)
Tactic: have h := @disjoint_sdiff_self_right _ t s _
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
this : t ⊆ s \ t
h : Disjoint t (s \ t)
⊢ False
have h₁ : t ≤ ⊥
Tactic: specialize h le_rfl this
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
this : t ⊆ s \ t
h : t ≤ ⊥
⊢ False
have h₁ : t = ∅
Tactic: simp only [Set.bot_eq_empty, Set.le_eq_subset, subset_empty_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
this : t ⊆ s \ t
h : t = ∅
⊢ False
have refine : ∅ ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
Tactic: refine hC.empty_notMem_disjointOfDiff hs ht ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
⊢ False
have suffices : t ⊆ s \ t
Tactic: suffices t ⊆ s \ t by
    have h := @disjoint_sdiff_self_right _ t s _
    specialize h le_rfl this
    simp only [Set.bot_eq_empty, Set.le_eq_subset, subset_empty_iff] at h
    refine hC.empty_notMem_disjointOfDiff hs ht ?_
    rwa [← h]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
⊢ t ⊆ s \ t
have rw : t ⊆ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))
Tactic: rw [← hC.sUnion_disjointOfDiff hs ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : t ⊆ s
| s
have rw : t ∪ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))
Tactic: rw [← union_diff_cancel hst, ← hC.sUnion_disjointOfDiff hs ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : t ⊆ s
⊢ ⋃₀ insert t (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) = s
have conv_rhs : ⋃₀ insert t (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) =
  t ∪ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))
Tactic: conv_rhs => rw [← union_diff_cancel hst, ← hC.sUnion_disjointOfDiff hs ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ Disjoint t (⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)))
have rw : Disjoint t (s \ t)
Tactic: rw [hC.sUnion_disjointOfDiff]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ (insert t (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))).PairwiseDisjoint id
have h : (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id
Tactic: have h := hC.pairwiseDisjoint_disjointOfDiff hs ht
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id
⊢ (insert t (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))).PairwiseDisjoint id
have refine : ∀ (u : Set α) (hu : u ∈ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))), Disjoint (id t) (id u)
Tactic: refine PairwiseDisjoint.insert_of_notMem h (hC.notMem_disjointOfDiff hs ht) fun u hu ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id
u : Set α
hu : u ∈ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))
⊢ Disjoint (id t) (id u)
have simp_rw : Disjoint t u
Tactic: simp_rw [id]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id
u : Set α
hu : u ∈ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))
⊢ Disjoint t u
have refine : u ≤ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))
Tactic: refine Disjoint.mono_right ?_ (hC.disjoint_sUnion_disjointOfDiff hs ht)
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑∅ : Set (Set α)) ⊆ C
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑∅ : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
have empty : ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
Tactic: simp only [coe_empty, sUnion_empty, diff_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑∅ : Set (Set α)) ⊆ C
⊢ ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
have empty : (↑{s} : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑{s} : Set (Set α))
Tactic: refine ⟨{s}, singleton_subset_set_iff.mpr hs, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
have insert : ∀ (t : Set α) (I' : Finset (Set α)),
  t ∉ I' →
    ∀
      (h :
        ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
          ∃ (J : Finset (Set α)),
            (↑J : Set (Set α)) ⊆ C ∧
              (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))
      (hI : (↑(insert t I') : Set (Set α)) ⊆ C),
      ∃ (J : Finset (Set α)),
        (↑J : Set (Set α)) ⊆ C ∧
          (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Tactic: induction I using Finset.induction with
  | empty =>
    simp only [coe_empty, sUnion_empty, diff_empty]
    refine ⟨{s}, singleton_subset_set_iff.mpr hs, ?_⟩
    simp only [coe_singleton, pairwiseDisjoint_singleton, sUnion_singleton,
      and_self_iff]
  | insert t I' _ h => ?_
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : (↑(insert t I') : Set (Set α)) ⊆ C
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧
      (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
have hI₁ : insert t (↑I' : Set (Set α)) ⊆ C
Tactic: rw [coe_insert] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧
      (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
have ht : t ∈ C
Tactic: have ht : t ∈ C := hI (Set.mem_insert _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧
      (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
have insert : ∀ (J : Finset (Set α)) (h_ss : (↑J : Set (Set α)) ⊆ C) (h_dis : (↑J : Set (Set α)).PairwiseDisjoint id)
  (h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))),
  ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧
      (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Tactic: obtain ⟨J, h_ss, h_dis, h_eq⟩ := h ((Set.subset_insert _ _).trans hI)
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧
      (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
have hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
Tactic: have hJu_subset : ∀ (u) (hu : u ∈ C), ↑(Ju u hu) ⊆ C := by
    intro u hu x hx
    exact hC.subset_disjointOfDiff hu ht hx
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧
      (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
have hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
Tactic: have hJu_disj : ∀ (u) (hu : u ∈ C), (Ju u hu : Set (Set α)).PairwiseDisjoint id := fun u hu ↦
    hC.pairwiseDisjoint_disjointOfDiff hu ht
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧
      (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
have hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
Tactic: have hJu_sUnion : ∀ (u) (hu : u ∈ C), ⋃₀ (Ju u hu : Set (Set α)) = u \ t :=
    fun u hu ↦ hC.sUnion_disjointOfDiff hu ht
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
u : Set α
hu : u ∈ C
v : Set α
hv : v ∈ C
huv_disj : Disjoint u v
⊢ Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
have rw : Disjoint (u \ t) (v \ t)
Tactic: rw [hJu_sUnion, hJu_sUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧
      (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
have hJu_disj' : ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
  Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
Tactic: have hJu_disj' : ∀ (u) (hu : u ∈ C) (v) (hv : v ∈ C) (_h_dis : Disjoint u v),
      Disjoint (⋃₀ (Ju u hu : Set (Set α))) (⋃₀ ↑(Ju v hv)) := by
    intro u hu v hv huv_disj
    rw [hJu_sUnion, hJu_sUnion]
    exact disjoint_of_subset Set.diff_subset Set.diff_subset huv_disj
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
u : Set α
⊢ u ∈ (↑J' : Set (Set α)) → u ∈ C
have simp : ∀ (x : Set α) (h : x ∈ J), u ∈ Ju x sorry → u ∈ C
Tactic: simp only [J', univ_eq_attach, coe_biUnion, mem_coe, mem_attach, iUnion_true,
      mem_iUnion, Finset.exists_coe, exists₂_imp]