awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ht1' : ∀ x ∈ J, K1 x = K x
⊢ Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
have h : ∀ (i : Set α) (j : i ∈ J), (↑(K1 i) : Set (Set α)) = (↑(K i) : Set (Set α))
Tactic: apply iUnion₂_congr
-- 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
ht1' : ∀ x ∈ J, K1 x = K x
⊢ (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 ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
Tactic: have ht2 : (⋃ x ∈ J, (K1 x : Set (Set α))) = ⋃ x ∈ J, ((K x : Set (Set α))) := by
      apply iUnion₂_congr
      intro x hx
      exact_mod_cast hK1_of_ne _ (ne_of_mem_of_not_mem hx hJ)
-- 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
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 α)))
⊢ (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 h : (insert s (↑J : Set (Set α))).PairwiseDisjoint K1 ∧
  ((↑(hC.disjointOfDiffUnion (C := C) (s := s) sorry sorry) : 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' ∈ hC.disjointOfDiffUnion (C := C) (s := s) sorry sorry, t' ⊆ s) ∧ ∀ a ∈ J, ∀ t' ∈ K1 a, t' ⊆ a) ∧
        (∅ ∉ hC.disjointOfDiffUnion (C := C) (s := s) sorry sorry ∧ ∀ a ∈ J, ∅ ∉ K1 a) ∧
          s ∪ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))
Tactic: simp only [hK1s]
-- 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
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 α)))
⊢ (insert s (↑J : Set (Set α))).PairwiseDisjoint K1 ∧
    ((↑(hC.disjointOfDiffUnion (C := C) (s := 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' ∈ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯, t' ⊆ s) ∧ ∀ a ∈ J, ∀ t' ∈ K1 a, t' ⊆ a) ∧
          (∅ ∉ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ ∧ ∀ a ∈ J, ∅ ∉ K1 a) ∧
            s ∪ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))
have h : (insert s (↑J : Set (Set α))).PairwiseDisjoint K1
Tactic: refine ⟨?_, ⟨hC.disjointOfDiffUnion_subset h1.1 h1.2, ?_⟩, ?_,
      ⟨hC.subset_of_mem_disjointOfDiffUnion h1.1 h1.2, ?_⟩, ?_, ?_⟩
-- 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
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 : (insert s (↑J : Set (Set α))).PairwiseDisjoint K1
⊢ (insert s (↑J : Set (Set α))).PairwiseDisjoint K1 ∧
    ((↑(hC.disjointOfDiffUnion (C := C) (s := 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' ∈ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯, t' ⊆ s) ∧ ∀ a ∈ J, ∀ t' ∈ K1 a, t' ⊆ a) ∧
          (∅ ∉ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ ∧ ∀ a ∈ J, ∅ ∉ K1 a) ∧
            s ∪ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))
have h₁ : ∀ a ∈ J, (↑(K1 a) : Set (Set α)) ⊆ C
Tactic: refine ⟨?_, ⟨hC.disjointOfDiffUnion_subset h1.1 h1.2, ?_⟩, ?_,
      ⟨hC.subset_of_mem_disjointOfDiffUnion h1.1 h1.2, ?_⟩, ?_, ?_⟩
-- 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
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 : (insert s (↑J : Set (Set α))).PairwiseDisjoint K1
h₁ : ∀ a ∈ J, (↑(K1 a) : Set (Set α)) ⊆ C
⊢ (insert s (↑J : Set (Set α))).PairwiseDisjoint K1 ∧
    ((↑(hC.disjointOfDiffUnion (C := C) (s := 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' ∈ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯, t' ⊆ s) ∧ ∀ a ∈ J, ∀ t' ∈ K1 a, t' ⊆ a) ∧
          (∅ ∉ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ ∧ ∀ a ∈ J, ∅ ∉ K1 a) ∧
            s ∪ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))
have h₂ : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))) id
Tactic: refine ⟨?_, ⟨hC.disjointOfDiffUnion_subset h1.1 h1.2, ?_⟩, ?_,
      ⟨hC.subset_of_mem_disjointOfDiffUnion h1.1 h1.2, ?_⟩, ?_, ?_⟩
