DivisorialWeilPairingData_pair_eq_pair_of_coe_eq_nsmul.lean

def towerDatumTop (m n : ℕ) (D₁ D₂ : Divisor K F) (f₁ g : F)
    (hf₁0 : f₁ ≠ 0) (hg0 : g ≠ 0)
    (hf₁ : ∀ v : Place K F, v.ord f₁ = ↑(m * n) * D₁ v)
    (hg : ∀ v : Place K F, v.ord g = ↑m * D₂ v)
    (hdisj : ∀ v : Place K F, D₁ v = 0 ∨ D₂ v = 0)
    (hrat : ∀ v : Place K F, D₁ v ≠ 0 ∨ D₂ v ≠ 0 → v.IsRational) :
    WeilDatum K F (m * n) where
  D₁ := D₁
  D₂ := D₂
  f₁ := f₁
  f₂ := g ^ (n : ℤ)
  f₁_ne_zero := hf₁0
  f₂_ne_zero := zpow_ne_zero _ hg0
  ord_f₁ := hf₁
  ord_f₂ := by
    intro v
    rw [v.ord_zpow, hg v]
    push_cast
    ring
  disjoint := hdisj
  rational := hrat

def towerDatumBase (m n : ℕ) (D₁ D₂ : Divisor K F) (f₁ g : F)
    (hf₁0 : f₁ ≠ 0) (hg0 : g ≠ 0)
    (hf₁ : ∀ v : Place K F, v.ord f₁ = ↑(m * n) * D₁ v)
    (hg : ∀ v : Place K F, v.ord g = ↑m * D₂ v)
    (hdisj : ∀ v : Place K F, D₁ v = 0 ∨ D₂ v = 0)
    (hrat : ∀ v : Place K F, D₁ v ≠ 0 ∨ D₂ v ≠ 0 → v.IsRational) :
    WeilDatum K F m where
  D₁ := (n : ℤ) • D₁
  D₂ := D₂
  f₁ := f₁
  f₂ := g
  f₁_ne_zero := hf₁0
  f₂_ne_zero := hg0
  ord_f₁ := by
    intro v
    rw [hf₁ v, Finsupp.smul_apply, smul_eq_mul]
    push_cast
    ring
  ord_f₂ := hg
  disjoint := by
    intro v
    rcases hdisj v with h | h
    · exact Or.inl (by rw [Finsupp.smul_apply, smul_eq_mul, h, mul_zero])
    · exact Or.inr h
  rational := by
    intro v hv
    rcases hv with h1 | h2
    · refine hrat v (Or.inl fun h0 => h1 ?_)
      rw [Finsupp.smul_apply, smul_eq_mul, h0, mul_zero]
    · exact hrat v (Or.inr h2)

theorem _root_.AlgebraicCurve.DivisorialWeilPairingData.pair_eq_pair_of_coe_eq_nsmul {K F : Type*}
    [Field K] [Field F] [Algebra K F]
    (m n : ℕ) [NeZero m] [NeZero (m * n)] [HasPrincipalDivisors K F]
    (e_mn : DivisorialWeilPairingData K F (m * n))
    (e_m : DivisorialWeilPairingData K F m)
    (x : Pic0.torsion K F (m * n)) (y : Pic0.torsion K F m)
    (y' : Pic0.torsion K F (m * n)) (hy : (y' : Pic0 K F) = (y : Pic0 K F))
    (x' : Pic0.torsion K F m) (hx : (x' : Pic0 K F) = (n : ℤ) • (x : Pic0 K F)) :
    e_mn.pair x y' = e_m.pair x' y