awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ (↑s : Set α → ℝ) A
hB₂ : 0 ≤ (↑s : Set α → ℝ) B
hAB : (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) B = 0
⊢ (↑s : Set α → ℝ) A = 0
have linarith : (↑s : Set α → ℝ) A < 0 → 0 - (↑s : Set α → ℝ) A + ((↑s : Set α → ℝ) A - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ (↑s : Set α → ℝ) A
hB₂ : 0 ≤ (↑s : Set α → ℝ) B
hAB : (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) B = 0
linarith : (↑s : Set α → ℝ) A < 0 → 0 - (↑s : Set α → ℝ) A + ((↑s : Set α → ℝ) A - 0) = 0
⊢ (↑s : Set α → ℝ) A = 0
have linarith₁ : 0 < (↑s : Set α → ℝ) A →
  0 - (↑s : Set α → ℝ) B + ((↑s : Set α → ℝ) A + (↑s : Set α → ℝ) B - 0) + (0 - (↑s : Set α → ℝ) A) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : (↑s : Set α → ℝ) A ≤ 0
hB₂ : (↑s : Set α → ℝ) B ≤ 0
hAB : (↑s : Set α → ℝ) (A ∪ B) = 0
⊢ (↑s : Set α → ℝ) A = 0
have hAB₁ : (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) B = 0
Tactic: rw [of_union h hA₁ hB₁] at hAB
Cleared hypotheses: hAB
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : (↑s : Set α → ℝ) A ≤ 0
hB₂ : (↑s : Set α → ℝ) B ≤ 0
hAB : (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) B = 0
⊢ (↑s : Set α → ℝ) A = 0
have linarith : (↑s : Set α → ℝ) A < 0 →
  (↑s : Set α → ℝ) B - 0 + -((↑s : Set α → ℝ) A + (↑s : Set α → ℝ) B - 0) + ((↑s : Set α → ℝ) A - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : (↑s : Set α → ℝ) A ≤ 0
hB₂ : (↑s : Set α → ℝ) B ≤ 0
hAB : (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) B = 0
linarith :
  (↑s : Set α → ℝ) A < 0 →
    (↑s : Set α → ℝ) B - 0 + -((↑s : Set α → ℝ) A + (↑s : Set α → ℝ) B - 0) + ((↑s : Set α → ℝ) A - 0) = 0
⊢ (↑s : Set α → ℝ) A = 0
have linarith₁ : 0 < (↑s : Set α → ℝ) A → (↑s : Set α → ℝ) A - 0 + (0 - (↑s : Set α → ℝ) A) = 0
Tactic: linarith
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ insert a s, MeasurableSet (f b)
⊢ (↑v : Set α → M) (⋃ b ∈ insert a s, f b) = ∑ p ∈ insert a s, (↑v : Set α → M) (f p)
have insert : (↑v : Set α → M) (f a ∪ ⋃ x ∈ s, f x) = (↑v : Set α → M) (f a) + ∑ p ∈ s, (↑v : Set α → M) (f p)
Tactic: simp only [Finset.mem_insert, iUnion_iUnion_eq_or_left, has, not_false_eq_true,
      Finset.sum_insert]
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ insert a s, MeasurableSet (f b)
⊢ (↑v : Set α → M) (f a ∪ ⋃ x ∈ s, f x) = (↑v : Set α → M) (f a) + ∑ p ∈ s, (↑v : Set α → M) (f p)
have insert : (↑s : Set ι).PairwiseDisjoint f
Tactic: rw [of_union, ih]
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(Insert.insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ Insert.insert a s, MeasurableSet (f b)
insert : (↑s : Set ι).PairwiseDisjoint f
⊢ (↑v : Set α → M) (f a ∪ ⋃ x ∈ s, f x) = (↑v : Set α → M) (f a) + ∑ p ∈ s, (↑v : Set α → M) (f p)
have insert₁ : ∀ b ∈ s, MeasurableSet (f b)
Tactic: rw [of_union, ih]
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(Insert.insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ Insert.insert a s, MeasurableSet (f b)
insert : (↑s : Set ι).PairwiseDisjoint f
insert₁ : ∀ b ∈ s, MeasurableSet (f b)
⊢ (↑v : Set α → M) (f a ∪ ⋃ x ∈ s, f x) = (↑v : Set α → M) (f a) + ∑ p ∈ s, (↑v : Set α → M) (f p)
have insert₂ : Disjoint (f a) (⋃ x ∈ s, f x)
Tactic: rw [of_union, ih]
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(Insert.insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ Insert.insert a s, MeasurableSet (f b)
insert : (↑s : Set ι).PairwiseDisjoint f
insert₁ : ∀ b ∈ s, MeasurableSet (f b)
insert₂ : Disjoint (f a) (⋃ x ∈ s, f x)
⊢ (↑v : Set α → M) (f a ∪ ⋃ x ∈ s, f x) = (↑v : Set α → M) (f a) + ∑ p ∈ s, (↑v : Set α → M) (f p)
have insert₃ : MeasurableSet (f a)
Tactic: rw [of_union, ih]
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(Insert.insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ Insert.insert a s, MeasurableSet (f b)
insert : (↑s : Set ι).PairwiseDisjoint f
insert₁ : ∀ b ∈ s, MeasurableSet (f b)
insert₂ : Disjoint (f a) (⋃ x ∈ s, f x)
insert₃ : MeasurableSet (f a)
⊢ (↑v : Set α → M) (f a ∪ ⋃ x ∈ s, f x) = (↑v : Set α → M) (f a) + ∑ p ∈ s, (↑v : Set α → M) (f p)
have insert₄ : MeasurableSet.{u_1} (α := α) (⋃ x ∈ s, f x)
Tactic: rw [of_union, ih]
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ insert a s, MeasurableSet (f b)
⊢ Disjoint (f a) (⋃ x ∈ s, f x)
have insert : ∀ (i : ι) (i_1 : i ∈ s), Disjoint (f a) (f i)
Tactic: simp only [disjoint_iUnion_right]
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
ι : Type u_4
s : Finset ι
f : ι → Set α
hd : (↑s : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ s, MeasurableSet (f b)
⊢ (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
have empty : ∀ (hd : (↑∅ : Set ι).PairwiseDisjoint f) (hm : ∀ (b : ι), Membership.mem (γ := Finset ι) ∅ b → MeasurableSet (f b)),
  (↑v : Set α → M) (⋃ (b : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ b), f b) = ∑ p ∈ ∅, (↑v : Set α → M) (f p)
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert a s has ih =>
    simp only [Finset.mem_insert, iUnion_iUnion_eq_or_left, has, not_false_eq_true,
      Finset.sum_insert]
    rw [of_union, ih]
    · exact hd.subset (by simp)
    · grind
    · simp only [disjoint_iUnion_right]
      exact fun i hi ↦ hd (by simp) (by simp [hi]) (by grind)
    · apply hm _ (by simp)
    · apply Finset.measurableSet_biUnion _ (by grind)
Cleared hypotheses: s, hd, hm
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
ι : Type u_4
s : Finset ι
f : ι → Set α
hd : (↑s : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ s, MeasurableSet (f b)
empty :
  ∀ (hd : (↑∅ : Set ι).PairwiseDisjoint f) (hm : ∀ (b : ι), Membership.mem (γ := Finset ι) ∅ b → MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ (b : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ b), f b) = ∑ p ∈ ∅, (↑v : Set α → M) (f p)
⊢ (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (ih :
    ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
      (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p))
  (hd : (↑(insert a s) : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ insert a s, MeasurableSet (f b)),
  (↑v : Set α → M) (⋃ b ∈ insert a s, f b) = ∑ p ∈ insert a s, (↑v : Set α → M) (f p)
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert a s has ih =>
    simp only [Finset.mem_insert, iUnion_iUnion_eq_or_left, has, not_false_eq_true,
      Finset.sum_insert]
    rw [of_union, ih]
    · exact hd.subset (by simp)
    · grind
    · simp only [disjoint_iUnion_right]
      exact fun i hi ↦ hd (by simp) (by simp [hi]) (by grind)
    · apply hm _ (by simp)
    · apply Finset.measurableSet_biUnion _ (by grind)
Cleared hypotheses: s, hd, hm
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
ι : Type u_4
s : Finset ι
f : ι → Set α
hd : (↑s : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ s, MeasurableSet (f b)
⊢ (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
have empty : ∀ (hd : (↑∅ : Set ι).PairwiseDisjoint f) (hm : ∀ (b : ι), Membership.mem (γ := Finset ι) ∅ b → MeasurableSet (f b)),
  (↑v : Set α → M) (⋃ (b : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ b), f b) = ∑ p ∈ ∅, (↑v : Set α → M) (f p)
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s has ih =>
    simp only [Finset.mem_insert, iUnion_iUnion_eq_or_left, has, not_false_eq_true,
      Finset.sum_insert]
    rw [of_union, ih]
    · exact hd.subset (by simp)
    · grind
    · simp only [disjoint_iUnion_right]
      exact fun i hi ↦ hd (by simp) (by simp [hi]) (by grind)
    · apply hm _ (by simp)
    · apply Finset.measurableSet_biUnion _ (by grind)
Cleared hypotheses: s, hd, hm
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
ι : Type u_4
s : Finset ι
f : ι → Set α
hd : (↑s : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ s, MeasurableSet (f b)
empty :
  ∀ (hd : (↑∅ : Set ι).PairwiseDisjoint f) (hm : ∀ (b : ι), Membership.mem (γ := Finset ι) ∅ b → MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ (b : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ b), f b) = ∑ p ∈ ∅, (↑v : Set α → M) (f p)
⊢ (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (ih :
    ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
      (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p))
  (hd : (↑(insert a s) : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ insert a s, MeasurableSet (f b)),
  (↑v : Set α → M) (⋃ b ∈ insert a s, f b) = ∑ p ∈ insert a s, (↑v : Set α → M) (f p)
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s has ih =>
    simp only [Finset.mem_insert, iUnion_iUnion_eq_or_left, has, not_false_eq_true,
      Finset.sum_insert]
    rw [of_union, ih]
    · exact hd.subset (by simp)
    · grind
    · simp only [disjoint_iUnion_right]
      exact fun i hi ↦ hd (by simp) (by simp [hi]) (by grind)
    · apply hm _ (by simp)
    · apply Finset.measurableSet_biUnion _ (by grind)
Cleared hypotheses: s, hd, hm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
⊢ Tendsto (fun (n : ℕ) ↦ (↑v : Set α → M) (s n)) atTop (𝓝 ((↑v : Set α → M) (⋃ (n : ℕ), s n)))
have ht : ∀ (n : ℕ), MeasurableSet (t n)
Tactic: have ht n : MeasurableSet (t n) := .disjointed (fun n ↦ hs n) n
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
have rw : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (i : ℕ), disjointed s i))
Tactic: rw [← iUnion_disjointed]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ Tendsto (fun (n : ℕ) ↦ (↑v : Set α → M) (s n)) atTop (𝓝 ((↑v : Set α → M) (⋃ (n : ℕ), s n)))
have this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
Tactic: have : HasSum (fun n ↦ v (t n)) (v (⋃ n, s n)) := by
    rw [← iUnion_disjointed]
    apply m_iUnion _ ht (disjoint_disjointed _)
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
⊢ Tendsto (fun (n : ℕ) ↦ (↑v : Set α → M) (s n)) atTop (𝓝 ((↑v : Set α → M) (⋃ (n : ℕ), s n)))
have h : ∀ (n : ℕ),
  (↑v : Set α → M) (s n) = ((fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (↑v : Set α → M) (t i)) ∘ fun (a : ℕ) ↦ a + 1) n
Tactic: convert! (HasSum.tendsto_sum_nat this).comp (tendsto_add_atTop_nat 1) with n
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
n : ℕ
⊢ (↑v : Set α → M) (s n) = ((fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (↑v : Set α → M) (t i)) ∘ fun (a : ℕ) ↦ a + 1) n
have h : (↑v : Set α → M) (s n) = ∑ i ∈ Finset.range (n + 1), (↑v : Set α → M) (t i)
Tactic: dsimp
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
n : ℕ
⊢ (↑v : Set α → M) (s n) = ∑ i ∈ Finset.range (n + 1), (↑v : Set α → M) (t i)
have h : (↑v : Set α → M) (s n) = (↑v : Set α → M) (⋃ b ∈ Finset.range (n + 1), t b)
Tactic: rw [← of_biUnion_finset]
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
n : ℕ
h : (↑v : Set α → M) (s n) = (↑v : Set α → M) (⋃ b ∈ Finset.range (n + 1), t b)
⊢ (↑v : Set α → M) (s n) = ∑ i ∈ Finset.range (n + 1), (↑v : Set α → M) (t i)
have h₁ : (↑(Finset.range (n + 1)) : Set ℕ).PairwiseDisjoint t
Tactic: rw [← of_biUnion_finset]
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
n : ℕ
h : (↑v : Set α → M) (s n) = (↑v : Set α → M) (⋃ b ∈ Finset.range (n + 1), t b)
h₁ : (↑(Finset.range (n + 1)) : Set ℕ).PairwiseDisjoint t
⊢ (↑v : Set α → M) (s n) = ∑ i ∈ Finset.range (n + 1), (↑v : Set α → M) (t i)
have h₂ : ∀ b ∈ Finset.range (n + 1), MeasurableSet (t b)
Tactic: rw [← of_biUnion_finset]
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
n : ℕ
⊢ (↑v : Set α → M) (s n) = (↑v : Set α → M) (⋃ b ∈ Finset.range (n + 1), t b)
have h : (↑v : Set α → M) (s n) = (↑v : Set α → M) ((partialSups s : (a : ℕ) → Set α) n)
Tactic: rw [biUnion_range_succ_disjointed, Monotone.partialSups_eq hm]
-- 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
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
n : ℕ
h : (↑v : Set α → M) (s n) = (↑v : Set α → M) ((partialSups s : (a : ℕ) → Set α) n)
⊢ (↑v : Set α → M) (s n) = (↑v : Set α → M) (⋃ b ∈ Finset.range (n + 1), t b)
have h₁ : (↑v : Set α → M) (s n) = (↑v : Set α → M) (s n)
Tactic: rw [biUnion_range_succ_disjointed, Monotone.partialSups_eq hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
⊢ Tendsto (fun (n : ℕ) ↦ (↑v : Set α → M) (s n)) atTop (𝓝 ((↑v : Set α → M) (⋂ (n : ℕ), s n)))
have I : ∀ (n : ℕ), (↑v : Set α → M) (s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ
Tactic: have I n : v (s n) = v univ - v (s n)ᶜ := by simp [of_compl (hs n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), (↑v : Set α → M) (s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ
⊢ (↑v : Set α → M) (⋂ (n : ℕ), s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)
have rw : (↑v : Set α → M) (⋂ (n : ℕ), s n) = (↑v : Set α → M) (⋃ (b : ℕ), (s b)ᶜ)ᶜ
Tactic: rw [← of_compl (MeasurableSet.iUnion (fun n ↦ (hs n).compl))]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), (↑v : Set α → M) (s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ
⊢ Tendsto (fun (n : ℕ) ↦ (↑v : Set α → M) (s n)) atTop (𝓝 ((↑v : Set α → M) (⋂ (n : ℕ), s n)))
have J : (↑v : Set α → M) (⋂ (n : ℕ), s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)
Tactic: have J : v (⋂ n, s n) = v univ - v (⋃ n, (s n)ᶜ) := by
    rw [← of_compl (MeasurableSet.iUnion (fun n ↦ (hs n).compl))]
    simp
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), (↑v : Set α → M) (s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ
J : (↑v : Set α → M) (⋂ (n : ℕ), s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)
⊢ Tendsto (fun (n : ℕ) ↦ (↑v : Set α → M) (s n)) atTop (𝓝 ((↑v : Set α → M) (⋂ (n : ℕ), s n)))
have simp_rw : Tendsto (fun (n : ℕ) ↦ (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ) atTop
  (𝓝 ((↑v : Set α → M) univ - (↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)))
Tactic: simp_rw [I, J]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), (↑v : Set α → M) (s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ
J : (↑v : Set α → M) (⋂ (n : ℕ), s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)
⊢ Tendsto (fun (n : ℕ) ↦ (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ) atTop
    (𝓝 ((↑v : Set α → M) univ - (↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)))
have apply : Tendsto (fun (x : ℕ) ↦ (↑v : Set α → M) (s x)ᶜ) atTop (𝓝 ((↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)))
Tactic: apply tendsto_const_nhds.sub
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
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
r : R
v : VectorMeasure α M
⊢ (r • (↑v : Set α → M)) ∅ = 0
have rw : r • (↑v : Set α → M) ∅ = 0
Tactic: rw [Pi.smul_apply, empty, smul_zero]