awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.SetSemiring
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 :
  PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ (↑Finset.univ : Set ↥J), (↑(Ju (↑x : Set α) ⋯) : Set (Set α))) id
⊢ (↑J' : Set (Set α)).PairwiseDisjoint id

Tactic:
rw [Finset.coe_biUnion]

Premises used: Finset.coe_biUnion
-- Module: Mathlib.MeasureTheory.SetSemiring
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

Tactic:
PairwiseDisjoint.biUnion ?_ ?_

Premises used: Set.PairwiseDisjoint.biUnion
-- Module: Mathlib.MeasureTheory.SetSemiring
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
insert₁ : ∀ i ∈ (↑Finset.univ : Set ↥J), (↑(Ju (↑i : Set α) ⋯) : Set (Set α)).PairwiseDisjoint id
⊢ PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ (↑Finset.univ : Set ↥J), (↑(Ju (↑x : Set α) ⋯) : Set (Set α))) id

Tactic:
refine PairwiseDisjoint.biUnion ?_ ?_

Premises used: Set.PairwiseDisjoint.biUnion
-- Module: Mathlib.MeasureTheory.SetSemiring
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
x : ↥J
insert :
  x ∈ (↑J.attach : Set ↥J) →
    ∀ ⦃y : ↥J⦄,
      y ∈ (↑J.attach : Set ↥J) →
        x ≠ y → Function.onFun (β := Set α) Disjoint (fun (i' : ↥J) ↦ ⋃ i ∈ Ju (↑i' : Set α) ⋯, i) x y
⊢ x ∈ (↑J.attach : Set ↥J) →
    ∀ ⦃y : ↥J⦄,
      y ∈ (↑J.attach : Set ↥J) →
        x ≠ y → Function.onFun (β := Set α) Disjoint (fun (i' : ↥J) ↦ ⋃ i ∈ Ju (↑i' : Set α) ⋯, i) x y

Tactic:
_
-- Module: Mathlib.MeasureTheory.SetSemiring
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
x : ↥J
h_2 : x ∈ (↑J.attach : Set ↥J)
y : ↥J
insert :
  y ∈ (↑J.attach : Set ↥J) →
    x ≠ y → Function.onFun (β := Set α) Disjoint (fun (i' : ↥J) ↦ ⋃ i ∈ Ju (↑i' : Set α) ⋯, i) x y
⊢ y ∈ (↑J.attach : Set ↥J) →
    x ≠ y → Function.onFun (β := Set α) Disjoint (fun (i' : ↥J) ↦ ⋃ i ∈ Ju (↑i' : Set α) ⋯, i) x y

Tactic:
_
-- Module: Mathlib.MeasureTheory.SetSemiring
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
by_contra : ∀ (h_contra : ¬Disjoint (↑x : Set α) (↑y : Set α)), False
⊢ Disjoint (↑x : Set α) (↑y : Set α)

Tactic:
by_contra h_contra
-- Module: Mathlib.MeasureTheory.SetSemiring
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

Tactic:
hxy ?_
-- Module: Mathlib.MeasureTheory.SetSemiring
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 α)
refine : x = y
⊢ False

Tactic:
refine hxy ?_
-- Module: Mathlib.MeasureTheory.SetSemiring
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

Tactic:
Subtype.ext ?_

Premises used: Subtype.ext
-- Module: Mathlib.MeasureTheory.SetSemiring
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 α)
refine : (↑x : Set α) = (↑y : Set α)
⊢ x = y

Tactic:
refine Subtype.ext ?_

Premises used: Subtype.ext
-- Module: Mathlib.MeasureTheory.SetSemiring
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 : Set α) = (↑y : Set α)

Tactic:
h_dis.elim x.prop y.prop h_contra

Premises used: Set.PairwiseDisjoint.elim, Subtype.prop
-- Module: Mathlib.MeasureTheory.SetSemiring
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 : Set α) = (↑y : Set α)

Tactic:
exact h_dis.elim x.prop y.prop h_contra

Premises used: Set.PairwiseDisjoint.elim, Subtype.prop
-- Module: Mathlib.MeasureTheory.SetSemiring
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 α)

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
-- Module: Mathlib.MeasureTheory.SetSemiring
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 α)
⊢ Disjoint (⋃₀ (↑(Ju (↑x : Set α) ⋯) : Set (Set α))) (⋃₀ (↑(Ju (↑y : Set α) ⋯) : Set (Set α)))

Tactic:
hJu_disj' (x : Set α) (h_ss x.prop) y (h_ss y.prop) hxy_disj

Premises used: Subtype.prop, Subtype.val
-- Module: Mathlib.MeasureTheory.SetSemiring
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 α))
h₂ : (fun (i' : ↥J) ↦ (⋃ i ∈ Ju (↑i' : Set α) ⋯, i : Set α)) y = ⋃₀ (↑(Ju (↑y : Set α) ⋯) : Set (Set α))
⊢ Function.onFun (β := Set α) Disjoint (fun (i' : ↥J) ↦ ⋃ i ∈ Ju (↑i' : Set α) ⋯, i) x y

Tactic:
convert! hJu_disj' (x : Set α) (h_ss x.prop) y (h_ss y.prop) hxy_disj

Premises used: Subtype.prop, Subtype.val