awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧
      (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
have hJ'_subset : (↑J' : Set (Set α)) ⊆ C
Tactic: have hJ'_subset : ↑J' ⊆ C := by
    intro u
    simp only [J', univ_eq_attach, coe_biUnion, mem_coe, mem_attach, iUnion_true,
      mem_iUnion, Finset.exists_coe, exists₂_imp]
    intro v hv huvt
    exact hJu_subset v (h_ss hv) huvt
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧
      (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
have insert : (↑J' : Set (Set α)).PairwiseDisjoint id
Tactic: refine ⟨J', hJ'_subset, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : Insert.insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
insert : (↑J' : Set (Set α)).PairwiseDisjoint id
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧
      (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
have insert₁ : s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
Tactic: refine ⟨J', hJ'_subset, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
⊢ (↑J' : Set (Set α)).PairwiseDisjoint id
have insert : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ (↑Finset.univ : Set ↥J), (↑(Ju (↑x : Set α) sorry) : Set (Set α))) id
Tactic: rw [Finset.coe_biUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
⊢ PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ (↑Finset.univ : Set ↥J), (↑(Ju (↑x : Set α) ⋯) : Set (Set α))) id
have insert : (↑Finset.univ : Set ↥J).PairwiseDisjoint (α := Set α) fun (i' : ↥J) ↦ ⨆ i ∈ (↑(Ju (↑i' : Set α) sorry) : Set (Set α)), id i
Tactic: refine PairwiseDisjoint.biUnion ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : Insert.insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
insert :
  (↑Finset.univ : Set ↥J).PairwiseDisjoint (α := Set α) fun (i' : ↥J) ↦
    ⨆ i ∈ (↑(Ju (↑i' : Set α) ⋯) : Set (Set α)), id i
⊢ PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ (↑Finset.univ : Set ↥J), (↑(Ju (↑x : Set α) ⋯) : Set (Set α))) id
have insert₁ : ∀ i ∈ (↑Finset.univ : Set ↥J), (↑(Ju (↑i : Set α) sorry) : Set (Set α)).PairwiseDisjoint id
Tactic: refine PairwiseDisjoint.biUnion ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
x : ↥J
h_2 : x ∈ (↑J.attach : Set ↥J)
y : ↥J
h_3 : y ∈ (↑J.attach : Set ↥J)
hxy : x ≠ y
⊢ Disjoint (↑x : Set α) (↑y : Set α)
have by_contra : ∀ (h_contra : ¬Disjoint (↑x : Set α) (↑y : Set α)), False
Tactic: by_contra h_contra
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
x : ↥J
h_2 : x ∈ (↑J.attach : Set ↥J)
y : ↥J
h_3 : y ∈ (↑J.attach : Set ↥J)
hxy : x ≠ y
h_contra : ¬Disjoint (↑x : Set α) (↑y : Set α)
⊢ False
have refine : x = y
Tactic: refine hxy ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
x : ↥J
h_2 : x ∈ (↑J.attach : Set ↥J)
y : ↥J
h_3 : y ∈ (↑J.attach : Set ↥J)
hxy : x ≠ y
h_contra : ¬Disjoint (↑x : Set α) (↑y : Set α)
⊢ x = y
have refine : (↑x : Set α) = (↑y : Set α)
Tactic: refine Subtype.ext ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
x : ↥J
h_2 : x ∈ (↑J.attach : Set ↥J)
y : ↥J
h_3 : y ∈ (↑J.attach : Set ↥J)
hxy : x ≠ y
⊢ Function.onFun (β := Set α) Disjoint (fun (i' : ↥J) ↦ ⋃ i ∈ Ju (↑i' : Set α) ⋯, i) x y
have hxy_disj : Disjoint (↑x : Set α) (↑y : Set α)
Tactic: have hxy_disj : Disjoint (x : Set α) y := by
        by_contra h_contra
        refine hxy ?_
        refine Subtype.ext ?_
        exact h_dis.elim x.prop y.prop h_contra
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
x : ↥J
h_2 : x ∈ (↑J.attach : Set ↥J)
y : ↥J
h_3 : y ∈ (↑J.attach : Set ↥J)
hxy : x ≠ y
hxy_disj : Disjoint (↑x : Set α) (↑y : Set α)
⊢ Function.onFun (β := Set α) Disjoint (fun (i' : ↥J) ↦ ⋃ i ∈ Ju (↑i' : Set α) ⋯, i) x y
have h₁ : (fun (i' : ↥J) ↦ (⋃ i ∈ Ju (↑i' : Set α) sorry, i : Set α)) x = ⋃₀ (↑(Ju (↑x : Set α) sorry) : Set (Set α))
Tactic: convert! hJu_disj' (x : Set α) (h_ss x.prop) y (h_ss y.prop) hxy_disj
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
x : ↥J
h_2 : x ∈ (↑J.attach : Set ↥J)
y : ↥J
h_3 : y ∈ (↑J.attach : Set ↥J)
hxy : x ≠ y
hxy_disj : Disjoint (↑x : Set α) (↑y : Set α)
h₁ : (fun (i' : ↥J) ↦ (⋃ i ∈ Ju (↑i' : Set α) ⋯, i : Set α)) x = ⋃₀ (↑(Ju (↑x : Set α) ⋯) : Set (Set α))
⊢ Function.onFun (β := Set α) Disjoint (fun (i' : ↥J) ↦ ⋃ i ∈ Ju (↑i' : Set α) ⋯, i) x y
have h₂ : (fun (i' : ↥J) ↦ (⋃ i ∈ Ju (↑i' : Set α) sorry, i : Set α)) y = ⋃₀ (↑(Ju (↑y : Set α) sorry) : Set (Set α))
Tactic: convert! hJu_disj' (x : Set α) (h_ss x.prop) y (h_ss y.prop) hxy_disj
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
x : ↥J
h_2 : x ∈ (↑J.attach : Set ↥J)
y : ↥J
h_3 : y ∈ (↑J.attach : Set ↥J)
hxy : x ≠ y
hxy_disj : Disjoint (↑x : Set α) (↑y : Set α)
⊢ (fun (i' : ↥J) ↦ (⋃ i ∈ Ju (↑i' : Set α) ⋯, i : Set α)) x = ⋃₀ (↑(Ju (↑x : Set α) ⋯) : Set (Set α))
have h₁ : Eq.{u_1 + 1} (α := Set α) ((fun (i' : ↥J) ↦ (⋃ i ∈ Ju (↑i' : Set α) sorry, i : Set α)) x)
  (⋃ i ∈ (↑(Ju (↑x : Set α) sorry) : Set (Set α)), i)
Tactic: rw [sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
x : ↥J
h_2 : x ∈ (↑J.attach : Set ↥J)
y : ↥J
h_3 : y ∈ (↑J.attach : Set ↥J)
hxy : x ≠ y
hxy_disj : Disjoint (↑x : Set α) (↑y : Set α)
⊢ (fun (i' : ↥J) ↦ (⋃ i ∈ Ju (↑i' : Set α) ⋯, i : Set α)) y = ⋃₀ (↑(Ju (↑y : Set α) ⋯) : Set (Set α))
have h₁ : Eq.{u_1 + 1} (α := Set α) ((fun (i' : ↥J) ↦ (⋃ i ∈ Ju (↑i' : Set α) sorry, i : Set α)) y)
  (⋃ i ∈ (↑(Ju (↑y : Set α) sorry) : Set (Set α)), i)
Tactic: rw [sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
⊢ s \ ⋃₀ (↑(insert t I') : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
have insert : ⋃₀ (↑J : Set (Set α)) \ t = ⋃₀ (↑J' : Set (Set α))
Tactic: rw [coe_insert, sUnion_insert, Set.union_comm, ← Set.diff_diff, h_eq]