Differential_traceAlong_eq_traceDiff.lean

theorem _root_.AlgebraicCurve.Differential.traceAlong_eq_traceDiff
    (K F F' : Type*) [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
    (φ : F →ₐ[K] F') (h : AlgebraicCurve.SeparableAlong K φ) (η : Ω[F'⁄K]) :
    AlgebraicCurve.Differential.traceAlong φ η =
      (letI := AlgebraicCurve.algebraAlong φ
       haveI := AlgebraicCurve.isScalarTower_along φ
       AlgebraicCurve.traceDiff K F F' η) := by
  let := algebraAlong φ
  have := isScalarTower_along φ
  have : Algebra.IsSeparable F F' := h
  have : Algebra.FormallyEtale F F' := Algebra.FormallyEtale.of_isSeparable F F'
  obtain ⟨t, rfl⟩ := (KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale K F F').surjective η
  induction t using TensorProduct.inductionOn with
  | tmul y ω =>
    have he : KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale K F F' (y ⊗ₜ ω) =
        y • Differential.pullbackAlong φ ω := by
      rw [KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_apply,
        KaehlerDifferential.mapBaseChange_tmul]
      rfl
    rw [he, Differential.traceAlong_smul_pullbackAlong φ h y ω]
    change Algebra.trace F F' y • ω = traceDiff K F F' (y • KaehlerDifferential.map K K F F' ω)
    rw [traceDiff_apply]
  | add s t hs ht =>
    rw [map_add, map_add, map_add, hs, ht]