awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
h_mem₁ h_mem₂ h_mem₃ h_mem₄ : ⋃ i ∈ a, f i ∈ C
⊢ ⋃₀ (↑(Finset.image f a) : Set (Set α)) ∈ C

Tactic:
rwa [← A]
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
rw : (↑a : Set ι).Pairwise fun (i j : ι) ↦ f i = f j → Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (f i) : G) (0 : G)
⊢ Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))

Tactic:
rw [sum_image_of_pairwise_eq_zero]

Premises used: Finset.sum_image_of_pairwise_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
⊢ (↑a : Set ι).Pairwise fun (i j : ι) ↦ f i = f j → Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (f i) : G) (0 : G)

Tactic:
h_dis.imp ?_

Premises used: Set.Pairwise.imp
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
refine : ∀ ⦃a b : ι⦄, (Disjoint on f) a b → f a = f b → Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (f a) : G) (0 : G)
⊢ (↑a : Set ι).Pairwise fun (i j : ι) ↦ f i = f j → Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (f i) : G) (0 : G)

Tactic:
refine h_dis.imp ?_

Premises used: Set.Pairwise.imp
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
⊢ ∀ ⦃a b : ι⦄, (Disjoint on f) a b → f a = f b → Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (f a) : G) (0 : G)

Tactic:
grind [Set.bot_eq_empty (α := α), addContent_empty]

Premises used: Set.bot_eq_empty, MeasureTheory.addContent_empty
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
inst_1 : Fintype ι
f : ι → Set α
hf : ∀ (i : ι), f i ∈ C
h_dis : Pairwise (Disjoint on f)
h_mem : ⋃ (i : ι), f i ∈ C
⊢ Eq.{u_2 + 1} (α := G)
    ((m : (a : Set α) → G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) Finset.univ i), f i) : G)
    (∑ i : ι, (m : (a : Set α) → G) (f i) : G)

Tactic:
addContent_biUnion (a := Finset.univ) (f := f) (m := m) ?_ ?_ ?_

Premises used: MeasureTheory.addContent_biUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
inst_1 : Fintype ι
f : ι → Set α
hf : ∀ (i : ι), f i ∈ C
h_dis : Pairwise (Disjoint on f)
h_mem : ⋃ (i : ι), f i ∈ C
h :
  Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), f i) : G)
    ((m : (a : Set α) → G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) Finset.univ i), f i) : G)
convert_1 : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → f i ∈ C
convert_2 : (↑Finset.univ : Set ι).PairwiseDisjoint f
convert_3 : ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) Finset.univ i), f i ∈ C
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), f i) : G) (∑ i : ι, (m : (a : Set α) → G) (f i) : G)

Tactic:
convert! addContent_biUnion (a := Finset.univ) (f := f) (m := m) ?_ ?_ ?_ using 1

Premises used: MeasureTheory.addContent_biUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
inst_1 : Fintype ι
f : ι → Set α
hf : ∀ (i : ι), f i ∈ C
h_dis : Pairwise (Disjoint on f)
h_mem : ⋃ (i : ι), f i ∈ C
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), f i) : G)
    ((m : (a : Set α) → G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) Finset.univ i), f i) : G)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
inst_1 : Fintype ι
f : ι → Set α
hf : ∀ (i : ι), f i ∈ C
h_dis : Pairwise (Disjoint on f)
h_mem : ⋃ (i : ι), f i ∈ C
⊢ ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → f i ∈ C

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
inst_1 : Fintype ι
f : ι → Set α
hf : ∀ (i : ι), f i ∈ C
h_dis : Pairwise (Disjoint on f)
h_mem : ⋃ (i : ι), f i ∈ C
⊢ (↑Finset.univ : Set ι).PairwiseDisjoint f

Tactic:
simpa [Set.PairwiseDisjoint, Set.pairwise_univ] using h_dis

Premises used: Set.PairwiseDisjoint, Set.pairwise_univ
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
inst_1 : Fintype ι
f : ι → Set α
hf : ∀ (i : ι), f i ∈ C
h_dis : Pairwise (Disjoint on f)
h_mem : ⋃ (i : ι), f i ∈ C
⊢ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) Finset.univ i), f i ∈ C

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
h : ∀ (x : α), x ∈ s ∪ t ↔ Membership.mem (γ := Set α) (⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i) x
⊢ s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
x : α
⊢ x ∈ s ∪ t ↔ Membership.mem (γ := Set α) (⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i) x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
⊢ s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i

Tactic:
have A : s ∪ t = ⋃ i, ![s, t] i := by ext; simp
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i) : G)
    (∑ i : Fin (Nat.succ 0).succ, (m : (a : Set α) → G) (![s, t] i) : G)

Tactic:
addContent_iUnion (f := ![s, t]) (m := m) (fun i ↦ ?_) (fun i j hij ↦ ?_) ?_

Premises used: MeasureTheory.addContent_iUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
h :
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G) =
    ∑ i : Fin (Nat.succ 0).succ, (m : (a : Set α) → G) (![s, t] i)
convert_1 : ∀ (i : Fin (Nat.succ 0).succ), ![s, t] i ∈ C
convert_2 : ∀ (i j : Fin (Nat.succ 0).succ) (hij : i ≠ j), (Disjoint on ![s, t]) i j
convert_3 : ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i ∈ C
⊢ (m : (a : Set α) → G) (s ∪ t) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)

Tactic:
convert! addContent_iUnion (f := ![s, t]) (m := m) (fun i ↦ ?_) (fun i j hij ↦ ?_) ?_ using 2

