/-
Copyright (c) 2026 LANA Project. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: LANA Project
-/
import Iut.Tower.TorsionRigid
import Iut.Tripod.Tower
import Iut.Tripod.LogCond
import Iut.Anabelian.Torsion
import Iut.Torsion.EDS

/-!
# Néron–Ogg–Shafarevich for the curves of the tripod

For a point `λ` of the tripod, the tower `F_tpd = ℚ(λ) ⊆ F = F_λ ⊆ K = F(E_λ[ℓ])` is
unramified at the places `v` of `K` of residue characteristic `p ∉ {2, 3, 5, ℓ}` whose place `u`
of `F_tpd` is not bad (`Iut.Tripod.relRamIdx_eq_one_of_not_bad`, the field `relRamIdx_eq_one` of
`Iut.TowerLocalFacts`):

* at such a place `λ` and `λ − 1` are units (`Iut.Tripod.isBadTpdOf_of_mem_badT`), so the Legendre
  model `y² = x(x − 1)(x − λ)` is a good model at every place above `u`;
* `F/F_tpd` is Galois (`F_λ/ℚ(j)` is), generated by `√−1, √λ, √(1 − λ)` and the coordinates
  of the `3`- and `5`-torsion (`Iut.Tripod.adjoin_tpdGens`); the square roots of units and the
  prime-to-`p` torsion points are fixed by the inertia group (`Iut.Tripod.tpdGens_fixed`,
  from `Iut.sqrt_fixed_of_valuation_sub_lt` and `Iut.map_eq_self_of_nsmul_eq_zero`), so
  `e(w/u) = 1` (`Iut.Tripod.relRamIdx_placeUnder_eq_one`);
* `K/F` is Galois with `Gal(K/F)` acting faithfully on `E(K)[ℓ]`
  (`Iut.AdmissiblePrimeData.eq_one_of_forall_torsion`), so `e(v/w) = 1` by Néron–Ogg–Shafarevich
  (`Iut.relRamIdx_eq_one_of_torsion`, `Iut.Tripod.relRamIdx_torsionField_eq_one`).

The description `n • P = 0 ↔ ψₙ(P) = 0` of the multiples of a point by the division
polynomials, for the Legendre curves over the number fields in play, is the hypothesis
`Iut.Tripod.DivPolyLegendreHyp` (`Iut.ReductionKernel.DivPolyHyp`, proved in
`Iut.Torsion.smul_eq_zero_iff_eds`).
-/

namespace Iut

open NumberField IsDedekindDomain IsDedekindDomain.HeightOneSpectrum WeierstrassCurve
  WeierstrassCurve.Affine


/-! ### The Galois group of the torsion field acts faithfully on the torsion -/

namespace AdmissiblePrimeData

universe u

attribute [local instance 1100] AdmissiblePrimeData.instDecidableEqK

variable {F : Type u} [Field F] [NumberField F] {E : WeierstrassCurve F} [E.IsElliptic]
variable {Fbar : Type u} [Field Fbar] [Algebra F Fbar] [IsAlgClosure F Fbar]
variable {VBad : Set (FinitePlace ↥(fieldOfModuli F E))}
variable (Pr : Iut.AdmissiblePrimeData F E Fbar VBad)

