awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommGroup M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
rw : (↑(v.restrict i) : Set α → M) j ≤ (↑(w.restrict i) : Set α → M) j
⊢ (↑v : Set α → M) (j ∩ i) ≤ (↑w : Set α → M) (j ∩ i)

Tactic:
rw [← restrict_apply _ hi hj₁, ← restrict_apply _ hi hj₁]

Premises used: MeasureTheory.VectorMeasure.restrict_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommGroup M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ (↑(v.restrict i) : Set α → M) j ≤ (↑(w.restrict i) : Set α → M) j

Tactic:
h j hj₁
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommGroup M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ (↑(v.restrict i) : Set α → M) j ≤ (↑(w.restrict i) : Set α → M) j

Tactic:
exact h j hj₁
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommGroup M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ -w ≤[i] -v ↔ v ≤[i] w

Tactic:
⟨fun h => neg_neg v ▸ neg_neg w ▸ neg_le_neg _ _ hi h, fun h => neg_le_neg _ _ hi h⟩

Premises used: Eq.rec, neg_neg, Iff.intro, Neg.neg, MeasureTheory.VectorMeasure.neg_le_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
⊢ v ≤[⋃ (n : ℕ), f n] w

Tactic:
restrict_le_restrict_of_subset_le v w fun a ha₁ ha₂ => ?_

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
refine : ∀ (a : Set α) (ha₁ : MeasurableSet a) (ha₂ : a ⊆ ⋃ (n : ℕ), f n), (↑v : Set α → M) a ≤ (↑w : Set α → M) a
⊢ v ≤[⋃ (n : ℕ), f n] w

Tactic:
refine restrict_le_restrict_of_subset_le v w fun a ha₁ ha₂ => ?_

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
rwa : a ∩ ⋃ (i : ℕ), disjointed f i = a
rwa₁ : a ∩ ⋃ (i : ℕ), f i = a
rwa₂ rwa₃ rwa₄ rwa₅ : a ⊆ ⋃ (i : ℕ), f i
⊢ ⋃ (n : ℕ), a ∩ disjointed f n = a

Tactic:
rwa [← Set.inter_iUnion, iUnion_disjointed, Set.inter_eq_left]

Premises used: Set.inter_eq_left, iUnion_disjointed, Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
⊢ ⋃ (n : ℕ), a ∩ disjointed f n = a

Tactic:
have ha₃ : ⋃ n, a ∩ disjointed f n = a := by
    rwa [← Set.inter_iUnion, iUnion_disjointed, Set.inter_eq_left]
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
⊢ Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)

Tactic:
have ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n) :=
    (disjoint_disjointed _).mono fun i j => Disjoint.mono inf_le_right inf_le_right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
