awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
pos : ∀ (hi : MeasurableSet i), (c • v).restrict i = c • v.restrict i
⊢ (c • v).restrict i = c • v.restrict i
have neg : ∀ (hi : ¬MeasurableSet i), (c • v).restrict i = c • v.restrict i
Tactic: by_cases hi : MeasurableSet i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : MeasurableSet i
⊢ (c • v).restrict i = c • v.restrict i
have pos : ∀ (j : Set α) (hj : MeasurableSet j), (↑((c • v).restrict i) : Set α → M) j = (↑(c • v.restrict i) : Set α → M) j
Tactic: ext j hj
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
⊢ (c • v).restrict i = c • v.restrict i
have neg : 0 = HSMul.hSMul (β := VectorMeasure α M) c 0
Tactic: simp only [restrict_not_measurable _ hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
⊢ 0 = HSMul.hSMul (β := VectorMeasure α M) c 0
have neg : ∀ (j : Set α), MeasurableSet j → (↑0 : Set α → M) j = (↑(HSMul.hSMul (β := VectorMeasure α M) c 0) : Set α → M) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤ w ↔ ∀ (i : Set α), (↑v : Set α → M) i ≤ (↑w : Set α → M) i
have refine : ∀ (h : v ≤ w) (i : Set α), (↑v : Set α → M) i ≤ (↑w : Set α → M) i
Tactic: refine ⟨fun h i => ?_, fun h i _ => h i⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
⊢ (↑v : Set α → M) i ≤ (↑w : Set α → M) i
have pos : ∀ (hi : MeasurableSet i), (↑v : Set α → M) i ≤ (↑w : Set α → M) i
Tactic: by_cases hi : MeasurableSet i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
pos : ∀ (hi : MeasurableSet i), (↑v : Set α → M) i ≤ (↑w : Set α → M) i
⊢ (↑v : Set α → M) i ≤ (↑w : Set α → M) i
have neg : ∀ (hi : ¬MeasurableSet i), (↑v : Set α → M) i ≤ (↑w : Set α → M) i
Tactic: by_cases hi : MeasurableSet i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : ¬MeasurableSet i
⊢ (↑v : Set α → M) i ≤ (↑w : Set α → M) i
have neg : 0 ≤ (↑w : Set α → M) i
Tactic: rw [v.not_measurable hi, w.not_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : ¬MeasurableSet i
neg : 0 ≤ (↑w : Set α → M) i
⊢ (↑v : Set α → M) i ≤ (↑w : Set α → M) i
have neg₁ : LE.le.{u_3} (α := M) 0 0
Tactic: rw [v.not_measurable hi, w.not_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
⊢ (↑v : Set α → M) j ≤ (↑w : Set α → M) j
have pos : ∀ (hj₁ : MeasurableSet j), (↑v : Set α → M) j ≤ (↑w : Set α → M) j
Tactic: by_cases hj₁ : MeasurableSet j
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
pos : ∀ (hj₁ : MeasurableSet j), (↑v : Set α → M) j ≤ (↑w : Set α → M) j
⊢ (↑v : Set α → M) j ≤ (↑w : Set α → M) j
have neg : ∀ (hj₁ : ¬MeasurableSet j), (↑v : Set α → M) j ≤ (↑w : Set α → M) j
Tactic: by_cases hj₁ : MeasurableSet j
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : ¬MeasurableSet j
⊢ (↑v : Set α → M) j ≤ (↑w : Set α → M) j
have neg : 0 ≤ (↑w : Set α → M) j
Tactic: rw [v.not_measurable hj₁, w.not_measurable hj₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : ¬MeasurableSet j
neg : 0 ≤ (↑w : Set α → M) j
⊢ (↑v : Set α → M) j ≤ (↑w : Set α → M) j
have neg₁ : LE.le.{u_3} (α := M) 0 0
Tactic: rw [v.not_measurable hj₁, w.not_measurable hj₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑v : Set α → M) j ≤ (↑w : Set α → M) j
⊢ v ≤[i] w
have pos : ∀ (hi : MeasurableSet i), v ≤[i] w
Tactic: by_cases hi : MeasurableSet i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑v : Set α → M) j ≤ (↑w : Set α → M) j
pos : ∀ (hi : MeasurableSet i), v ≤[i] w
⊢ v ≤[i] w
have neg : ∀ (hi : ¬MeasurableSet i), v ≤[i] w
Tactic: by_cases hi : MeasurableSet i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑v : Set α → M) j ≤ (↑w : Set α → M) j
hi : ¬MeasurableSet i
⊢ v ≤[i] w
have neg : 0 ≤ w.restrict i
Tactic: rw [restrict_not_measurable v hi, restrict_not_measurable w hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑v : Set α → M) j ≤ (↑w : Set α → M) j
hi : ¬MeasurableSet i
neg : 0 ≤ w.restrict i
⊢ v ≤[i] w
have neg₁ : LE.le (α := VectorMeasure α M) 0 0
Tactic: rw [restrict_not_measurable v hi, restrict_not_measurable w hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑((-w).restrict i) : Set α → M) j ≤ (↑((-v).restrict i) : Set α → M) j
have rw : -(↑w : Set α → M) (j ∩ i) ≤ -(↑v : Set α → M) (j ∩ i)
Tactic: rw [restrict_apply _ hi hj₁, restrict_apply _ hi hj₁, neg_apply, neg_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ -(↑w : Set α → M) (j ∩ i) ≤ -(↑v : Set α → M) (j ∩ i)
have refine : (↑v : Set α → M) (j ∩ i) ≤ (↑w : Set α → M) (j ∩ i)
Tactic: refine neg_le_neg ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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 : Set α → M) (j ∩ i) ≤ (↑w : Set α → M) (j ∩ i)
have rw : (↑(v.restrict i) : Set α → M) j ≤ (↑(w.restrict i) : Set α → M) j
Tactic: rw [← restrict_apply _ hi hj₁, ← restrict_apply _ hi hj₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
have refine : ∀ (a : Set α) (ha₁ : MeasurableSet a) (ha₂ : a ⊆ ⋃ (n : ℕ), f n), (↑v : Set α → M) a ≤ (↑w : Set α → M) a
Tactic: refine restrict_le_restrict_of_subset_le v w fun a ha₁ ha₂ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
have rwa : a ∩ ⋃ (i : ℕ), disjointed f i = a
Tactic: rwa [← Set.inter_iUnion, iUnion_disjointed, Set.inter_eq_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ ⋃ (n : ℕ), a ∩ disjointed f n = a
have rwa₁ : a ∩ ⋃ (i : ℕ), f i = a
Tactic: rwa [← Set.inter_iUnion, iUnion_disjointed, Set.inter_eq_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
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
⊢ (↑v : Set α → M) a ≤ (↑w : Set α → M) a
have ha₃ : ⋃ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
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
⊢ (↑v : Set α → M) a ≤ (↑w : Set α → M) a
have ha₄ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
⊢ (↑v : Set α → M) a ≤ (↑w : Set α → M) a
have rw : LE.le.{u_3} (α := M) (∑' (i : ℕ), (↑v : Set α → M) (a ∩ disjointed f i))
  (∑' (i : ℕ), (↑w : Set α → M) (a ∩ disjointed f i))
Tactic: rw [← ha₃, v.of_disjoint_iUnion _ ha₄, w.of_disjoint_iUnion _ ha₄]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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))
⊢ (↑v : Set α → M) a ≤ (↑w : Set α → M) a
have rw₁ : ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)
Tactic: rw [← ha₃, v.of_disjoint_iUnion _ ha₄, w.of_disjoint_iUnion _ ha₄]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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))
have refine_1 : ∀ (n : ℕ), MeasurableSet (a ∩ disjointed f n)
Tactic: refine Summable.tsum_le_tsum (fun n => (restrict_le_restrict_iff v w (hf₁ n)).1 (hf₂ n) ?_ ?_)
      ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
⊢ LE.le.{u_3} (α := M) (∑' (i : ℕ), (↑v : Set α → M) (a ∩ disjointed f i))
    (∑' (i : ℕ), (↑w : Set α → M) (a ∩ disjointed f i))
have refine_2 : ∀ (n : ℕ), a ∩ disjointed f n ⊆ f n
Tactic: refine Summable.tsum_le_tsum (fun n => (restrict_le_restrict_iff v w (hf₁ n)).1 (hf₂ n) ?_ ?_)
      ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ LE.le.{u_3} (α := M) (∑' (i : ℕ), (↑v : Set α → M) (a ∩ disjointed f i))
    (∑' (i : ℕ), (↑w : Set α → M) (a ∩ disjointed f i))
have refine_3 : Summable.{u_3, 0} (α := M) fun (i : ℕ) ↦ (↑v : 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) ?_ ?_)
      ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
⊢ LE.le.{u_3} (α := M) (∑' (i : ℕ), (↑v : Set α → M) (a ∩ disjointed f i))
    (∑' (i : ℕ), (↑w : Set α → M) (a ∩ disjointed f i))
have refine_4 : Summable.{u_3, 0} (α := M) fun (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) ?_ ?_)
      ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
have refine_3 : ∀ (n : ℕ), MeasurableSet (a ∩ disjointed f n)
Tactic: refine (v.m_iUnion (fun n => ?_) ?_).summable
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
have refine_4 : ∀ (n : ℕ), MeasurableSet (a ∩ disjointed f n)
Tactic: refine (w.m_iUnion (fun n => ?_) ?_).summable
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ v ≤[⋃ (b : β), f b] w
have intro : ∀ (val : Encodable β), v ≤[⋃ (b : β), f b] w
Tactic: cases nonempty_encodable β
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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 ≤[⋃ (b : β), f b] w
have intro : v ≤[⋃ (i : ℕ), ⋃ b ∈ Encodable.decode₂ β i, f b] w
Tactic: rw [← Encodable.iUnion_decode₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
have intro : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) (⋃ b ∈ Encodable.decode₂ β n, f b)
Tactic: refine restrict_le_restrict_iUnion v w ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
⊢ v ≤[⋃ (i : ℕ), ⋃ b ∈ Encodable.decode₂ β i, f b] w
have intro₁ : ∀ (n : ℕ), v ≤[⋃ b ∈ Encodable.decode₂ β n, f b] w
Tactic: refine restrict_le_restrict_iUnion v w ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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 ∈ Encodable.decode₂ β n, f b] w
have intro : v ≤[⋃ (b : β), ⋃ (_ : Membership.mem (γ := Option β) none b), f b] w
Tactic: rcases Encodable.decode₂ β n with - | b
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ v ≤[⋃ b ∈ Encodable.decode₂ β n, f b] w
have intro₁ : ∀ (b : β), v ≤[⋃ b_1 ∈ some b, f b_1] w
Tactic: rcases Encodable.decode₂ β n with - | b
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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 ≤[i ∪ j] w
have rw : v ≤[⋃ (b : Bool), bif b then i else j] w
Tactic: rw [Set.union_eq_iUnion]