awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : Countable ι
inst_1 : TopologicalSpace β
f : α → β
inst_2 : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
A : ∀ (i : ι), ∃ (t : Set β), IsSeparable t ∧ f ⁻¹' t ∈ ae (μ i)
choose :
  ∀ (t : (i : ι) → Set β) (t_sep : ∀ (i : ι), IsSeparable (t i)) (ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)),
    ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t

Tactic:
choose t t_sep ht using A
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : Countable ι
inst_1 : TopologicalSpace β
f : α → β
inst_2 : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t : (i : ι) → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t

Tactic:
⟨⋃ i, t i, .iUnion t_sep, ?_⟩

Premises used: TopologicalSpace.IsSeparable.iUnion, And.intro, Exists.intro, Set.iUnion
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : Countable ι
inst_1 : TopologicalSpace β
f : α → β
inst_2 : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t : (i : ι) → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
refine : ∀ᵐ (x : α) ∂sum μ, Membership.mem (γ := Set β) (⋃ (i : ι), t i) (f x)
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t

Tactic:
refine ⟨⋃ i, t i, .iUnion t_sep, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : Countable ι
inst_1 : TopologicalSpace β
f : α → β
inst_2 : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t : (i : ι) → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
simp : ∀ (b : ι), ∀ᵐ (x : α) ∂μ b, ∃ (i : ι), f x ∈ t i
⊢ ∀ᵐ (x : α) ∂sum μ, Membership.mem (γ := Set β) (⋃ (i : ι), t i) (f x)

Tactic:
simp only [Measure.ae_sum_eq, mem_iUnion, eventually_iSup]

