awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : PseudoMetrizableSpace β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
inst_7 : PseudoMetrizableSpace γ
inst_8 : SecondCountableTopologyEither β γ
inst_9 : MeasurableSpace γ
inst_10 : BorelSpace γ
inst_11 : PseudoMetrizableSpace δ
inst_12 : SecondCountableTopology δ
inst_13 : MeasurableSpace δ
inst_14 : OpensMeasurableSpace δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁_1 : α →ₘ[μ] β
f₂_1 : α →ₘ[μ] γ
f₁ : α → β
h : AEStronglyMeasurable f₁ μ
f₂ : α → γ
h_1 : AEStronglyMeasurable f₂ μ
⊢ toGerm (comp₂Measurable g hg (mk f₁ h) (mk f₂ h_1)) = Germ.map₂ g (mk f₁ h).toGerm (mk f₂ h_1).toGerm

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
r : β → γ → Prop
f : α → β
g : α → γ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ LiftRel r (mk f hf) (mk g hg) ↔ ∀ᵐ (a : α) ∂μ, r (f a) (g a)

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, MeasureTheory.AEEqFun.LiftRel, Filter.Germ.LiftRel, Quotient.liftOn₂'
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
r : β → γ → Prop
f : α →ₘ[μ] β
g : α →ₘ[μ] γ
rw : LiftRel r f g ↔ LiftRel r (mk (↑f : α → β) ⋯) (mk (↑g : α → γ) ⋯)
rw₁ : LiftRel r f g ↔ LiftRel r f (mk (↑g : α → γ) ⋯)
rw₂ rw₃ : LiftRel r f g ↔ LiftRel r f g
⊢ LiftRel r f g ↔ ∀ᵐ (a : α) ∂μ, r ((↑f : α → β) a) ((↑g : α → γ) a)

Tactic:
rw [← liftRel_mk_mk (hf := f.aestronglyMeasurable) (hg := g.aestronglyMeasurable),
    mk_coeFn, mk_coeFn]

Premises used: MeasureTheory.AEEqFun.liftRel_mk_mk, MeasureTheory.AEEqFun.mk_coeFn
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : Preorder β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ mk f hf ≤ mk g hg ↔ f ≤ᶠ[ae μ] g

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Filter.Germ.LiftRel, Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : Preorder β
f g : α →ₘ[μ] β
⊢ (↑f : α → β) ≤ᶠ[ae μ] (↑g : α → β) ↔ f ≤ g

Tactic:
liftRel_iff_coeFn.symm

Premises used: MeasureTheory.AEEqFun.LiftRel, MeasureTheory.AEEqFun.liftRel_iff_coeFn, Filter.EventuallyLE, Iff.symm
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
⊢ (↑(f ⊔ g) : α → β) =ᶠ[ae μ] fun (x : α) ↦ (↑f : α → β) x ⊔ (↑g : α → β) x

Tactic:
coeFn_comp₂ _ _ _ _

Premises used: MeasureTheory.AEEqFun.coeFn_comp₂
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
rw : (↑f : α → β) ≤ᶠ[ae μ] (↑(f ⊔ g) : α → β)
⊢ f ≤ f ⊔ g

Tactic:
rw [← coeFn_le]

Premises used: MeasureTheory.AEEqFun.coeFn_le
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
h : ∀ (a : α) (ha : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a), (↑f : α → β) a ≤ (↑(f ⊔ g) : α → β) a
⊢ (↑f : α → β) ≤ᶠ[ae μ] (↑(f ⊔ g) : α → β)

Tactic:
filter_upwards [coeFn_sup f g] with _ ha

Premises used: MeasureTheory.AEEqFun.coeFn_sup
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
a : α
ha : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a
h : (↑f : α → β) a ≤ (↑f : α → β) a ⊔ (↑g : α → β) a
⊢ (↑f : α → β) a ≤ (↑(f ⊔ g) : α → β) a

Tactic:
rw [ha]
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
a : α
ha : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a
⊢ (↑f : α → β) a ≤ (↑f : α → β) a ⊔ (↑g : α → β) a

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
a : α
ha : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a
⊢ (↑f : α → β) a ≤ (↑f : α → β) a ⊔ (↑g : α → β) a

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
rw : (↑g : α → β) ≤ᶠ[ae μ] (↑(f ⊔ g) : α → β)
⊢ g ≤ f ⊔ g

Tactic:
rw [← coeFn_le]

Premises used: MeasureTheory.AEEqFun.coeFn_le
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
h : ∀ (a : α) (ha : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a), (↑g : α → β) a ≤ (↑(f ⊔ g) : α → β) a
⊢ (↑g : α → β) ≤ᶠ[ae μ] (↑(f ⊔ g) : α → β)

