awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : 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
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set β
hs : s ∈ S
⊢ f ⁻¹' s ∩ vᶜ = T s \ v

Tactic:
Set.ext fun x ↦ and_congr_left fun hxv ↦ ⟨fun hx ↦ ?_, fun hx ↦ hTf s hs hx⟩

Premises used: Set.ext, and_congr_left, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : 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
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set β
hs : s ∈ S
h₁ : ∀ (x : α) (hxv : x ∈ vᶜ) (hx : x ∈ f ⁻¹' s), x ∈ T s
⊢ f ⁻¹' s ∩ vᶜ = T s \ v

Tactic:
refine Set.ext fun x ↦ and_congr_left fun hxv ↦ ⟨fun hx ↦ ?_, fun hx ↦ hTf s hs hx⟩

Premises used: Set.ext, and_congr_left, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : 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
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set β
hs : s ∈ S
x : α
hxv : x ∈ vᶜ
hx : x ∈ f ⁻¹' s
⊢ x ∈ T s

Tactic:
by_contra fun hx' ↦ hxv <| mem_biUnion hs ⟨hUf s hs hx, hx'⟩

Premises used: Set.mem_biUnion, And.intro, by_contra
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : 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
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set β
hs : s ∈ S
x : α
hxv : x ∈ vᶜ
hx : x ∈ f ⁻¹' s
⊢ x ∈ T s

Tactic:
exact by_contra fun hx' ↦ hxv <| mem_biUnion hs ⟨hUf s hs hx, hx'⟩

Premises used: Set.mem_biUnion, And.intro, by_contra
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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 μ
inr : ∀ (hne : t.Nonempty), AEMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
rcases eq_empty_or_nonempty t with rfl | hne

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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)
⊢ μ = 0

Tactic:
simpa using hft
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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)
inl : ∀ (h : NullMeasurable f 0) (hft : ∀ᵐ (x : α) ∂0, Membership.mem (γ := Set β) ∅ (f x)), AEMeasurable (_m := m0) f 0
⊢ AEMeasurable f μ

Tactic:
obtain rfl : μ = 0 := by simpa using hft

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : MeasurableSpace.CountablyGenerated.{u_3} (↑∅ : Type u_3)
h : NullMeasurable f 0
hft : ∀ᵐ (x : α) ∂0, Membership.mem (γ := Set β) ∅ (f x)
⊢ AEMeasurable (_m := m0) f 0

Tactic:
apply aemeasurable_zero_measure

Premises used: aemeasurable_zero_measure
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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
⊢ ∀ᵐ (x : α) ∂μ.completion, f x ∈ t

Tactic:
rw [← μ.ae_completion] at hft

Premises used: MeasureTheory.Measure.ae_completion
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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
hft₁ : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
⊢ t.Nonempty

Tactic:
rw [← μ.ae_completion] at hft

Premises used: MeasureTheory.Measure.ae_completion
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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' : α → β), NullMeasurable f' μ ∧ range f' ⊆ t ∧ f =ᶠ[ae μ] f'

Tactic:
h.measurable'.aemeasurable.exists_ae_eq_range_subset hft hne

Premises used: MeasureTheory.ae, AEMeasurable.exists_ae_eq_range_subset, MeasureTheory.NullMeasurable.measurable', Measurable.aemeasurable, Measurable, MeasureTheory.NullMeasurableSet, MeasureTheory.Measure.completion, MeasureTheory.NullMeasurableSpace, MeasureTheory.NullMeasurable
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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
inr : ∀ (f' : α → β) (hf'm : NullMeasurable f' μ) (hf't : range f' ⊆ t) (hff' : f =ᶠ[ae μ] f'), AEMeasurable 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

Premises used: AEMeasurable.exists_ae_eq_range_subset, MeasureTheory.NullMeasurable.measurable', Measurable.aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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'
⊢ ∀ (y : α), f' y ∈ t

Tactic:
rw [range_subset_iff] at hf't

Premises used: Set.range_subset_iff
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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'
hf't₁ : ∀ (y : α), f' y ∈ t
⊢ f =ᶠ[ae μ] f'

Tactic:
rw [range_subset_iff] at hf't

Premises used: Set.range_subset_iff
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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'
⊢ ∀ (i : α), f' i ∈ t

Tactic:
hf't
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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'
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 μ
⊢ AEMeasurable f μ

Tactic:
lift f' to α → t using hf't
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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) : β)
⊢ NullMeasurable f' μ

