awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : IsFiniteMeasure ν₁
inst_6 : IsFiniteMeasure ν₂
inst_7 : ν₁.HaveLebesgueDecomposition μ
inst_8 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
this : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : G), (ν₁ ∗ₘ ν₂).rnDeriv μ x ∂μ ≠ ∞

Tactic:
exact (lintegral_rnDeriv_lt_top (ν₁ ∗ₘ ν₂) μ).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, MeasureTheory.Measure.mconv, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SigmaFinite μ
ν₁ ν₂ : Measure G
inst_5 : SigmaFinite ν₁
inst_6 : SigmaFinite ν₂
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ AEMeasurable ((ν₁ ∗ₘ ν₂).rnDeriv μ) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SigmaFinite μ
ν₁ ν₂ : Measure G
inst_5 : SigmaFinite ν₁
inst_6 : SigmaFinite ν₂
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ AEMeasurable (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SigmaFinite μ
ν₁ ν₂ : Measure G
inst_5 : SigmaFinite ν₁
inst_6 : SigmaFinite ν₂
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
rw : μ.withDensity ((ν₁ ∗ₘ ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ)
rw₁ : μ.withDensity ((ν₁ ∗ₘ ν₂).rnDeriv μ) = ν₁ ∗ₘ ν₂
rw₂ rw₃ : ν₁ ∗ₘ ν₂ = ν₁ ∗ₘ ν₂
⊢ (ν₁ ∗ₘ ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ

Tactic:
rw [← withDensity_eq_iff_of_sigmaFinite (by fun_prop) (by fun_prop),
    ← mconv_eq_withDensity_mlconvolution_rnDeriv hν₁ hν₂,
    withDensity_rnDeriv_eq _ _ (mconv_absolutelyContinuous hν₂)]

Premises used: MeasureTheory.mconv_eq_withDensity_mlconvolution_rnDeriv, MeasureTheory.Measure.mconv_absolutelyContinuous, MeasureTheory.withDensity_eq_iff_of_sigmaFinite, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
⊢ (↑v : Set α → M) ∅ = 0

Tactic:
v.empty'

Premises used: MeasureTheory.VectorMeasure.empty'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ (↑v : Set α → M) i = 0

Tactic:
v.not_measurable' hi

Premises used: MeasureTheory.VectorMeasure.not_measurable'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (fun (i : ℕ) ↦ (↑v : Set α → M) (f i)) ((↑v : Set α → M) (⋃ (i : ℕ), f i))

Tactic:
v.m_iUnion' hf₁ hf₂

Premises used: MeasureTheory.VectorMeasure.m_iUnion'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
h : (↑v : Set α → M) = (↑w : Set α → M)
mk :
  ∀ (measureOf' : Set α → M) (empty' : measureOf' ∅ = 0)
    (not_measurable' : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf' i = 0)
    (m_iUnion' :
      ∀ ⦃f : ℕ → Set α⦄,
        (∀ (i : ℕ), MeasurableSet (f i)) →
          Pairwise (Disjoint on f) → HasSum (fun (i : ℕ) ↦ measureOf' (f i)) (measureOf' (⋃ (i : ℕ), f i)))
    (h :
      (↑{ measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' :
              VectorMeasure α M } :
          Set α → M) =
        (↑w : Set α → M)),
    { measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' :
        VectorMeasure α M } =
      w
⊢ v = w

Tactic:
cases v
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
w : VectorMeasure α M
measureOf' : Set α → M
empty' : measureOf' ∅ = 0
not_measurable' : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf' i = 0
m_iUnion' :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Disjoint on f) → HasSum (fun (i : ℕ) ↦ measureOf' (f i)) (measureOf' (⋃ (i : ℕ), f i))
h :
  (↑{ measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' :
          VectorMeasure α M } :
      Set α → M) =
    (↑w : Set α → M)
mk :
  ∀ (measureOf'_1 : Set α → M) (empty'_1 : measureOf'_1 ∅ = 0)
    (not_measurable'_1 : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf'_1 i = 0)
    (m_iUnion'_1 :
      ∀ ⦃f : ℕ → Set α⦄,
        (∀ (i : ℕ), MeasurableSet (f i)) →
          Pairwise (Disjoint on f) → HasSum (fun (i : ℕ) ↦ measureOf'_1 (f i)) (measureOf'_1 (⋃ (i : ℕ), f i)))
    (h :
      (↑{ measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' :
              VectorMeasure α M } :
          Set α → M) =
        (↑{ measureOf' := measureOf'_1, empty' := empty'_1, not_measurable' := not_measurable'_1,
              m_iUnion' := m_iUnion'_1 : VectorMeasure α M } :
          Set α → M)),
    { measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' :
        VectorMeasure α M } =
      { measureOf' := measureOf'_1, empty' := empty'_1, not_measurable' := not_measurable'_1, m_iUnion' := m_iUnion'_1 }
⊢ { measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' :
      VectorMeasure α M } =
    w

Tactic:
cases w
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
measureOf' : Set α → M
empty' : measureOf' ∅ = 0
not_measurable' : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf' i = 0
m_iUnion' :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Disjoint on f) → HasSum (fun (i : ℕ) ↦ measureOf' (f i)) (measureOf' (⋃ (i : ℕ), f i))
measureOf'_1 : Set α → M
empty'_1 : measureOf'_1 ∅ = 0
not_measurable'_1 : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf'_1 i = 0
m_iUnion'_1 :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Disjoint on f) → HasSum (fun (i : ℕ) ↦ measureOf'_1 (f i)) (measureOf'_1 (⋃ (i : ℕ), f i))
h :
  (↑{ measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' :
          VectorMeasure α M } :
      Set α → M) =
    (↑{ measureOf' := measureOf'_1, empty' := empty'_1, not_measurable' := not_measurable'_1, m_iUnion' := m_iUnion'_1 :
          VectorMeasure α M } :
      Set α → M)
⊢ { measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' :
      VectorMeasure α M } =
    { measureOf' := measureOf'_1, empty' := empty'_1, not_measurable' := not_measurable'_1, m_iUnion' := m_iUnion'_1 }

Tactic:
congr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
rw : (↑v : Set α → M) = (↑w : Set α → M) ↔ ∀ (i : Set α), (↑v : Set α → M) i = (↑w : Set α → M) i
rw₁ rw₂ :
  (∀ (x : Set α), (↑v : Set α → M) x = (↑w : Set α → M) x) ↔ ∀ (i : Set α), (↑v : Set α → M) i = (↑w : Set α → M) i
⊢ v = w ↔ ∀ (i : Set α), (↑v : Set α → M) i = (↑w : Set α → M) i

Tactic:
rw [← coe_injective.eq_iff, funext_iff]

Premises used: MeasureTheory.VectorMeasure.coe_injective, Function.Injective.eq_iff, funext_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
mp : v = w → ∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i
mpr : (∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i) → v = w
⊢ v = w ↔ ∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
i : Set α
h : MeasurableSet i
⊢ (↑v : Set α → M) i = (↑v : Set α → M) i

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
mpr :
  (∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i) →
    ∀ (i : Set α), (↑v : Set α → M) i = (↑w : Set α → M) i
⊢ (∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i) → v = w

Tactic:
rw [ext_iff']

Premises used: MeasureTheory.VectorMeasure.ext_iff'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i
i : Set α
pos : ∀ (hi : MeasurableSet i), (↑v : Set α → M) i = (↑w : Set α → M) i
neg : ∀ (hi : ¬MeasurableSet i), (↑v : Set α → M) i = (↑w : Set α → M) i
⊢ (↑v : Set α → M) i = (↑w : Set α → M) i

Tactic:
by_cases hi : MeasurableSet i

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i
i : Set α
hi : MeasurableSet i
⊢ (↑v : Set α → M) i = (↑w : Set α → M) i

Tactic:
h i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i
i : Set α
hi : MeasurableSet i
⊢ (↑v : Set α → M) i = (↑w : Set α → M) i

Tactic:
exact h i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i = (↑w : Set α → M) i
i : Set α
hi : ¬MeasurableSet i
⊢ (↑v : Set α → M) i = (↑w : Set α → M) i

Tactic:
simp_rw [not_measurable _ hi]

Premises used: MeasureTheory.VectorMeasure.not_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
s t : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → (↑s : Set α → M) i = (↑t : Set α → M) i
⊢ s = t

Tactic:
(ext_iff s t).2 h

Premises used: Iff.mpr, MeasureTheory.VectorMeasure.ext_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
rcases :
  ∀ (e : β → ℕ) (he : Function.Injective e),
    HasSum (fun (i : β) ↦ (↑v : Set α → M) (f i)) ((↑v : Set α → M) (⋃ (i : β), f i))
⊢ HasSum (fun (i : β) ↦ (↑v : Set α → M) (f i)) ((↑v : Set α → M) (⋃ (i : β), f i))

Tactic:
rcases Countable.exists_injective_nat β with ⟨e, he⟩

Premises used: Countable.exists_injective_nat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
rw : HasSum (Function.extend e (fun (i : β) ↦ (↑v : Set α → M) (f i)) 0) ((↑v : Set α → M) (⋃ (i : β), f i))
⊢ HasSum (fun (i : β) ↦ (↑v : Set α → M) (f i)) ((↑v : Set α → M) (⋃ (i : β), f i))

Tactic:
rw [← hasSum_extend_zero he]

Premises used: hasSum_extend_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ HasSum (fun (i : ℕ) ↦ (↑v : Set α → M) (Function.extend e f (fun (x : ℕ) ↦ ∅) i))
    ((↑v : Set α → M) (⋃ (i : ℕ), Function.extend e f (fun (x : ℕ) ↦ ∅) i))

Tactic:
m_iUnion v (f := Function.extend e f fun _ ↦ ∅) _ _

Premises used: MeasureTheory.VectorMeasure.m_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
h :
  ∀ (x : ℕ),
    Function.extend e (fun (i : β) ↦ (↑v : Set α → M) (f i)) 0 x =
      (↑v : Set α → M) (Function.extend e f (fun (x : ℕ) ↦ ∅) x)
h₁ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : β), f i) (⋃ (i : ℕ), Function.extend e f (fun (x : ℕ) ↦ ∅) i)
convert_1 : ∀ (i : ℕ), MeasurableSet (Function.extend e f (fun (x : ℕ) ↦ ∅) i)
convert_2 : Pairwise (Disjoint on Function.extend e f fun (x : ℕ) ↦ ∅)
⊢ HasSum (Function.extend e (fun (i : β) ↦ (↑v : Set α → M) (f i)) 0) ((↑v : Set α → M) (⋃ (i : β), f i))

Tactic:
convert! m_iUnion v (f := Function.extend e f fun _ ↦ ∅) _ _

Premises used: MeasureTheory.VectorMeasure.m_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
x : ℕ
⊢ Function.extend e (fun (i : β) ↦ (↑v : Set α → M) (f i)) 0 x =
    (↑v : Set α → M) (Function.extend e f (fun (x : ℕ) ↦ ∅) x)

Tactic:
simp only [Pi.zero_def, Function.apply_extend v, Function.comp_def, empty]

Premises used: MeasureTheory.VectorMeasure.empty, MeasureTheory.VectorMeasure.measureOf', Pi.zero_def, Function.apply_extend, Function.comp_def
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : β), f i) (⋃ (i : ℕ), Function.extend e f (fun (x : ℕ) ↦ ∅) i)

Tactic:
(iSup_extend_bot he _).symm

Premises used: Eq.symm, Set.iUnion, iSup_extend_bot
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : β), f i) (⋃ (i : ℕ), Function.extend e f (fun (x : ℕ) ↦ ∅) i)

Tactic:
exact (iSup_extend_bot he _).symm

Premises used: Eq.symm, iSup_extend_bot
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ ∀ (i : ℕ), MeasurableSet (Function.extend e f (fun (x : ℕ) ↦ ∅) i)

Tactic:
simp [Function.apply_extend MeasurableSet, Function.comp_def, hm]

Premises used: MeasurableSet, Function.apply_extend, Function.comp_def
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ Pairwise (Disjoint on Function.extend e f fun (x : ℕ) ↦ ∅)

Tactic:
hd.disjoint_extend_bot (he.factorsThrough _)

Premises used: Pairwise.disjoint_extend_bot, Function.Injective.factorsThrough
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ Pairwise (Disjoint on Function.extend e f fun (x : ℕ) ↦ ∅)

Tactic:
exact hd.disjoint_extend_bot (he.factorsThrough _)

Premises used: Pairwise.disjoint_extend_bot, Function.Injective.factorsThrough
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : Countable β
v : VectorMeasure α M
f : β → Set α
inst_3 : T2Space M
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
⊢ (↑v : Set α → M) (⋃ (i : β), f i) = ∑' (i : β), (↑v : Set α → M) (f i)

Tactic:
(hasSum_of_disjoint_iUnion hm hd).tsum_eq.symm

