awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
a : Set α
ha : a ∈ J
⊢ ⋃₀ (↑(K a) : Set (Set α)) ⊆ a

Tactic:
hK3 a ha
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
a : Set α
ha : a ∈ J
⊢ ⋃₀ (↑(K a) : Set (Set α)) ⊆ a

Tactic:
exact hK3 a ha
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
⊢ ∅ ∉ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ ∧ ∀ a ∈ J, ∅ ∉ K1 a

Tactic:
⟨hC.empty_notMem_disjointOfDiffUnion h1.1 h1.2, ?_⟩

Premises used: And.right, And.left, MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiffUnion, And.intro
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
h : ∀ a ∈ J, ∅ ∉ K1 a
⊢ ∅ ∉ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ ∧ ∀ a ∈ J, ∅ ∉ K1 a

Tactic:
refine ⟨hC.empty_notMem_disjointOfDiffUnion h1.1 h1.2, ?_⟩
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
a : Set α
ha : a ∈ J
h : ∅ ∉ K a
⊢ ∅ ∉ K1 a

Tactic:
rw [ht1' a ha]
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
a : Set α
ha : a ∈ J
⊢ ∅ ∉ K a

Tactic:
hK4 a ha
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
a : Set α
ha : a ∈ J
⊢ ∅ ∉ K a

Tactic:
exact hK4 a ha
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
h :
  s ∪ ⋃₀ (↑J : Set (Set α)) =
    ⋃₀ (↑(if True then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K s) : Set (Set α)) ∪
      ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
⊢ s ∪ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))

Tactic:
simp only [iUnion_iUnion_eq_or_left, sUnion_union, ht2, K1]

Premises used: Set.iUnion_iUnion_eq_or_left, Set.sUnion_union
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
h :
  s ∪ ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α)) =
    (if True then s \ ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α)) else ⋃₀ (↑(K s) : Set (Set α))) ∪
      ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
⊢ s ∪ ⋃₀ (↑J : Set (Set α)) =
    ⋃₀ (↑(if True then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K s) : Set (Set α)) ∪
      ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))

Tactic:
simp_rw [apply_ite, hK5,
      ← hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion h1.1 h1.2, hK5]

Premises used: MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_disjointOfDiffUnion, apply_ite, And.right, And.left
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
⊢ s ∪ ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α)) =
    (if True then s \ ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α)) else ⋃₀ (↑(K s) : Set (Set α))) ∪
      ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))

Tactic:
simp only [↓reduceIte, diff_union_self]

Premises used: Set.diff_union_self, reduceIte
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : (↑J : Set (Set α)) ⊆ C
⊢ (↑J : Set (Set α)).PairwiseDisjoint (hC.disjointOfUnion (C := C) hJ)

Tactic:
(Exists.choose_spec (hC.disjointOfUnion_props hJ)).1

Premises used: Exists.choose_spec, MeasureTheory.IsSetSemiring.disjointOfUnion_props, And.left, MeasureTheory.IsSetSemiring.disjointOfUnion
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
j : Set α
J : Finset (Set α)
hC : IsSetSemiring C
hJ : (↑J : Set (Set α)) ⊆ C
hj : j ∈ J
⊢ (↑(hC.disjointOfUnion (C := C) hJ j) : Set (Set α)) ⊆ C

Tactic:
(Exists.choose_spec (hC.disjointOfUnion_props hJ)).2.1 _ hj

Premises used: Exists.choose_spec, MeasureTheory.IsSetSemiring.disjointOfUnion_props, setOf, And.right, And.left
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : (↑J : Set (Set α)) ⊆ C
⊢ PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) hJ x) : Set (Set α))) id

Tactic:
(Exists.choose_spec (hC.disjointOfUnion_props hJ)).2.2.1

Premises used: Exists.choose_spec, MeasureTheory.IsSetSemiring.disjointOfUnion_props, setOf, And.right, And.left
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
j : Set α
J : Finset (Set α)
hC : IsSetSemiring C
hJ : (↑J : Set (Set α)) ⊆ C
hj : j ∈ J
apply :
  (↑(hC.disjointOfUnion (C := C) hJ j) : Set (Set α)) ⊆ ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) hJ x) : Set (Set α))
⊢ (↑(hC.disjointOfUnion (C := C) hJ j) : Set (Set α)).PairwiseDisjoint id

Tactic:
apply PairwiseDisjoint.subset (hC.pairwiseDisjoint_biUnion_disjointOfUnion hJ)

Premises used: MeasureTheory.IsSetSemiring.pairwiseDisjoint_biUnion_disjointOfUnion, Set.PairwiseDisjoint.subset
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
j : Set α
J : Finset (Set α)
hC : IsSetSemiring C
hJ : (↑J : Set (Set α)) ⊆ C
hj : j ∈ J
⊢ (↑(hC.disjointOfUnion (C := C) hJ j) : Set (Set α)) ⊆ ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) hJ x) : Set (Set α))

Tactic:
subset_iUnion₂_of_subset j hj fun ⦃a⦄ a ↦ a

Premises used: Set.subset_iUnion₂_of_subset
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
j : Set α
J : Finset (Set α)
hC : IsSetSemiring C
hJ : (↑J : Set (Set α)) ⊆ C
hj : j ∈ J
⊢ (↑(hC.disjointOfUnion (C := C) hJ j) : Set (Set α)) ⊆ ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) hJ x) : Set (Set α))

Tactic:
exact subset_iUnion₂_of_subset j hj fun ⦃a⦄ a ↦ a

Premises used: Set.subset_iUnion₂_of_subset
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
j : Set α
J : Finset (Set α)
hC : IsSetSemiring C
hJ : (↑J : Set (Set α)) ⊆ C
hj : j ∈ J
⊢ ⋃₀ (↑(hC.disjointOfUnion (C := C) hJ j) : Set (Set α)) ⊆ j

Tactic:
(Exists.choose_spec (hC.disjointOfUnion_props hJ)).2.2.2.1 j hj

Premises used: Exists.choose_spec, MeasureTheory.IsSetSemiring.disjointOfUnion_props, setOf, And.right, And.left
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
j : Set α
J : Finset (Set α)
hC : IsSetSemiring C
hJ : (↑J : Set (Set α)) ⊆ C
hj : j ∈ J
x : Set α
hx : x ∈ hC.disjointOfUnion (C := C) hJ j
⊢ x ⊆ j

Tactic:
sUnion_subset_iff.mp (hC.disjointOfUnion_subset_of_mem hJ hj) x hx

Premises used: Set.sUnion_subset_iff, Iff.mp, MeasureTheory.IsSetSemiring.disjointOfUnion_subset_of_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
j : Set α
J : Finset (Set α)
hC : IsSetSemiring C
hJ : (↑J : Set (Set α)) ⊆ C
hj : j ∈ J
⊢ ∅ ∉ hC.disjointOfUnion (C := C) hJ j

Tactic:
(Exists.choose_spec (hC.disjointOfUnion_props hJ)).2.2.2.2.1 j hj

Premises used: Exists.choose_spec, Set.Mem, MeasureTheory.IsSetSemiring.disjointOfUnion_props, setOf, And.right, And.left
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : (↑J : Set (Set α)) ⊆ C
⊢ ⋃₀ ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) hJ x) : Set (Set α)) = ⋃₀ (↑J : Set (Set α))

Tactic:
(Exists.choose_spec (hC.disjointOfUnion_props hJ)).2.2.2.2.2.symm

Premises used: Exists.choose_spec, MeasureTheory.IsSetSemiring.disjointOfUnion_props, setOf, And.right, Eq.symm
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
u v : α
⊢ u ≤ max u v

Tactic:
grind
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
u v : α
⊢ Set.Ioc u v = Set.Ioc u (max u v)

Tactic:
grind
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
inhabit :
  ∀ (inhabited_h : Inhabited α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∅
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∅

Tactic:
inhabit α
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
inhabited_h : Inhabited α
⊢ Eq.{u_1 + 1} (α := Set α) ∅ (Set.Ioc default default)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
inhabited_h : Inhabited α
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∅

Tactic:
exact ⟨default, default, le_rfl, by simp⟩
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
rw :
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
    (Set.Ioc (max u u') (min v v'))
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
    (Set.Ioc u v ∩ Set.Ioc u' v')

Tactic:
rw [Set.Ioc_inter_Ioc]

Premises used: Set.Ioc_inter_Ioc
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
    (Set.Ioc (max u u') (min v v'))

Tactic:
apply Ioc_mem_setOf_Ioc_le

Premises used: _private.0.Set.Ioc_mem_setOf_Ioc_le
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
inl :
  ∀ (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 :
  ∀ (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 α))
⊢ ∃ (I : Finset (Set α)),
    (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∧
      (↑I : Set (Set α)).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ (↑I : Set (Set α))

Tactic:
rcases le_or_gt u' u with hu | hu

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

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

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

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

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

Tactic:
grind [coe_singleton, pairwiseDisjoint_singleton]

Premises used: Finset.coe_singleton, Set.pairwiseDisjoint_singleton