Tactic:
replace hf'm : NullMeasurable f' μ := hf'm.measurable'.subtype_mk
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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)
hff' : f =ᶠ[ae μ] fun (i : α) ↦ (↑(f' i) : β)
hf'm : NullMeasurable f' μ
⊢ AEMeasurable f μ

Tactic:
(measurable_subtype_coe.comp_aemeasurable hf'm.aemeasurable).congr hff'.symm

Premises used: AEMeasurable.congr, measurable_subtype_coe, MeasureTheory.NullMeasurable.aemeasurable, Measurable.comp_aemeasurable, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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)
hff' : f =ᶠ[ae μ] fun (i : α) ↦ (↑(f' i) : β)
hf'm : NullMeasurable f' μ
⊢ AEMeasurable f μ

Tactic:
exact (measurable_subtype_coe.comp_aemeasurable hf'm.aemeasurable).congr hff'.symm

Premises used: AEMeasurable.congr, measurable_subtype_coe, MeasureTheory.NullMeasurable.aemeasurable, Measurable.comp_aemeasurable, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
ι : Type u_7
m : ι → Measure α
f : α → β
hf : AEMeasurable f (sum m)
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∞)
⊢ Eq (α := Measure β) (map f (sum m)) (sum fun (i : ι) ↦ map f (m i))

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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
h :
  Eq (α := ℝ≥0∞) (∑' (i : ι), (m i : (a : Set α) → ℝ≥0∞) (f ⁻¹' s))
    (∑' (i : ι), ((map f (m i) : Measure β) : (a : Set β) → ℝ≥0∞) 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:
rw [map_apply_of_aemeasurable hf hs, sum_apply₀ _ (hf.nullMeasurable hs), sum_apply _ hs]

Premises used: AEMeasurable.nullMeasurable, MeasureTheory.Measure.sum_apply, MeasureTheory.Measure.sum_apply₀, MeasureTheory.Measure.map_apply_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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
⊢ ∀ (i : ι), AEMeasurable f (m i)

Tactic:
have M i : AEMeasurable f (m i) := hf.mono_measure (le_sum m i)
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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
M : ∀ (i : ι), AEMeasurable f (m i)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ι), (m i : (a : Set α) → ℝ≥0∞) (f ⁻¹' s))
    (∑' (i : ι), ((map f (m i) : Measure β) : (a : Set β) → ℝ≥0∞) s)

Tactic:
simp_rw [map_apply_of_aemeasurable (M _) hs]

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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)
rw : AEMeasurable (_m := m0) f (sum fun (i : ↥s) ↦ m (↑i : ι))
⊢ Eq (α := Measure β) (map f (∑ i ∈ s, m i)) (∑ i ∈ s, map f (m i))

Tactic:
rw [← sum_coe_finset, ← sum_coe_finset, Measure.map_sum]

Premises used: MeasureTheory.Measure.map_sum, MeasureTheory.Measure.sum_coe_finset
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
ι : Type u_7
β : Type u_8
mβ : MeasurableSpace β
m : ι → Measure α
f : α → β
s : Finset ι
hf rwa rwa₁ rwa₂ rwa₃ : AEMeasurable (_m := m0) f (∑ i ∈ s, m i)
⊢ AEMeasurable (_m := m0) f (sum fun (i : ↥s) ↦ m (↑i : ι))

Tactic:
rwa [sum_coe_finset]

Premises used: MeasureTheory.Measure.sum_coe_finset
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
ι : Type u_7
β : Type u_8
inst : Fintype ι
mβ : MeasurableSpace β
m : ι → Measure α
f : α → β
hf : AEMeasurable (_m := m0) f (∑ i : ι, m i)
⊢ Eq (α := Measure β) (map f (∑ i : ι, m i)) (∑ i : ι, map f (m i))

Tactic:
map_finset_sum hf

Premises used: MeasureTheory.Measure.map_finset_sum
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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 μ)
neg : ∀ (H : ¬AEMeasurable f μ), SFinite (m0 := inst) (map f μ)
⊢ SFinite (m0 := inst) (map f μ)