ha₄ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)
rw :
  LE.le.{u_3} (α := M) (∑' (i : ℕ), (↑v : Set α → M) (a ∩ disjointed f i))
    (∑' (i : ℕ), (↑w : Set α → M) (a ∩ disjointed f i))
rw₁ rw₂ : ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)
⊢ (↑v : Set α → M) a ≤ (↑w : Set α → M) a

Tactic:
rw [← ha₃, v.of_disjoint_iUnion _ ha₄, w.of_disjoint_iUnion _ ha₄]

Premises used: MeasureTheory.VectorMeasure.of_disjoint_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
ha₄ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)
⊢ LE.le.{u_3} (α := M) (∑' (i : ℕ), (↑v : Set α → M) (a ∩ disjointed f i))
    (∑' (i : ℕ), (↑w : Set α → M) (a ∩ disjointed f i))

Tactic:
Summable.tsum_le_tsum (fun n => (restrict_le_restrict_iff v w (hf₁ n)).1 (hf₂ n) ?_ ?_)
      ?_ ?_

Premises used: Summable.tsum_le_tsum, Iff.mp, MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
ha₄ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)
refine_1 : ∀ (n : ℕ), MeasurableSet (a ∩ disjointed f n)
refine_2 : ∀ (n : ℕ), a ∩ disjointed f n ⊆ f n
refine_3 : Summable.{u_3, 0} (α := M) fun (i : ℕ) ↦ (↑v : Set α → M) (a ∩ disjointed f i)
refine_4 : Summable.{u_3, 0} (α := M) fun (i : ℕ) ↦ (↑w : Set α → M) (a ∩ disjointed f i)
⊢ LE.le.{u_3} (α := M) (∑' (i : ℕ), (↑v : Set α → M) (a ∩ disjointed f i))
    (∑' (i : ℕ), (↑w : Set α → M) (a ∩ disjointed f i))

Tactic:
refine Summable.tsum_le_tsum (fun n => (restrict_le_restrict_iff v w (hf₁ n)).1 (hf₂ n) ?_ ?_)
      ?_ ?_

Premises used: Summable.tsum_le_tsum, Iff.mp, MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
ha₄ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)
n : ℕ
⊢ MeasurableSet (a ∩ disjointed f n)

Tactic:
ha₁.inter (MeasurableSet.disjointed hf₁ n)

Premises used: MeasurableSet.disjointed, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
ha₄ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)
n : ℕ
⊢ MeasurableSet (a ∩ disjointed f n)

Tactic:
exact ha₁.inter (MeasurableSet.disjointed hf₁ n)

Premises used: MeasurableSet.disjointed, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
ha₄ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)
n : ℕ
⊢ a ∩ disjointed f n ⊆ f n

Tactic:
Set.Subset.trans Set.inter_subset_right (disjointed_subset _ _)

Premises used: Set.Subset.trans, disjointed_subset, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
ha₄ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)
n : ℕ
⊢ a ∩ disjointed f n ⊆ f n

Tactic:
exact Set.Subset.trans Set.inter_subset_right (disjointed_subset _ _)

Premises used: Set.Subset.trans, disjointed_subset, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
ha₄ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)
⊢ Summable.{u_3, 0} (α := M) fun (i : ℕ) ↦ (↑v : Set α → M) (a ∩ disjointed f i)

Tactic:
(v.m_iUnion (fun n => ?_) ?_).summable

Premises used: HasSum.summable, MeasureTheory.VectorMeasure.m_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
ha₄ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)
refine_3 : ∀ (n : ℕ), MeasurableSet (a ∩ disjointed f n)
refine_3₁ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ℕ) ↦ a ∩ disjointed f i)
⊢ Summable.{u_3, 0} (α := M) fun (i : ℕ) ↦ (↑v : Set α → M) (a ∩ disjointed f i)

Tactic:
refine (v.m_iUnion (fun n => ?_) ?_).summable

Premises used: HasSum.summable, MeasureTheory.VectorMeasure.m_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
ha₄ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)
⊢ Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ℕ) ↦ a ∩ disjointed f i)

Tactic:
(disjoint_disjointed _).mono fun i j => Disjoint.mono inf_le_right inf_le_right

Premises used: inf_le_right, disjoint_disjointed, Disjoint.mono, Pairwise.mono
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
ha₄ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)
⊢ Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ℕ) ↦ a ∩ disjointed f i)

Tactic:
exact (disjoint_disjointed _).mono fun i j => Disjoint.mono inf_le_right inf_le_right

Premises used: inf_le_right, disjoint_disjointed, Disjoint.mono, Pairwise.mono
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
ha₄ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)
⊢ Summable.{u_3, 0} (α := M) fun (i : ℕ) ↦ (↑w : Set α → M) (a ∩ disjointed f i)

Tactic:
(w.m_iUnion (fun n => ?_) ?_).summable

Premises used: HasSum.summable, MeasureTheory.VectorMeasure.m_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
ha₄ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)
refine_4 : ∀ (n : ℕ), MeasurableSet (a ∩ disjointed f n)
refine_4₁ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ℕ) ↦ a ∩ disjointed f i)
⊢ Summable.{u_3, 0} (α := M) fun (i : ℕ) ↦ (↑w : Set α → M) (a ∩ disjointed f i)