Premises used: MeasureTheory.VectorMeasure.hasSum_of_disjoint_iUnion, HasSum.tsum_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
hm : ∀ (i : Bool), MeasurableSet (bif i then A else B)
hd : Pairwise (α := Bool) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (b : Bool) ↦ bif b then A else B)
⊢ (↑v : Set α → M) (A ∪ B) = (↑v : Set α → M) A + (↑v : Set α → M) B

Tactic:
rw [Set.union_eq_iUnion, of_disjoint_iUnion, tsum_fintype, Fintype.sum_bool, cond, cond]

Premises used: cond, Fintype.sum_bool, MeasureTheory.VectorMeasure.of_disjoint_iUnion, tsum_fintype, Set.union_eq_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∀ (i : Bool), MeasurableSet (bif i then A else B)

Tactic:
fun b => Bool.casesOn b hB hA

Premises used: Bool.casesOn
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ Pairwise (α := Bool) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (b : Bool) ↦ bif b then A else B)

Tactic:
pairwise_disjoint_on_bool.2 h

Premises used: Iff.mpr, pairwise_disjoint_on_bool
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∀ (i : Bool), MeasurableSet (bif i then A else B)

Tactic:
exacts [fun b => Bool.casesOn b hB hA, pairwise_disjoint_on_bool.2 h]