-- 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
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 : (insert s (↑J : Set (Set α))).PairwiseDisjoint K1
h₁ : ∀ a ∈ J, (↑(K1 a) : Set (Set α)) ⊆ C
h₂ : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))) id
⊢ (insert s (↑J : Set (Set α))).PairwiseDisjoint K1 ∧
    ((↑(hC.disjointOfDiffUnion (C := C) (s := 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' ∈ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯, t' ⊆ s) ∧ ∀ a ∈ J, ∀ t' ∈ K1 a, t' ⊆ a) ∧
          (∅ ∉ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ ∧ ∀ a ∈ J, ∅ ∉ K1 a) ∧
            s ∪ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))
have h₃ : ∀ a ∈ J, ∀ t' ∈ K1 a, t' ⊆ a
Tactic: refine ⟨?_, ⟨hC.disjointOfDiffUnion_subset h1.1 h1.2, ?_⟩, ?_,
      ⟨hC.subset_of_mem_disjointOfDiffUnion h1.1 h1.2, ?_⟩, ?_, ?_⟩
-- 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
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 : (insert s (↑J : Set (Set α))).PairwiseDisjoint K1
h₁ : ∀ a ∈ J, (↑(K1 a) : Set (Set α)) ⊆ C
h₂ : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))) id
h₃ : ∀ a ∈ J, ∀ t' ∈ K1 a, t' ⊆ a
⊢ (insert s (↑J : Set (Set α))).PairwiseDisjoint K1 ∧
    ((↑(hC.disjointOfDiffUnion (C := C) (s := 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' ∈ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯, t' ⊆ s) ∧ ∀ a ∈ J, ∀ t' ∈ K1 a, t' ⊆ a) ∧
          (∅ ∉ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ ∧ ∀ a ∈ J, ∅ ∉ K1 a) ∧
            s ∪ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))
have h₄ : ∅ ∉ hC.disjointOfDiffUnion (C := C) (s := s) sorry sorry ∧ ∀ a ∈ J, ∅ ∉ K1 a
Tactic: refine ⟨?_, ⟨hC.disjointOfDiffUnion_subset h1.1 h1.2, ?_⟩, ?_,
      ⟨hC.subset_of_mem_disjointOfDiffUnion h1.1 h1.2, ?_⟩, ?_, ?_⟩
-- 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
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 : (insert s (↑J : Set (Set α))).PairwiseDisjoint K1
h₁ : ∀ a ∈ J, (↑(K1 a) : Set (Set α)) ⊆ C
h₂ : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))) id
h₃ : ∀ a ∈ J, ∀ t' ∈ K1 a, t' ⊆ a
h₄ : ∅ ∉ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ ∧ ∀ a ∈ J, ∅ ∉ K1 a
⊢ (insert s (↑J : Set (Set α))).PairwiseDisjoint K1 ∧
    ((↑(hC.disjointOfDiffUnion (C := C) (s := 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' ∈ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯, t' ⊆ s) ∧ ∀ a ∈ J, ∀ t' ∈ K1 a, t' ⊆ a) ∧
          (∅ ∉ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ ∧ ∀ a ∈ J, ∅ ∉ K1 a) ∧
            s ∪ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))
have h₅ : s ∪ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))
Tactic: refine ⟨?_, ⟨hC.disjointOfDiffUnion_subset h1.1 h1.2, ?_⟩, ?_,
      ⟨hC.subset_of_mem_disjointOfDiffUnion h1.1 h1.2, ?_⟩, ?_, ?_⟩
-- 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
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 α)))
⊢ (insert s (↑J : Set (Set α))).PairwiseDisjoint K1
have h : (↑J : Set (Set α)).Pairwise (Function.onFun Disjoint K1)
Tactic: apply Set.Pairwise.insert
-- 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
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 : (↑J : Set (Set α)).Pairwise (Function.onFun Disjoint K1)
⊢ (insert s (↑J : Set (Set α))).PairwiseDisjoint K1
have h₁ : ∀ b ∈ (↑J : Set (Set α)), s ≠ b → Function.onFun Disjoint K1 s b ∧ Function.onFun Disjoint K1 b s
Tactic: apply Set.Pairwise.insert
-- 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
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 α)))
j : Set α
hj : j ∈ (↑J : Set (Set α))
i : Set α
hi : i ∈ (↑J : Set (Set α))
hij : j ≠ i
⊢ Function.onFun Disjoint K1 j i
have h : Disjoint (K j) (K i)
Tactic: rw [Function.onFun, ht1' j hj, ht1' i hi]