awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
i : Set α
hi : i ∈ K1 s
j x : Set α
hx : x ∈ J
h3 : j ∈ K1 x
h4 : ¬i = j
⊢ Disjoint i j
have ki : i ⊆ s \ ⋃₀ (↑J : Set (Set α))
Tactic: obtain ki : i ⊆ s \ ⋃₀ J := hC.subset_of_diffUnion_disjointOfDiffUnion h1.1 h1.2 _
          (hK1s ▸ hi)
-- 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
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
i : Set α
hi : i ∈ K1 s
j x : Set α
hx : x ∈ J
h3 : j ∈ K1 x
h4 : ¬i = j
ki : i ⊆ s \ ⋃₀ (↑J : Set (Set α))
⊢ Disjoint i j
have hx2 : j ⊆ x
Tactic: obtain hx2 : j ⊆ x := subset_trans (subset_sUnion_of_mem (ht1' x hx ▸ h3)) (hK3 x hx)
-- 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
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
i : Set α
hi : i ∈ K1 s
j x : Set α
hx : x ∈ J
h3 : j ∈ K1 x
h4 : ¬i = j
ki : i ⊆ s \ ⋃₀ (↑J : Set (Set α))
hx2 : j ⊆ x
⊢ Disjoint i j
have kj : j ⊆ ⋃₀ (↑J : Set (Set α))
Tactic: obtain kj : j ⊆ ⋃₀ J := hx2.trans <| subset_sUnion_of_mem hx
-- 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 α)))
a : Set α
ha : a ∈ J
⊢ ∀ t' ∈ K1 a, t' ⊆ a
have h : ∀ t' ∈ K a, t' ⊆ a
Tactic: simp_rw [hK1_of_ne _ (ne_of_mem_of_not_mem ha 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 α)))
a : Set α
ha : a ∈ J
⊢ ∀ t' ∈ (↑(K a) : Set (Set α)), t' ⊆ a
have h : ⋃₀ (↑(K a) : Set (Set α)) ⊆ a
Tactic: rw [← sUnion_subset_iff]
-- 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 α)))
⊢ ∅ ∉ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ ∧ ∀ a ∈ J, ∅ ∉ K1 a
have h : ∀ a ∈ J, ∅ ∉ K1 a
Tactic: refine ⟨hC.empty_notMem_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 α)))
a : Set α
ha : a ∈ J
⊢ ∅ ∉ K1 a
have h : ∅ ∉ K a
Tactic: rw [ht1' a ha]
-- 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 α)))
⊢ s ∪ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))
have h : s ∪ ⋃₀ (↑J : Set (Set α)) =
  ⋃₀ (↑(if True then hC.disjointOfDiffUnion (C := C) (s := s) sorry sorry else K s) : Set (Set α)) ∪
    ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
Tactic: simp only [iUnion_iUnion_eq_or_left, sUnion_union, ht2, 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
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 ∪ ⋃₀ (↑J : Set (Set α)) =
    ⋃₀ (↑(if True then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K s) : Set (Set α)) ∪
      ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
have 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 α))
Tactic: simp_rw [apply_ite, hK5,
      ← hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion h1.1 h1.2, hK5]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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 α)).PairwiseDisjoint id
have apply : (↑(hC.disjointOfUnion (C := C) hJ j) : Set (Set α)) ⊆ ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) hJ x) : Set (Set α))
Tactic: apply PairwiseDisjoint.subset (hC.pairwiseDisjoint_biUnion_disjointOfUnion hJ)
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∅
have inhabit : ∀ (inhabited_h : Inhabited α),
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} ∅
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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 u v ∩ Set.Ioc u' v')
have rw : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
  (Set.Ioc (max u u') (min v v'))
Tactic: rw [Set.Ioc_inter_Ioc]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : 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 α))
have 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 α))
Tactic: rcases le_or_gt u' u with hu | hu
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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 α))
⊢ ∃ (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 α))
have 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 α))
Tactic: rcases le_or_gt u' u with hu | hu
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
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 α))
have 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 α))
Tactic: rcases Ioc_mem_setOf_Ioc_le (max u v') v with ⟨u'', v'', h'', heq⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
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''
⊢ ∃ (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 α))
have 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 α))
Tactic: exists {Set.Ioc u'' v''}
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
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 α))
have inr : ∀ (hv : v ≤ 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 α))
Tactic: rcases le_or_gt v v' with hv | hv
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
inr :
  ∀ (hv : v ≤ 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 α))
have inr₁ : ∀ (hv : v' < 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 α))
Tactic: rcases le_or_gt v v' with hv | hv
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v ≤ 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 α))
have inr : ∀ (u'' v'' : α) (h'' : u'' ≤ v'') (heq : Set.Ioc u (min u' 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 α))
Tactic: rcases Ioc_mem_setOf_Ioc_le u (min u' v) with ⟨u'', v'', h'', heq⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v ≤ v'
u'' v'' : α
h'' : u'' ≤ v''
heq : Set.Ioc u (min u' 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 α))
have inr : (↑{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: exists {Set.Ioc u'' v''}
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < 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 α))
have inr : ∃ (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 u' ∪ Set.Ioc v' v = ⋃₀ (↑I : Set (Set α))
Tactic: rw [show Set.Ioc u v \ Set.Ioc u' v' = Set.Ioc u u' ∪ Set.Ioc v' v by grind]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < 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 u' ∪ Set.Ioc v' v = ⋃₀ (↑I : Set (Set α))
have inr : (↑{Set.Ioc u u', Set.Ioc v' v} : Set (Set α)).PairwiseDisjoint id
Tactic: refine ⟨{Set.Ioc u u', Set.Ioc v' v}, by grind, ?_, by simp⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
a : Set α
ha : a ∈ (↑{Set.Ioc u u', Set.Ioc v' v} : Set (Set α))
b : Set α
hb : b ∈ (↑{Set.Ioc u u', Set.Ioc v' v} : Set (Set α))
hab : a ≠ b
⊢ Function.onFun Disjoint id a b
have inr : Disjoint a b
Tactic: simp [Function.onFun]