Premises used: MeasureTheory.addContent_iUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
⊢ HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G) =
    ∑ i : Fin (Nat.succ 0).succ, (m : (a : Set α) → G) (![s, t] i)

Tactic:
simp [Fin.univ_castSuccEmb, add_comm]

Premises used: add_comm, Fin.univ_castSuccEmb
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
i : Fin (Nat.succ 0).succ
convert_1 : ![s, t] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) ∈ C
convert_1₁ : ![s, t] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) ∈ C
⊢ ![s, t] i ∈ C

Tactic:
fin_cases i
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
⊢ ![s, t] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) ∈ C

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
⊢ ![s, t] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) ∈ C

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
i j : Fin (Nat.succ 0).succ
hij : i ≠ j
convert_2 :
  ∀ (hij : (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩ ≠ j),
    (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) j
convert_2₁ :
  ∀ (hij : (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩ ≠ j),
    (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) j
⊢ (Disjoint on ![s, t]) i j

Tactic:
fin_cases i
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
j : Fin (Nat.succ 0).succ
hij : (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩ ≠ j
convert_2 :
  ∀
    (hij :
      Ne (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)),
    (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
convert_2₁ :
  ∀
    (hij :
      Ne (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)),
    (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
j : Fin (Nat.succ 0).succ
hij : (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩ ≠ j
convert_2 :
  ∀
    (hij :
      Ne (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)),
    (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
convert_2₁ :
  ∀
    (hij :
      Ne (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)),
    (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
hij :
  Ne (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
⊢ (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
hij :
  Ne (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
hij :
  Ne (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
⊢ (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)

Tactic:
h_dis.symm

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Disjoint.symm, Fin.induction, Fin.cases, Matrix.vecCons
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
hij :
  Ne (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
⊢ (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)

Tactic:
exact h_dis.symm

Premises used: Disjoint.symm
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
hij :
  Ne (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
convert_3 convert_3₁ convert_3₂ convert_3₃ : s ∪ t ∈ C
⊢ ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i ∈ C

Tactic:
rwa [← A]
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
rw : ((m : (a : Set α) → G) (⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) : G)
| ((m : (a : Set α) → G) s : G)

Tactic:
rw [← hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]

Premises used: MeasureTheory.IsSetSemiring.sUnion_union_disjointOfDiffUnion_of_subset
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
conv_lhs :
  (m : (a : Set α) → G) (⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
⊢ (m : (a : Set α) → G) s =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)

Tactic:
conv_lhs => rw [← hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]

Premises used: MeasureTheory.IsSetSemiring.sUnion_union_disjointOfDiffUnion_of_subset
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
rw :
  ∑ u ∈ I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
h_ss : (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ C
h_dis₁ : (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)).PairwiseDisjoint id
h_mem : ⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ∈ C
⊢ (m : (a : Set α) → G) (⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)

Tactic:
rw [addContent_sUnion]

Premises used: MeasureTheory.addContent_sUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
rw : Disjoint I (hC.disjointOfDiffUnion (C := C) (s := s) hs hI)
⊢ ∑ u ∈ I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)

Tactic:
rw [sum_union]

Premises used: Finset.sum_union
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
⊢ Disjoint I (hC.disjointOfDiffUnion (C := C) (s := s) hs hI)

Tactic:
hC.disjoint_disjointOfDiffUnion hs hI

Premises used: MeasureTheory.IsSetSemiring.disjoint_disjointOfDiffUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
⊢ Disjoint I (hC.disjointOfDiffUnion (C := C) (s := s) hs hI)

Tactic:
exact hC.disjoint_disjointOfDiffUnion hs hI

Premises used: MeasureTheory.IsSetSemiring.disjoint_disjointOfDiffUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
h_ss : (↑I : Set (Set α)) ∪ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ C
⊢ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ C

Tactic:
rw [coe_union]

Premises used: Finset.coe_union
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
⊢ (↑I : Set (Set α)) ∪ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ C

Tactic:
Set.union_subset hI (hC.disjointOfDiffUnion_subset hs hI)

Premises used: Set.union_subset, MeasureTheory.IsSetSemiring.disjointOfDiffUnion_subset
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
⊢ (↑I : Set (Set α)) ∪ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ C

Tactic:
exact Set.union_subset hI (hC.disjointOfDiffUnion_subset hs hI)

Premises used: Set.union_subset, MeasureTheory.IsSetSemiring.disjointOfDiffUnion_subset
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
h_dis₁ : ((↑I : Set (Set α)) ∪ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))).PairwiseDisjoint id
⊢ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)).PairwiseDisjoint id

Tactic:
rw [coe_union]

Premises used: Finset.coe_union
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
⊢ ((↑I : Set (Set α)) ∪ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))).PairwiseDisjoint id

Tactic:
hC.pairwiseDisjoint_union_disjointOfDiffUnion hs hI h_dis

Premises used: MeasureTheory.IsSetSemiring.pairwiseDisjoint_union_disjointOfDiffUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
⊢ ((↑I : Set (Set α)) ∪ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))).PairwiseDisjoint id

Tactic:
exact hC.pairwiseDisjoint_union_disjointOfDiffUnion hs hI h_dis

Premises used: MeasureTheory.IsSetSemiring.pairwiseDisjoint_union_disjointOfDiffUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
h_mem h_mem₁ h_mem₂ h_mem₃ : s ∈ C
⊢ ⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ∈ C

Tactic:
rwa [hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]

Premises used: MeasureTheory.IsSetSemiring.sUnion_union_disjointOfDiffUnion_of_subset