awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∀ (t : Set α) (ht : t ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))),
    t ⊆ s \ ⋃₀ (↑I : Set (Set α))
have rw : ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ s \ ⋃₀ (↑I : Set (Set α))
Tactic: rw [← sUnion_subset_iff, hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion hs hI]
-- 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
rw : ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ s \ ⋃₀ (↑I : Set (Set α))
⊢ ∀ (t : Set α) (ht : t ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))),
    t ⊆ s \ ⋃₀ (↑I : Set (Set α))
have rw₁ : ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆
  ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
Tactic: rw [← sUnion_subset_iff, hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion hs hI]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
I : Finset (Set α)
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
t : Set α
ht : t ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
⊢ t ⊆ s
have apply : s \ ⋃₀ (↑I : Set (Set α)) ≤ s
Tactic: apply le_trans <| hC.subset_of_diffUnion_disjointOfDiffUnion hs hI t 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 : (↑I : Set (Set α)) ⊆ C
⊢ Disjoint (⋃₀ (↑I : Set (Set α))) (⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)))
have rw : Disjoint (⋃₀ (↑I : Set (Set α))) (s \ ⋃₀ (↑I : Set (Set α)))
Tactic: rw [← hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion]
-- 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
⊢ Disjoint I (hC.disjointOfDiffUnion (C := C) (s := s) hs hI)
have by_contra : ∀ (h : ¬Disjoint I (hC.disjointOfDiffUnion (C := C) (s := s) hs hI)), False
Tactic: by_contra h
-- 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
hI : (↑I : Set (Set α)) ⊆ C
h : ¬Disjoint I (hC.disjointOfDiffUnion (C := C) (s := s) hs hI)
⊢ False
have h₁ : ∃ a ∈ I, a ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
Tactic: rw [Finset.not_disjoint_iff] at h
Cleared hypotheses: h
-- 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
h : ∃ a ∈ I, a ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
⊢ False
have obtain : ∀ (u : Set α) (huI : u ∈ I) (hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI), False
Tactic: obtain ⟨u, huI, hu_disjointOfDiffUnion⟩ := h
Cleared hypotheses: h
-- 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
hI : (↑I : Set (Set α)) ⊆ C
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
⊢ False
have h_disj : u ≤ ⊥
Tactic: have h_disj : u ≤ ⊥ :=
    hC.disjoint_sUnion_disjointOfDiffUnion hs hI (subset_sUnion_of_mem huI)
    (subset_sUnion_of_mem hu_disjointOfDiffUnion)
-- 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
hI : (↑I : Set (Set α)) ⊆ C
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
h_disj : u ≤ ⊥
⊢ False
have h_disj₁ : u = ∅
Tactic: simp only [Set.bot_eq_empty, Set.le_eq_subset, subset_empty_iff] at h_disj
Cleared hypotheses: h_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
hI : (↑I : Set (Set α)) ⊆ C
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
h_disj : u = ∅
⊢ False
have refine : ∅ ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
Tactic: refine hC.empty_notMem_disjointOfDiffUnion hs hI ?_
-- 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
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
h_disj : u = ∅
⊢ ∅ ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
have rwa : ∀ (hu_disjointOfDiffUnion : ∅ ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) (h_disj : u = ∅),
  ∅ ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
Tactic: rwa [h_disj] at hu_disjointOfDiffUnion
Cleared hypotheses: hu_disjointOfDiffUnion, h_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
hI : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
⊢ ((↑I : Set (Set α)) ∪ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))).PairwiseDisjoint id
have rw : (↑I : Set (Set α)).PairwiseDisjoint id ∧
  (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)).PairwiseDisjoint id ∧
    ∀ ⦃i : Set α⦄,
      i ∈ (↑I : Set (Set α)) →
        ∀ ⦃j : Set α⦄,
          j ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) → i ≠ j → Disjoint (id i) (id j)
Tactic: rw [pairwiseDisjoint_union]
-- 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
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
⊢ (↑I : Set (Set α)).PairwiseDisjoint id ∧
    (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)).PairwiseDisjoint id ∧
      ∀ ⦃i : Set α⦄,
        i ∈ (↑I : Set (Set α)) →
          ∀ ⦃j : Set α⦄,
            j ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) → i ≠ j → Disjoint (id i) (id j)
have refine : ∀ (u : Set α) (hu : u ∈ (↑I : Set (Set α))) (v : Set α)
  (hv : v ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))), u ≠ v → Disjoint (id u) (id v)
Tactic: refine ⟨h_dis, hC.pairwiseDisjoint_disjointOfDiffUnion hs hI, fun u hu v hv _ ↦ ?_⟩
-- 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
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
u : Set α
hu : u ∈ (↑I : Set (Set α))
v : Set α
hv : v ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
h : u ≠ v
⊢ Disjoint (id u) (id v)
have simp_rw : Disjoint u v
Tactic: simp_rw [id]
-- 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
hI_ss : ∀ t ∈ I, t ⊆ s
| s
have rw : ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
Tactic: rw [← union_diff_cancel (Set.sUnion_subset hI_ss : ⋃₀ ↑I ⊆ s),
    hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion hs hI]