Tactic:
refine (w.m_iUnion (fun n => ?_) ?_).summable

Premises used: HasSum.summable, MeasureTheory.VectorMeasure.m_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
ha₄ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)

Tactic:
fun n => ha₁.inter (MeasurableSet.disjointed hf₁ n)

Premises used: MeasurableSet.disjointed, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
ha₄ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)

Tactic:
exact fun n => ha₁.inter (MeasurableSet.disjointed hf₁ n)

Premises used: MeasurableSet.disjointed, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
inst_5 : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), v ≤[f b] w
intro : ∀ (val : Encodable β), v ≤[⋃ (b : β), f b] w
⊢ v ≤[⋃ (b : β), f b] w

Tactic:
cases nonempty_encodable β

Premises used: nonempty_encodable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
inst_5 : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), v ≤[f b] w
val : Encodable β
intro : v ≤[⋃ (i : ℕ), ⋃ b ∈ Encodable.decode₂ β i, f b] w
⊢ v ≤[⋃ (b : β), f b] w

Tactic:
rw [← Encodable.iUnion_decode₂]

Premises used: Encodable.iUnion_decode₂
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
inst_5 : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), v ≤[f b] w
val : Encodable β
⊢ v ≤[⋃ (i : ℕ), ⋃ b ∈ Encodable.decode₂ β i, f b] w

Tactic:
restrict_le_restrict_iUnion v w ?_ ?_

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
inst_5 : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), v ≤[f b] w
val : Encodable β
intro : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) (⋃ b ∈ Encodable.decode₂ β n, f b)
intro₁ : ∀ (n : ℕ), v ≤[⋃ b ∈ Encodable.decode₂ β n, f b] w
⊢ v ≤[⋃ (i : ℕ), ⋃ b ∈ Encodable.decode₂ β i, f b] w

Tactic:
refine restrict_le_restrict_iUnion v w ?_ ?_

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
inst_5 : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), v ≤[f b] w
val : Encodable β
n : ℕ
⊢ MeasurableSet.{u_1} (α := α) (⋃ b ∈ Encodable.decode₂ β n, f b)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
inst_5 : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), v ≤[f b] w
val : Encodable β
n : ℕ
intro : v ≤[⋃ (b : β), ⋃ (_ : Membership.mem (γ := Option β) none b), f b] w
intro₁ : ∀ (b : β), v ≤[⋃ b_1 ∈ some b, f b_1] w
⊢ v ≤[⋃ b ∈ Encodable.decode₂ β n, f b] w

Tactic:
rcases Encodable.decode₂ β n with - | b

Premises used: Encodable.decode₂
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
inst_5 : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), v ≤[f b] w
val : Encodable β
n : ℕ
⊢ v ≤[⋃ (b : β), ⋃ (_ : Membership.mem (γ := Option β) none b), f b] w

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
inst_5 : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), v ≤[f b] w
val : Encodable β
n : ℕ
b : β
⊢ v ≤[⋃ b_1 ∈ some b, f b_1] w

Tactic:
simp [hf₂ b]
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
rw : v ≤[⋃ (b : Bool), bif b then i else j] w
⊢ v ≤[i ∪ j] w

Tactic:
rw [Set.union_eq_iUnion]

Premises used: Set.union_eq_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ v ≤[⋃ (b : Bool), bif b then i else j] w

Tactic:
restrict_le_restrict_countable_iUnion v w ?_ ?_

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_countable_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
refine_1 : ∀ (b : Bool), MeasurableSet (bif b then i else j)
refine_2 : ∀ (b : Bool), v ≤[bif b then i else j] w
⊢ v ≤[⋃ (b : Bool), bif b then i else j] w

Tactic:
refine restrict_le_restrict_countable_iUnion v w ?_ ?_

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_countable_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ ∀ (b : Bool), MeasurableSet (bif b then i else j)

Tactic:
measurability