awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
nontriviality : Subsingleton β → AEMeasurable f μ
nontriviality₁ nontriviality₂ : Nontrivial β → AEMeasurable f μ
nontriviality₃ : Nontrivial β → ∀ (inhabited_h : Inhabited β), AEMeasurable f μ
nontriviality₄ :
  Nontrivial β →
    ∀ (inhabited_h : Inhabited β) (S : Set (Set β)) (hSc : S.Countable) [hc : MeasurableSpace.CountablyGenerated β]
      (h : NullMeasurable f μ), AEMeasurable f μ
nontriviality₅ :
  Nontrivial β →
    ∀ (inhabited_h : Inhabited β) (S : Set (Set β)) (hSc : S.Countable) [hc : MeasurableSpace.CountablyGenerated β]
      (h : NullMeasurable f μ) (T : (s : Set β) → Set α) (hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s)
      (hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)) (hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s),
      AEMeasurable f μ
⊢ AEMeasurable f μ
have nontriviality₆ : Nontrivial β →
  ∀ (inhabited_h : Inhabited β) (S : Set (Set β)) (hSc : S.Countable) [hc : MeasurableSpace.CountablyGenerated β]
    (h : NullMeasurable f μ) (T : (s : Set β) → Set α) (hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s)
    (hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)) (hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s)
    (U : (s : Set β) → Set α) (hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s)
    (hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)) (hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s),
    AEMeasurable f μ
Tactic: classical
  nontriviality β; inhabit β
  rcases hc.1 with ⟨S, hSc, rfl⟩
  choose! T hTf hTm hTeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_subset_ae_eq
  choose! U hUf hUm hUeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_superset_ae_eq
  set v := ⋃ s ∈ S, U s \ T s
  have hvm : MeasurableSet v := .biUnion hSc fun s hs ↦ (hUm s hs).diff (hTm s hs)
  have hvμ : μ v = 0 := (measure_biUnion_null_iff hSc).2 fun s hs ↦ ae_le_set.1 <|
    ((hUeq s hs).trans (hTeq s hs).symm).le
  refine ⟨v.piecewise (fun _ ↦ default) f, ?_, measure_mono_null (fun x ↦
    not_imp_comm.2 fun hxv ↦ (piecewise_eq_of_notMem _ _ _ hxv).symm) hvμ⟩
  refine measurable_of_restrict_of_restrict_compl hvm ?_ ?_
  · rw [restrict_piecewise]
    apply measurable_const
  · rw [restrict_piecewise_compl, restrict_eq]
    refine measurable_generateFrom fun s hs ↦ .of_subtype_image ?_
    rw [preimage_comp, Subtype.image_preimage_coe]
    convert! (hTm s hs).diff hvm using 1
    rw [inter_comm]
    refine Set.ext fun x ↦ and_congr_left fun hxv ↦ ⟨fun hx ↦ ?_, fun hx ↦ hTf s hs hx⟩
    exact by_contra fun hx' ↦ hxv <| mem_biUnion hs ⟨hUf s hs hx, hx'⟩
Cleared hypotheses: inst, hc, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst_1 : MeasurableSpace.CountablyGenerated.{u_3} (↑t : Type u_3)
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ AEMeasurable f μ
have inl : ∀ [MeasurableSpace.CountablyGenerated.{u_3} (↑∅ : Type u_3)] (hft : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set β) ∅ (f x)),
  AEMeasurable f μ
Tactic: rcases eq_empty_or_nonempty t with rfl | hne
Cleared hypotheses: t, inst_1, hft
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst_1 : MeasurableSpace.CountablyGenerated.{u_3} (↑t : Type u_3)
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ, f x ∈ t
inl :
  ∀ [MeasurableSpace.CountablyGenerated.{u_3} (↑∅ : Type u_3)]
    (hft : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set β) ∅ (f x)), AEMeasurable f μ
⊢ AEMeasurable f μ
have inr : ∀ (hne : t.Nonempty), AEMeasurable f μ
Tactic: rcases eq_empty_or_nonempty t with rfl | hne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
h : NullMeasurable f μ
inst_1 : MeasurableSpace.CountablyGenerated.{u_3} (↑∅ : Type u_3)
hft : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set β) ∅ (f x)
⊢ AEMeasurable f μ
have inl : ∀ (h : NullMeasurable f 0) (hft : ∀ᵐ (x : α) ∂0, Membership.mem (γ := Set β) ∅ (f x)), AEMeasurable (_m := m0) f 0
Tactic: obtain rfl : μ = 0 := by simpa using hft
Cleared hypotheses: μ, h, hft
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst_1 : MeasurableSpace.CountablyGenerated.{u_3} (↑t : Type u_3)
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ, f x ∈ t
hne : t.Nonempty
⊢ AEMeasurable f μ
have hft₁ : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
Tactic: rw [← μ.ae_completion] at hft
Cleared hypotheses: hft, hne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst_1 : MeasurableSpace.CountablyGenerated.{u_3} (↑t : Type u_3)
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
⊢ AEMeasurable f μ
have inr : ∀ (f' : α → β) (hf'm : NullMeasurable f' μ) (hf't : range f' ⊆ t) (hff' : f =ᶠ[ae μ] f'), AEMeasurable f μ
Tactic: obtain ⟨f', hf'm, hf't, hff'⟩ :
        ∃ f' : α → β, NullMeasurable f' μ ∧ range f' ⊆ t ∧ f =ᵐ[μ] f' :=
      h.measurable'.aemeasurable.exists_ae_eq_range_subset hft hne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst_1 : MeasurableSpace.CountablyGenerated.{u_3} (↑t : Type u_3)
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : α → β
hf'm : NullMeasurable f' μ
hf't : range f' ⊆ t
hff' : f =ᶠ[ae μ] f'
⊢ AEMeasurable f μ
have hf't₁ : ∀ (y : α), f' y ∈ t
Tactic: rw [range_subset_iff] at hf't
Cleared hypotheses: hf't, hff'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst_1 : MeasurableSpace.CountablyGenerated.{u_3} (↑t : Type u_3)
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : α → β
hf'm : NullMeasurable f' μ
hf't : ∀ (y : α), f' y ∈ t
hff' : f =ᶠ[ae μ] f'
⊢ AEMeasurable f μ
have inr : ∀ (f' : (i : α) → (↑t : Type u_3)) (hf'm : NullMeasurable.{u_2, u_3} (β := β) (fun (i : α) ↦ (↑(f' i) : β)) μ)
  (hff' : f =ᶠ[ae μ] fun (i : α) ↦ (↑(f' i) : β)), AEMeasurable f μ
Tactic: lift f' to α → t using hf't
Cleared hypotheses: f', hf'm, hf't, hff'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst_1 : MeasurableSpace.CountablyGenerated.{u_3} (↑t : Type u_3)
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : (i : α) → (↑t : Type u_3)
hf'm : NullMeasurable.{u_2, u_3} (β := β) (fun (i : α) ↦ (↑(f' i) : β)) μ
hff' : f =ᶠ[ae μ] fun (i : α) ↦ (↑(f' i) : β)
⊢ AEMeasurable f μ
have hf'm₁ : NullMeasurable f' μ
Tactic: replace hf'm : NullMeasurable f' μ := hf'm.measurable'.subtype_mk
Cleared hypotheses: hf'm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
ι : Type u_7
m : ι → Measure α
f : α → β
hf : AEMeasurable f (sum m)
⊢ Eq (α := Measure β) (map f (sum m)) (sum fun (i : ι) ↦ map f (m i))
have h : ∀ (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((map f (sum m) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (i : ι) ↦ map f (m i) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
ι : Type u_7
m : ι → Measure α
f : α → β
hf : AEMeasurable f (sum m)
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((map f (sum m) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (i : ι) ↦ map f (m i) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (∑' (i : ι), (m i : (a : Set α) → ℝ≥0∞) (f ⁻¹' s))
  (∑' (i : ι), ((map f (m i) : Measure β) : (a : Set β) → ℝ≥0∞) s)
Tactic: rw [map_apply_of_aemeasurable hf hs, sum_apply₀ _ (hf.nullMeasurable hs), sum_apply _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
ι : Type u_7
m : ι → Measure α
f : α → β
hf : AEMeasurable f (sum m)
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (∑' (i : ι), (m i : (a : Set α) → ℝ≥0∞) (f ⁻¹' s))
    (∑' (i : ι), ((map f (m i) : Measure β) : (a : Set β) → ℝ≥0∞) s)
have M : ∀ (i : ι), AEMeasurable f (m i)
Tactic: have M i : AEMeasurable f (m i) := hf.mono_measure (le_sum m i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
ι : Type u_7
β : Type u_8
mβ : MeasurableSpace β
m : ι → Measure α
f : α → β
s : Finset ι
hf : AEMeasurable (_m := m0) f (∑ i ∈ s, m i)
⊢ Eq (α := Measure β) (map f (∑ i ∈ s, m i)) (∑ i ∈ s, map f (m i))
have rw : AEMeasurable (_m := m0) f (sum fun (i : ↥s) ↦ m (↑i : ι))
Tactic: rw [← sum_coe_finset, ← sum_coe_finset, Measure.map_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
inst_2 : MeasurableSpace δ
f_1 g : α → β
μ_1 ν μ : Measure α
f : α → β
inst_3 : SFinite μ
⊢ SFinite (m0 := inst) (map f μ)
have pos : ∀ (H : AEMeasurable f μ), SFinite (m0 := inst) (map f μ)
Tactic: by_cases H : AEMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
inst_2 : MeasurableSpace δ
f_1 g : α → β
μ_1 ν μ : Measure α
f : α → β
inst_3 : SFinite μ
pos : ∀ (H : AEMeasurable f μ), SFinite (m0 := inst) (map f μ)
⊢ SFinite (m0 := inst) (map f μ)
have neg : ∀ (H : ¬AEMeasurable f μ), SFinite (m0 := inst) (map f μ)
Tactic: by_cases H : AEMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
inst_2 : MeasurableSpace δ
f_1 g : α → β
μ_1 ν μ : Measure α
f : α → β
inst_3 : SFinite μ
H : AEMeasurable f μ
⊢ SFinite (m0 := inst) (map f μ)
have pos : ∀ (H : AEMeasurable f (sum (sfiniteSeq μ))), SFinite (m0 := inst) (map f (sum (sfiniteSeq μ)))
Tactic: rw [← sum_sfiniteSeq μ] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
inst_2 : MeasurableSpace δ
f_1 g : α → β
μ_1 ν μ : Measure α
f : α → β
inst_3 : SFinite μ
H : AEMeasurable f (sum (sfiniteSeq μ))
⊢ SFinite (m0 := inst) (map f (sum (sfiniteSeq μ)))
have pos : SFinite.{u_3} (α := β) (m0 := inst) (sum fun (i : ℕ) ↦ map f (sfiniteSeq μ i))
Tactic: rw [map_sum H]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
inst_2 : MeasurableSpace δ
f_1 g : α → β
μ_1 ν μ : Measure α
f : α → β
inst_3 : SFinite μ
H : ¬AEMeasurable f μ
⊢ SFinite (m0 := inst) (map f μ)
have neg : SFinite.{u_3} (α := β) (m0 := inst) 0
Tactic: rw [map_of_not_aemeasurable H]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set α
hs : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rcases : ∀ (t : Set α) (h1t : s ⊆ t) (h2t : MeasurableSet t)
  (h3t : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases exists_measurable_superset_of_null hs with ⟨t, h1t, h2t, h3t⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
s : Set α
hνs : Eq (α := ℝ≥0∞) ((c • ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : ∀ (hνs : HSMul.hSMul (β := ℝ≥0∞) c 1 = 0 ∨ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  HSMul.hSMul (β := ℝ≥0∞) c 1 = 0 ∨ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [smul_apply, ← smul_one_smul ℝ≥0∞, smul_eq_mul, mul_eq_zero] at hνs ⊢
Cleared hypotheses: hνs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
s : Set α
hs : Eq (α := ℝ≥0∞) ((ν + ν' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ₁ + μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have simp : ∀
  (hs :
    Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((ν' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [coe_add, Pi.add_apply, add_eq_zero] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
⊢ μ₁ + μ₂ ≪ ν ↔ μ₁ ≪ ν ∧ μ₂ ≪ ν
have refine_1 : ∀ (h : μ₁ + μ₂ ≪ ν), μ₁ ≪ ν ∧ μ₂ ≪ ν
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ (h.1.add h.2).trans ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
refine_1 : ∀ (h : μ₁ + μ₂ ≪ ν), μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ μ₁ + μ₂ ≪ ν ↔ μ₁ ≪ ν ∧ μ₂ ≪ ν
have refine_2 : ∀ (h : μ₁ ≪ ν ∧ μ₂ ≪ ν), ν + ν ≪ ν
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ (h.1.add h.2).trans ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AbsolutelyContinuous (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
⊢ μ₁ ≪ ν ∧ μ₂ ≪ ν
have this : ∀ (s : Set α),
  Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have : ∀ s, ν s = 0 → μ₁ s = 0 ∧ μ₂ s = 0 := by intro s hs0; simpa using h hs0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ ν + ν ≪ ν
have refine_2 : HSMul.hSMul (α := ℝ≥0) 2 ν ≪ ν
Tactic: rw [← two_smul ℝ≥0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AbsolutelyContinuous (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
ν' : Measure α
s : Set α
hs : Eq (α := ℝ≥0∞) ((ν + ν' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have hs₁ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
  Eq (α := ℝ≥0∞) ((ν' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [coe_add, Pi.add_apply, add_eq_zero] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
t : Set α
ht : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have contrapose! : ∀ (ht : LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: contrapose! ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
i : ι
hνμ : ν ≪ μs i
⊢ ν ≪ sum μs
have refine : ∀ (s : Set α) (hs : MeasurableSet s) (hs0 : Eq (α := ℝ≥0∞) ((sum μs : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine AbsolutelyContinuous.mk fun s hs hs0 ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AbsolutelyContinuous (hypothesis)
Goal:
α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
i : ι
hνμ : ν ≪ μs i
s : Set α
hs : MeasurableSet s
hs0 : Eq (α := ℝ≥0∞) ((sum μs : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have hs0₁ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μs i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [sum_apply _ hs, ENNReal.tsum_eq_zero] at hs0
Cleared hypotheses: hs0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ae μ ≤ ae ν
s : Set α
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : (∀ᵐ (a : α) ∂ν, a ∉ s) → ∀ᵐ (a : α) ∂μ, a ∉ s
Tactic: rw [measure_eq_zero_iff_ae_notMem, measure_eq_zero_iff_ae_notMem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
μ ν : Measure α
hf : MeasurableEmbedding f
hμν : μ ≪ ν
t : Set β
ht : Eq (α := ENNReal) (((map f ν : Measure β) : (a : Set β) → ENNReal) t : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) (((map f μ : Measure β) : (a : Set β) → ENNReal) t : ENNReal) (0 : ENNReal)
have rw : ∀ (ht : Eq (α := ENNReal) ((ν : (a : Set α) → ENNReal) (f ⁻¹' t) : ENNReal) (0 : ENNReal)),
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (f ⁻¹' t) : ENNReal) (0 : ENNReal)
Tactic: rw [hf.map_apply] at ht ⊢
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m m' : AddContent G C
h :
  Eq (α := (a : Set α) → G) ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) m)
    ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) m')
⊢ m = m'
have mk : ∀ (toFun : Set α → G) (empty' : toFun ∅ = 0)
  (sUnion' :
    ∀ (I : Finset (Set α)) (_h_ss : (↑I : Set (Set α)) ⊆ C) (_h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
      (_h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), toFun (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, toFun u),
  Eq (α := (a : Set α) → G)
      ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) (AddContent.mk (C := C) toFun empty' sUnion'))
      ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) m') →
    AddContent.mk (C := C) toFun empty' sUnion' = m'
Tactic: cases m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m' : AddContent G C
toFun : Set α → G
empty' : toFun ∅ = 0
sUnion' :
  ∀ (I : Finset (Set α)) (_h_ss : (↑I : Set (Set α)) ⊆ C) (_h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
    (_h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), toFun (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, toFun u
h :
  Eq (α := (a : Set α) → G)
    ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) (AddContent.mk (C := C) toFun empty' sUnion'))
    ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) m')
⊢ AddContent.mk (C := C) toFun empty' sUnion' = m'
have mk : ∀ (toFun_1 : Set α → G) (empty'_1 : toFun_1 ∅ = 0)
  (sUnion'_1 :
    ∀ (I : Finset (Set α)) (_h_ss : (↑I : Set (Set α)) ⊆ C) (_h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
      (_h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), toFun_1 (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, toFun_1 u),
  Eq (α := (a : Set α) → G)
      ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) (AddContent.mk (C := C) toFun empty' sUnion'))
      ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s)
        (AddContent.mk (C := C) toFun_1 empty'_1 sUnion'_1)) →
    AddContent.mk (C := C) toFun empty' sUnion' = AddContent.mk (C := C) toFun_1 empty'_1 sUnion'_1
Tactic: cases m'
Cleared hypotheses: m', h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
Tactic: have A : ⋃ i ∈ a, f i = ⋃₀ (a.image f) := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have rw : Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))
Tactic: rw [A, addContent_sUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
rw : Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have h_ss : (↑(Finset.image f a) : Set (Set α)) ⊆ C
Tactic: rw [A, addContent_sUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
rw : Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))
h_ss : (↑(Finset.image f a) : Set (Set α)) ⊆ C
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have h_dis₁ : (↑(Finset.image f a) : Set (Set α)).PairwiseDisjoint id
Tactic: rw [A, addContent_sUnion]