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 : 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
have refine_1 : ∀ (b : Bool), MeasurableSet (bif b then i else j)
Tactic: refine restrict_le_restrict_countable_iUnion v w ?_ ?_
-- 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
refine_1 : ∀ (b : Bool), MeasurableSet (bif b then i else j)
⊢ v ≤[⋃ (b : Bool), bif b then i else j] w
have refine_2 : ∀ (b : Bool), v ≤[bif b then i else j] w
Tactic: refine restrict_le_restrict_countable_iUnion v w ?_ ?_
-- 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 : VectorMeasure α M
i : Set α
hi₂ : 0 ≤[i] v
⊢ 0 ≤ (↑v : Set α → M) i
have pos : ∀ (hi₁ : MeasurableSet i), 0 ≤ (↑v : 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 : VectorMeasure α M
i : Set α
hi₂ : 0 ≤[i] v
pos : ∀ (hi₁ : MeasurableSet i), 0 ≤ (↑v : Set α → M) i
⊢ 0 ≤ (↑v : Set α → M) i
have neg : ∀ (hi₁ : ¬MeasurableSet i), 0 ≤ (↑v : 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 : VectorMeasure α M
i : Set α
hi₂ : 0 ≤[i] v
hi₁ : ¬MeasurableSet i
⊢ 0 ≤ (↑v : Set α → M) i
have neg : LE.le.{u_3} (α := M) 0 0
Tactic: rw [v.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 : VectorMeasure α M
i : Set α
hi₂ : v ≤[i] 0
⊢ (↑v : Set α → M) i ≤ 0
have pos : ∀ (hi₁ : MeasurableSet i), (↑v : Set α → M) i ≤ 0
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 : VectorMeasure α M
i : Set α
hi₂ : v ≤[i] 0
pos : ∀ (hi₁ : MeasurableSet i), (↑v : Set α → M) i ≤ 0
⊢ (↑v : Set α → M) i ≤ 0
have neg : ∀ (hi₁ : ¬MeasurableSet i), (↑v : Set α → M) i ≤ 0
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 : VectorMeasure α M
i : Set α
hi₂ : v ≤[i] 0
hi₁ : ¬MeasurableSet i
⊢ (↑v : Set α → M) i ≤ 0
have neg : LE.le.{u_3} (α := M) 0 0
Tactic: rw [v.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 : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ 0 ≤[i] v
have rw : 0 ≤ v.restrict i
Tactic: rw [restrict_zero, 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 : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
rw : 0 ≤ v.restrict i
⊢ 0 ≤[i] v
have rw₁ : LE.le (α := VectorMeasure α M) 0 0
Tactic: rw [restrict_zero, 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 : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ v ≤[i] 0
have rw : v.restrict i ≤ 0
Tactic: rw [restrict_zero, 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 : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
rw : v.restrict i ≤ 0
⊢ v ≤[i] 0
have rw₁ : LE.le (α := VectorMeasure α M) 0 0
Tactic: rw [restrict_zero, restrict_not_measurable _ hi]
-- 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 : LinearOrder M
v : VectorMeasure α M
i : Set α
hi : ¬v ≤[i] 0
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ 0 < (↑v : Set α → M) j
have hi₁ : MeasurableSet i
Tactic: have hi₁ : MeasurableSet i := measurable_of_not_restrict_le_zero _ hi
-- 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 : LinearOrder M
v : VectorMeasure α M
i : Set α
hi : ¬v ≤[i] 0
hi₁ : MeasurableSet i
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ 0 < (↑v : Set α → M) j
have hi₂ : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑v : Set α → M) j ≤ (↑0 : Set α → M) j
Tactic: rw [restrict_le_restrict_iff _ _ hi₁] at hi
Cleared hypotheses: hi, hi₁
-- 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 : LinearOrder M
v : VectorMeasure α M
i : Set α
hi : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑v : Set α → M) j ≤ (↑0 : Set α → M) j
hi₁ : MeasurableSet i
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ 0 < (↑v : Set α → M) j
have hi₂ : ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ (↑0 : Set α → M) j < (↑v : Set α → M) j
Tactic: push Not at hi
Cleared hypotheses: hi
-- 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 : AddLeftMono M
inst_4 : ContinuousAdd M
x x_1 x_2 : VectorMeasure α M
h : x_1 ≤ x_2
i : Set α
hi : MeasurableSet i
⊢ (↑(x + x_1) : Set α → M) i ≤ (↑(x + x_2) : Set α → M) i
have dsimp : (↑x : Set α → M) i + (↑x_1 : Set α → M) i ≤ (↑x : Set α → M) i + (↑x_2 : Set α → M) i
Tactic: dsimp
-- 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 : AddLeftMono M
inst_4 : ContinuousAdd M
x x_1 x_2 : VectorMeasure α M
h : x_1 ≤ x_2
i : Set α
hi : MeasurableSet i
⊢ (↑x : Set α → M) i + (↑x_1 : Set α → M) i ≤ (↑x : Set α → M) i + (↑x_2 : Set α → M) i
have grw : (↑x : Set α → M) i + (↑x_2 : Set α → M) i ≤ (↑x : Set α → M) i + (↑x_2 : Set α → M) i
Tactic: grw [h i hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → (↑w : Set α → N) s = 0 → (↑v : Set α → M) s = 0
s : Set α
hs : (↑w : Set α → N) s = 0
⊢ (↑v : Set α → M) s = 0
have pos : ∀ (hmeas : MeasurableSet s), (↑v : Set α → M) s = 0
Tactic: by_cases hmeas : MeasurableSet s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → (↑w : Set α → N) s = 0 → (↑v : Set α → M) s = 0
s : Set α
hs : (↑w : Set α → N) s = 0
pos : ∀ (hmeas : MeasurableSet s), (↑v : Set α → M) s = 0
⊢ (↑v : Set α → M) s = 0
have neg : ∀ (hmeas : ¬MeasurableSet s), (↑v : Set α → M) s = 0
Tactic: by_cases hmeas : MeasurableSet s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst : AddCommMonoid N
inst_1 : TopologicalSpace N
M : Type u_6
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
⊢ (↑(-v) : Set α → M) s = 0
have rw : -(↑v : Set α → M) s = 0
Tactic: rw [neg_apply, h hs, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst : AddCommMonoid N
inst_1 : TopologicalSpace N
M : Type u_6
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
rw : -(↑v : Set α → M) s = 0
⊢ (↑(-v) : Set α → M) s = 0
have rw₁ : Eq.{u_6 + 1} (α := M) (-0) 0
Tactic: rw [neg_apply, h hs, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst : AddCommMonoid N
inst_1 : TopologicalSpace N
M : Type u_6
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
rw : -(↑v : Set α → M) s = 0
rw₁ : Eq.{u_6 + 1} (α := M) (-0) 0
⊢ (↑(-v) : Set α → M) s = 0
have rw₂ : Eq.{u_6 + 1} (α := M) 0 0
Tactic: rw [neg_apply, h hs, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
N : Type u_6
inst_2 : AddCommGroup N
inst_3 : TopologicalSpace N
inst_4 : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : (↑(-w) : Set α → N) s = 0
⊢ (↑v : Set α → M) s = 0
have hs₁ : (↑w : Set α → N) s = 0
Tactic: rw [neg_apply, neg_eq_zero] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
inst_4 : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
⊢ (↑(v₁ + v₂) : Set α → M) s = 0
have rw : (↑v₁ : Set α → M) s + (↑v₂ : Set α → M) s = 0
Tactic: rw [add_apply, hv₁ hs, hv₂ hs, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
inst_4 : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
rw : (↑v₁ : Set α → M) s + (↑v₂ : Set α → M) s = 0
⊢ (↑(v₁ + v₂) : Set α → M) s = 0
have rw₁ : 0 + (↑v₂ : Set α → M) s = 0
Tactic: rw [add_apply, hv₁ hs, hv₂ hs, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
inst_4 : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
rw : (↑v₁ : Set α → M) s + (↑v₂ : Set α → M) s = 0
rw₁ : 0 + (↑v₂ : Set α → M) s = 0
⊢ (↑(v₁ + v₂) : Set α → M) s = 0
have rw₂ : HAdd.hAdd (α := M) 0 0 = 0
Tactic: rw [add_apply, hv₁ hs, hv₂ hs, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
inst_4 : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
rw : (↑v₁ : Set α → M) s + (↑v₂ : Set α → M) s = 0
rw₁ : 0 + (↑v₂ : Set α → M) s = 0
rw₂ : HAdd.hAdd (α := M) 0 0 = 0
⊢ (↑(v₁ + v₂) : Set α → M) s = 0
have rw₃ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [add_apply, hv₁ hs, hv₂ hs, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst : AddCommMonoid N
inst_1 : TopologicalSpace N
M : Type u_6
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
⊢ (↑(v₁ - v₂) : Set α → M) s = 0
have rw : (↑v₁ : Set α → M) s - (↑v₂ : Set α → M) s = 0
Tactic: rw [sub_apply, hv₁ hs, hv₂ hs, zero_sub, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst : AddCommMonoid N
inst_1 : TopologicalSpace N
M : Type u_6
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
rw : (↑v₁ : Set α → M) s - (↑v₂ : Set α → M) s = 0
⊢ (↑(v₁ - v₂) : Set α → M) s = 0
have rw₁ : 0 - (↑v₂ : Set α → M) s = 0
Tactic: rw [sub_apply, hv₁ hs, hv₂ hs, zero_sub, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst : AddCommMonoid N
inst_1 : TopologicalSpace N
M : Type u_6
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
rw : (↑v₁ : Set α → M) s - (↑v₂ : Set α → M) s = 0
rw₁ : 0 - (↑v₂ : Set α → M) s = 0
⊢ (↑(v₁ - v₂) : Set α → M) s = 0
have rw₂ : HSub.hSub (α := M) 0 0 = 0
Tactic: rw [sub_apply, hv₁ hs, hv₂ hs, zero_sub, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst : AddCommMonoid N
inst_1 : TopologicalSpace N
M : Type u_6
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
rw : (↑v₁ : Set α → M) s - (↑v₂ : Set α → M) s = 0
rw₁ : 0 - (↑v₂ : Set α → M) s = 0
rw₂ : HSub.hSub (α := M) 0 0 = 0
⊢ (↑(v₁ - v₂) : Set α → M) s = 0
have rw₃ : Eq.{u_6 + 1} (α := M) (-0) 0
Tactic: rw [sub_apply, hv₁ hs, hv₂ hs, zero_sub, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst : AddCommMonoid N
inst_1 : TopologicalSpace N
M : Type u_6
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
rw : (↑v₁ : Set α → M) s - (↑v₂ : Set α → M) s = 0
rw₁ : 0 - (↑v₂ : Set α → M) s = 0
rw₂ : HSub.hSub (α := M) 0 0 = 0
rw₃ : Eq.{u_6 + 1} (α := M) (-0) 0
⊢ (↑(v₁ - v₂) : Set α → M) s = 0
have rw₄ : Eq.{u_6 + 1} (α := M) 0 0
Tactic: rw [sub_apply, hv₁ hs, hv₂ hs, zero_sub, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
R : Type u_6
inst_4 : Semiring R
inst_5 : DistribMulAction R M
inst_6 : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
⊢ (↑(r • v) : Set α → M) s = 0
have rw : r • (↑v : Set α → M) s = 0
Tactic: rw [smul_apply, h hs, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
R : Type u_6
inst_4 : Semiring R
inst_5 : DistribMulAction R M
inst_6 : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
rw : r • (↑v : Set α → M) s = 0
⊢ (↑(r • v) : Set α → M) s = 0
have rw₁ : HSMul.hSMul (β := M) r 0 = 0
Tactic: rw [smul_apply, h hs, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
R : Type u_6
inst_4 : Semiring R
inst_5 : DistribMulAction R M
inst_6 : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
rw : r • (↑v : Set α → M) s = 0
rw₁ : HSMul.hSMul (β := M) r 0 = 0
⊢ (↑(r • v) : Set α → M) s = 0
have rw₂ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [smul_apply, h hs, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst_4 : MeasureSpace β
h : v ≪ᵥ w
f : α → β
⊢ AbsolutelyContinuous (m := MeasureSpace.toMeasurableSpace) (v.map f) (w.map f)
have pos : ∀ (hf : Measurable f), AbsolutelyContinuous (m := MeasureSpace.toMeasurableSpace) (v.map f) (w.map f)
Tactic: by_cases hf : Measurable f
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst_4 : MeasureSpace β
h : v ≪ᵥ w
f : α → β
pos : ∀ (hf : Measurable f), AbsolutelyContinuous (m := MeasureSpace.toMeasurableSpace) (v.map f) (w.map f)
⊢ AbsolutelyContinuous (m := MeasureSpace.toMeasurableSpace) (v.map f) (w.map f)
have neg : ∀ (hf : ¬Measurable f), AbsolutelyContinuous (m := MeasureSpace.toMeasurableSpace) (v.map f) (w.map f)
Tactic: by_cases hf : Measurable f
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst_4 : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
⊢ AbsolutelyContinuous (m := MeasureSpace.toMeasurableSpace) (v.map f) (w.map f)
have pos : ∀ (s : Set β) (hs : MeasurableSet s) (hws : (↑(w.map f) : Set β → N) s = 0), (↑(v.map f) : Set β → M) s = 0
Tactic: refine mk fun s hs hws => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst_4 : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
hws : (↑(w.map f) : Set β → N) s = 0
⊢ (↑(v.map f) : Set β → M) s = 0
have pos : ∀ (hws : (↑w : Set α → N) (f ⁻¹' s) = 0), (↑v : Set α → M) (f ⁻¹' s) = 0
Tactic: rw [map_apply _ hf hs] at hws ⊢
Cleared hypotheses: hws
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst_4 : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : ¬Measurable f
s : Set β
h_1 : (↑(w.map f) : Set β → N) s = 0
⊢ (↑(v.map f) : Set β → M) s = 0
have neg : Eq.{u_4 + 1} (α := M) ((↑0 : Set β → M) s) 0
Tactic: rw [map_not_measurable v hf, zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst_4 : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : ¬Measurable f
s : Set β
h_1 : (↑(w.map f) : Set β → N) s = 0
neg : Eq.{u_4 + 1} (α := M) ((↑0 : Set β → M) s) 0
⊢ (↑(v.map f) : Set β → M) s = 0
have neg₁ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [map_not_measurable v hf, zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
⊢ (∀ ⦃s : Set α⦄,
      Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → (↑v : Set α → M) s = 0) ↔
    v ≪ᵥ μ
have mp : (∀ ⦃s : Set α⦄,
    Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → (↑v : Set α → M) s = 0) →
  v ≪ᵥ μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
mp :
  (∀ ⦃s : Set α⦄,
      Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → (↑v : Set α → M) s = 0) →
    v ≪ᵥ μ
⊢ (∀ ⦃s : Set α⦄,
      Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → (↑v : Set α → M) s = 0) ↔
    v ≪ᵥ μ
have mpr : v ≪ᵥ μ →
  ∀ ⦃s : Set α⦄, Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → (↑v : Set α → M) s = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h :
  ∀ ⦃s : Set α⦄, Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → (↑v : Set α → M) s = 0
⊢ v ≪ᵥ μ
have mp : ∀ (s : Set α) (hmeas : MeasurableSet s) (hs : (↑μ : Set α → ℝ≥0∞) s = 0),
  Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine mk fun s hmeas hs => h ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h :
  ∀ ⦃s : Set α⦄, Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → (↑v : Set α → M) s = 0
s : Set α
hmeas : MeasurableSet s
hs : (↑μ : Set α → ℝ≥0∞) s = 0
⊢ Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have mp : (μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s = (↑μ : Set α → ℝ≥0∞) s
Tactic: rw [← hs, ennrealToMeasure_apply hmeas]