WeilDatum_pairing_eq_pairing_of_pullbackAlong_of_pushforwardAlong_of_separableAlong.lean

theorem main
    {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
    [HasPrincipalDivisors K F] [HasPrincipalDivisors K F']
    (u : F →ₐ[K] F') (hu : u.toRingHom.IsIntegral) (hfin : FiniteAlong K u)
    (hsep : SeparableAlong K u)
    (hratF : ∀ v : Place K F, v.IsRational) (hratF' : ∀ w : Place K F', w.IsRational)
    {n : ℕ} (d : WeilDatum K F' n) (d₀ : WeilDatum K F n)
    (hD₁ : d.D₁ = Divisor.pullbackAlong u hu d₀.D₁) (hf₁ : d.f₁ = u d₀.f₁)
    (hD₂ : d₀.D₂ = Divisor.pushforwardAlong u hu d.D₂)
    (hf₂ : d₀.f₂ = (let _ : Algebra F F' := algebraAlong u; Algebra.norm F d.f₂)) :
    d.pairing = d₀.pairing := by
  let := algebraAlong u
  have := isScalarTower_along u
  have := isIntegral_along u hu
  have : Module.Finite F F' := hfin
  have : Algebra.IsSeparable F F' := hsep
  have hD₁w : ∀ w : Place K F', d.D₁ w = w.ramificationIndex F * d₀.D₁ (w.restrict F) := by
    intro w
    rw [hD₁]
    exact Divisor.pullback_apply d₀.D₁ w
  have hnum : Divisor.evalFun d.f₁ d.D₂ = Divisor.evalFun d₀.f₁ d₀.D₂ := by
    rw [hf₁, hD₂]
    refine Divisor.evalFun_algebraMap_pushforward d₀.f₁_ne_zero d.D₂ (fun w _ => hratF' w)
      (fun w _ => hratF _) (fun w hw => ?_)
    have h2 : d.D₂ w ≠ 0 := Finsupp.mem_support_iff.mp hw
    have h1 : d.D₁ w = 0 := (d.disjoint w).resolve_right h2
    rw [hD₁w w] at h1
    have he : (w.ramificationIndex F : ℤ) ≠ 0 := by
      have := w.ramificationIndex_pos (F := F)
      exact_mod_cast this.ne'
    have h0 : d₀.D₁ (w.restrict F) = 0 := (mul_eq_zero.mp h1).resolve_left he
    rw [d₀.ord_f₁, h0, mul_zero]
  have hden : Divisor.evalFun d.f₂ d.D₁ = Divisor.evalFun d₀.f₂ d₀.D₁ := by
    rw [hD₁, hf₂]
    refine Divisor.evalFun_pullback d.f₂_ne_zero d₀.D₁ (fun v _ => hratF v)
      (fun v _ w _ => hratF' w) (fun v hv w hw => ?_)
    have hwv : w.restrict F = v := Place.mem_fiber.mp hw
    have hv' : d₀.D₁ v ≠ 0 := Finsupp.mem_support_iff.mp hv
    have he : (w.ramificationIndex F : ℤ) ≠ 0 := by
      have := w.ramificationIndex_pos (F := F)
      exact_mod_cast this.ne'
    have h1 : d.D₁ w ≠ 0 := by
      rw [hD₁w w, hwv]
      exact mul_ne_zero he hv'
    have h2 : d.D₂ w = 0 := (d.disjoint w).resolve_left h1
    rw [d.ord_f₂, h2, mul_zero]
  rw [WeilDatum.pairing, WeilDatum.pairing, hnum, hden]

theorem pairing_eq_pairing_of_pullbackAlong_of_pushforwardAlong_of_separableAlong
    {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
    [HasPrincipalDivisors K F] [HasPrincipalDivisors K F']
    (u : F →ₐ[K] F') (hu : u.toRingHom.IsIntegral) (hfin : FiniteAlong K u)
    (hsep : SeparableAlong K u)
    (hratF : ∀ v : Place K F, v.IsRational) (hratF' : ∀ w : Place K F', w.IsRational)
    {n : ℕ} (d : WeilDatum K F' n) (d₀ : WeilDatum K F n)
    (hD₁ : d.D₁ = Divisor.pullbackAlong u hu d₀.D₁) (hf₁ : d.f₁ = u d₀.f₁)
    (hD₂ : d₀.D₂ = Divisor.pushforwardAlong u hu d.D₂)
    (hf₂ : d₀.f₂ = (let _ : Algebra F F' := algebraAlong u; Algebra.norm F d.f₂)) :
    d.pairing = d₀.pairing :=
  pairingTransfer u hu hfin hsep hratF hratF' d d₀ hD₁ hf₁ hD₂ hf₂