Tactic:
by_cases H : AEMeasurable f μ

Premises used: AEMeasurable
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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 μ
pos : ∀ (H : AEMeasurable f (sum (sfiniteSeq μ))), SFinite (m0 := inst) (map f (sum (sfiniteSeq μ)))
⊢ SFinite (m0 := inst) (map f μ)

Tactic:
rw [← sum_sfiniteSeq μ] at H ⊢

Premises used: MeasureTheory.sum_sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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 μ))
pos : SFinite.{u_3} (α := β) (m0 := inst) (sum fun (i : ℕ) ↦ map f (sfiniteSeq μ i))
⊢ SFinite (m0 := inst) (map f (sum (sfiniteSeq μ)))

Tactic:
rw [map_sum H]

Premises used: MeasureTheory.Measure.map_sum
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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.{u_3} (α := β) (m0 := inst) (sum fun (i : ℕ) ↦ map f (sfiniteSeq μ i))

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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 μ
neg : SFinite.{u_3} (α := β) (m0 := inst) 0
⊢ SFinite (m0 := inst) (map f μ)

Tactic:
rw [map_of_not_aemeasurable H]

Premises used: MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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.{u_3} (α := β) (m0 := inst) 0

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : μ ≤ ν
⊢ μ ≪ ν

Tactic:
fun s hs =>
  nonpos_iff_eq_zero.1 <| hs ▸ le_iff'.1 h s

Premises used: MeasureTheory.Measure.AbsolutelyContinuous, Iff.mp, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : μ = ν
⊢ μ ≪ ν

Tactic:
h.le.absolutelyContinuous

Premises used: Eq.le, LE.le.absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
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∞)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rcases exists_measurable_superset_of_null hs with ⟨t, h1t, h2t, h3t⟩

Premises used: MeasureTheory.exists_measurable_superset_of_null
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
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∞)
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:
measure_mono_null h1t (h h2t h3t)

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
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∞)
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:
exact measure_mono_null h1t (h h2t h3t)

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
_m0 : MeasurableSpace α
μ : Measure α
⊢ μ ≪ μ

Tactic:
rfl.absolutelyContinuous

Premises used: Eq.absolutelyContinuous, rfl
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ μ ≪ μ

Tactic:
fun _s hs => hs

Premises used: MeasureTheory.Measure.AbsolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
R : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ μ₁ μ₂ μ₃ ν ν' : Measure α
s t : Set α
x : MeasurableSpace α
⊢ Std.Refl fun (x1 x2 : Measure α) ↦ x1 ≪ x2

Tactic:
⟨fun _ => AbsolutelyContinuous.rfl⟩

Premises used: Std.Refl.mk, MeasureTheory.Measure.AbsolutelyContinuous.rfl
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
x : Set α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ μ₃ : Measure α
h1 : μ₁ ≪ μ₂
h2 : μ₂ ≪ μ₃
⊢ μ₁ ≪ μ₃

Tactic:
fun _s hs => h1 <| h2 hs

Premises used: MeasureTheory.Measure.AbsolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
h : μ ≪ ν
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((map f ν : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa [hf, hs] using @h _
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
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∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [h hνs, smul_apply, smul_zero, ← smul_one_smul ℝ≥0∞ c (0 : ℝ≥0∞)]

Premises used: smul_zero, smul_one_smul, ENNReal, MeasureTheory.Measure.smul_apply, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
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∞)
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∞)
⊢ Eq (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [smul_apply, ← smul_one_smul ℝ≥0∞, smul_eq_mul, mul_eq_zero] at hνs ⊢

Premises used: mul_eq_zero, smul_one_smul, ENNReal, MeasureTheory.Measure.smul_apply, smul_eq_mul