Premises used: Iff.mpr, pairwise_disjoint_on_bool
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h : A ⊆ B
rw : (↑v : Set α → M) (A ∪ B \ A) = (↑v : Set α → M) B
rw₁ rw₂ : (↑v : Set α → M) B = (↑v : Set α → M) B
⊢ (↑v : Set α → M) A + (↑v : Set α → M) (B \ A) = (↑v : Set α → M) B

Tactic:
rw [← of_union (@Set.disjoint_sdiff_right _ A B) hA (hB.diff hA), Set.union_diff_cancel h]

Premises used: MeasurableSet.diff, MeasureTheory.VectorMeasure.of_union, Set.union_diff_cancel, Set.disjoint_sdiff_right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
v : VectorMeasure α M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h : A ⊆ B
rw : (↑v : Set α → M) (B \ A) = (↑v : Set α → M) A + (↑v : Set α → M) (B \ A) - (↑v : Set α → M) A
rw₁ rw₂ : (↑v : Set α → M) (B \ A) = (↑v : Set α → M) (B \ A)
⊢ (↑v : Set α → M) (B \ A) = (↑v : Set α → M) B - (↑v : Set α → M) A

Tactic:
rw [← of_add_of_diff hA hB h, add_sub_cancel_left]

Premises used: add_sub_cancel_left, MeasureTheory.VectorMeasure.of_add_of_diff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
v : VectorMeasure α M
A : Set α
hA : MeasurableSet A
⊢ (↑v : Set α → M) Aᶜ = (↑v : Set α → M) univ - (↑v : Set α → M) A

Tactic:
simpa [compl_eq_univ_diff] using of_diff hA .univ (v := v) (subset_univ _)

Premises used: Set.subset_univ, MeasureTheory.VectorMeasure.of_diff, Set.compl_eq_univ_diff, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
symm : (↑v : Set α → M) A = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
⊢ (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B = (↑v : Set α → M) A

Tactic:
symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ (↑v : Set α → M) A = (↑v : Set α → M) (A \ B ∪ A ∩ B)

Tactic:
simp only [Set.diff_union_inter]

Premises used: Set.diff_union_inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
h : Disjoint (A \ B) (A ∩ B)
hA₁ : MeasurableSet (A \ B)
hB₁ : MeasurableSet (A ∩ B)
⊢ (↑v : Set α → M) (A \ B ∪ A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B)

Tactic:
rw [of_union]

Premises used: MeasureTheory.VectorMeasure.of_union
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
h : Disjoint (A ∩ B) (A \ B)
⊢ Disjoint (A \ B) (A ∩ B)

Tactic:
rw [disjoint_comm]

Premises used: disjoint_comm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ Disjoint (A ∩ B) (A \ B)

Tactic:
Set.disjoint_of_subset_left A.inter_subset_right disjoint_sdiff_self_right

Premises used: disjoint_sdiff_self_right, Set.disjoint_of_subset_left, Set.inter_subset_right