open scoped Classical in
/-- **`Gal(K/F)` acts faithfully on `E(K)[ℓ]`**: an automorphism of `K = F(E[ℓ])` over `F`
fixing every `ℓ`-torsion point of `E(K)` is the identity. -/
theorem eq_one_of_forall_torsion (σ : ↥Pr.torsionField ≃ₐ[F] ↥Pr.torsionField)
    (h : ∀ Q : Pr.EK.toAffine.Point, Pr.ℓ • Q = 0 → Pr.galK σ Q = Q) : σ = 1 := by
  obtain ⟨τ, rfl⟩ := AlgEquiv.restrictNormalHom_surjective (F := F) (K₁ := ↥Pr.torsionField)
    Fbar σ
  have hrep : Pr.rep τ = 1 := by
    have key : ∀ w : Fin 2 → ZMod Pr.ℓ, (Pr.rep τ : Matrix (Fin 2) (Fin 2) (ZMod Pr.ℓ)).mulVec w
        = w := by
      intro w
      obtain ⟨R, rfl⟩ := Pr.basisK.surjective w
      rw [← Pr.basisK_galTK τ R]
      congr 1
      apply Subtype.ext
      rw [AdmissiblePrimeData.coe_galTK]
      have hR := R.2
      rw [AddSubgroup.torsionBy.nsmul_iff] at hR
      exact h R.1 hR
    apply Units.ext
    ext i j
    have := congrFun (key (Pi.single j 1)) i
    rw [Matrix.mulVec_single, MulOpposite.op_one, one_smul, Matrix.col_apply] at this
    rw [this, Units.val_one, Matrix.one_apply, Pi.single_apply]
  ext y
  rw [AlgEquiv.one_apply, AlgEquiv.restrictNormalHom_apply]
  exact (IntermediateField.mem_fixedField_iff _ _).mp y.2 τ hrep

end AdmissiblePrimeData

end Iut

namespace Iut.Tripod

open Iut Iut.EllipticCurveData NumberField IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
  WeierstrassCurve WeierstrassCurve.Affine


open scoped Classical in
/-- **The division-polynomial description of the multiples of a point on a Legendre curve**,
over any field of characteristic `≠ 2` in `Type` (`Iut.ReductionKernel.DivPolyHyp`; proved by
`Iut.Torsion.smul_eq_zero_iff_eds`). -/
def DivPolyLegendreHyp : Prop :=
  ∀ (L : Type) [Field L] [DecidableEq L] [NeZero (2 : L)] (l : L),
    ReductionKernel.DivPolyHyp (legendre l).toAffine

open scoped Classical in
/-- **The division polynomials describe the multiples of a point on a Legendre curve**
(`Iut.Torsion.smul_eq_zero_iff_eds`). -/
theorem divPolyLegendreHyp : DivPolyLegendreHyp := by
  intro L _ inst _ l x y h n
  have hi : inst = fun a b => Classical.propDecidable (a = b) := Subsingleton.elim _ _
  subst hi
  exact Iut.Torsion.smul_eq_zero_iff_eds (W := (legendre l).toAffine) rfl rfl h n

attribute [local instance 1100] AdmissiblePrimeData.instDecidableEqK

variable (P : CurveProviders) (x : Pt)

/-! ### The Legendre model at a place where `λ` and `λ − 1` are units -/

section GoodModel

variable {L : Type} [Field L] [NumberField L] [Algebra (tpd P x) L]
  (w : FinitePlace L)

open scoped Classical in
/-- The valuation hypotheses of `Iut.map_eq_self_of_nsmul_eq_zero` for the Legendre model of
`λ ∈ F_tpd` at a place `w` of an extension `L` of `F_tpd` with `w(λ) = w(λ − 1) = w(2) = 1`. -/
lemma legendre_genT_good (h2 : w.maximalIdeal.valuation L 2 = 1)
    (hl : w.maximalIdeal.valuation L (algebraMap (tpd P x) L (genT P x)) = 1)
    (hl1 : w.maximalIdeal.valuation L (algebraMap (tpd P x) L (genT P x - 1)) = 1) :
    w.maximalIdeal.valuation L (algebraMap (tpd P x) L (legendre (genT P x)).a₂) ≤ 1 ∧
    w.maximalIdeal.valuation L (algebraMap (tpd P x) L (legendre (genT P x)).a₄) ≤ 1 ∧
    w.maximalIdeal.valuation L (algebraMap (tpd P x) L (legendre (genT P x)).a₆) ≤ 1 ∧
    w.maximalIdeal.valuation L (algebraMap (tpd P x) L (legendre (genT P x)).Δ) = 1 := by
  set v := w.maximalIdeal.valuation L
  refine ⟨?_, hl.le, by simp [legendre], ?_⟩
  · change v (algebraMap (tpd P x) L (-(1 + genT P x))) ≤ 1
    rw [map_neg, map_add, map_one, Valuation.map_neg]
    exact (Valuation.map_add _ _ _).trans (max_le (by rw [map_one]) hl.le)
  · have h16 : v (algebraMap (tpd P x) L 16) = 1 := by
      have : (algebraMap (tpd P x) L 16) = 2 ^ 4 := by
        rw [map_ofNat]; norm_num
      rw [this, map_pow, h2, one_pow]
    rw [legendre_Δ, map_mul, map_mul, map_pow, map_pow, map_mul, map_mul, map_pow, map_pow, hl,
      hl1, h16]
    simp

end GoodModel

/-! ### The generators of `F/F_tpd` -/

open scoped Classical in
/-- The generators `√−1, √λ, √(1 − λ)` and the coordinates of the `3`- and `5`-torsion of
`F = F_λ` over `F_tpd = ℚ(λ)`. -/
def tpdGens : Set (P.curve x).F :=
  {sqrtNegOne' x.1, sqrtLam' x.1, sqrtOneSubLam' x.1} ∪
    {c | Subtype.val c ∈ torsionCoords x.1 3} ∪ {c | Subtype.val c ∈ torsionCoords x.1 5}

open scoped Classical in
/-- The subfield `F_tpd(√−1, √λ, √(1 − λ), E[3], E[5])` of `F`. -/
noncomputable abbrev tpdAdjoin : IntermediateField (tpd P x) (P.curve x).F :=
  IntermediateField.adjoin (tpd P x) (tpdGens P x)

open scoped Classical in
/-- **`F = F_tpd(√−1, √λ, √(1 − λ), E[3], E[5])`.** -/
theorem adjoin_tpdGens : tpdAdjoin P x = ⊤ := by
  rw [eq_top_iff]
  rintro ⟨t, ht⟩ -
  refine IntermediateField.adjoin_induction (F := ℚ) (E := Qbar)
    (s := ({x.1, sqrtNegOne, sqrtLam x.1, sqrtOneSubLam x.1} ∪ torsionCoords x.1 3 ∪
      torsionCoords x.1 5))
    (p := fun y hy => (⟨y, hy⟩ : (P.curve x).F) ∈ tpdAdjoin P x) ?_ ?_ ?_ ?_ ?_ ht
  · intro y hy
    rcases hy with (hy | hy) | hy
    · simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hy
      rcases hy with rfl | rfl | rfl | rfl
      · have hmem : algebraMap (tpd P x) (P.curve x).F (genT P x) ∈ tpdAdjoin P x :=
          IntermediateField.algebraMap_mem _ _
        exact hmem
      · exact IntermediateField.subset_adjoin _ _ (Or.inl (Or.inl (Set.mem_insert _ _)))
      · exact IntermediateField.subset_adjoin _ _
          (Or.inl (Or.inl (Set.mem_insert_of_mem _ (Set.mem_insert _ _))))
      · exact IntermediateField.subset_adjoin _ _
          (Or.inl (Or.inl (Set.mem_insert_of_mem _
            (Set.mem_insert_of_mem _ (Set.mem_singleton _)))))
    · exact IntermediateField.subset_adjoin _ _ (Or.inl (Or.inr hy))
    · exact IntermediateField.subset_adjoin _ _ (Or.inr hy)
  · intro r
    have hmem : algebraMap (tpd P x) (P.curve x).F (algebraMap ℚ (tpd P x) r) ∈ tpdAdjoin P x :=
      IntermediateField.algebraMap_mem _ _
    rw [← IsScalarTower.algebraMap_apply] at hmem
    exact hmem
  · intro y z _ _ hy hz
    exact add_mem hy hz
  · intro y _ hy
    exact inv_mem hy
  · intro y z _ _ hy hz
    exact mul_mem hy hz

open scoped Classical in
/-- **The Legendre curve of `λ ∈ F_tpd` base changed to `ℚ̄` is `E_λ`.** -/
theorem baseChange_legendre_genT_Fbar :
    Affine.baseChange (legendre (genT P x)) (P.curve x).Fbar = legendre x.1 := by
  change (legendre (genT P x)).baseChange (P.curve x).Fbar = _
  rw [legendre_baseChange, IsScalarTower.algebraMap_apply (tpd P x) (P.curve x).F, algebraMap_genT]
  rfl

open scoped Classical in
/-- **The Legendre curve of `λ ∈ F_tpd` base changed to `F` is `E_λ/F`.** -/
theorem baseChange_legendre_genT :
    Affine.baseChange (legendre (genT P x)) (P.curve x).F = (legendre (genC' P x)).toAffine := by
  change (legendre (genT P x)).baseChange (P.curve x).F = _
  rw [legendre_baseChange, algebraMap_genT]

/-! ### Rigidity of the generators at a good place -/

variable {P x}

open scoped Classical in
/-- **The `n`-torsion coordinates are fixed by the inertia group at a good place** (`n` odd,
`p ∤ 2n`, `λ` and `λ − 1` units). -/
theorem torsionCoord_fixed (hdiv : DivPolyLegendreHyp) {n : ℕ} (hodd : Odd n)
    (hsub : torsionCoords x.1 n ⊆ (fieldOf' x.1 : Set Qbar)) {w : FinitePlace (P.curve x).F}
    (h2 : residueChar w ≠ 2) (hn : w.maximalIdeal.valuation _ (n : (P.curve x).F) = 1)
    (hl : w.maximalIdeal.valuation _ (genC' P x) = 1)
    (hl1 : w.maximalIdeal.valuation _ (genC' P x - 1) = 1)
    (σ : (P.curve x).F ≃ₐ[tpd P x] (P.curve x).F)
    (hσ : ∀ z, w.maximalIdeal.valuation _ z ≤ 1 → w.maximalIdeal.valuation _ (σ z - z) < 1)
    {c : Qbar} (hc : c ∈ torsionCoords x.1 n) (hcF : c ∈ fieldOf' x.1) :
    σ ⟨c, hcF⟩ = ⟨c, hcF⟩ := by
  obtain ⟨Q, hQ, hcQ⟩ := Set.mem_iUnion₂.mp hc
  cases Q with
  | zero => exact absurd hcQ (Set.notMem_empty c)
  | some x₀ y₀ h₀ =>
    have hQ' : n • Affine.Point.some x₀ y₀ h₀ = 0 := hQ
    have hx₀ : x₀ ∈ fieldOf' x.1 := hsub (mem_torsionCoords hQ' (by rw [coords_some]; simp))
    have hy₀ : y₀ ∈ fieldOf' x.1 := hsub (mem_torsionCoords hQ' (by rw [coords_some]; simp))
    obtain ⟨xF, hxF⟩ : ∃ xF : (P.curve x).F, algebraMap (P.curve x).F (P.curve x).Fbar xF = x₀ :=
      ⟨⟨x₀, hx₀⟩, rfl⟩
    obtain ⟨yF, hyF⟩ : ∃ yF : (P.curve x).F, algebraMap (P.curve x).F (P.curve x).Fbar yF = y₀ :=
      ⟨⟨y₀, hy₀⟩, rfl⟩
    subst hxF hyF
    have hcurve := baseChange_legendre_genT_Fbar P x
    set ι := IsScalarTower.toAlgHom (tpd P x) (P.curve x).F (P.curve x).Fbar
    have hns' : (Affine.baseChange (legendre (genT P x)) (P.curve x).Fbar).Nonsingular (ι xF)
        (ι yF) := by
      rw [hcurve]; exact h₀
    have hnsF : (Affine.baseChange (legendre (genT P x)) (P.curve x).F).Nonsingular xF yF :=
      (Affine.baseChange_nonsingular (W := legendre (genT P x)) ι.injective _ _).mp hns'
    have hQF : n • Affine.Point.some xF yF hnsF = 0 := by
      apply Affine.Point.map_injective (W' := legendre (genT P x)) (S := tpd P x) ι
      rw [map_nsmul, Affine.Point.map_some, map_zero]
      exact nsmul_some_eq_zero_of_eq hcurve.symm h₀ hns' n hQ'
    have h2' := valuation_two_eq_one w h2
    obtain ⟨ha₂, ha₄, ha₆, hΔ⟩ := legendre_genT_good P x w h2' (by rw [algebraMap_genT]; exact hl)
      (by rw [map_sub, map_one, algebraMap_genT]; exact hl1)
    have hψ : ReductionKernel.DivPolyHyp
        (Affine.baseChange (legendre (genT P x)) (P.curve x).F) := by
      rw [baseChange_legendre_genT]
      exact hdiv _ _
    have hfix := map_eq_self_of_nsmul_eq_zero (w.maximalIdeal.valuation _) (legendre (genT P x))
      rfl rfl ha₂ ha₄ ha₆ hΔ h2' hψ hodd hn (σ : (P.curve x).F →ₐ[tpd P x] (P.curve x).F) hσ _ hQF
    rw [Affine.Point.map_some] at hfix
    obtain ⟨hfx, hfy⟩ := Affine.Point.some.inj hfix
    rw [coords_some, Set.mem_insert_iff, Set.mem_singleton_iff] at hcQ
    rcases hcQ with rfl | rfl
    · have hc : (⟨_, hcF⟩ : (P.curve x).F) = xF := Subtype.ext rfl
      rw [hc]; exact hfx
    · have hc : (⟨_, hcF⟩ : (P.curve x).F) = yF := Subtype.ext rfl
      rw [hc]; exact hfy

open scoped Classical in
/-- **The generators of `F/F_tpd` are fixed by the inertia group at a good place** of residue
characteristic `∉ {2, 3, 5}`. -/
theorem tpdGens_fixed (hdiv : DivPolyLegendreHyp) {w : FinitePlace (P.curve x).F}
    (h2 : residueChar w ≠ 2) (h3 : residueChar w ≠ 3) (h5 : residueChar w ≠ 5)
    (hl : w.maximalIdeal.valuation _ (genC' P x) = 1)
    (hl1 : w.maximalIdeal.valuation _ (genC' P x - 1) = 1)
    (σ : (P.curve x).F ≃ₐ[tpd P x] (P.curve x).F)
    (hσ : ∀ z, w.maximalIdeal.valuation _ z ≤ 1 → w.maximalIdeal.valuation _ (σ z - z) < 1) :
    ∀ s ∈ tpdGens P x, σ s = s := by
  have h2' := valuation_two_eq_one w h2
  intro s hs
  rcases hs with (hs | hs) | hs
  · rcases hs with rfl | rfl | rfl
    · have hsq : (sqrtNegOne' x.1 : (P.curve x).F) ^ 2 =
          algebraMap (tpd P x) (P.curve x).F (-1) := by
        rw [map_neg, map_one]; exact sqrtNegOne'_sq x.1
      have ha : w.maximalIdeal.valuation _ (algebraMap (tpd P x) (P.curve x).F (-1)) = 1 := by
        rw [map_neg, map_one, Valuation.map_neg, map_one]
      exact sqrt_fixed_of_valuation_sub_lt _ (σ : (P.curve x).F →+* (P.curve x).F) hsq
        (σ.commutes _) ha h2'
        (hσ _ (valuation_eq_one_of_sq _ ((congrArg _ hsq).trans ha)).le)
    · have hsq : (sqrtLam' x.1 : (P.curve x).F) ^ 2 =
          algebraMap (tpd P x) (P.curve x).F (genT P x) := by
        rw [algebraMap_genT]; exact sqrtLam'_sq x.1
      have ha : w.maximalIdeal.valuation _ (algebraMap (tpd P x) (P.curve x).F (genT P x)) = 1 := by
        rw [algebraMap_genT]; exact hl
      exact sqrt_fixed_of_valuation_sub_lt _ (σ : (P.curve x).F →+* (P.curve x).F) hsq
        (σ.commutes _) ha h2'
        (hσ _ (valuation_eq_one_of_sq _ ((congrArg _ hsq).trans ha)).le)
    · have hsq : (sqrtOneSubLam' x.1 : (P.curve x).F) ^ 2 =
          algebraMap (tpd P x) (P.curve x).F (1 - genT P x) := by
        rw [map_sub, map_one, algebraMap_genT]; exact sqrtOneSubLam'_sq x.1
      have ha : w.maximalIdeal.valuation _
          (algebraMap (tpd P x) (P.curve x).F (1 - genT P x)) = 1 := by
        rw [map_sub, map_one, algebraMap_genT, Valuation.map_sub_swap]; exact hl1
      exact sqrt_fixed_of_valuation_sub_lt _ (σ : (P.curve x).F →+* (P.curve x).F) hsq
        (σ.commutes _) ha h2'
        (hσ _ (valuation_eq_one_of_sq _ ((congrArg _ hsq).trans ha)).le)
  · exact torsionCoord_fixed hdiv (by decide) (torsionCoords_three_subset_fieldOf' x.1) h2
      (by have := valuation_three_eq_one w h3; exact_mod_cast this) hl hl1 σ hσ hs s.2
  · exact torsionCoord_fixed hdiv (by decide) (torsionCoords_five_subset_fieldOf' x.1) h2
      (by have := (valuation_natCast_eq_one_iff w Nat.prime_five).2 h5; exact_mod_cast this)
      hl hl1 σ hσ hs s.2

/-! ### `F/F_tpd` and `K/F` are unramified at the good places -/

open scoped Classical in
/-- `F/F_tpd` is Galois. -/
theorem isGalois_tpd_curve' : IsGalois (tpd P x) (P.curve x).F := by
  haveI : IsGalois ↥(fieldOfModuli (P.curve x).F (P.curve x).E) (P.curve x).F :=
    ((P.arith x).galois_deg_prime 7 (by norm_num) le_rfl).1
  exact IsGalois.tower_top_of_isGalois ↥(fieldOfModuli (P.curve x).F (P.curve x).E) (tpd P x)
    (P.curve x).F

open scoped Classical in
/-- **`F/F_tpd` is unramified at the places of residue characteristic `∉ {2, 3, 5}` over a place
of `F_tpd` at which `λ` and `λ − 1` are units.** -/
theorem relRamIdx_placeUnder_eq_one (hdiv : DivPolyLegendreHyp) {w : FinitePlace (P.curve x).F}
    {𝔭 : FinitePlace (tpd P x)} (hw𝔭 : FinitePlace.LiesOver w 𝔭) (h2 : residueChar w ≠ 2)
    (h3 : residueChar w ≠ 3) (h5 : residueChar w ≠ 5) (h𝔭 : 𝔭 ∉ badT P x) :
    relRamIdx w 𝔭 = 1 := by
  haveI := isGalois_tpd_curve' (P := P) (x := x)
  have h𝔭' : 𝔭 (genT P x) = 1 ∧ 𝔭 (genT P x - 1) = 1 := by
    rw [mem_badT] at h𝔭
    obtain ⟨hb1, hb2⟩ := not_or.mp h𝔭
    exact ⟨not_not.mp hb1, not_not.mp hb2⟩
  have hl : w.maximalIdeal.valuation _ (genC' P x) = 1 :=
    (valuation_genC_eq_one_iff P x hw𝔭).mpr ((FinitePlace.apply_eq_one_iff _ _).mp h𝔭'.1)
  have hl1 : w.maximalIdeal.valuation _ (genC' P x - 1) = 1 :=
    (valuation_genC_sub_one_eq_one_iff P x hw𝔭).mpr ((FinitePlace.apply_eq_one_iff _ _).mp h𝔭'.2)
  exact relRamIdx_eq_one_of_inertia_trivial hw𝔭 fun σ hσ =>
    algEquiv_eq_one_of_fixed (adjoin_tpdGens P x) σ (tpdGens_fixed hdiv h2 h3 h5 hl hl1 σ hσ)

variable {ℓ : ℕ} (hℓ : ℓ.Prime) (h7 : 7 ≤ ℓ)
  (hsl : ∀ A : Matrix.SpecialLinearGroup (Fin 2) (ZMod ℓ), A.toGL ∈ (P.modRep x ℓ hℓ).rep.range)
  (hP2 : ∀ w (hw : w ∈ (P.curve x).badAll), ¬ ℓ ∣ (P.tate x).qOrder w hw)

variable (P x) in
open scoped Classical in
/-- The admissible-prime datum of the curve of `x` and the prime `ℓ`. -/
noncomputable abbrev primeDataOf : AdmissiblePrimeData (P.curve x).F (P.curve x).E (P.curve x).Fbar
    ((P.curve x).VBadOf ℓ) :=
  (P.curve x).primeData (P.arith x) (P.tate x) hℓ h7 (P.modRep x ℓ hℓ) hsl hP2

open scoped Classical in
/-- **`K/F` is unramified at the places of residue characteristic `∉ {2, ℓ}` over a place of `F`
at which `λ` and `λ − 1` are units** (Néron–Ogg–Shafarevich). -/
theorem relRamIdx_torsionField_eq_one (hdiv : DivPolyLegendreHyp)
    [NumberField ↥(primeDataOf P x hℓ h7 hsl hP2).torsionField]
    (v : FinitePlace ↥(primeDataOf P x hℓ h7 hsl hP2).torsionField)
    (h2 : residueChar v ≠ 2) (hpℓ : residueChar v ≠ ℓ)
    (hl : (placeUnder (k := (P.curve x).F) v).maximalIdeal.valuation _ (genC' P x) = 1)
    (hl1 : (placeUnder (k := (P.curve x).F) v).maximalIdeal.valuation _ (genC' P x - 1) = 1) :
    relRamIdx v (placeUnder (k := (P.curve x).F) v) = 1 := by
  set Pr := primeDataOf P x hℓ h7 hsl hP2
  set K := ↥Pr.torsionField
  set w := placeUnder (k := (P.curve x).F) v
  have hvw : FinitePlace.LiesOver v w := liesOver_placeUnder v
  have h2w : residueChar w ≠ 2 := by rwa [← residueChar_eq_of_liesOver hvw]
  have h2' := valuation_two_eq_one w h2w
  obtain ⟨ha₂, ha₄, ha₆, hΔ⟩ := legendre_genT_good P x w h2' (by rw [algebraMap_genT]; exact hl)
    (by rw [map_sub, map_one, algebraMap_genT]; exact hl1)
  have hE : (P.curve x).E = (legendre (genT P x)).baseChange (P.curve x).F := by
    rw [legendre_baseChange, algebraMap_genT]; rfl
  refine relRamIdx_eq_one_of_torsion hvw (P.curve x).E rfl rfl ?_ ?_ ?_ ?_ h2 ?_ (hℓ.odd_of_ne_two
    (by omega)) ((valuation_natCast_eq_one_iff v hℓ).2 hpℓ) ?_
  · rw [valuation_algebraMap_le_one_iff hvw, hE]; exact ha₂
  · rw [valuation_algebraMap_le_one_iff hvw, hE]; exact ha₄
  · rw [valuation_algebraMap_le_one_iff hvw, hE]; exact ha₆
  · rw [valuation_algebraMap_eq_one_iff hvw, hE]; exact hΔ
  · change ReductionKernel.DivPolyHyp ((legendre (genC' P x)).baseChange K)
    rw [legendre_baseChange]
    exact hdiv _ _
  · intro σ hσ
    exact Pr.eq_one_of_forall_torsion σ fun Q hQ => hσ Q hQ

open scoped Classical in
/-- **Néron–Ogg–Shafarevich for the tower of the tripod** (the field `relRamIdx_eq_one` of
`Iut.TowerLocalFacts`): `K/F_tpd` is unramified at the places of residue characteristic
`∉ {2, 3, 5, ℓ}` whose place of `F_tpd` is not bad. -/
theorem relRamIdx_eq_one_of_not_bad (hdiv : DivPolyLegendreHyp)
    [NumberField ↥(primeDataOf P x hℓ h7 hsl hP2).torsionField]
    (v : FinitePlace ↥(primeDataOf P x hℓ h7 hsl hP2).torsionField)
    (hp : residueChar v ∉ ({2, 3, 5, ℓ} : Finset ℕ))
    (hbad : ¬ IsBadTpdOf (P.curve x).F (P.curve x).E ((P.curve x).VBadOf ℓ)
      (placeTpd (P.curve x).F (P.curve x).E (primeDataOf P x hℓ h7 hsl hP2).torsionField v)) :
    relRamIdx v (placeTpd (P.curve x).F (P.curve x).E
      (primeDataOf P x hℓ h7 hsl hP2).torsionField v) = 1 := by
  simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at hp
  obtain ⟨h2, h3, h5, hℓ'⟩ := hp
  set u := placeTpd (P.curve x).F (P.curve x).E (primeDataOf P x hℓ h7 hsl hP2).torsionField v
  set w := placeUnder (k := (P.curve x).F) v
  have hvu : FinitePlace.LiesOver v u := liesOver_placeTpd v
  have hvw : FinitePlace.LiesOver v w := liesOver_placeUnder v
  have hwu : FinitePlace.LiesOver w u := liesOver_placeUnder_of_liesOver hvu
  have hpw : residueChar w = residueChar v := (residueChar_eq_of_liesOver hvw).symm
  have hpu : residueChar u = residueChar v := residueChar_placeTpd v
  have hu : u ∉ badT P x := fun h =>
    hbad (isBadTpdOf_of_mem_badT P x h (by rw [hpu]; exact h2) (by rw [hpu]; exact hℓ'))
  have hu' : u (genT P x) = 1 ∧ u (genT P x - 1) = 1 := by
    rw [mem_badT] at hu
    obtain ⟨hb1, hb2⟩ := not_or.mp hu
    exact ⟨not_not.mp hb1, not_not.mp hb2⟩
  have hl : w.maximalIdeal.valuation _ (genC' P x) = 1 :=
    (valuation_genC_eq_one_iff P x hwu).mpr ((FinitePlace.apply_eq_one_iff _ _).mp hu'.1)
  have hl1 : w.maximalIdeal.valuation _ (genC' P x - 1) = 1 :=
    (valuation_genC_sub_one_eq_one_iff P x hwu).mpr ((FinitePlace.apply_eq_one_iff _ _).mp hu'.2)
  rw [relRamIdx_eq_mul_placeUnder (k := (P.curve x).F) hvu,
    relRamIdx_placeUnder_eq_one hdiv hwu (by rw [hpw]; exact h2) (by rw [hpw]; exact h3)
      (by rw [hpw]; exact h5) hu,
    relRamIdx_torsionField_eq_one hℓ h7 hsl hP2 hdiv v h2 hℓ' hl hl1]

end Iut.Tripod