Tactic:
filter_upwards [coeFn_sup f g] with _ ha

Premises used: MeasureTheory.AEEqFun.coeFn_sup
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
a : α
ha : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a
h : (↑g : α → β) a ≤ (↑f : α → β) a ⊔ (↑g : α → β) a
⊢ (↑g : α → β) a ≤ (↑(f ⊔ g) : α → β) a

Tactic:
rw [ha]
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
a : α
ha : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a
⊢ (↑g : α → β) a ≤ (↑f : α → β) a ⊔ (↑g : α → β) a

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
a : α
ha : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a
⊢ (↑g : α → β) a ≤ (↑f : α → β) a ⊔ (↑g : α → β) a

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : f ≤ f'
hg : g ≤ f'
rw :
  ∀ (hf : (↑f : α → β) ≤ᶠ[ae μ] (↑f' : α → β)) (hg : (↑g : α → β) ≤ᶠ[ae μ] (↑f' : α → β)),
    (↑(f ⊔ g) : α → β) ≤ᶠ[ae μ] (↑f' : α → β)
⊢ f ⊔ g ≤ f'

Tactic:
rw [← coeFn_le] at hf hg ⊢

Premises used: MeasureTheory.AEEqFun.coeFn_le
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : (↑f : α → β) ≤ᶠ[ae μ] (↑f' : α → β)
hg : (↑g : α → β) ≤ᶠ[ae μ] (↑f' : α → β)
h :
  ∀ (a : α) (haf : (↑f : α → β) a ≤ (↑f' : α → β) a) (hag : (↑g : α → β) a ≤ (↑f' : α → β) a)
    (ha_sup : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a), (↑(f ⊔ g) : α → β) a ≤ (↑f' : α → β) a
⊢ (↑(f ⊔ g) : α → β) ≤ᶠ[ae μ] (↑f' : α → β)

Tactic:
filter_upwards [hf, hg, coeFn_sup f g] with _ haf hag ha_sup

Premises used: MeasureTheory.AEEqFun.coeFn_sup
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : (↑f : α → β) ≤ᶠ[ae μ] (↑f' : α → β)
hg : (↑g : α → β) ≤ᶠ[ae μ] (↑f' : α → β)
a : α
haf : (↑f : α → β) a ≤ (↑f' : α → β) a
hag : (↑g : α → β) a ≤ (↑f' : α → β) a
ha_sup : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a
h : (↑f : α → β) a ⊔ (↑g : α → β) a ≤ (↑f' : α → β) a
⊢ (↑(f ⊔ g) : α → β) a ≤ (↑f' : α → β) a

Tactic:
rw [ha_sup]
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : (↑f : α → β) ≤ᶠ[ae μ] (↑f' : α → β)
hg : (↑g : α → β) ≤ᶠ[ae μ] (↑f' : α → β)
a : α
haf : (↑f : α → β) a ≤ (↑f' : α → β) a
hag : (↑g : α → β) a ≤ (↑f' : α → β) a
ha_sup : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a
⊢ (↑f : α → β) a ⊔ (↑g : α → β) a ≤ (↑f' : α → β) a

Tactic:
sup_le haf hag

Premises used: sup_le
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : (↑f : α → β) ≤ᶠ[ae μ] (↑f' : α → β)
hg : (↑g : α → β) ≤ᶠ[ae μ] (↑f' : α → β)
a : α
haf : (↑f : α → β) a ≤ (↑f' : α → β) a
hag : (↑g : α → β) a ≤ (↑f' : α → β) a
ha_sup : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a
⊢ (↑f : α → β) a ⊔ (↑g : α → β) a ≤ (↑f' : α → β) a

Tactic:
exact sup_le haf hag

Premises used: sup_le
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
⊢ (↑(f ⊓ g) : α → β) =ᶠ[ae μ] fun (x : α) ↦ (↑f : α → β) x ⊓ (↑g : α → β) x

Tactic:
coeFn_comp₂ _ _ _ _

Premises used: MeasureTheory.AEEqFun.coeFn_comp₂
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
rw : (↑(f ⊓ g) : α → β) ≤ᶠ[ae μ] (↑f : α → β)
⊢ f ⊓ g ≤ f

Tactic:
rw [← coeFn_le]

Premises used: MeasureTheory.AEEqFun.coeFn_le
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
h : ∀ (a : α) (ha : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a), (↑(f ⊓ g) : α → β) a ≤ (↑f : α → β) a
⊢ (↑(f ⊓ g) : α → β) ≤ᶠ[ae μ] (↑f : α → β)

Tactic:
filter_upwards [coeFn_inf f g] with _ ha

Premises used: MeasureTheory.AEEqFun.coeFn_inf
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
a : α
ha : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a
h : (↑f : α → β) a ⊓ (↑g : α → β) a ≤ (↑f : α → β) a
⊢ (↑(f ⊓ g) : α → β) a ≤ (↑f : α → β) a

Tactic:
rw [ha]
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
a : α
ha : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a
⊢ (↑f : α → β) a ⊓ (↑g : α → β) a ≤ (↑f : α → β) a

Tactic:
inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
a : α
ha : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a
⊢ (↑f : α → β) a ⊓ (↑g : α → β) a ≤ (↑f : α → β) a

Tactic:
exact inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
rw : (↑(f ⊓ g) : α → β) ≤ᶠ[ae μ] (↑g : α → β)
⊢ f ⊓ g ≤ g

Tactic:
rw [← coeFn_le]

Premises used: MeasureTheory.AEEqFun.coeFn_le
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
h : ∀ (a : α) (ha : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a), (↑(f ⊓ g) : α → β) a ≤ (↑g : α → β) a
⊢ (↑(f ⊓ g) : α → β) ≤ᶠ[ae μ] (↑g : α → β)

Tactic:
filter_upwards [coeFn_inf f g] with _ ha

Premises used: MeasureTheory.AEEqFun.coeFn_inf
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
a : α
ha : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a
h : (↑f : α → β) a ⊓ (↑g : α → β) a ≤ (↑g : α → β) a
⊢ (↑(f ⊓ g) : α → β) a ≤ (↑g : α → β) a

Tactic:
rw [ha]
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
a : α
ha : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a
⊢ (↑f : α → β) a ⊓ (↑g : α → β) a ≤ (↑g : α → β) a

Tactic:
inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
a : α
ha : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a
⊢ (↑f : α → β) a ⊓ (↑g : α → β) a ≤ (↑g : α → β) a

Tactic:
exact inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : f' ≤ f
hg : f' ≤ g
rw :
  ∀ (hf : (↑f' : α → β) ≤ᶠ[ae μ] (↑f : α → β)) (hg : (↑f' : α → β) ≤ᶠ[ae μ] (↑g : α → β)),
    (↑f' : α → β) ≤ᶠ[ae μ] (↑(f ⊓ g) : α → β)
⊢ f' ≤ f ⊓ g

Tactic:
rw [← coeFn_le] at hf hg ⊢

Premises used: MeasureTheory.AEEqFun.coeFn_le
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : (↑f' : α → β) ≤ᶠ[ae μ] (↑f : α → β)
hg : (↑f' : α → β) ≤ᶠ[ae μ] (↑g : α → β)
h :
  ∀ (a : α) (haf : (↑f' : α → β) a ≤ (↑f : α → β) a) (hag : (↑f' : α → β) a ≤ (↑g : α → β) a)
    (ha_inf : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a), (↑f' : α → β) a ≤ (↑(f ⊓ g) : α → β) a
⊢ (↑f' : α → β) ≤ᶠ[ae μ] (↑(f ⊓ g) : α → β)

Tactic:
filter_upwards [hf, hg, coeFn_inf f g] with _ haf hag ha_inf

Premises used: MeasureTheory.AEEqFun.coeFn_inf
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : (↑f' : α → β) ≤ᶠ[ae μ] (↑f : α → β)
hg : (↑f' : α → β) ≤ᶠ[ae μ] (↑g : α → β)
a : α
haf : (↑f' : α → β) a ≤ (↑f : α → β) a
hag : (↑f' : α → β) a ≤ (↑g : α → β) a
ha_inf : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a
h : (↑f' : α → β) a ≤ (↑f : α → β) a ⊓ (↑g : α → β) a
⊢ (↑f' : α → β) a ≤ (↑(f ⊓ g) : α → β) a

Tactic:
rw [ha_inf]
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : (↑f' : α → β) ≤ᶠ[ae μ] (↑f : α → β)
hg : (↑f' : α → β) ≤ᶠ[ae μ] (↑g : α → β)
a : α
haf : (↑f' : α → β) a ≤ (↑f : α → β) a
hag : (↑f' : α → β) a ≤ (↑g : α → β) a
ha_inf : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a
⊢ (↑f' : α → β) a ≤ (↑f : α → β) a ⊓ (↑g : α → β) a

Tactic:
le_inf haf hag

Premises used: le_inf
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : (↑f' : α → β) ≤ᶠ[ae μ] (↑f : α → β)
hg : (↑f' : α → β) ≤ᶠ[ae μ] (↑g : α → β)
a : α
haf : (↑f' : α → β) a ≤ (↑f : α → β) a
hag : (↑f' : α → β) a ≤ (↑g : α → β) a
ha_inf : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a
⊢ (↑f' : α → β) a ≤ (↑f : α → β) a ⊓ (↑g : α → β) a

Tactic:
exact le_inf haf hag

Premises used: le_inf
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
b : β
⊢ (↑(const α b) : α → β) =ᶠ[ae μ] Function.const α b

Tactic:
coeFn_mk _ _

Premises used: MeasureTheory.AEEqFun.coeFn_mk, MeasureTheory.AEEqFun.const
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
simp :
  (if h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯) then
        Function.const α
          (Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h)
      else AEStronglyMeasurable.mk (m := inst) (μ := μ) (↑(Quotient.out (const α b)) : α → β) ⋯)
      x =
    b
⊢ (↑(const α b) : α → β) x = b

Tactic:
simp only [cast]

Premises used: MeasureTheory.AEEqFun.cast
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
pos :
  ∀ (h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯)),
    Function.const α
        (Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h) x =
      b
split_ifs :
  ∀ (h : ¬∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯)),
    AEStronglyMeasurable.mk (↑(Quotient.out (const α b)) : α → β) ⋯ x = b
⊢ (if h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯) then
        Function.const α
          (Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h)
      else AEStronglyMeasurable.mk (m := inst) (μ := μ) (↑(Quotient.out (const α b)) : α → β) ⋯)
      x =
    b

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
h : ¬∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯)
⊢ AEStronglyMeasurable.mk (↑(Quotient.out (const α b)) : α → β) ⋯ x = b

Tactic:
h.elim ⟨b, rfl⟩

Premises used: Not.elim, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
h : ¬∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯)
⊢ AEStronglyMeasurable.mk (↑(Quotient.out (const α b)) : α → β) ⋯ x = b

Tactic:
exact h.elim ⟨b, rfl⟩

Premises used: Not.elim, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
h : ¬∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯)
⊢ AEStronglyMeasurable.mk (↑(Quotient.out (const α b)) : α → β) ⋯ x = b

Tactic:
case neg => exact h.elim ⟨b, rfl⟩

Premises used: Not.elim, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯)
⊢ Eq (α := α →ₘ[μ] β) (const α b)
    (mk
      (Function.const α
        (Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h))
      ⋯)

Tactic:
have := Classical.choose_spec h
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯)
this :
  Eq (α := α →ₘ[μ] β) (const α b)
    (mk
      (Function.const α
        (Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h))
      ⋯)
pos :
  let b' := Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h;
  ∀ (this : Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b') ⋯)), Function.const α b' x = b
⊢ Function.const α (Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h)
      x =
    b

Tactic:
set b' := Classical.choose h

Premises used: Classical.choose
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯)
b' : β := Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h
this : Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b') ⋯)
⊢ b = b'

Tactic:
simp_rw [const, mk_eq_mk, EventuallyEq, ← const_def, eventually_const] at this

Premises used: Filter.EventuallyEq, Function.const_def, Filter.eventually_const, MeasureTheory.AEEqFun.mk_eq_mk, MeasureTheory.AEEqFun.const
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯)
b' : β := Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h
this : b = b'
pos : b' = b
pos₁ pos₂ : b' = b'
⊢ Function.const α b' x = b

Tactic:
rw [Function.const, this]

Premises used: Function.const
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : One β
⊢ Eq (α := α →ₘ[μ] β) 1 (mk (fun (x : α) ↦ 1) ⋯)

Tactic:
rfl

Premises used: rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.const
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : One β
⊢ EventuallyEq.{u_1, u_2} (β := β) (ae μ) (↑1 : α → β) 1

Tactic:
coeFn_const ..

Premises used: MeasureTheory.AEEqFun.coeFn_const
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
inst_3 : One β
x : α
⊢ Eq.{u_2 + 1} (α := β) ((↑1 : α → β) x) 1

Tactic:
coeFn_const_eq ..

Premises used: MeasureTheory.AEEqFun.coeFn_const_eq
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : One β
⊢ Eq (α := (ae μ).Germ β) (toGerm 1) 1

Tactic:
rfl

Premises used: Filter.Germ.ofFun, MeasureTheory.AEEqFun.toGerm, Quotient.liftOn', Filter.Germ.const, Quotient.mk', rfl
-- 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 : α → γ
hf : AEStronglyMeasurable f μ
⊢ c • mk f hf = mk (c • f) ⋯

Tactic:
rfl

Premises used: Quotient.liftOn', rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp