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 γ
g : α →ₘ[μ] γ
f : α → α
hf : MeasurePreserving f μ μ
n : ℕ
⊢ (fun (x : α →ₘ[μ] γ) ↦ x.compMeasurePreserving f hf)^[n] g = g.compMeasurePreserving f^[n] ⋯

Tactic:
compQuasiMeasurePreserving_iterate _ _ _

Premises used: MeasureTheory.AEEqFun.compMeasurePreserving, MeasureTheory.AEEqFun.compQuasiMeasurePreserving_iterate
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : β → γ
hg : Continuous[inst_1, inst_2] g
f : α → β
hf : AEStronglyMeasurable f μ
⊢ comp g hg (mk f hf) = mk (g ∘ 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_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
mk :
  ∀ (a : { f : α → β // AEStronglyMeasurable f μ }),
    comp id ⋯
        (Quot.mk
          (⇑(Measure.aeEqSetoid β μ) :
            { f : α → β // AEStronglyMeasurable f μ } → { f : α → β // AEStronglyMeasurable f μ } → Prop)
          a) =
      Quot.mk
        (⇑(Measure.aeEqSetoid β μ) :
          { f : α → β // AEStronglyMeasurable f μ } → { f : α → β // AEStronglyMeasurable f μ } → Prop)
        a
⊢ comp id ⋯ f = f

Tactic:
rcases f
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
a : { f : α → β // AEStronglyMeasurable f μ }
⊢ comp id ⋯
      (Quot.mk
        (⇑(Measure.aeEqSetoid β μ) :
          { f : α → β // AEStronglyMeasurable f μ } → { f : α → β // AEStronglyMeasurable f μ } → Prop)
        a) =
    Quot.mk
      (⇑(Measure.aeEqSetoid β μ) :
        { f : α → β // AEStronglyMeasurable f μ } → { f : α → β // AEStronglyMeasurable f μ } → Prop)
      a

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : β → γ
hg : Continuous[inst_1, inst_2] g
f : α →ₘ[μ] β
rw : comp g hg f = comp g hg (mk (↑f : α → β) ⋯)
rw₁ rw₂ : comp g hg f = comp g hg f
⊢ comp g hg f = mk (g ∘ (↑f : α → β)) ⋯

Tactic:
rw [← comp_mk g hg f f.aestronglyMeasurable, mk_coeFn]

Premises used: MeasureTheory.AEEqFun.cast, MeasureTheory.AEEqFun.comp_mk, MeasureTheory.AEEqFun.mk_coeFn, MeasureTheory.AEEqFun.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : β → γ
hg : Continuous[inst_1, inst_2] g
f : α →ₘ[μ] β
rw : (↑(mk (g ∘ (↑f : α → β)) ⋯) : α → γ) =ᶠ[ae μ] g ∘ (↑f : α → β)
⊢ (↑(comp g hg f) : α → γ) =ᶠ[ae μ] g ∘ (↑f : α → β)

Tactic:
rw [comp_eq_mk]

Premises used: MeasureTheory.AEEqFun.comp_eq_mk
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : β → γ
hg : Continuous[inst_1, inst_2] g
f : α →ₘ[μ] β
⊢ (↑(mk (g ∘ (↑f : α → β)) ⋯) : α → γ) =ᶠ[ae μ] g ∘ (↑f : α → β)

Tactic:
apply coeFn_mk

Premises used: MeasureTheory.AEEqFun.coeFn_mk
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace δ
inst_2 : TopologicalSpace γ
β : Type u_5
inst_3 : MeasurableSpace β
ν : Measure β
g : γ → δ
hg : Continuous[inst_2, inst_1] g
f : β →ₘ[ν] γ
φ : α → β
hφ : Measure.QuasiMeasurePreserving φ μ ν
mk :
  ∀ (a : { f : β → γ // AEStronglyMeasurable f ν }),
    (comp g hg
            (Quot.mk
              (⇑(Measure.aeEqSetoid γ ν) :
                { f : β → γ // AEStronglyMeasurable f ν } → { f : β → γ // AEStronglyMeasurable f ν } → Prop)
              a)).compQuasiMeasurePreserving
        φ hφ =
      comp g hg
        (compQuasiMeasurePreserving
          (Quot.mk
            (⇑(Measure.aeEqSetoid γ ν) :
              { f : β → γ // AEStronglyMeasurable f ν } → { f : β → γ // AEStronglyMeasurable f ν } → Prop)
            a)
          φ hφ)
⊢ (comp g hg f).compQuasiMeasurePreserving φ hφ = comp g hg (f.compQuasiMeasurePreserving φ hφ)

Tactic:
rcases f
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace δ
inst_2 : TopologicalSpace γ
β : Type u_5
inst_3 : MeasurableSpace β
ν : Measure β
g : γ → δ
hg : Continuous[inst_2, inst_1] g
f : β →ₘ[ν] γ
φ : α → β
hφ : Measure.QuasiMeasurePreserving φ μ ν
a : { f : β → γ // AEStronglyMeasurable f ν }
⊢ (comp g hg
          (Quot.mk
            (⇑(Measure.aeEqSetoid γ ν) :
              { f : β → γ // AEStronglyMeasurable f ν } → { f : β → γ // AEStronglyMeasurable f ν } → Prop)
            a)).compQuasiMeasurePreserving
      φ hφ =
    comp g hg
      (compQuasiMeasurePreserving
        (Quot.mk
          (⇑(Measure.aeEqSetoid γ ν) :
            { f : β → γ // AEStronglyMeasurable f ν } → { f : β → γ // AEStronglyMeasurable f ν } → Prop)
          a)
        φ hφ)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : MeasurableSpace β
inst_4 : PseudoMetrizableSpace β
inst_5 : BorelSpace β
inst_6 : MeasurableSpace γ
inst_7 : PseudoMetrizableSpace γ
inst_8 : OpensMeasurableSpace γ
inst_9 : SecondCountableTopology γ
g : β → γ
hg : Measurable g
f : α → β
hf : AEStronglyMeasurable f μ
⊢ Eq (α := α →ₘ[μ] γ) (compMeasurable g hg (mk f hf)) (mk (g ∘ f) ⋯)

Tactic:
rfl

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.compMeasurable, rfl, MeasureTheory.AEEqFun.mk
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : MeasurableSpace β
inst_4 : PseudoMetrizableSpace β
inst_5 : BorelSpace β
inst_6 : MeasurableSpace γ
inst_7 : PseudoMetrizableSpace γ
inst_8 : OpensMeasurableSpace γ
inst_9 : SecondCountableTopology γ
g : β → γ
hg : Measurable g
f : α →ₘ[μ] β
rw : Eq (α := α →ₘ[μ] γ) (compMeasurable g hg f) (compMeasurable g hg (mk (↑f : α → β) ⋯))
rw₁ rw₂ : Eq (α := α →ₘ[μ] γ) (compMeasurable g hg f) (compMeasurable g hg f)
⊢ Eq (α := α →ₘ[μ] γ) (compMeasurable g hg f) (mk (g ∘ (↑f : α → β)) ⋯)

Tactic:
rw [← compMeasurable_mk g hg f f.aestronglyMeasurable, mk_coeFn]

Premises used: MeasureTheory.AEEqFun.compMeasurable_mk, MeasureTheory.AEEqFun.cast, MeasureTheory.AEEqFun.mk_coeFn, MeasureTheory.AEEqFun.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : MeasurableSpace β
inst_4 : PseudoMetrizableSpace β
inst_5 : BorelSpace β
inst_6 : MeasurableSpace γ
inst_7 : PseudoMetrizableSpace γ
inst_8 : OpensMeasurableSpace γ
inst_9 : SecondCountableTopology γ
g : β → γ
hg : Measurable g
f : α →ₘ[μ] β
rw : (↑(mk (g ∘ (↑f : α → β)) ⋯) : α → γ) =ᶠ[ae μ] g ∘ (↑f : α → β)
⊢ (↑(compMeasurable g hg f) : α → γ) =ᶠ[ae μ] g ∘ (↑f : α → β)

Tactic:
rw [compMeasurable_eq_mk]

Premises used: MeasureTheory.AEEqFun.compMeasurable_eq_mk
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : MeasurableSpace β
inst_4 : PseudoMetrizableSpace β
inst_5 : BorelSpace β
inst_6 : MeasurableSpace γ
inst_7 : PseudoMetrizableSpace γ
inst_8 : OpensMeasurableSpace γ
inst_9 : SecondCountableTopology γ
g : β → γ
hg : Measurable g
f : α →ₘ[μ] β
⊢ (↑(mk (g ∘ (↑f : α → β)) ⋯) : α → γ) =ᶠ[ae μ] g ∘ (↑f : α → β)

Tactic:
apply coeFn_mk

Premises used: MeasureTheory.AEEqFun.coeFn_mk
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
hf : AEStronglyMeasurable f μ
g : α → γ
hg : AEStronglyMeasurable g μ
⊢ (mk f hf).pair (mk g hg) = mk (fun (x : α) ↦ (f x, g x)) ⋯

Tactic:
rfl

Premises used: MeasureTheory.AEEqFun.pair, rfl, MeasureTheory.AEEqFun.mk, 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 γ
f : α →ₘ[μ] β
g : α →ₘ[μ] γ
⊢ f.pair g = mk (fun (x : α) ↦ ((↑f : α → β) x, (↑g : α → γ) x)) ⋯

Tactic:
simp only [← pair_mk_mk, mk_coeFn, f.aestronglyMeasurable, g.aestronglyMeasurable]

Premises used: MeasureTheory.AEEqFun.mk_coeFn, MeasureTheory.AEEqFun.aestronglyMeasurable, MeasureTheory.AEEqFun.pair_mk_mk
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α →ₘ[μ] β
g : α →ₘ[μ] γ
rw :
  (↑(mk (fun (x : α) ↦ ((↑f : α → β) x, (↑g : α → γ) x)) ⋯) : α → β × γ) =ᶠ[ae μ] fun (x : α) ↦
    ((↑f : α → β) x, (↑g : α → γ) x)
⊢ (↑(f.pair g) : α → β × γ) =ᶠ[ae μ] fun (x : α) ↦ ((↑f : α → β) x, (↑g : α → γ) x)

Tactic:
rw [pair_eq_mk]

Premises used: MeasureTheory.AEEqFun.pair_eq_mk
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α →ₘ[μ] β
g : α →ₘ[μ] γ
⊢ (↑(mk (fun (x : α) ↦ ((↑f : α → β) x, (↑g : α → γ) x)) ⋯) : α → β × γ) =ᶠ[ae μ] fun (x : α) ↦
    ((↑f : α → β) x, (↑g : α → γ) x)

Tactic:
apply coeFn_mk

Premises used: MeasureTheory.AEEqFun.coeFn_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 γ
g : β → γ → δ
hg : Continuous[instTopologicalSpaceProd, inst_1] (uncurry g)
f₁ : α → β
f₂ : α → γ
hf₁ : AEStronglyMeasurable f₁ μ
hf₂ : AEStronglyMeasurable f₂ μ
⊢ comp₂ g hg (mk f₁ hf₁) (mk f₂ hf₂) = mk (fun (a : α) ↦ g (f₁ a) (f₂ a)) ⋯

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_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace δ
inst_2 : TopologicalSpace β
inst_3 : TopologicalSpace γ
g : β → γ → δ
hg : Continuous[instTopologicalSpaceProd, inst_1] (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ comp₂ g hg f₁ f₂ = comp (uncurry g) hg (f₁.pair f₂)

Tactic:
rfl

Premises used: MeasureTheory.AEEqFun.comp₂, rfl
-- 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 γ
g : β → γ → δ
hg : Continuous[instTopologicalSpaceProd, inst_1] (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
rw :
  mk (uncurry g ∘ fun (x : α) ↦ ((↑f₁ : α → β) x, (↑f₂ : α → γ) x)) ⋯ =
    mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) ⋯
⊢ comp₂ g hg f₁ f₂ = mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) ⋯

Tactic:
rw [comp₂_eq_pair, pair_eq_mk, comp_mk]

Premises used: MeasureTheory.AEEqFun.pair_eq_mk, MeasureTheory.AEEqFun.comp_mk, MeasureTheory.AEEqFun.comp₂_eq_pair
-- 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 γ
g : β → γ → δ
hg : Continuous[instTopologicalSpaceProd, inst_1] (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ mk (uncurry g ∘ fun (x : α) ↦ ((↑f₁ : α → β) x, (↑f₂ : α → γ) x)) ⋯ =
    mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) ⋯

Tactic:
rfl
-- 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 γ
g : β → γ → δ
hg : Continuous[instTopologicalSpaceProd, inst_1] (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
rw :
  (↑(mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) ⋯) : α → δ) =ᶠ[ae μ] fun (a : α) ↦
    g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)
⊢ (↑(comp₂ g hg f₁ f₂) : α → δ) =ᶠ[ae μ] fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)

Tactic:
rw [comp₂_eq_mk]

Premises used: MeasureTheory.AEEqFun.comp₂_eq_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 γ
g : β → γ → δ
hg : Continuous[instTopologicalSpaceProd, inst_1] (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ (↑(mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) ⋯) : α → δ) =ᶠ[ae μ] fun (a : α) ↦
    g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)

Tactic:
apply coeFn_mk

Premises used: MeasureTheory.AEEqFun.coeFn_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 γ
inst_4 : MeasurableSpace β
inst_5 : PseudoMetrizableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSpace γ
inst_8 : PseudoMetrizableSpace γ
inst_9 : BorelSpace γ
inst_10 : SecondCountableTopologyEither β γ
inst_11 : MeasurableSpace δ
inst_12 : PseudoMetrizableSpace δ
inst_13 : OpensMeasurableSpace δ
inst_14 : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α → β
f₂ : α → γ
hf₁ : AEStronglyMeasurable f₁ μ
hf₂ : AEStronglyMeasurable f₂ μ
⊢ Eq (α := α →ₘ[μ] δ) (comp₂Measurable g hg (mk f₁ hf₁) (mk f₂ hf₂)) (mk (fun (a : α) ↦ g (f₁ a) (f₂ a)) ⋯)

Tactic:
rfl

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.comp₂Measurable, MeasureTheory.AEEqFun.compMeasurable, rfl, MeasureTheory.AEEqFun.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 γ
inst_4 : MeasurableSpace β
inst_5 : PseudoMetrizableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSpace γ
inst_8 : PseudoMetrizableSpace γ
inst_9 : BorelSpace γ
inst_10 : SecondCountableTopologyEither β γ
inst_11 : MeasurableSpace δ
inst_12 : PseudoMetrizableSpace δ
inst_13 : OpensMeasurableSpace δ
inst_14 : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ Eq (α := α →ₘ[μ] δ) (comp₂Measurable g hg f₁ f₂) (compMeasurable (uncurry g) hg (f₁.pair f₂))

Tactic:
rfl

Premises used: MeasureTheory.AEEqFun.comp₂Measurable, rfl
-- 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 : MeasurableSpace β
inst_5 : PseudoMetrizableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSpace γ
inst_8 : PseudoMetrizableSpace γ
inst_9 : BorelSpace γ
inst_10 : SecondCountableTopologyEither β γ
inst_11 : MeasurableSpace δ
inst_12 : PseudoMetrizableSpace δ
inst_13 : OpensMeasurableSpace δ
inst_14 : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
rw :
  Eq (α := α →ₘ[μ] δ) (mk (uncurry g ∘ fun (x : α) ↦ ((↑f₁ : α → β) x, (↑f₂ : α → γ) x)) ⋯)
    (mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) ⋯)
⊢ Eq (α := α →ₘ[μ] δ) (comp₂Measurable g hg f₁ f₂) (mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) ⋯)

Tactic:
rw [comp₂Measurable_eq_pair, pair_eq_mk, compMeasurable_mk]

Premises used: MeasureTheory.AEEqFun.pair_eq_mk, MeasureTheory.AEEqFun.compMeasurable_mk, MeasureTheory.AEEqFun.comp₂Measurable_eq_pair
-- 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 : MeasurableSpace β
inst_5 : PseudoMetrizableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSpace γ
inst_8 : PseudoMetrizableSpace γ
inst_9 : BorelSpace γ
inst_10 : SecondCountableTopologyEither β γ
inst_11 : MeasurableSpace δ
inst_12 : PseudoMetrizableSpace δ
inst_13 : OpensMeasurableSpace δ
inst_14 : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ Eq (α := α →ₘ[μ] δ) (mk (uncurry g ∘ fun (x : α) ↦ ((↑f₁ : α → β) x, (↑f₂ : α → γ) x)) ⋯)
    (mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) ⋯)

Tactic:
rfl
-- 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 : MeasurableSpace β
inst_5 : PseudoMetrizableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSpace γ
inst_8 : PseudoMetrizableSpace γ
inst_9 : BorelSpace γ
inst_10 : SecondCountableTopologyEither β γ
inst_11 : MeasurableSpace δ
inst_12 : PseudoMetrizableSpace δ
inst_13 : OpensMeasurableSpace δ
inst_14 : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
rw :
  (↑(mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) ⋯) : α → δ) =ᶠ[ae μ] fun (a : α) ↦
    g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)
⊢ (↑(comp₂Measurable g hg f₁ f₂) : α → δ) =ᶠ[ae μ] fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)

Tactic:
rw [comp₂Measurable_eq_mk]

Premises used: MeasureTheory.AEEqFun.comp₂Measurable_eq_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 γ
inst_4 : MeasurableSpace β
inst_5 : PseudoMetrizableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSpace γ
inst_8 : PseudoMetrizableSpace γ
inst_9 : BorelSpace γ
inst_10 : SecondCountableTopologyEither β γ
inst_11 : MeasurableSpace δ
inst_12 : PseudoMetrizableSpace δ
inst_13 : OpensMeasurableSpace δ
inst_14 : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ (↑(mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) ⋯) : α → δ) =ᶠ[ae μ] fun (a : α) ↦
    g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)

Tactic:
apply coeFn_mk

Premises used: MeasureTheory.AEEqFun.coeFn_mk
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ (mk f hf).toGerm = (↑f : (ae μ).Germ β)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, MeasureTheory.AEEqFun.toGerm, Quotient.mk', rfl
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
rw : f.toGerm = (mk (↑f : α → β) ⋯).toGerm
rw₁ rw₂ : f.toGerm = f.toGerm
⊢ f.toGerm = (↑(↑f : α → β) : (ae μ).Germ β)

Tactic:
rw [← mk_toGerm f f.aestronglyMeasurable, mk_coeFn]

Premises used: MeasureTheory.AEEqFun.cast, MeasureTheory.AEEqFun.mk_coeFn, MeasureTheory.AEEqFun.mk_toGerm, MeasureTheory.AEEqFun.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f g : α →ₘ[μ] β
H : f.toGerm = g.toGerm
rwa : f.toGerm = (↑(↑g : α → β) : (ae μ).Germ β)
rwa₁ rwa₂ rwa₃ rwa₄ : f.toGerm = g.toGerm
⊢ Eq (α := (ae μ).Germ β) (↑(↑f : α → β) : (ae μ).Germ β) (↑(↑g : α → β) : (ae μ).Germ β)

Tactic:
rwa [← toGerm_eq, ← toGerm_eq]

Premises used: MeasureTheory.AEEqFun.toGerm_eq
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
β : Type u_5
inst_2 : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] γ
hf : Measure.QuasiMeasurePreserving f μ ν
mk :
  ∀ (a : { f : β → γ // AEStronglyMeasurable f ν }),
    (compQuasiMeasurePreserving
          (Quot.mk
            (⇑(Measure.aeEqSetoid γ ν) :
              { f : β → γ // AEStronglyMeasurable f ν } → { f : β → γ // AEStronglyMeasurable f ν } → Prop)
            a)
          f hf).toGerm =
      (toGerm
            (Quot.mk
              (⇑(Measure.aeEqSetoid γ ν) :
                { f : β → γ // AEStronglyMeasurable f ν } → { f : β → γ // AEStronglyMeasurable f ν } → Prop)
              a)).compTendsto
        f ⋯
⊢ (g.compQuasiMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f ⋯

Tactic:
rcases g
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
β : Type u_5
inst_2 : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] γ
hf : Measure.QuasiMeasurePreserving f μ ν
a : { f : β → γ // AEStronglyMeasurable f ν }
⊢ (compQuasiMeasurePreserving
        (Quot.mk
          (⇑(Measure.aeEqSetoid γ ν) :
            { f : β → γ // AEStronglyMeasurable f ν } → { f : β → γ // AEStronglyMeasurable f ν } → Prop)
          a)
        f hf).toGerm =
    (toGerm
          (Quot.mk
            (⇑(Measure.aeEqSetoid γ ν) :
              { f : β → γ // AEStronglyMeasurable f ν } → { f : β → γ // AEStronglyMeasurable f ν } → Prop)
            a)).compTendsto
      f ⋯

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
β : Type u_5
inst_2 : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] γ
hf : MeasurePreserving f μ ν
⊢ (g.compMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f ⋯

Tactic:
compQuasiMeasurePreserving_toGerm _ _

Premises used: MeasureTheory.AEEqFun.compMeasurePreserving, MeasureTheory.AEEqFun.compQuasiMeasurePreserving_toGerm
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : β → γ
hg : Continuous[inst_1, inst_2] g
f_1 : α →ₘ[μ] β
f : α → β
h : AEStronglyMeasurable f μ
⊢ (comp g hg (mk f h)).toGerm = Germ.map g (mk f h).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 γ
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
inst_5 : PseudoMetrizableSpace β
inst_6 : PseudoMetrizableSpace γ
inst_7 : SecondCountableTopology γ
inst_8 : MeasurableSpace γ
inst_9 : OpensMeasurableSpace γ
g : β → γ
hg : Measurable g
f_1 : α →ₘ[μ] β
f : α → β
h : AEStronglyMeasurable f μ
⊢ toGerm (compMeasurable g hg (mk f h)) = Germ.map g (mk f h).toGerm

Tactic:
simp
-- 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 γ
g : β → γ → δ
hg : Continuous[instTopologicalSpaceProd, inst_1] (uncurry g)
f₁_1 : α →ₘ[μ] β
f₂_1 : α →ₘ[μ] γ
f₁ : α → β
h : AEStronglyMeasurable f₁ μ
f₂ : α → γ
h_1 : AEStronglyMeasurable f₂ μ
⊢ (comp₂ g hg (mk f₁ h) (mk f₂ h_1)).toGerm = Germ.map₂ g (mk f₁ h).toGerm (mk f₂ h_1).toGerm

Tactic:
simp