Premises used: MeasureTheory.Measure.ae_sum_eq, Set.mem_iUnion, Filter.eventually_iSup
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : Countable ι
inst_1 : TopologicalSpace β
f : α → β
inst_2 : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t : (i : ι) → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
i : ι
h₁ : ∀ (x : α) (hx : x ∈ f ⁻¹' t i), ∃ (i : ι), f x ∈ t i
⊢ ∀ᵐ (x : α) ∂μ i, ∃ (i : ι), f x ∈ t i

Tactic:
filter_upwards [ht i] with x hx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : Countable ι
inst_1 : TopologicalSpace β
f : α → β
inst_2 : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t : (i : ι) → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
i : ι
x : α
hx : x ∈ f ⁻¹' t i
⊢ ∃ (i : ι), f x ∈ t i

Tactic:
⟨i, hx⟩

Premises used: Exists.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : Countable ι
inst_1 : TopologicalSpace β
f : α → β
inst_2 : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
t : (i : ι) → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
i : ι
x : α
hx : x ∈ f ⁻¹' t i
⊢ ∃ (i : ι), f x ∈ t i

Tactic:
exact ⟨i, hx⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : Countable ι
inst_1 : TopologicalSpace β
f : α → β
inst_2 : PseudoMetrizableSpace β
_m : MeasurableSpace α
μ : ι → Measure α
⊢ AEStronglyMeasurable f (sum μ) ↔ ∀ (i : ι), AEStronglyMeasurable f (μ i)

Tactic:
⟨fun h _ => h.mono_measure (Measure.le_sum _ _), sum_measure⟩

Premises used: MeasureTheory.AEStronglyMeasurable.sum_measure, MeasureTheory.AEStronglyMeasurable.mono_measure, MeasureTheory.Measure.le_sum, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : PseudoMetrizableSpace β
ν : Measure α
rw :
  AEStronglyMeasurable f (bif true then μ else ν) ∧ AEStronglyMeasurable f (bif false then μ else ν) ↔
    AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν
⊢ AEStronglyMeasurable f (μ + ν) ↔ AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν

Tactic:
rw [← sum_cond, aestronglyMeasurable_sum_measure_iff, Bool.forall_bool, and_comm]

Premises used: aestronglyMeasurable_sum_measure_iff, Bool.forall_bool, MeasureTheory.Measure.sum_cond, and_comm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : PseudoMetrizableSpace β
ν : Measure α
⊢ AEStronglyMeasurable f (bif true then μ else ν) ∧ AEStronglyMeasurable f (bif false then μ else ν) ↔
    AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : PseudoMetrizableSpace β
ν : Measure α
f : α → β
hμ : AEStronglyMeasurable f μ
hν : AEStronglyMeasurable f ν
⊢ AEStronglyMeasurable f (μ + ν)

Tactic:
aestronglyMeasurable_add_measure_iff.2 ⟨hμ, hν⟩

Premises used: Iff.mpr, aestronglyMeasurable_add_measure_iff, And.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : Countable ι
inst_1 : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_2 : PseudoMetrizableSpace β
s : ι → Set α
h : ∀ (i : ι), AEStronglyMeasurable f (μ.restrict (s i))
⊢ AEStronglyMeasurable f (μ.restrict (⋃ (i : ι), s i))

Tactic:
(sum_measure h).mono_measure <| restrict_iUnion_le

Premises used: MeasureTheory.AEStronglyMeasurable.sum_measure, MeasureTheory.AEStronglyMeasurable.mono_measure, MeasureTheory.Measure.restrict_iUnion_le
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : Countable ι
inst_1 : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_2 : PseudoMetrizableSpace β
s : ι → Set α
⊢ AEStronglyMeasurable f (μ.restrict (⋃ (i : ι), s i)) ↔ ∀ (i : ι), AEStronglyMeasurable f (μ.restrict (s i))

Tactic:
⟨fun h _ => h.mono_measure <| restrict_mono (subset_iUnion _ _) le_rfl,
    AEStronglyMeasurable.iUnion⟩

Premises used: le_rfl, MeasureTheory.Measure.restrict_mono, Set.subset_iUnion, MeasureTheory.AEStronglyMeasurable.mono_measure, Iff.intro, MeasureTheory.AEStronglyMeasurable.iUnion
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : PseudoMetrizableSpace β
s t : Set α
⊢ AEStronglyMeasurable f (μ.restrict (s ∪ t)) ↔
    AEStronglyMeasurable f (μ.restrict s) ∧ AEStronglyMeasurable f (μ.restrict t)

Tactic:
simp only [union_eq_iUnion, aestronglyMeasurable_iUnion_iff, Bool.forall_bool, cond, and_comm]

Premises used: cond, Bool.forall_bool, and_comm, aestronglyMeasurable_iUnion_iff, Set.union_eq_iUnion
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : LinearOrder α
inst_2 : PseudoMetrizableSpace β
f : α → β
a b : α
rw :
  AEStronglyMeasurable f (μ.restrict (Ioc a b ∪ Ioc b a)) ↔
    AEStronglyMeasurable f (μ.restrict (Ioc a b)) ∧ AEStronglyMeasurable f (μ.restrict (Ioc b a))
rw₁ rw₂ :
  AEStronglyMeasurable f (μ.restrict (Ioc a b)) ∧ AEStronglyMeasurable f (μ.restrict (Ioc b a)) ↔
    AEStronglyMeasurable f (μ.restrict (Ioc a b)) ∧ AEStronglyMeasurable f (μ.restrict (Ioc b a))
⊢ AEStronglyMeasurable f (μ.restrict (uIoc a b)) ↔
    AEStronglyMeasurable f (μ.restrict (Ioc a b)) ∧ AEStronglyMeasurable f (μ.restrict (Ioc b a))

Tactic:
rw [uIoc_eq_union, aestronglyMeasurable_union_iff]

Premises used: aestronglyMeasurable_union_iff, Set.uIoc_eq_union
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
R : Type u_5
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : AEStronglyMeasurable f μ
c : R
⊢ AEStronglyMeasurable f (c • μ)

Tactic:
⟨h.mk f, h.stronglyMeasurable_mk, ae_smul_measure h.ae_eq_mk c⟩

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, MeasureTheory.Measure.ae_smul_measure, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
G : Type u_6
inst_1 : Group G
inst_2 : MulAction G β
inst_3 : ContinuousConstSMul G β
c : G
h : AEStronglyMeasurable.{u_1, u_2} (β := β) (fun (x : α) ↦ c • f x) μ
⊢ AEStronglyMeasurable f μ

Tactic:
simpa only [inv_smul_smul] using h.const_smul' c⁻¹

Premises used: inv_smul_smul, Inv.inv, MeasureTheory.AEStronglyMeasurable.const_smul'
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
M : Type u_5
inst_1 : Monoid M
inst_2 : MulAction M β
inst_3 : ContinuousConstSMul M β
c : M
hc : IsUnit c
⊢ AEStronglyMeasurable.{u_1, u_2} (β := β) (fun (x : α) ↦ c • f x) μ ↔ AEStronglyMeasurable f μ

Tactic:
let ⟨u, hu⟩ := hc
  hu ▸ aestronglyMeasurable_const_smul_iff u

Premises used: aestronglyMeasurable_const_smul_iff, Eq.rec, _private.0.IsUnit.aestronglyMeasurable_const_smul_iff.match_1, Iff, HSMul.hSMul, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
G₀ : Type u_7
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ β
inst_3 : ContinuousConstSMul G₀ β
c : G₀
hc : c ≠ 0
⊢ AEStronglyMeasurable.{u_1, u_2} (β := β) (fun (x : α) ↦ c • f x) μ ↔ AEStronglyMeasurable f μ

Tactic:
(IsUnit.mk0 _ hc).aestronglyMeasurable_const_smul_iff

Premises used: IsUnit.aestronglyMeasurable_const_smul_iff, IsUnit.mk0
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
hf : AEFinStronglyMeasurable f μ
⊢ FinStronglyMeasurable (AEFinStronglyMeasurable.mk f hf) μ

Tactic:
hf.choose_spec.1

Premises used: Exists.choose_spec, And.left, MeasureTheory.AEFinStronglyMeasurable.mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
hf : AEFinStronglyMeasurable f μ
⊢ f =ᶠ[ae μ] AEFinStronglyMeasurable.mk f hf

Tactic:
hf.choose_spec.2

Premises used: Exists.choose_spec, And.right, MeasureTheory.AEFinStronglyMeasurable.mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : Zero β
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
inst_4 : BorelSpace β
f : α → β
hf : AEFinStronglyMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
⟨hf.mk f, hf.finStronglyMeasurable_mk.measurable, hf.ae_eq_mk⟩

Premises used: AEMeasurable, MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk, MeasureTheory.FinStronglyMeasurable.measurable, And.intro, Exists.intro, MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk, MeasureTheory.AEFinStronglyMeasurable.mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f g : α → β
inst_1 : MulZeroClass β
inst_2 : ContinuousMul β
hf : AEFinStronglyMeasurable f μ
hg : AEFinStronglyMeasurable g μ
⊢ AEFinStronglyMeasurable (f * g) μ

Tactic:
⟨hf.mk f * hg.mk g, hf.finStronglyMeasurable_mk.mul hg.finStronglyMeasurable_mk,
    hf.ae_eq_mk.mul hg.ae_eq_mk⟩

Premises used: HMul.hMul, Filter.EventuallyEq.mul, MeasureTheory.FinStronglyMeasurable.mul, MeasureTheory.AEFinStronglyMeasurable, MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk, And.intro, Exists.intro, MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk, MeasureTheory.AEFinStronglyMeasurable.mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f g : α → β
inst_1 : AddZeroClass β
inst_2 : ContinuousAdd β
hf : AEFinStronglyMeasurable f μ
hg : AEFinStronglyMeasurable g μ
⊢ AEFinStronglyMeasurable (f + g) μ

Tactic:
⟨hf.mk f + hg.mk g, hf.finStronglyMeasurable_mk.add hg.finStronglyMeasurable_mk,
    hf.ae_eq_mk.add hg.ae_eq_mk⟩

Premises used: MeasureTheory.AEFinStronglyMeasurable, MeasureTheory.FinStronglyMeasurable.add, HAdd.hAdd, MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk, And.intro, Exists.intro, MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk, Filter.EventuallyEq.add, MeasureTheory.AEFinStronglyMeasurable.mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : SubtractionMonoid β
inst_2 : ContinuousNeg β
hf : AEFinStronglyMeasurable f μ
⊢ AEFinStronglyMeasurable (-f) μ

Tactic:
⟨-hf.mk f, hf.finStronglyMeasurable_mk.neg, hf.ae_eq_mk.neg⟩

Premises used: MeasureTheory.AEFinStronglyMeasurable, MeasureTheory.FinStronglyMeasurable.neg, MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk, Filter.EventuallyEq.neg, And.intro, Exists.intro, MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk, MeasureTheory.AEFinStronglyMeasurable.mk, Neg.neg
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f g : α → β
inst_1 : SubtractionMonoid β
inst_2 : ContinuousSub β
hf : AEFinStronglyMeasurable f μ
hg : AEFinStronglyMeasurable g μ
⊢ AEFinStronglyMeasurable (f - g) μ

Tactic:
⟨hf.mk f - hg.mk g, hf.finStronglyMeasurable_mk.sub hg.finStronglyMeasurable_mk,
    hf.ae_eq_mk.sub hg.ae_eq_mk⟩

Premises used: HSub.hSub, MeasureTheory.AEFinStronglyMeasurable, MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk, And.intro, Exists.intro, MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk, MeasureTheory.FinStronglyMeasurable.sub, MeasureTheory.AEFinStronglyMeasurable.mk, Filter.EventuallyEq.sub
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Zero β
inst_3 : SMulZeroClass 𝕜 β
inst_4 : ContinuousSMul 𝕜 β
hf : AEFinStronglyMeasurable f μ
c : 𝕜
⊢ AEFinStronglyMeasurable (c • f) μ

Tactic:
⟨c • hf.mk f, hf.finStronglyMeasurable_mk.const_smul c, hf.ae_eq_mk.const_smul c⟩

Premises used: MeasureTheory.FinStronglyMeasurable.const_smul, MeasureTheory.AEFinStronglyMeasurable, MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk, And.intro, Exists.intro, MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk, HSMul.hSMul, MeasureTheory.AEFinStronglyMeasurable.mk, Filter.EventuallyEq.const_smul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f g : α → β
inst_1 : Zero β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
hf : AEFinStronglyMeasurable f μ
hg : AEFinStronglyMeasurable g μ
⊢ AEFinStronglyMeasurable (f ⊔ g) μ

Tactic:
⟨hf.mk f ⊔ hg.mk g, hf.finStronglyMeasurable_mk.sup hg.finStronglyMeasurable_mk,
    hf.ae_eq_mk.sup hg.ae_eq_mk⟩

Premises used: Filter.EventuallyEq.sup, MeasureTheory.AEFinStronglyMeasurable, Max.max, MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk, And.intro, MeasureTheory.FinStronglyMeasurable.sup, Exists.intro, MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk, MeasureTheory.AEFinStronglyMeasurable.mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f g : α → β
inst_1 : Zero β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
hf : AEFinStronglyMeasurable f μ
hg : AEFinStronglyMeasurable g μ
⊢ AEFinStronglyMeasurable (f ⊓ g) μ

Tactic:
⟨hf.mk f ⊓ hg.mk g, hf.finStronglyMeasurable_mk.inf hg.finStronglyMeasurable_mk,
    hf.ae_eq_mk.inf hg.ae_eq_mk⟩

Premises used: MeasureTheory.FinStronglyMeasurable.inf, MeasureTheory.AEFinStronglyMeasurable, MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk, And.intro, Exists.intro, MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk, MeasureTheory.AEFinStronglyMeasurable.mk, Min.min, Filter.EventuallyEq.inf
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
hf : AEFinStronglyMeasurable f μ
rcases :
  ∀ (g : α → β) (hg : FinStronglyMeasurable g μ) (hfg : f =ᶠ[ae μ] g),
    ∃ (t : Set α), MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)
⊢ ∃ (t : Set α), MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)

Tactic:
rcases hf with ⟨g, hg, hfg⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
obtain :
  ∀ (t : Set α) (ht : MeasurableSet t) (hgt_zero : ∀ x ∈ tᶜ, g x = 0) (htμ : SigmaFinite (μ.restrict t)),
    ∃ (t : Set α), MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)
⊢ ∃ (t : Set α), MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)

Tactic:
obtain ⟨t, ht, hgt_zero, htμ⟩ := hg.exists_set_sigmaFinite

Premises used: MeasureTheory.FinStronglyMeasurable.exists_set_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ ∃ (t : Set α), MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)

Tactic:
⟨t, ht, ?_, htμ⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
refine : f =ᶠ[ae (μ.restrict tᶜ)] 0
⊢ ∃ (t : Set α), MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)

Tactic:
refine ⟨t, ht, ?_, htμ⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ f =ᶠ[ae (μ.restrict tᶜ)] 0

Tactic:
EventuallyEq.trans (ae_restrict_of_ae hfg) ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
refine : g =ᶠ[ae (μ.restrict tᶜ)] 0
⊢ f =ᶠ[ae (μ.restrict tᶜ)] 0

Tactic:
refine EventuallyEq.trans (ae_restrict_of_ae hfg) ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
rw : ∀ᵐ (x : α) ∂μ, x ∈ tᶜ → g x = 0 x
⊢ g =ᶠ[ae (μ.restrict tᶜ)] 0

Tactic:
rw [EventuallyEq, ae_restrict_iff' ht.compl]

Premises used: Filter.EventuallyEq, MeasurableSet.compl, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ tᶜ → g x = 0 x

Tactic:
Eventually.of_forall hgt_zero

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ tᶜ → g x = 0 x

Tactic:
exact Eventually.of_forall hgt_zero

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
hf : AEFinStronglyMeasurable f μ
⊢ MeasurableSet hf.sigmaFiniteSet

Tactic:
hf.exists_set_sigmaFinite.choose_spec.1

Premises used: Exists.choose_spec, MeasureTheory.AEFinStronglyMeasurable.sigmaFiniteSet, And.left, MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite