awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
𝕜 : Type u_5
inst_2 : SMul 𝕜 γ
inst_3 : ContinuousConstSMul 𝕜 γ
c : 𝕜
f : α →ₘ[μ] γ
⊢ (↑(c • f) : α → γ) =ᶠ[ae μ] c • (↑f : α → γ)

Tactic:
coeFn_comp _ _ _

Premises used: MeasureTheory.AEEqFun.coeFn_comp
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
𝕜 : Type u_5
inst_2 : SMul 𝕜 γ
inst_3 : ContinuousConstSMul 𝕜 γ
c : 𝕜
f : α →ₘ[μ] γ
⊢ (c • f).toGerm = c • f.toGerm

Tactic:
comp_toGerm _ _ _

Premises used: MeasureTheory.AEEqFun.comp_toGerm
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
μ ν : Measure α
inst_1 : TopologicalSpace δ
inst_2 : TopologicalSpace β
inst_3 : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst_4 : SMul 𝕜 γ
inst_5 : ContinuousConstSMul 𝕜 γ
inst_6 : SMul 𝕜' γ
inst_7 : ContinuousConstSMul 𝕜' γ
inst_8 : SMulCommClass 𝕜 𝕜' γ
a : 𝕜
b : 𝕜'
f_1 : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
simp_rw : mk (a • b • f) ⋯ = mk (b • a • f) ⋯
⊢ a • b • mk f hf = b • a • mk f hf

Tactic:
simp_rw [smul_mk, smul_comm]

Premises used: MeasureTheory.AEEqFun.smul_mk, SMulCommClass.smul_comm
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
μ ν : Measure α
inst_1 : TopologicalSpace δ
inst_2 : TopologicalSpace β
inst_3 : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst_4 : SMul 𝕜 γ
inst_5 : ContinuousConstSMul 𝕜 γ
inst_6 : SMul 𝕜' γ
inst_7 : ContinuousConstSMul 𝕜' γ
inst_8 : SMul 𝕜 𝕜'
inst_9 : IsScalarTower 𝕜 𝕜' γ
a : 𝕜
b : 𝕜'
f_1 : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
simp_rw : mk ((a • b) • f) ⋯ = mk (a • b • f) ⋯
⊢ (a • b) • mk f hf = a • b • mk f hf

Tactic:
simp_rw [smul_mk, smul_assoc]

Premises used: smul_assoc, MeasureTheory.AEEqFun.smul_mk
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
μ ν : Measure α
inst_1 : TopologicalSpace δ
inst_2 : TopologicalSpace β
inst_3 : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst_4 : SMul 𝕜 γ
inst_5 : ContinuousConstSMul 𝕜 γ
inst_6 : SMul 𝕜' γ
inst_7 : ContinuousConstSMul 𝕜' γ
inst_8 : SMul.{u_5, u_3} 𝕜ᵐᵒᵖ γ
inst_9 : IsCentralScalar 𝕜 γ
a : 𝕜
f_1 : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
simp_rw : mk (MulOpposite.op a • f) ⋯ = mk (a • f) ⋯
⊢ MulOpposite.op a • mk f hf = a • mk f hf

Tactic:
simp_rw [smul_mk, op_smul_eq_smul]

Premises used: MeasureTheory.AEEqFun.smul_mk, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : Mul γ
inst_3 : ContinuousMul γ
f g : α → γ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ mk f hf * mk g hg = mk (f * g) ⋯

Tactic:
rfl

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.comp₂, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : Mul γ
inst_3 : ContinuousMul γ
f g : α →ₘ[μ] γ
⊢ (↑(f * g) : α → γ) =ᶠ[ae μ] (↑f : α → γ) * (↑g : α → γ)

Tactic:
coeFn_comp₂ _ _ _ _

Premises used: MeasureTheory.AEEqFun.coeFn_comp₂
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : Mul γ
inst_3 : ContinuousMul γ
f g : α →ₘ[μ] γ
⊢ (f * g).toGerm = f.toGerm * g.toGerm

Tactic:
comp₂_toGerm _ _ _ _

Premises used: MeasureTheory.AEEqFun.comp₂_toGerm
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : Monoid γ
inst_3 : ContinuousMul γ
f : α → γ
hf : AEStronglyMeasurable f μ
n : ℕ
⊢ mk f hf ^ n = mk (f ^ n) ⋯

Tactic:
rfl

Premises used: Quotient.liftOn', rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : Monoid γ
inst_3 : ContinuousMul γ
f : α →ₘ[μ] γ
n : ℕ
⊢ (↑(f ^ n) : α → γ) =ᶠ[ae μ] (↑f : α → γ) ^ n

Tactic:
coeFn_comp _ _ _

Premises used: MeasureTheory.AEEqFun.coeFn_comp
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : Monoid γ
inst_3 : ContinuousMul γ
f : α →ₘ[μ] γ
n : ℕ
⊢ (f ^ n).toGerm = f.toGerm ^ n

Tactic:
comp_toGerm _ _ _

Premises used: MeasureTheory.AEEqFun.comp_toGerm
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : Group γ
inst_3 : IsTopologicalGroup γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ (mk f hf)⁻¹ = mk f⁻¹ ⋯

Tactic:
rfl

Premises used: Quotient.liftOn', rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : Group γ
inst_3 : IsTopologicalGroup γ
f : α →ₘ[μ] γ
⊢ (↑f⁻¹ : α → γ) =ᶠ[ae μ] (↑f : α → γ)⁻¹

Tactic:
coeFn_comp _ _ _

Premises used: MeasureTheory.AEEqFun.coeFn_comp
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : Group γ
inst_3 : IsTopologicalGroup γ
f : α →ₘ[μ] γ
⊢ f⁻¹.toGerm = f.toGerm⁻¹

Tactic:
comp_toGerm _ _ _

Premises used: MeasureTheory.AEEqFun.comp_toGerm
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : Group γ
inst_3 : IsTopologicalGroup γ
f g : α → γ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ mk (f / g) ⋯ = mk f hf / mk g hg

Tactic:
rfl

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.comp₂, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : Group γ
inst_3 : IsTopologicalGroup γ
f g : α →ₘ[μ] γ
⊢ (↑(f / g) : α → γ) =ᶠ[ae μ] (↑f : α → γ) / (↑g : α → γ)

Tactic:
coeFn_comp₂ _ _ _ _

Premises used: MeasureTheory.AEEqFun.coeFn_comp₂
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : Group γ
inst_3 : IsTopologicalGroup γ
f g : α →ₘ[μ] γ
⊢ (f / g).toGerm = f.toGerm / g.toGerm

Tactic:
comp₂_toGerm _ _ _ _

Premises used: MeasureTheory.AEEqFun.comp₂_toGerm
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : Group γ
inst_3 : IsTopologicalGroup γ
f : α → γ
hf : AEStronglyMeasurable f μ
n : ℤ
⊢ mk f hf ^ n = mk (f ^ n) ⋯

Tactic:
rfl

Premises used: Quotient.liftOn', rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : Group γ
inst_3 : IsTopologicalGroup γ
f : α →ₘ[μ] γ
n : ℤ
⊢ (↑(f ^ n) : α → γ) =ᶠ[ae μ] (↑f : α → γ) ^ n

Tactic:
coeFn_comp _ _ _

Premises used: MeasureTheory.AEEqFun.coeFn_comp
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : Group γ
inst_3 : IsTopologicalGroup γ
f : α →ₘ[μ] γ
n : ℤ
⊢ (f ^ n).toGerm = f.toGerm ^ n

Tactic:
comp_toGerm _ _ _

Premises used: MeasureTheory.AEEqFun.comp_toGerm
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEStronglyMeasurable f μ
⊢ (mk f hf).lintegral = ∫⁻ (a : α), f a ∂μ

Tactic:
rfl

Premises used: Quotient.liftOn', rfl, MeasureTheory.AEEqFun.lintegral
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α →ₘ[μ] ℝ≥0∞
rw : (mk (↑f : α → ℝ≥0∞) ⋯).lintegral = f.lintegral
rw₁ rw₂ : f.lintegral = f.lintegral
⊢ ∫⁻ (a : α), (↑f : α → ℝ≥0∞) a ∂μ = f.lintegral

Tactic:
rw [← lintegral_mk (hf := f.aestronglyMeasurable), mk_coeFn]

Premises used: MeasureTheory.AEEqFun.lintegral_mk, MeasureTheory.AEEqFun.mk_coeFn, MeasureTheory.AEEqFun.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
⊢ lintegral.{u_1} (α := α) (μ := μ) 0 = 0

Tactic:
lintegral_zero

Premises used: Quotient.liftOn', MeasureTheory.lintegral_zero, MeasureTheory.AEEqFun.lintegral
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α →ₘ[μ] ℝ≥0∞
⊢ f.lintegral = 0 ↔ f = 0

Tactic:
induction_on f fun _f hf => (lintegral_eq_zero_iff' hf.aemeasurable).trans mk_eq_mk.symm

Premises used: MeasureTheory.AEEqFun.induction_on
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f_1 g_1 : α →ₘ[μ] ℝ≥0∞
f : α → ℝ≥0∞
hf : AEStronglyMeasurable f μ
g : α → ℝ≥0∞
h : AEStronglyMeasurable g μ
⊢ (mk f hf + mk g h).lintegral = (mk f hf).lintegral + (mk g h).lintegral

Tactic:
simp [lintegral_add_left' hf.aemeasurable]

Premises used: MeasureTheory.lintegral_add_left', MeasureTheory.AEStronglyMeasurable.aemeasurable
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α →ₘ[μ] ℝ≥0∞
⊢ f ≤ g → f.lintegral ≤ g.lintegral

Tactic:
induction_on₂ f g fun _f _ _g _ hfg => lintegral_mono_ae hfg

Premises used: MeasureTheory.AEEqFun.induction_on₂
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
β : Type u_5
inst_1 : TopologicalSpace β
inst_2 : Lattice β
inst_3 : TopologicalLattice β
inst_4 : AddGroup β
inst_5 : IsTopologicalAddGroup β
f : α →ₘ[μ] β
simp_rw : (↑(f ⊔ -f) : α → β) =ᶠ[ae μ] fun (x : α) ↦ (↑f : α → β) x ⊔ -(↑f : α → β) x
⊢ (↑|f| : α → β) =ᶠ[ae μ] fun (x : α) ↦ |(↑f : α → β) x|

Tactic:
simp_rw [abs]

Premises used: abs
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
β : Type u_5
inst_1 : TopologicalSpace β
inst_2 : Lattice β
inst_3 : TopologicalLattice β
inst_4 : AddGroup β
inst_5 : IsTopologicalAddGroup β
f : α →ₘ[μ] β
h :
  ∀ (x : α) (hx_sup : (↑(f ⊔ -f) : α → β) x = (↑f : α → β) x ⊔ (↑(-f) : α → β) x)
    (hx_neg : (↑(-f) : α → β) x = (-(↑f : α → β)) x), (↑(f ⊔ -f) : α → β) x = (↑f : α → β) x ⊔ -(↑f : α → β) x
⊢ (↑(f ⊔ -f) : α → β) =ᶠ[ae μ] fun (x : α) ↦ (↑f : α → β) x ⊔ -(↑f : α → β) x

Tactic:
filter_upwards [AEEqFun.coeFn_sup f (-f), AEEqFun.coeFn_neg f] with x hx_sup hx_neg

Premises used: MeasureTheory.AEEqFun.coeFn_neg, MeasureTheory.AEEqFun.coeFn_sup, Neg.neg
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
β : Type u_5
inst_1 : TopologicalSpace β
inst_2 : Lattice β
inst_3 : TopologicalLattice β
inst_4 : AddGroup β
inst_5 : IsTopologicalAddGroup β
f : α →ₘ[μ] β
x : α
hx_sup : (↑(f ⊔ -f) : α → β) x = (↑f : α → β) x ⊔ (↑(-f) : α → β) x
hx_neg : (↑(-f) : α → β) x = (-(↑f : α → β)) x
h : (↑f : α → β) x ⊔ (↑(-f) : α → β) x = (↑f : α → β) x ⊔ -(↑f : α → β) x
h₁ : (↑f : α → β) x ⊔ (-(↑f : α → β)) x = (↑f : α → β) x ⊔ -(↑f : α → β) x
h₂ h₃ : (↑f : α → β) x ⊔ -(↑f : α → β) x = (↑f : α → β) x ⊔ -(↑f : α → β) x
⊢ (↑(f ⊔ -f) : α → β) x = (↑f : α → β) x ⊔ -(↑f : α → β) x

Tactic:
rw [hx_sup, hx_neg, Pi.neg_apply]

Premises used: Pi.neg_apply
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
R : Type u_5
inst_1 : TopologicalSpace R
inst_2 : Star R
inst_3 : ContinuousStar R
f : α →ₘ[μ] R
⊢ (↑(star f) : α → R) =ᶠ[ae μ] star (↑f : α → R)

Tactic:
coeFn_comp _ (continuous_star) f

Premises used: ContinuousStar.continuous_star, MeasureTheory.AEEqFun.coeFn_comp
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
μ ν : Measure α
inst_1 : TopologicalSpace δ
inst_2 : TopologicalSpace β
inst_3 : TopologicalSpace γ
R : Type u_5
inst_4 : TopologicalSpace R
inst_5 : InvolutiveStar R
inst_6 : ContinuousStar R
f : α →ₘ[μ] R
⊢ comp (star ∘ star) ⋯ f = f

Tactic:
simp [star_involutive.comp_self]

Premises used: InvolutiveStar.star_involutive, Function.Involutive.comp_self
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
μ ν : Measure α
inst_1 : TopologicalSpace δ
inst_2 : TopologicalSpace β
inst_3 : TopologicalSpace γ
R : Type u_5
inst_4 : TopologicalSpace R
inst_5 : Star R
inst_6 : TrivialStar R
inst_7 : ContinuousStar R
f : α →ₘ[μ] R
⊢ comp star ⋯ f = f

Tactic:
simp [funext star_trivial, ← Function.id_def]

Premises used: Function.id_def, TrivialStar.star_trivial, funext
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
μ ν : Measure α
inst_1 : TopologicalSpace δ
inst_2 : TopologicalSpace β
inst_3 : TopologicalSpace γ
inst_4 : LinearOrder γ
inst_5 : OrderClosedTopology γ
inst_6 : Zero γ
f : α →ₘ[μ] γ
⊢ Continuous[inst_3, inst_3] fun (x : γ) ↦ max x 0

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
μ ν : Measure α
inst_1 : TopologicalSpace δ
inst_2 : TopologicalSpace β
inst_3 : TopologicalSpace γ
inst_4 : LinearOrder γ
inst_5 : OrderClosedTopology γ
inst_6 : Zero γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ max (f x) 0) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : LinearOrder γ
inst_3 : OrderClosedTopology γ
inst_4 : Zero γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ (mk f hf).posPart = mk (fun (x : α) ↦ max (f x) 0) ⋯

Tactic:
rfl

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.posPart, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : LinearOrder γ
inst_3 : OrderClosedTopology γ
inst_4 : Zero γ
f : α →ₘ[μ] γ
⊢ (↑f.posPart : α → γ) =ᶠ[ae μ] fun (a : α) ↦ max ((↑f : α → γ) a) 0

Tactic:
coeFn_comp _ _ _

Premises used: MeasureTheory.AEEqFun.coeFn_comp, MeasureTheory.AEEqFun.posPart
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
ι : Type u_5
inst_2 : T2Space β
g h : α → β
f : ι → α → β
l : Filter ι
inst_3 : l.NeBot
hg : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (g ω))
hh : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (h ω))
ω : α
hg1 : Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (g ω))
hh1 : Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (h ω))
⊢ g ω = h ω

Tactic:
tendsto_nhds_unique hg1 hh1

Premises used: tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
ι : Type u_5
inst_2 : T2Space β
g h : α → β
f : ι → α → β
l : Filter ι
inst_3 : l.NeBot
hg : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (g ω))
hh : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (h ω))
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (ω : α) ↦ Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (g ω))) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (ω : α) ↦ Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (h ω))) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x = h x) x} x}
            x}
      a
h₂ h₃ :
  ∀ (ω : α) (hg1 : Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (g ω))) (hh1 : Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (h ω))),
    g ω = h ω
⊢ g =ᶠ[ae μ] h

Tactic:
filter_upwards [hg, hh] with ω hg1 hh1 using tendsto_nhds_unique hg1 hh1
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : TopologicalSpace β
inst_4 : SecondCountableTopologyEither α β
inst_5 : PseudoMetrizableSpace β
f : C(α, β)
⊢ (↑(toAEEqFun μ f) : α → β) =ᶠ[ae μ] (⇑f : (a : α) → β)

Tactic:
AEEqFun.coeFn_mk f _

Premises used: ContinuousMap.toAEEqFun, MeasureTheory.AEEqFun.coeFn_mk, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ ⟪c, f x⟫_𝕜) 0
s : ℕ → E := denseSeq E
⊢ DenseRange s

Tactic:
have hs : DenseRange s := denseRange_denseSeq E
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ ⟪c, f x⟫_𝕜) 0
s : ℕ → E := denseSeq E
hs : DenseRange s
⊢ ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0

Tactic:
have hf' : ∀ᵐ x ∂μ, ∀ n : ℕ, ⟪s n, f x⟫_𝕜 = 0 := ae_all_iff.mpr fun n => hf (s n)
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ ⟪c, f x⟫_𝕜) 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
⊢ f =ᶠ[ae μ] 0

Tactic:
hf'.mono fun x hx => ?_

Premises used: Filter.EventuallyEq, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ ⟪c, f x⟫_𝕜) 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
refine : ∀ (x : α) (hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0), f x = 0 x
⊢ f =ᶠ[ae μ] 0

Tactic:
refine hf'.mono fun x hx => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ ⟪c, f x⟫_𝕜) 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
x : α
hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
rw : ⟪f x, f x⟫_𝕜 = 0
⊢ f x = 0 x

Tactic:
rw [Pi.zero_apply, ← @inner_self_eq_zero 𝕜]

Premises used: Pi.zero_apply, inner_self_eq_zero
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ ⟪c, f x⟫_𝕜) 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
x : α
hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (c : E) ↦ ⟪c, f x⟫_𝕜

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ ⟪c, f x⟫_𝕜) 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
x : α
hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (c : E) ↦ 0

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ ⟪c, f x⟫_𝕜) 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
x : α
hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {c : E | ⟪c, f x⟫_𝕜 = 0}

Tactic:
have h_closed : IsClosed {c : E | ⟪c, f x⟫_𝕜 = 0} :=
    isClosed_eq (by fun_prop) (by fun_prop)
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ ⟪c, f x⟫_𝕜) 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
x : α
hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
h_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {c : E | ⟪c, f x⟫_𝕜 = 0}
⊢ ⟪f x, f x⟫_𝕜 = 0

Tactic:
@isClosed_property ℕ E _ s (fun c => ⟪c, f x⟫_𝕜 = 0) hs h_closed hx _

Premises used: isClosed_property
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ ⟪c, f x⟫_𝕜) 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
x : α
hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
h_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {c : E | ⟪c, f x⟫_𝕜 = 0}
⊢ ⟪f x, f x⟫_𝕜 = 0

Tactic:
exact @isClosed_property ℕ E _ s (fun c => ⟪c, f x⟫_𝕜 = 0) hs h_closed hx _

Premises used: isClosed_property
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
t : Set E
ht : IsSeparable t
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ (c : (a : E) → 𝕜) (f x)) 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
rcases :
  ∀ (d : Set E) (d_count : d.Countable) (hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d),
    f =ᶠ[ae μ] 0
⊢ f =ᶠ[ae μ] 0

Tactic:
rcases ht with ⟨d, d_count, hd⟩
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ (c : (a : E) → 𝕜) (f x)) 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
haveI : ∀ (this : Encodable (↑d : Type u_2)), f =ᶠ[ae μ] 0
⊢ f =ᶠ[ae μ] 0

Tactic:
haveI : Encodable d := d_count.toEncodable