-- 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
hI_ss : ∀ t ∈ I, t ⊆ s
⊢ ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) = s
have conv_rhs : ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) = s
Tactic: conv_rhs => rw [← union_diff_cancel (Set.sUnion_subset hI_ss : ⋃₀ ↑I ⊆ s),
    hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion hs hI]
-- 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
hI_ss : ∀ t ∈ I, t ⊆ s
conv_rhs : ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) = s
⊢ ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) = s
have conv_rhs₁ : ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) =
  ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
Tactic: conv_rhs => rw [← union_diff_cancel (Set.sUnion_subset hI_ss : ⋃₀ ↑I ⊆ s),
    hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion hs hI]
-- 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
hI_ss : ∀ t ∈ I, t ⊆ s
| s
have rw : ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
Tactic: rw [← sUnion_union_sUnion_disjointOfDiffUnion_of_subset hC hs hI hI_ss]
-- 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
hI_ss : ∀ t ∈ I, t ⊆ s
⊢ ⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) = s
have conv_rhs : ⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) =
  ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
Tactic: conv_rhs => rw [← sUnion_union_sUnion_disjointOfDiffUnion_of_subset hC hs hI hI_ss]
-- 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
hI_ss : ∀ t ∈ I, t ⊆ s
⊢ ⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) =
    ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
have simp_rw : ⋃₀ ((↑I : Set (Set α)) ∪ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
  ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
Tactic: simp_rw [coe_union]
-- 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
hI_ss : ∀ t ∈ I, t ⊆ s
⊢ ⋃₀ ((↑I : Set (Set α)) ∪ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
    ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
have rw : ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) =
  ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
Tactic: rw [sUnion_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
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 : (↑(cons s J hJ) : Set (Set α)) ⊆ C
⊢ ∃ (K : Set α → Finset (Set α)),
    (↑(cons s J hJ) : Set (Set α)).PairwiseDisjoint K ∧
      (∀ i ∈ cons s J hJ, (↑(K i) : Set (Set α)) ⊆ C) ∧
        PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ cons s J hJ, (↑(K x) : Set (Set α))) id ∧
          (∀ j ∈ cons s J hJ, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
            (∀ j ∈ cons s J hJ, ∅ ∉ K j) ∧
              ⋃₀ (↑(cons s J hJ) : Set (Set α)) = ⋃₀ ⋃ x ∈ cons s J hJ, (↑(K x) : Set (Set α))
have h1₁ : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
Tactic: rw [cons_eq_insert, coe_insert, Set.insert_subset_iff] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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 α)),
    (↑(cons s J hJ) : Set (Set α)).PairwiseDisjoint K ∧
      (∀ i ∈ cons s J hJ, (↑(K i) : Set (Set α)) ⊆ C) ∧
        PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ cons s J hJ, (↑(K x) : Set (Set α))) id ∧
          (∀ j ∈ cons s J hJ, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
            (∀ j ∈ cons s J hJ, ∅ ∉ K j) ∧
              ⋃₀ (↑(cons s J hJ) : Set (Set α)) = ⋃₀ ⋃ x ∈ cons s J hJ, (↑(K x) : Set (Set α))
have cons : ∀ (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 α))),
  ∃ (K : Set α → Finset (Set α)),
    (↑(cons s J hJ) : Set (Set α)).PairwiseDisjoint K ∧
      (∀ i ∈ cons s J hJ, (↑(K i) : Set (Set α)) ⊆ C) ∧
        PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ cons s J hJ, (↑(K x) : Set (Set α))) id ∧
          (∀ j ∈ cons s J hJ, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
            (∀ j ∈ cons s J hJ, ∅ ∉ K j) ∧
              ⋃₀ (↑(cons s J hJ) : Set (Set α)) = ⋃₀ ⋃ x ∈ cons s J hJ, (↑(K x) : Set (Set α))
Tactic: obtain ⟨K, hK0, ⟨hK1, hK2, hK3, hK4, hK5⟩⟩ := hind h1.2
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
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
⊢ ∃ (K : Set α → Finset (Set α)),
    (↑(cons s J hJ) : Set (Set α)).PairwiseDisjoint K ∧
      (∀ i ∈ cons s J hJ, (↑(K i) : Set (Set α)) ⊆ C) ∧
        PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ cons s J hJ, (↑(K x) : Set (Set α))) id ∧
          (∀ j ∈ cons s J hJ, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
            (∀ j ∈ cons s J hJ, ∅ ∉ K j) ∧
              ⋃₀ (↑(cons s J hJ) : Set (Set α)) = ⋃₀ ⋃ x ∈ cons s J hJ, (↑(K x) : Set (Set α))
have hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) sorry sorry
Tactic: have hK1s : K1 s = hC.disjointOfDiffUnion h1.1 h1.2 := by simp [K1]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
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) ⋯ ⋯
⊢ ∃ (K : Set α → Finset (Set α)),
    (↑(cons s J hJ) : Set (Set α)).PairwiseDisjoint K ∧
      (∀ i ∈ cons s J hJ, (↑(K i) : Set (Set α)) ⊆ C) ∧
        PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ cons s J hJ, (↑(K x) : Set (Set α))) id ∧
          (∀ j ∈ cons s J hJ, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
            (∀ j ∈ cons s J hJ, ∅ ∉ K j) ∧
              ⋃₀ (↑(cons s J hJ) : Set (Set α)) = ⋃₀ ⋃ x ∈ cons s J hJ, (↑(K x) : Set (Set α))
have hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
Tactic: have hK1_of_ne t (ht : t ≠ s) : K1 t = K t := by simp [K1, ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ ∃ (K : Set α → Finset (Set α)),
    (↑(cons s J hJ) : Set (Set α)).PairwiseDisjoint K ∧
      (∀ i ∈ cons s J hJ, (↑(K i) : Set (Set α)) ⊆ C) ∧
        PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ cons s J hJ, (↑(K x) : Set (Set α))) id ∧
          (∀ j ∈ cons s J hJ, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
            (∀ j ∈ cons s J hJ, ∅ ∉ K j) ∧
              ⋃₀ (↑(cons s J hJ) : Set (Set α)) = ⋃₀ ⋃ x ∈ cons s J hJ, (↑(K x) : Set (Set α))
have h : (↑(cons s J hJ) : Set (Set α)).PairwiseDisjoint K1 ∧
  (∀ i ∈ cons s J hJ, (↑(K1 i) : Set (Set α)) ⊆ C) ∧
    PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ cons s J hJ, (↑(K1 x) : Set (Set α))) id ∧
      (∀ j ∈ cons s J hJ, ⋃₀ (↑(K1 j) : Set (Set α)) ⊆ j) ∧
        (∀ j ∈ cons s J hJ, ∅ ∉ K1 j) ∧
          ⋃₀ (↑(cons s J hJ) : Set (Set α)) = ⋃₀ ⋃ x ∈ cons s J hJ, (↑(K1 x) : Set (Set α))
Tactic: use K1
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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
⊢ (↑(cons s J hJ) : Set (Set α)).PairwiseDisjoint K1 ∧
    (∀ i ∈ cons s J hJ, (↑(K1 i) : Set (Set α)) ⊆ C) ∧
      PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ cons s J hJ, (↑(K1 x) : Set (Set α))) id ∧
        (∀ j ∈ cons s J hJ, ⋃₀ (↑(K1 j) : Set (Set α)) ⊆ j) ∧
          (∀ j ∈ cons s J hJ, ∅ ∉ K1 j) ∧
            ⋃₀ (↑(cons s J hJ) : Set (Set α)) = ⋃₀ ⋃ x ∈ cons s J hJ, (↑(K1 x) : Set (Set α))
have h : (insert s (↑J : Set (Set α))).PairwiseDisjoint K1 ∧
  ((↑(K1 s) : Set (Set α)) ⊆ C ∧ ∀ a ∈ J, (↑(K1 a) : Set (Set α)) ⊆ C) ∧
    PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))) id ∧
      ((∀ t' ∈ K1 s, t' ⊆ s) ∧ ∀ a ∈ J, ∀ t' ∈ K1 a, t' ⊆ a) ∧
        (∅ ∉ K1 s ∧ ∀ a ∈ J, ∅ ∉ K1 a) ∧
          s ∪ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))
Tactic: simp only [cons_eq_insert,
      mem_coe, Finset.mem_insert, sUnion_subset_iff,
      forall_eq_or_imp, coe_insert, sUnion_insert]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
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
⊢ (insert s (↑J : Set (Set α))).PairwiseDisjoint K1 ∧
    ((↑(K1 s) : Set (Set α)) ⊆ C ∧ ∀ a ∈ J, (↑(K1 a) : Set (Set α)) ⊆ C) ∧
      PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))) id ∧
        ((∀ t' ∈ K1 s, t' ⊆ s) ∧ ∀ a ∈ J, ∀ t' ∈ K1 a, t' ⊆ a) ∧
          (∅ ∉ K1 s ∧ ∀ a ∈ J, ∅ ∉ K1 a) ∧
            s ∪ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))
have ht1' : ∀ x ∈ J, K1 x = K x
Tactic: have ht1' : ∀ x ∈ J, K1 x = K x := fun x hx ↦ hK1_of_ne _ (fun h_eq ↦ hJ (h_eq ▸ hx))