awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AEEqFun.DomAct
Goal:
M : Type u_1
N : Type ?u.9110
α : Type u_2
β : Type u_3
inst : MeasurableSpace N
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : TopologicalSpace β
inst_3 : SMul M α
inst_4 : MeasurableConstSMul M α
inst_5 : SMulInvariantMeasure M α μ
inst_6 : AddMonoid β
inst_7 : ContinuousAdd β
a : Mᵈᵐᵃ
x : α →ₘ[μ] β
a_1 : { f : α → β // AEStronglyMeasurable f μ }
y : α →ₘ[μ] β
a_2 : { f : α → β // AEStronglyMeasurable f μ }
⊢ a •
      HAdd.hAdd (α := α →ₘ[μ] β)
        (Quot.mk
          (⇑(Measure.aeEqSetoid β μ) :
            { f : α → β // AEStronglyMeasurable f μ } → { f : α → β // AEStronglyMeasurable f μ } → Prop)
          a_1)
        (Quot.mk
          (⇑(Measure.aeEqSetoid β μ) :
            { f : α → β // AEStronglyMeasurable f μ } → { f : α → β // AEStronglyMeasurable f μ } → Prop)
          a_2) =
    HSMul.hSMul (β := α →ₘ[μ] β) a
        (Quot.mk
          (⇑(Measure.aeEqSetoid β μ) :
            { f : α → β // AEStronglyMeasurable f μ } → { f : α → β // AEStronglyMeasurable f μ } → Prop)
          a_1) +
      HSMul.hSMul (β := α →ₘ[μ] β) a
        (Quot.mk
          (⇑(Measure.aeEqSetoid β μ) :
            { f : α → β // AEStronglyMeasurable f μ } → { f : α → β // AEStronglyMeasurable f μ } → Prop)
          a_2)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.AEEqFun.DomAct
Goal:
M : Type u_1
N : Type ?u.26214
α : Type u_2
β : Type u_3
inst : MeasurableSpace N
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : TopologicalSpace β
inst_3 : Monoid M
inst_4 : MulAction M α
inst_5 : MeasurableConstSMul M α
inst_6 : SMulInvariantMeasure M α μ
inst_7 : Monoid β
inst_8 : ContinuousMul β
r : Mᵈᵐᵃ
x : α →ₘ[μ] β
a : { f : α → β // AEStronglyMeasurable f μ }
y : α →ₘ[μ] β
a_1 : { f : α → β // AEStronglyMeasurable f μ }
⊢ r •
      HMul.hMul (α := α →ₘ[μ] β)
        (Quot.mk
          (⇑(Measure.aeEqSetoid β μ) :
            { f : α → β // AEStronglyMeasurable f μ } → { f : α → β // AEStronglyMeasurable f μ } → Prop)
          a)
        (Quot.mk
          (⇑(Measure.aeEqSetoid β μ) :
            { f : α → β // AEStronglyMeasurable f μ } → { f : α → β // AEStronglyMeasurable f μ } → Prop)
          a_1) =
    HSMul.hSMul (β := α →ₘ[μ] β) r
        (Quot.mk
          (⇑(Measure.aeEqSetoid β μ) :
            { f : α → β // AEStronglyMeasurable f μ } → { f : α → β // AEStronglyMeasurable f μ } → Prop)
          a) *
      HSMul.hSMul (β := α →ₘ[μ] β) r
        (Quot.mk
          (⇑(Measure.aeEqSetoid β μ) :
            { f : α → β // AEStronglyMeasurable f μ } → { f : α → β // AEStronglyMeasurable f μ } → Prop)
          a_1)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
pos :
  ∀ (h : ∃ (b : β), f = mk (const α b) ⋯),
    StronglyMeasurable (const α (Classical.choose (p := fun (x : β) ↦ f = mk (const α x) ⋯) h))
neg :
  ∀ (h : ¬∃ (b : β), f = mk (const α b) ⋯), StronglyMeasurable (AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) ⋯)
⊢ StronglyMeasurable.{u_1, u_2} (α := α) (β := β)
    (if h : ∃ (b : β), f = mk (const α b) ⋯ then const α (Classical.choose (p := fun (x : β) ↦ f = mk (const α x) ⋯) h)
    else AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) ⋯)

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
h : ∃ (b : β), f = mk (const α b) ⋯
⊢ StronglyMeasurable (const α (Classical.choose (p := fun (x : β) ↦ f = mk (const α x) ⋯) h))

Tactic:
stronglyMeasurable_const

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

Tactic:
exact stronglyMeasurable_const

Premises used: MeasureTheory.stronglyMeasurable_const
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ (b : β), f = mk (const α b) ⋯
⊢ StronglyMeasurable (AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) ⋯)

Tactic:
apply AEStronglyMeasurable.stronglyMeasurable_mk

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
⊢ AEStronglyMeasurable (↑f : α → β) μ

Tactic:
f.stronglyMeasurable.aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.AEEqFun.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
f : α →ₘ[μ] β
⊢ Measurable (↑f : α → β)

Tactic:
f.stronglyMeasurable.measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.AEEqFun.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
f : α →ₘ[μ] β
⊢ AEMeasurable (↑f : α → β) μ

Tactic:
f.measurable.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.AEEqFun.measurable
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ Quot.mk
      (⇑(Measure.aeEqSetoid β μ) :
        { f : α → β // AEStronglyMeasurable f μ } → { f : α → β // AEStronglyMeasurable f μ } → Prop)
      (Subtype.mk (p := fun (f : α → β) ↦ AEStronglyMeasurable f μ) f hf) =
    mk f hf

Tactic:
rfl

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

Tactic:
Quotient.eq''

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

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
h : ∃ (b : β), f = mk (const α b) ⋯
⊢ mk (const α (Classical.choose (p := fun (x : β) ↦ f = mk (const α x) ⋯) h)) ⋯ = f

Tactic:
Classical.choose_spec h |>.symm

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

Tactic:
exact Classical.choose_spec h |>.symm

Premises used: Classical.choose_spec, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ (b : β), f = mk (const α b) ⋯
rw : Quotient.mk'' (Quotient.out f)
| f

Tactic:
rw [← Quotient.out_eq' f]

Premises used: Quotient.out_eq'
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ (b : β), f = mk (const α b) ⋯
neg : mk (AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) ⋯) ⋯ = Quotient.mk'' (Quotient.out f)
⊢ mk (AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) ⋯) ⋯ = f

Tactic:
conv_rhs => rw [← Quotient.out_eq' f]

Premises used: Quotient.out_eq'
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ (b : β), f = mk (const α b) ⋯
neg : AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) ⋯ =ᶠ[ae μ] (↑(Quotient.out f) : α → β)
⊢ mk (AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) ⋯) ⋯ = Quotient.mk'' (Quotient.out f)

Tactic:
rw [← mk, mk_eq_mk]

Premises used: MeasureTheory.AEEqFun.mk_eq_mk, MeasureTheory.AEEqFun.mk
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ (b : β), f = mk (const α b) ⋯
⊢ AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) ⋯ =ᶠ[ae μ] (↑(Quotient.out f) : α → β)

Tactic:
(AEStronglyMeasurable.ae_eq_mk _).symm

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ (b : β), f = mk (const α b) ⋯
⊢ AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) ⋯ =ᶠ[ae μ] (↑(Quotient.out f) : α → β)

Tactic:
exact (AEStronglyMeasurable.ae_eq_mk _).symm

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f g : α →ₘ[μ] β
h : (↑f : α → β) =ᶠ[ae μ] (↑g : α → β)
rwa : mk (↑f : α → β) ⋯ = g
rwa₁ : mk (↑f : α → β) ⋯ = mk (↑g : α → β) ⋯
rwa₂ rwa₃ rwa₄ rwa₅ : (↑f : α → β) =ᶠ[ae μ] (↑g : α → β)
⊢ f = g

Tactic:
rwa [← f.mk_coeFn, ← g.mk_coeFn, mk_eq_mk]

Premises used: MeasureTheory.AEEqFun.mk_coeFn, MeasureTheory.AEEqFun.mk_eq_mk
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α → β
hf : AEStronglyMeasurable f μ
rw : mk (↑(mk f hf) : α → β) ⋯ = mk f hf
rw₁ rw₂ : mk f hf = mk f hf
⊢ (↑(mk f hf) : α → β) =ᶠ[ae μ] f

Tactic:
rw [← mk_eq_mk (hf := AEEqFun.aestronglyMeasurable ..) (hg := hf), mk_coeFn]

Premises used: MeasureTheory.AEEqFun.mk_coeFn, MeasureTheory.AEEqFun.mk_eq_mk
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
p : (α →ₘ[μ] β) → Prop
H : ∀ (f : α → β) (hf : AEStronglyMeasurable f μ), p (mk f hf)
⊢ p f

Tactic:
Quotient.inductionOn' f <| Subtype.forall.2 H

Premises used: Quotient.inductionOn'
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
α' : Type u_5
β' : Type u_6
inst_2 : MeasurableSpace α'
inst_3 : TopologicalSpace β'
μ' : Measure α'
f : α →ₘ[μ] β
f' : α' →ₘ[μ'] β'
p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → Prop
H :
  ∀ (f : α → β) (hf : AEStronglyMeasurable f μ) (f' : α' → β') (hf' : AEStronglyMeasurable f' μ'),
    p (mk f hf) (mk f' hf')
⊢ p f f'

Tactic:
induction_on f fun f hf => induction_on f' <| H f hf

Premises used: MeasureTheory.AEEqFun.induction_on
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
α' : Type u_5
β' : Type u_6
inst_2 : MeasurableSpace α'
inst_3 : TopologicalSpace β'
μ' : Measure α'
α'' : Type u_7
β'' : Type u_8
inst_4 : MeasurableSpace α''
inst_5 : TopologicalSpace β''
μ'' : Measure α''
f : α →ₘ[μ] β
f' : α' →ₘ[μ'] β'
f'' : α'' →ₘ[μ''] β''
p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → (α'' →ₘ[μ''] β'') → Prop
H :
  ∀ (f : α → β) (hf : AEStronglyMeasurable f μ) (f' : α' → β') (hf' : AEStronglyMeasurable f' μ') (f'' : α'' → β'')
    (hf'' : AEStronglyMeasurable f'' μ''), p (mk f hf) (mk f' hf') (mk f'' hf'')
⊢ p f f' f''

Tactic:
induction_on f fun f hf => induction_on₂ f' f'' <| H f hf

Premises used: MeasureTheory.AEEqFun.induction_on
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : MeasurableSpace β
ν : Measure β
f : α → β
g : β → γ
hg : AEStronglyMeasurable g ν
hf : QuasiMeasurePreserving f μ ν
⊢ (mk g hg).compQuasiMeasurePreserving f hf = mk (g ∘ f) ⋯

Tactic:
rfl

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.compQuasiMeasurePreserving, 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 : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
rw : g.compQuasiMeasurePreserving f hf = (mk (↑g : β → γ) ⋯).compQuasiMeasurePreserving f hf
rw₁ rw₂ : g.compQuasiMeasurePreserving f hf = g.compQuasiMeasurePreserving f hf
⊢ g.compQuasiMeasurePreserving f hf = mk ((↑g : β → γ) ∘ f) ⋯

Tactic:
rw [← compQuasiMeasurePreserving_mk g.aestronglyMeasurable hf, mk_coeFn]

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

Tactic:
rw [compQuasiMeasurePreserving_eq_mk]

Premises used: MeasureTheory.AEEqFun.compQuasiMeasurePreserving_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 : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving 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 : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
f' : α → β
hf' : Measurable f'
h : f =ᶠ[ae μ] f'
h₁ : (↑(g.compQuasiMeasurePreserving f hf) : α → γ) =ᶠ[ae μ] (↑(g.compQuasiMeasurePreserving f' ⋯) : α → γ)
⊢ g.compQuasiMeasurePreserving f hf = g.compQuasiMeasurePreserving f' ⋯

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
f' : α → β
hf' : Measurable f'
h : f =ᶠ[ae μ] f'
h₁ : (↑g : β → γ) ∘ f =ᶠ[ae μ] (↑(g.compQuasiMeasurePreserving f' ⋯) : α → γ)
h₂ : (↑g : β → γ) ∘ f =ᶠ[ae μ] (↑g : β → γ) ∘ f'
h₃ h₄ : (↑g : β → γ) ∘ f' =ᶠ[ae μ] (↑g : β → γ) ∘ f'
⊢ (↑(g.compQuasiMeasurePreserving f hf) : α → γ) =ᶠ[ae μ] (↑(g.compQuasiMeasurePreserving f' ⋯) : α → γ)

Tactic:
grw [coeFn_compQuasiMeasurePreserving, coeFn_compQuasiMeasurePreserving, h]

Premises used: MeasureTheory.AEEqFun.coeFn_compQuasiMeasurePreserving
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
β : Type u_2
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : MeasurableSpace β
ν : Measure β
g : β →ₘ[ν] γ
h : (↑(g.compQuasiMeasurePreserving id ⋯) : β → γ) =ᶠ[ae ν] (↑g : β → γ)
⊢ g.compQuasiMeasurePreserving id ⋯ = g

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
β : Type u_2
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : MeasurableSpace β
ν : Measure β
g : β →ₘ[ν] γ
⊢ (↑(g.compQuasiMeasurePreserving id ⋯) : β → γ) =ᶠ[ae ν] (↑g : β → γ)

Tactic:
coeFn_compQuasiMeasurePreserving _ _

Premises used: MeasureTheory.AEEqFun.cast, MeasureTheory.AEEqFun.coeFn_compQuasiMeasurePreserving, dite
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
β : Type u_2
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : MeasurableSpace β
ν : Measure β
g : β →ₘ[ν] γ
⊢ (↑(g.compQuasiMeasurePreserving id ⋯) : β → γ) =ᶠ[ae ν] (↑g : β → γ)

Tactic:
exact coeFn_compQuasiMeasurePreserving _ _

Premises used: MeasureTheory.AEEqFun.coeFn_compQuasiMeasurePreserving
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
δ : Type u_4
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace δ
inst_2 : MeasurableSpace β
ν : Measure β
γ : Type u_5
mγ : MeasurableSpace γ
ξ : Measure γ
g : γ →ₘ[ξ] δ
f : β → γ
hf : QuasiMeasurePreserving f ν ξ
f' : α → β
hf' : QuasiMeasurePreserving f' μ ν
h :
  (↑(g.compQuasiMeasurePreserving (f ∘ f') ⋯) : α → δ) =ᶠ[ae μ]
    (↑((g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf') : α → δ)
⊢ g.compQuasiMeasurePreserving (f ∘ f') ⋯ = (g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf'

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
δ : Type u_4
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace δ
inst_2 : MeasurableSpace β
ν : Measure β
γ : Type u_5
mγ : MeasurableSpace γ
ξ : Measure γ
g : γ →ₘ[ξ] δ
f : β → γ
hf : QuasiMeasurePreserving f ν ξ
f' : α → β
hf' : QuasiMeasurePreserving f' μ ν
h : (↑g : γ → δ) ∘ f ∘ f' =ᶠ[ae μ] (↑((g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf') : α → δ)
h₁ : (↑g : γ → δ) ∘ f ∘ f' =ᶠ[ae μ] (↑(g.compQuasiMeasurePreserving f hf) : β → δ) ∘ f'
h₂ : (↑g : γ → δ) ∘ f ∘ f' =ᶠ[ae μ] ((↑g : γ → δ) ∘ f) ∘ f'
h₃ h₄ : (↑g : γ → δ) ∘ f ∘ f' =ᶠ[ae μ] (↑g : γ → δ) ∘ f ∘ f'
⊢ (↑(g.compQuasiMeasurePreserving (f ∘ f') ⋯) : α → δ) =ᶠ[ae μ]
    (↑((g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf') : α → δ)

Tactic:
grw [coeFn_compQuasiMeasurePreserving, coeFn_compQuasiMeasurePreserving,
    coeFn_compQuasiMeasurePreserving, comp_assoc]

Premises used: MeasureTheory.AEEqFun.coeFn_compQuasiMeasurePreserving, Function.comp_assoc
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
g : α →ₘ[μ] γ
f : α → α
hf : QuasiMeasurePreserving f μ μ
⊢ (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[0] g = g.compQuasiMeasurePreserving f^[0] ⋯

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
g : α →ₘ[μ] γ
f : α → α
hf : QuasiMeasurePreserving f μ μ
n : ℕ
hind : (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[n] g = g.compQuasiMeasurePreserving f^[n] ⋯
succ : (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[1 + n] g = g.compQuasiMeasurePreserving f^[n + 1] ⋯
⊢ (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[n + 1] g = g.compQuasiMeasurePreserving f^[n + 1] ⋯

Tactic:
nth_rewrite 1 [add_comm]

Premises used: add_comm
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
g : α →ₘ[μ] γ
f : α → α
hf : QuasiMeasurePreserving f μ μ
n : ℕ
hind : (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[n] g = g.compQuasiMeasurePreserving f^[n] ⋯
⊢ (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[1 + n] g = g.compQuasiMeasurePreserving f^[n + 1] ⋯

Tactic:
simp [iterate_add, hind, ← compQuasiMeasurePreserving_comp]

Premises used: MeasureTheory.AEEqFun.compQuasiMeasurePreserving_comp, Function.iterate_add
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
g : α →ₘ[μ] γ
f : α → α
hf : QuasiMeasurePreserving f μ μ
n : ℕ
zero : (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[0] g = g.compQuasiMeasurePreserving f^[0] ⋯
succ :
  ∀ (n : ℕ)
    (hind : (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[n] g = g.compQuasiMeasurePreserving f^[n] ⋯),
    (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[n + 1] g = g.compQuasiMeasurePreserving f^[n + 1] ⋯
⊢ (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[n] g = g.compQuasiMeasurePreserving f^[n] ⋯

Tactic:
induction n with
  | zero => simp
  | succ n hind =>
    nth_rewrite 1 [add_comm]
    simp [iterate_add, hind, ← compQuasiMeasurePreserving_comp]

Premises used: MeasureTheory.AEEqFun.compQuasiMeasurePreserving_comp, Function.iterate_add, add_comm
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : MeasurableSpace β
ν : Measure β
f : α → β
g : β → γ
hg : AEStronglyMeasurable g ν
hf : MeasurePreserving f μ ν
⊢ (mk g hg).compMeasurePreserving f hf = mk (g ∘ f) ⋯

Tactic:
rfl

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.compMeasurePreserving, MeasureTheory.AEEqFun.compQuasiMeasurePreserving, 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 : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : MeasurePreserving f μ ν
⊢ g.compMeasurePreserving f hf = mk ((↑g : β → γ) ∘ f) ⋯

Tactic:
g.compQuasiMeasurePreserving_eq_mk _

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

Tactic:
g.coeFn_compQuasiMeasurePreserving _

Premises used: MeasureTheory.AEEqFun.compMeasurePreserving, MeasureTheory.AEEqFun.coeFn_compQuasiMeasurePreserving
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : MeasurePreserving f μ ν
f' : α → β
hf' : Measurable f'
h : f =ᶠ[ae μ] f'
⊢ g.compMeasurePreserving f hf = g.compMeasurePreserving f' ⋯

Tactic:
compQuasiMeasurePreserving_congr _ _ hf' h

Premises used: MeasureTheory.AEEqFun.compMeasurePreserving, MeasureTheory.AEEqFun.compQuasiMeasurePreserving_congr
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
β : Type u_2
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : MeasurableSpace β
ν : Measure β
g : β →ₘ[ν] γ
⊢ g.compMeasurePreserving id ⋯ = g

Tactic:
compQuasiMeasurePreserving_id _

Premises used: MeasureTheory.AEEqFun.compMeasurePreserving, MeasureTheory.AEEqFun.compQuasiMeasurePreserving_id
-- Module: Mathlib.MeasureTheory.Function.AEEqFun
Goal:
α : Type u_1
β : Type u_2
δ : Type u_4
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace δ
inst_2 : MeasurableSpace β
ν : Measure β
γ : Type u_5
mγ : MeasurableSpace γ
ξ : Measure γ
g : γ →ₘ[ξ] δ
f : β → γ
hf : MeasurePreserving f ν ξ
f' : α → β
hf' : MeasurePreserving f' μ ν
⊢ g.compMeasurePreserving (f ∘ f') ⋯ = (g.compMeasurePreserving f hf).compMeasurePreserving f' hf'

Tactic:
compQuasiMeasurePreserving_comp _ _ _

Premises used: MeasureTheory.AEEqFun.compQuasiMeasurePreserving_comp, MeasureTheory.AEEqFun.compMeasurePreserving