awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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 μ ν
⊢ (↑(g.compQuasiMeasurePreserving f hf) : α → γ) =ᶠ[ae μ] (↑g : β → γ) ∘ f
have rw : (↑(mk ((↑g : β → γ) ∘ f) sorry) : α → γ) =ᶠ[ae μ] (↑g : β → γ) ∘ f
Tactic: rw [compQuasiMeasurePreserving_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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'
⊢ g.compQuasiMeasurePreserving f hf = g.compQuasiMeasurePreserving f' ⋯
have h₁ : (↑(g.compQuasiMeasurePreserving f hf) : α → γ) =ᶠ[ae μ] (↑(g.compQuasiMeasurePreserving f' sorry) : α → γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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'
⊢ (↑(g.compQuasiMeasurePreserving f hf) : α → γ) =ᶠ[ae μ] (↑(g.compQuasiMeasurePreserving f' ⋯) : α → γ)
have h₁ : (↑g : β → γ) ∘ f =ᶠ[ae μ] (↑(g.compQuasiMeasurePreserving f' sorry) : α → γ)
Tactic: grw [coeFn_compQuasiMeasurePreserving, coeFn_compQuasiMeasurePreserving, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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' ⋯) : α → γ)
⊢ (↑(g.compQuasiMeasurePreserving f hf) : α → γ) =ᶠ[ae μ] (↑(g.compQuasiMeasurePreserving f' ⋯) : α → γ)
have h₂ : (↑g : β → γ) ∘ f =ᶠ[ae μ] (↑g : β → γ) ∘ f'
Tactic: grw [coeFn_compQuasiMeasurePreserving, coeFn_compQuasiMeasurePreserving, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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'
⊢ (↑(g.compQuasiMeasurePreserving f hf) : α → γ) =ᶠ[ae μ] (↑(g.compQuasiMeasurePreserving f' ⋯) : α → γ)
have h₃ : (↑g : β → γ) ∘ f' =ᶠ[ae μ] (↑g : β → γ) ∘ f'
Tactic: grw [coeFn_compQuasiMeasurePreserving, coeFn_compQuasiMeasurePreserving, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
β : Type u_2
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : MeasurableSpace β
ν : Measure β
g : β →ₘ[ν] γ
⊢ g.compQuasiMeasurePreserving id ⋯ = g
have h : (↑(g.compQuasiMeasurePreserving id sorry) : β → γ) =ᶠ[ae ν] (↑g : β → γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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' μ ν
⊢ g.compQuasiMeasurePreserving (f ∘ f') ⋯ = (g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf'
have h : (↑(g.compQuasiMeasurePreserving (f ∘ f') sorry) : α → δ) =ᶠ[ae μ]
  (↑((g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf') : α → δ)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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' μ ν
⊢ (↑(g.compQuasiMeasurePreserving (f ∘ f') ⋯) : α → δ) =ᶠ[ae μ]
    (↑((g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf') : α → δ)
have h : (↑g : γ → δ) ∘ f ∘ f' =ᶠ[ae μ] (↑((g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf') : α → δ)
Tactic: grw [coeFn_compQuasiMeasurePreserving, coeFn_compQuasiMeasurePreserving,
    coeFn_compQuasiMeasurePreserving, comp_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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') : α → δ)
⊢ (↑(g.compQuasiMeasurePreserving (f ∘ f') ⋯) : α → δ) =ᶠ[ae μ]
    (↑((g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf') : α → δ)
have h₁ : (↑g : γ → δ) ∘ f ∘ f' =ᶠ[ae μ] (↑(g.compQuasiMeasurePreserving f hf) : β → δ) ∘ f'
Tactic: grw [coeFn_compQuasiMeasurePreserving, coeFn_compQuasiMeasurePreserving,
    coeFn_compQuasiMeasurePreserving, comp_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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'
⊢ (↑(g.compQuasiMeasurePreserving (f ∘ f') ⋯) : α → δ) =ᶠ[ae μ]
    (↑((g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf') : α → δ)
have h₂ : (↑g : γ → δ) ∘ f ∘ f' =ᶠ[ae μ] ((↑g : γ → δ) ∘ f) ∘ f'
Tactic: grw [coeFn_compQuasiMeasurePreserving, coeFn_compQuasiMeasurePreserving,
    coeFn_compQuasiMeasurePreserving, comp_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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'
⊢ (↑(g.compQuasiMeasurePreserving (f ∘ f') ⋯) : α → δ) =ᶠ[ae μ]
    (↑((g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf') : α → δ)
have h₃ : (↑g : γ → δ) ∘ f ∘ f' =ᶠ[ae μ] (↑g : γ → δ) ∘ f ∘ f'
Tactic: grw [coeFn_compQuasiMeasurePreserving, coeFn_compQuasiMeasurePreserving,
    coeFn_compQuasiMeasurePreserving, comp_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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)^[n + 1] g = g.compQuasiMeasurePreserving f^[n + 1] ⋯
have succ : (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[1 + n] g = g.compQuasiMeasurePreserving f^[n + 1] sorry
Tactic: nth_rewrite 1 [add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
g : α →ₘ[μ] γ
f : α → α
hf : QuasiMeasurePreserving f μ μ
n : ℕ
⊢ (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[n] g = g.compQuasiMeasurePreserving f^[n] ⋯
have zero : (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[0] g = g.compQuasiMeasurePreserving f^[0] sorry
Tactic: induction n with
  | zero => simp
  | succ n hind =>
    nth_rewrite 1 [add_comm]
    simp [iterate_add, hind, ← compQuasiMeasurePreserving_comp]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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] ⋯
⊢ (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[n] g = g.compQuasiMeasurePreserving f^[n] ⋯
have succ : ∀ (n : ℕ)
  (hind : (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[n] g = g.compQuasiMeasurePreserving f^[n] sorry),
  (fun (x : α →ₘ[μ] γ) ↦ x.compQuasiMeasurePreserving f hf)^[n + 1] g = g.compQuasiMeasurePreserving f^[n + 1] sorry
Tactic: induction n with
  | zero => simp
  | succ n hind =>
    nth_rewrite 1 [add_comm]
    simp [iterate_add, hind, ← compQuasiMeasurePreserving_comp]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
⊢ comp id ⋯ f = f
have mk : ∀ (a : { f : α → β // AEStronglyMeasurable f μ }),
  comp id sorry
      (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: rcases f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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 : α →ₘ[μ] β
⊢ comp g hg f = mk (g ∘ (↑f : α → β)) ⋯
have rw : comp g hg f = comp g hg (mk (↑f : α → β) sorry)
Tactic: rw [← comp_mk g hg f f.aestronglyMeasurable, mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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 : α → β) ⋯)
⊢ comp g hg f = mk (g ∘ (↑f : α → β)) ⋯
have rw₁ : comp g hg f = comp g hg f
Tactic: rw [← comp_mk g hg f f.aestronglyMeasurable, mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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 : α →ₘ[μ] β
⊢ (↑(comp g hg f) : α → γ) =ᶠ[ae μ] g ∘ (↑f : α → β)
have rw : (↑(mk (g ∘ (↑f : α → β)) sorry) : α → γ) =ᶠ[ae μ] g ∘ (↑f : α → β)
Tactic: rw [comp_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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 φ μ ν
⊢ (comp g hg f).compQuasiMeasurePreserving φ hφ = comp g hg (f.compQuasiMeasurePreserving φ hφ)
have 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φ)
Tactic: rcases f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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 : α →ₘ[μ] β
⊢ Eq (α := α →ₘ[μ] γ) (compMeasurable g hg f) (mk (g ∘ (↑f : α → β)) ⋯)
have rw : Eq (α := α →ₘ[μ] γ) (compMeasurable g hg f) (compMeasurable g hg (mk (↑f : α → β) sorry))
Tactic: rw [← compMeasurable_mk g hg f f.aestronglyMeasurable, mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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 : α → β) ⋯))
⊢ Eq (α := α →ₘ[μ] γ) (compMeasurable g hg f) (mk (g ∘ (↑f : α → β)) ⋯)
have rw₁ : Eq (α := α →ₘ[μ] γ) (compMeasurable g hg f) (compMeasurable g hg f)
Tactic: rw [← compMeasurable_mk g hg f f.aestronglyMeasurable, mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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 : α →ₘ[μ] β
⊢ (↑(compMeasurable g hg f) : α → γ) =ᶠ[ae μ] g ∘ (↑f : α → β)
have rw : (↑(mk (g ∘ (↑f : α → β)) sorry) : α → γ) =ᶠ[ae μ] g ∘ (↑f : α → β)
Tactic: rw [compMeasurable_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α →ₘ[μ] β
g : α →ₘ[μ] γ
⊢ (↑(f.pair g) : α → β × γ) =ᶠ[ae μ] fun (x : α) ↦ ((↑f : α → β) x, (↑g : α → γ) x)
have rw : (↑(mk (fun (x : α) ↦ ((↑f : α → β) x, (↑g : α → γ) x)) sorry) : α → β × γ) =ᶠ[ae μ] fun (x : α) ↦
  ((↑f : α → β) x, (↑g : α → γ) x)
Tactic: rw [pair_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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₂ = mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) ⋯
have rw : mk (uncurry g ∘ fun (x : α) ↦ ((↑f₁ : α → β) x, (↑f₂ : α → γ) x)) sorry =
  mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) sorry
Tactic: rw [comp₂_eq_pair, pair_eq_mk, comp_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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₂) : α → δ) =ᶠ[ae μ] fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)
have rw : (↑(mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) sorry) : α → δ) =ᶠ[ae μ] fun (a : α) ↦
  g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)
Tactic: rw [comp₂_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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₂) (mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) ⋯)
have rw : Eq (α := α →ₘ[μ] δ) (mk (uncurry g ∘ fun (x : α) ↦ ((↑f₁ : α → β) x, (↑f₂ : α → γ) x)) sorry)
  (mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) sorry)
Tactic: rw [comp₂Measurable_eq_pair, pair_eq_mk, compMeasurable_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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₂ : α →ₘ[μ] γ
⊢ (↑(comp₂Measurable g hg f₁ f₂) : α → δ) =ᶠ[ae μ] fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)
have rw : (↑(mk (fun (a : α) ↦ g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)) sorry) : α → δ) =ᶠ[ae μ] fun (a : α) ↦
  g ((↑f₁ : α → β) a) ((↑f₂ : α → γ) a)
Tactic: rw [comp₂Measurable_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
⊢ f.toGerm = (↑(↑f : α → β) : (ae μ).Germ β)
have rw : f.toGerm = (mk (↑f : α → β) sorry).toGerm
Tactic: rw [← mk_toGerm f f.aestronglyMeasurable, mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
rw : f.toGerm = (mk (↑f : α → β) ⋯).toGerm
⊢ f.toGerm = (↑(↑f : α → β) : (ae μ).Germ β)
have rw₁ : f.toGerm = f.toGerm
Tactic: rw [← mk_toGerm f f.aestronglyMeasurable, mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f g : α →ₘ[μ] β
H : f.toGerm = g.toGerm
⊢ Eq (α := (ae μ).Germ β) (↑(↑f : α → β) : (ae μ).Germ β) (↑(↑g : α → β) : (ae μ).Germ β)
have rwa : f.toGerm = (↑(↑g : α → β) : (ae μ).Germ β)
Tactic: rwa [← toGerm_eq, ← toGerm_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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 μ ν
⊢ (g.compQuasiMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f ⋯
have 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 sorry
Tactic: rcases g
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
r : β → γ → Prop
f : α →ₘ[μ] β
g : α →ₘ[μ] γ
⊢ LiftRel r f g ↔ ∀ᵐ (a : α) ∂μ, r ((↑f : α → β) a) ((↑g : α → γ) a)
have rw : LiftRel r f g ↔ LiftRel r (mk (↑f : α → β) sorry) (mk (↑g : α → γ) sorry)
Tactic: rw [← liftRel_mk_mk (hf := f.aestronglyMeasurable) (hg := g.aestronglyMeasurable),
    mk_coeFn, mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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 : α → γ) ⋯)
⊢ LiftRel r f g ↔ ∀ᵐ (a : α) ∂μ, r ((↑f : α → β) a) ((↑g : α → γ) a)
have rw₁ : LiftRel r f g ↔ LiftRel r f (mk (↑g : α → γ) sorry)
Tactic: rw [← liftRel_mk_mk (hf := f.aestronglyMeasurable) (hg := g.aestronglyMeasurable),
    mk_coeFn, mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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 : α → γ) ⋯)
⊢ LiftRel r f g ↔ ∀ᵐ (a : α) ∂μ, r ((↑f : α → β) a) ((↑g : α → γ) a)
have rw₂ : LiftRel r f g ↔ LiftRel r f g
Tactic: rw [← liftRel_mk_mk (hf := f.aestronglyMeasurable) (hg := g.aestronglyMeasurable),
    mk_coeFn, mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
⊢ f ≤ f ⊔ g
have rw : (↑f : α → β) ≤ᶠ[ae μ] (↑(f ⊔ g) : α → β)
Tactic: rw [← coeFn_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
⊢ (↑f : α → β) ≤ᶠ[ae μ] (↑(f ⊔ g) : α → β)
have h : ∀ (a : α) (ha : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a), (↑f : α → β) a ≤ (↑(f ⊔ g) : α → β) a
Tactic: filter_upwards [coeFn_sup f g] with _ ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
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 ⊔ g) : α → β) a
have h : (↑f : α → β) a ≤ (↑f : α → β) a ⊔ (↑g : α → β) a
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
⊢ g ≤ f ⊔ g
have rw : (↑g : α → β) ≤ᶠ[ae μ] (↑(f ⊔ g) : α → β)
Tactic: rw [← coeFn_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
⊢ (↑g : α → β) ≤ᶠ[ae μ] (↑(f ⊔ g) : α → β)
have h : ∀ (a : α) (ha : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a), (↑g : α → β) a ≤ (↑(f ⊔ g) : α → β) a
Tactic: filter_upwards [coeFn_sup f g] with _ ha