Place_sum_ramificationIndex_mul_inertiaDeg_bifiber_defect.lean

theorem card_eq_mul_of_card_fiber {α β : Type*} [Finite α] [Finite β] (f : α → β) (c : ℕ)
    (hc : ∀ b, Nat.card {a // f a = b} = c) : Nat.card α = Nat.card β * c

theorem card_eq_sum_card_fiber {α β : Type*} [Finite α] [Fintype β] (f : α → β) :
    Nat.card α = ∑ b : β, Nat.card {a // f a = b}

theorem card_preimage_eq_mul_of_card_fiber {α β : Type*} [Finite α] [Finite β] (f : α → β)
  (c : ℕ)
    (hc : ∀ b, Nat.card {a // f a = b} = c) (t : Set β) :
    Nat.card {a // f a ∈ t} = Nat.card t * c

theorem card_fiber_smul_eq (x : X) (g₀ : G) :
    Nat.card {g : G // g • x = g₀ • x} = Nat.card (stabilizer G x)

theorem card_smul_mem_eq [Finite G] (H : Subgroup G) (x : X) (B : Set X) :
    Nat.card {h : H // (h : G) • x ∈ B} = (orbit H x ∩ B).ncard * Nat.card (stabilizer H x)

theorem card_pair_set [Finite G] (H₁ H₂ : Subgroup G) (x₁ x₂ : X) :
    Nat.card {p : H₁ × H₂ // (p.1 : G) • x₁ = (p.2 : G) • x₂} =
      (orbit H₁ x₁ ∩ orbit H₂ x₂).ncard * Nat.card (stabilizer H₂ x₂)
        * Nat.card (stabilizer H₁ x₁)

theorem card_fiber_psi_eq_of_base (H₁ H₂ : Subgroup G) {g : G} (a₁ : H₁) (a₂ : H₂)
    (hbase : (a₂ : G)⁻¹ * a₁ = g) :
    Nat.card {p : H₁ × H₂ // (p.2 : G)⁻¹ * p.1 = g} = Nat.card (H₁ ⊓ H₂ : Subgroup G)

theorem card_fiber_psi_eq_zero (H₁ H₂ : Subgroup G) {g : G}
    (h : ¬ ∃ h₂ ∈ H₂, ∃ h₁ ∈ H₁, g = (h₂ : G) * h₁) :
    Nat.card {p : H₁ × H₂ // (p.2 : G)⁻¹ * p.1 = g} = 0

theorem card_fiber_psi'_eq_of_base (H₁ H₂ : Subgroup G)
    (hconj : ∀ h : G, h ∈ H₁ ↔ s⁻¹ * h * s ∈ H₂) {g : G} (a₁ : H₁) (a₂ : H₂)
    (hbase : (a₂ : G)⁻¹ * s⁻¹ * a₁ = g) :
    Nat.card {p : H₁ × H₂ // (p.2 : G)⁻¹ * s⁻¹ * p.1 = g} = Nat.card H₂

theorem card_fiber_psi'_eq_zero (H₁ H₂ : Subgroup G) {g : G}
    (h : ¬ ∃ h₂ ∈ H₂, ∃ h₁ ∈ H₁, g = (h₂ : G) * s⁻¹ * h₁) :
    Nat.card {p : H₁ × H₂ // (p.2 : G)⁻¹ * s⁻¹ * p.1 = g} = 0

theorem card_subtype_mul_eq_sum {α : Type*} [Fintype α] (Q : α → Prop) (c : ℕ) :
    Nat.card {a : α // Q a} * c = ∑ a : α, if Q a then c else 0 := by
  rw [Nat.card_eq_fintype_card, Fintype.card_subtype, ← Finset.sum_filter, Finset.sum_const,
    smul_eq_mul]

theorem card_subtype_eq_sum' {α : Type*} [Fintype α] (Q : α → Prop) :
    Nat.card {a : α // Q a} = ∑ a : α, if Q a then 1 else 0 := by
  simpa using card_subtype_mul_eq_sum Q 1

theorem card_pairA_eq [Finite G] (H₁ H₂ : Subgroup G) (x₁ x₂ : X) :
    Nat.card {p : H₁ × H₂ // (p.1 : G) • x₁ = (p.2 : G) • x₂}
      = Nat.card {g : G // (g • x₁ = x₂) ∧ ∃ h₂ ∈ H₂, ∃ h₁ ∈ H₁, g = h₂ * h₁}
          * Nat.card (H₁ ⊓ H₂ : Subgroup G)

theorem card_pairA'_eq [Finite G] (H₁ H₂ : Subgroup G)
    (hconj : ∀ h : G, h ∈ H₁ ↔ s⁻¹ * h * s ∈ H₂) (x₁ x₂ : X) :
    Nat.card {p : H₁ × H₂ // (((p.2 : G)⁻¹ * s⁻¹ * p.1) • x₁ = x₂)}
      = Nat.card {g : G // (g • x₁ = x₂) ∧ ∃ h₂ ∈ H₂, ∃ h₁ ∈ H₁, g = h₂ * s⁻¹ * h₁}
          * Nat.card H₂

theorem card_pairA'_transmute (H₁ H₂ : Subgroup G)
    (hconj : ∀ h : G, h ∈ H₁ ↔ s⁻¹ * h * s ∈ H₂) (x₁ x₂ : X) :
    Nat.card {p : H₁ × H₂ // (((p.2 : G)⁻¹ * s⁻¹ * p.1) • x₁ = x₂)}
      = Nat.card {q : H₂ × H₂ // (q.1 : G) • (s⁻¹ • x₁) = (q.2 : G) • x₂}

theorem card_t_split [Finite G]
    (P₁ P₂ : G → Prop) (hcover : ∀ g : G, P₁ g ∨ P₂ g) (hdisj : ∀ g : G, ¬(P₁ g ∧ P₂ g))
    (x₁ x₂ : X) :
    Nat.card {g : G // (g • x₁ = x₂) ∧ P₁ g} + Nat.card {g : G // (g • x₁ = x₂) ∧ P₂ g}
      = Nat.card {g : G // g • x₁ = x₂}

theorem card_t_eq [IsPretransitive G X] (x₁ x₂ : X) :
    Nat.card {g : G // g • x₁ = x₂} = Nat.card (stabilizer G x₁)

theorem ncard_orbit_inter_orbit_defect [Finite G] [IsPretransitive G X]
    (H₁ H₂ : Subgroup G) (s : G)
    (hconj : ∀ h : G, h ∈ H₁ ↔ s⁻¹ * h * s ∈ H₂)
    (hcover : ∀ g : G,
      (∃ h₂ ∈ H₂, ∃ h₁ ∈ H₁, g = h₂ * h₁) ∨ (∃ h₂ ∈ H₂, ∃ h₁ ∈ H₁, g = h₂ * s⁻¹ * h₁))
    (hdisj : ∀ g : G,
      ¬((∃ h₂ ∈ H₂, ∃ h₁ ∈ H₁, g = h₂ * h₁) ∧ (∃ h₂ ∈ H₂, ∃ h₁ ∈ H₁, g = h₂ * s⁻¹ * h₁)))
    (x₁ x₂ : X) :
    (H₁ ⊓ H₂ : Subgroup G).index * ((orbit H₁ x₁ ∩ orbit H₂ x₂).ncard * Nat.card X)
      + (if x₂ ∈ orbit H₂ (s⁻¹ • x₁) then H₁.index * ((orbit H₁ x₁).ncard * Nat.card X) else 0)
      = H₁.index * H₂.index * ((orbit H₁ x₁).ncard * (orbit H₂ x₂).ncard) := by
  classical
  have : Finite X := Finite.of_surjective (fun g : G => g • x₁) (surjective_smul G x₁)
  have hA₂ := card_pair_set H₁ H₂ x₁ x₂
  have hA₁ := card_pairA_eq H₁ H₂ x₁ x₂
  have hA'' := (card_pairA'_transmute s H₁ H₂ hconj x₁ x₂).symm.trans
    (card_pairA'_eq s H₁ H₂ hconj x₁ x₂)
  have hA''₂ := card_pair_set H₂ H₂ (s⁻¹ • x₁) x₂
  have hsplit : Nat.card {g : G // (g • x₁ = x₂) ∧ ∃ h₂ ∈ H₂, ∃ h₁ ∈ H₁, g = h₂ * h₁}
      + Nat.card {g : G // (g • x₁ = x₂) ∧ ∃ h₂ ∈ H₂, ∃ h₁ ∈ H₁, g = h₂ * s⁻¹ * h₁}
      = Nat.card {g : G // g • x₁ = x₂} :=
    card_t_split (X := X) _ _ hcover hdisj x₁ x₂
  have hT := card_t_eq (G := G) x₁ x₂
  set c₁ := Nat.card (stabilizer H₁ x₁) with hc₁
  set c₂ := Nat.card (stabilizer H₂ x₂) with hc₂
  set c₂' := Nat.card (stabilizer H₂ (s⁻¹ • x₁)) with hc₂'
  set d := Nat.card (H₁ ⊓ H₂ : Subgroup G) with hd
  set S := Nat.card (stabilizer G x₁) with hS
  set nO₁ := (orbit H₁ x₁).ncard with hnO₁
  set nO₂ := (orbit H₂ x₂).ncard with hnO₂
  set nI := (orbit H₁ x₁ ∩ orbit H₂ x₂).ncard with hnI
  set nI' := (orbit H₂ (s⁻¹ • x₁) ∩ orbit H₂ x₂).ncard with hnI'
  have hdiam : (nI * c₂ * c₁) * Nat.card H₂ + (nI' * c₂ * c₂') * d = S * d * Nat.card H₂ := by
    rw [← hA₂, ← hA''₂, hA₁, hA'', ← hT, ← hsplit]
    ring
  have hO₁ : nO₁ * c₁ = Nat.card H₁ := by
    rw [hnO₁, hc₁, ← MulAction.index_stabilizer H₁ x₁, mul_comm, Subgroup.card_mul_index]
  have hO₂ : nO₂ * c₂ = Nat.card H₂ := by
    rw [hnO₂, hc₂, ← MulAction.index_stabilizer H₂ x₂, mul_comm, Subgroup.card_mul_index]
  have hX : Nat.card X * S = Nat.card G := by
    rw [hS, ← MulAction.index_stabilizer_of_transitive G x₁, mul_comm, Subgroup.card_mul_index]
  have hL₁ : Nat.card H₁ * H₁.index = Nat.card G := Subgroup.card_mul_index H₁
  have hL₂ : Nat.card H₂ * H₂.index = Nat.card G := Subgroup.card_mul_index H₂
  have hLd : d * (H₁ ⊓ H₂ : Subgroup G).index = Nat.card G := by
    rw [hd]; exact Subgroup.card_mul_index _
  have hpos : 0 < c₁ * c₂ * d * S :=
    Nat.mul_pos (Nat.mul_pos (Nat.mul_pos Nat.card_pos Nat.card_pos) Nat.card_pos) Nat.card_pos
  by_cases hm : x₂ ∈ orbit H₂ (s⁻¹ • x₁)
  · have horb : orbit H₂ (s⁻¹ • x₁) = orbit H₂ x₂ := by
      obtain ⟨k, hk⟩ := hm
      have hk' : (k : G) • (s⁻¹ • x₁) = x₂ := hk
      ext y
      constructor
      · rintro ⟨h, rfl⟩
        refine ⟨h * k⁻¹, ?_⟩
        change ((h * k⁻¹ : H₂) : G) • x₂ = (h : G) • (s⁻¹ • x₁)
        push_cast
        rw [mul_smul, ← hk', inv_smul_smul]
      · rintro ⟨h, rfl⟩
        refine ⟨h * k, ?_⟩
        change ((h * k : H₂) : G) • (s⁻¹ • x₁) = (h : G) • x₂
        push_cast
        rw [mul_smul, hk']
    have hI' : nI' = nO₂ := by rw [hnI', horb, Set.inter_self, hnO₂]
    have hc₂'₂ : nO₂ * c₂' = Nat.card H₂ := by
      have h1 : (orbit H₂ (s⁻¹ • x₁)).ncard * c₂' = Nat.card H₂ := by
        rw [hc₂', ← MulAction.index_stabilizer H₂ (s⁻¹ • x₁), mul_comm,
          Subgroup.card_mul_index]
      rwa [horb, ← hnO₂] at h1
    have hO₂pos : 0 < nO₂ := by
      rw [hnO₂]
      exact (Set.ncard_pos (Set.toFinite _)).mpr ⟨x₂, MulAction.mem_orbit_self x₂⟩
    have hcc : c₂' = c₂ := Nat.eq_of_mul_eq_mul_left hO₂pos (hc₂'₂.trans hO₂.symm)
    rw [ite_eq_left hm]
    have key : nI * c₂ * c₁ + c₂ * d = S * d := by
      refine Nat.eq_of_mul_eq_mul_right (Nat.card_pos (α := H₂)) ?_
      have e3 : (nI' * c₂ * c₂') * d = (c₂ * d) * Nat.card H₂ := by
        rw [hI', hcc]
        calc nO₂ * c₂ * c₂ * d = (nO₂ * c₂) * (c₂ * d) := by ring
          _ = Nat.card H₂ * (c₂ * d) := by rw [hO₂]
          _ = (c₂ * d) * Nat.card H₂ := by ring
      calc (nI * c₂ * c₁ + c₂ * d) * Nat.card H₂
          = (nI * c₂ * c₁) * Nat.card H₂ + (c₂ * d) * Nat.card H₂ := by ring
        _ = (nI * c₂ * c₁) * Nat.card H₂ + (nI' * c₂ * c₂') * d := by rw [e3]
        _ = S * d * Nat.card H₂ := hdiam
        _ = (S * d) * Nat.card H₂ := by ring
    refine Nat.eq_of_mul_eq_mul_right hpos ?_
    calc ((H₁ ⊓ H₂ : Subgroup G).index * (nI * Nat.card X)
          + H₁.index * (nO₁ * Nat.card X)) * (c₁ * c₂ * d * S)
        = (d * (H₁ ⊓ H₂ : Subgroup G).index) * (Nat.card X * S) * (nI * c₂ * c₁)
            + (nO₁ * c₁ * H₁.index) * (Nat.card X * S) * (c₂ * d) := by ring
      _ = Nat.card G * Nat.card G * (nI * c₂ * c₁)
            + (Nat.card H₁ * H₁.index) * Nat.card G * (c₂ * d) := by rw [hLd, hX, hO₁]
      _ = Nat.card G * Nat.card G * (nI * c₂ * c₁ + c₂ * d) := by rw [hL₁]; ring
      _ = Nat.card G * Nat.card G * (S * d) := by rw [key]
      _ = (Nat.card H₁ * H₁.index) * (Nat.card H₂ * H₂.index) * (S * d) := by rw [hL₁, hL₂]
      _ = (nO₁ * c₁ * H₁.index) * (nO₂ * c₂ * H₂.index) * (S * d) := by rw [hO₁, hO₂]
      _ = (H₁.index * H₂.index * (nO₁ * nO₂)) * (c₁ * c₂ * d * S) := by ring
  · have hI' : nI' = 0 := by
      rw [hnI', Set.ncard_eq_zero (Set.toFinite _)]
      ext y
      simp only [Set.mem_inter_iff, Set.mem_empty_iff_false, iff_false, not_and]
      rintro ⟨h, rfl⟩ ⟨k, hk⟩
      have hk' : (k : G) • x₂ = (h : G) • (s⁻¹ • x₁) := hk
      refine hm ⟨k⁻¹ * h, ?_⟩
      change ((k⁻¹ * h : H₂) : G) • (s⁻¹ • x₁) = x₂
      push_cast
      rw [mul_smul, ← hk', inv_smul_smul]
    rw [ite_eq_right hm, add_zero]
    have key : nI * c₂ * c₁ = S * d := by
      refine Nat.eq_of_mul_eq_mul_right (Nat.card_pos (α := H₂)) ?_
      have h2 := hdiam
      rw [hI'] at h2
      simpa using h2
    refine Nat.eq_of_mul_eq_mul_right hpos ?_
    calc ((H₁ ⊓ H₂ : Subgroup G).index * (nI * Nat.card X)) * (c₁ * c₂ * d * S)
        = (d * (H₁ ⊓ H₂ : Subgroup G).index) * (Nat.card X * S) * (nI * c₂ * c₁) := by ring
      _ = Nat.card G * Nat.card G * (nI * c₂ * c₁) := by rw [hLd, hX]
      _ = Nat.card G * Nat.card G * (S * d) := by rw [key]
      _ = (Nat.card H₁ * H₁.index) * (Nat.card H₂ * H₂.index) * (S * d) := by rw [hL₁, hL₂]
      _ = (nO₁ * c₁ * H₁.index) * (nO₂ * c₂ * H₂.index) * (S * d) := by rw [hO₁, hO₂]
      _ = (H₁.index * H₂.index * (nO₁ * nO₂)) * (c₁ * c₂ * d * S) := by ring

theorem cover_disjoint_of_index [Finite G] (H₁ H₂ : Subgroup G) (s : G)
    (hconj : ∀ h : G, h ∈ H₁ ↔ s⁻¹ * h * s ∈ H₂)
    (hidx : (H₁ ⊓ H₂ : Subgroup G).index + H₁.index = H₁.index * H₂.index)
    (hn : H₂.index ≠ 2) :
    (∀ g : G,
      (∃ h₂ ∈ H₂, ∃ h₁ ∈ H₁, g = h₂ * h₁) ∨ (∃ h₂ ∈ H₂, ∃ h₁ ∈ H₁, g = h₂ * s⁻¹ * h₁))
      ∧ (∀ g : G,
        ¬((∃ h₂ ∈ H₂, ∃ h₁ ∈ H₁, g = h₂ * h₁) ∧ (∃ h₂ ∈ H₂, ∃ h₁ ∈ H₁, g = h₂ * s⁻¹ * h₁)))

theorem inertiaDegAlong_congr {φ φ' : F →ₐ[K] F'} (h : φ = φ') (hφ : φ.toRingHom.IsIntegral)
    (hφ' : φ'.toRingHom.IsIntegral) (w : Place K F') :
    w.inertiaDegAlong φ hφ = w.inertiaDegAlong φ' hφ'

theorem isIntegral_toAlgHom [Algebra.IsIntegral F F'] :
    (IsScalarTower.toAlgHom K F F').toRingHom.IsIntegral

theorem toAlgHom_comp_toAlgHom :
    (IsScalarTower.toAlgHom K E M).comp (IsScalarTower.toAlgHom K F E) =
      IsScalarTower.toAlgHom K F M

theorem restrict_restrict [Algebra.IsIntegral F E] [Algebra.IsIntegral E M]
    [Algebra.IsIntegral F M] (W : Place K M) : (W.restrict E).restrict F = W.restrict F

theorem ramificationIndex_eq_mul_restrict
    [Algebra.IsIntegral F E] [Algebra.IsIntegral E M] (W : Place K M) :
    W.ramificationIndex F = W.ramificationIndex E * (W.restrict E).ramificationIndex F

theorem inertiaDeg_eq_mul_restrict
    [Algebra.IsIntegral F E] [Algebra.IsIntegral E M] [Algebra.IsIntegral F M] (W : Place K M) :
    W.inertiaDeg F = W.inertiaDeg E * (W.restrict E).inertiaDeg F

def resHom (L : Type*) [Field L] [Algebra F L] [Algebra L M] [IsScalarTower F L M] :
    (M ≃ₐ[L] M) →* (M ≃ₐ[F] M) where
  toFun σ := σ.restrictScalars F
  map_one' := AlgEquiv.ext fun _ => rfl
  map_mul' _ _ := AlgEquiv.ext fun _ => rfl

def galAction : MulAction (M ≃ₐ[F] M) (Place K M)

theorem gal_smul_def (g : M ≃ₐ[F] M) (W : Place K M) :
    g • W = SemilinearAut.ofAlgAut (g.restrictScalars K) • W

theorem mem_range_resHom_iff {g : M ≃ₐ[F] M} :
    g ∈ (resHom F M L).range ↔ ∀ x : L, g (algebraMap L M x) = algebraMap L M x

theorem card_range_resHom : Nat.card (resHom F M L).range = Nat.card (M ≃ₐ[L] M)

theorem index_range_resHom [FiniteDimensional F M] [IsGalois F M] [FiniteDimensional L M]
    [IsGalois L M] : (resHom F M L).range.index = Module.finrank F L

theorem orbit_range_resHom_eq [FiniteDimensional L M] [IsGalois L M] (P : Place K M) :
    MulAction.orbit (resHom F M L).range P = ↑((P.restrict L).fiberOver M)

theorem orbit_gal_eq [FiniteDimensional F M] [IsGalois F M] (P : Place K M) :
    MulAction.orbit (M ≃ₐ[F] M) P = ↑((P.restrict F).fiberOver M)

theorem image_val_orbit {G X : Type*} [Group G] [MulAction G X] (H : Subgroup G) (a : X)
    (x : MulAction.orbit G a) :
    Subtype.val '' MulAction.orbit H x = MulAction.orbit H (x : X)

theorem forall_apply_algebraMap_eq_of_adjoin_eq_top
    (hgen : Algebra.adjoin F (Set.range (algebraMap F₁ E) ∪ Set.range (algebraMap F₂ E)) = ⊤)
    (g : M ≃ₐ[F] M) (h₁ : ∀ x : F₁, g (algebraMap F₁ M x) = algebraMap F₁ M x)
    (h₂ : ∀ x : F₂, g (algebraMap F₂ M x) = algebraMap F₂ M x) (z : E) :
    g (algebraMap E M z) = algebraMap E M z

theorem mem_smul_valuationSubring_iff {K F : Type*} [Field K] [Field F] [Algebra K F]
    (g : SemilinearAut K F) (O : ValuationSubring F) (x : F) :
    x ∈ g • O ↔ g⁻¹ • x ∈ O

theorem bifiber_defect {K F F₁ F₂ E : Type*} (M : Type*) [Field K] [Field F] [Field F₁]
    [Field F₂] [Field E] [Field M] [Algebra K F] [Algebra K F₁] [Algebra K F₂] [Algebra K E]
    [Algebra K M] [Algebra F F₁] [Algebra F F₂] [Algebra F E] [Algebra F M] [Algebra F₁ E]
    [Algebra F₂ E] [Algebra F₁ M] [Algebra F₂ M] [Algebra E M] [IsScalarTower K F F₁]
    [IsScalarTower K F F₂] [IsScalarTower K F E] [IsScalarTower K F M] [IsScalarTower K F₁ E]
    [IsScalarTower K F₂ E] [IsScalarTower K F₁ M] [IsScalarTower K F₂ M] [IsScalarTower K E M]
    [IsScalarTower F F₁ M] [IsScalarTower F F₂ M] [IsScalarTower F E M] [IsScalarTower F₁ E M]
    [IsScalarTower F₂ E M] [FiniteDimensional F F₁] [FiniteDimensional F F₂]
    [FiniteDimensional F E] [FiniteDimensional F₁ E] [FiniteDimensional F₂ E]
    [FiniteDimensional F M] [IsGalois F M]
    [Algebra F₂ F₁] [IsScalarTower F F₂ F₁] [IsScalarTower K F₂ F₁] [Algebra.IsIntegral F₂ F₁]
    (hθ : Function.Surjective (algebraMap F₂ F₁))
    (hgen : Algebra.adjoin F (Set.range (algebraMap F₁ E) ∪ Set.range (algebraMap F₂ E)) = ⊤)
    (hLD2 : Module.finrank F E + Module.finrank F F₁ = Module.finrank F F₁ * Module.finrank F F₂)
    (hn : Module.finrank F F₂ ≠ 2)
    (v : Place K F) (w₁ : Place K F₁) (w₂ : Place K F₂) (hw₁ : w₁.restrict F = v)
    (hw₂ : w₂.restrict F = v)
    (T : Finset (Place K E)) (hT : ∀ W, W ∈ T ↔ W.restrict F₁ = w₁ ∧ W.restrict F₂ = w₂) :
    ∑ W ∈ T, W.ramificationIndex F * W.inertiaDeg F
        + (if w₁.restrict F₂ = w₂ then w₁.ramificationIndex F * w₁.inertiaDeg F else 0) =
      (w₁.ramificationIndex F * w₁.inertiaDeg F) * (w₂.ramificationIndex F * w₂.inertiaDeg F) := by
  classical
  have : FiniteDimensional F₁ M := Module.Finite.of_restrictScalars_finite F F₁ M
  have : FiniteDimensional F₂ M := Module.Finite.of_restrictScalars_finite F F₂ M
  have : FiniteDimensional E M := Module.Finite.of_restrictScalars_finite F E M
  have : IsGalois F₁ M := IsGalois.tower_top_of_isGalois F F₁ M
  have : IsGalois F₂ M := IsGalois.tower_top_of_isGalois F F₂ M
  have : IsGalois E M := IsGalois.tower_top_of_isGalois F E M
  have hθinj : Function.Injective (IsScalarTower.toAlgHom F F₂ F₁) := (algebraMap F₂ F₁).injective
  let θe : F₂ ≃ₐ[F] F₁ := AlgEquiv.ofBijective (IsScalarTower.toAlgHom F F₂ F₁) ⟨hθinj, hθ⟩
  let s : M ≃ₐ[F] M := θe.liftNormal M
  have hcomm : ∀ y : F₂, s (algebraMap F₂ M y) = algebraMap F₁ M (algebraMap F₂ F₁ y) :=
    fun y => AlgEquiv.liftNormal_commutes θe M y
  have hs_inv : ∀ z : M, (s⁻¹ : M ≃ₐ[F] M) (s z) = z := fun z => s.symm_apply_apply z
  have hs_inv' : ∀ z : M, s ((s⁻¹ : M ≃ₐ[F] M) z) = z := fun z => s.apply_symm_apply z
  have hconjₛ : ∀ h : M ≃ₐ[F] M,
      h ∈ (resHom F M F₁).range ↔ s⁻¹ * h * s ∈ (resHom F M F₂).range := by
    intro h
    rw [mem_range_resHom_iff, mem_range_resHom_iff]
    constructor
    · intro hfix y
      change (s⁻¹ : M ≃ₐ[F] M) (h (s (algebraMap F₂ M y))) = algebraMap F₂ M y
      rw [hcomm y, hfix (algebraMap F₂ F₁ y), ← hcomm y, hs_inv]
    · intro hfix x
      obtain ⟨y, rfl⟩ := hθ x
      rw [show algebraMap F₁ M (algebraMap F₂ F₁ y) = s (algebraMap F₂ M y) from (hcomm y).symm]
      have h2 : h (s (algebraMap F₂ M y)) = s ((s⁻¹ * h * s) (algebraMap F₂ M y)) := by
        change h (s _) = s ((s⁻¹ : M ≃ₐ[F] M) (h (s _)))
        rw [hs_inv']
      rw [h2, hfix y]
  have hle : (resHom F M F₁).range ⊓ (resHom F M F₂).range ≤ (resHom F M E).range :=
    fun g hg => mem_range_resHom_iff.mpr (forall_apply_algebraMap_eq_of_adjoin_eq_top hgen g
      (mem_range_resHom_iff.mp hg.1) (mem_range_resHom_iff.mp hg.2))
  have hge : (resHom F M E).range ≤ (resHom F M F₁).range ⊓ (resHom F M F₂).range := by
    intro g hg
    rw [Subgroup.mem_inf, mem_range_resHom_iff, mem_range_resHom_iff]
    refine ⟨fun x => ?_, fun x => ?_⟩
    · rw [IsScalarTower.algebraMap_apply F₁ E M x]
      exact mem_range_resHom_iff.mp hg _
    · rw [IsScalarTower.algebraMap_apply F₂ E M x]
      exact mem_range_resHom_iff.mp hg _
  have hHE : (resHom F M F₁).range ⊓ (resHom F M F₂).range = (resHom F M E).range :=
    le_antisymm hle hge
  have hidxₛ : ((resHom F M F₁).range ⊓ (resHom F M F₂).range).index + (resHom F M F₁).range.index
      = (resHom F M F₁).range.index * (resHom F M F₂).range.index := by
    rw [hHE, index_range_resHom, index_range_resHom, index_range_resHom]
    exact hLD2
  have hnₛ : (resHom F M F₂).range.index ≠ 2 := by
    rw [index_range_resHom]; exact hn
  obtain ⟨hcover, hdisj⟩ :=
    cover_disjoint_of_index (resHom F M F₁).range (resHom F M F₂).range s hconjₛ hidxₛ hnₛ
  obtain ⟨P₁, hP₁⟩ := Place.exists_restrict_eq (M := M) w₁
  obtain ⟨P₂, hP₂⟩ := Place.exists_restrict_eq (M := M) w₂
  have hP₁F : P₁.restrict F = v := by rw [← restrict_restrict (E := F₁) P₁, hP₁, hw₁]
  have hP₂F : P₂.restrict F = v := by rw [← restrict_restrict (E := F₂) P₂, hP₂, hw₂]
  have hP₂P₁ : P₂.restrict F = P₁.restrict F := by rw [hP₁F, hP₂F]
  have hA : (v.fiberOver M).card * (P₁.ramificationIndex F * P₁.inertiaDeg F) =
      Module.finrank F M :=
    Place.card_fiberOver_mul_ramificationIndex_mul_inertiaDeg v P₁ hP₁F
  have hA₁ : (w₁.ramificationIndex F * w₁.inertiaDeg F) * Module.finrank F₁ M =
      (w₁.fiberOver M).card * (P₁.ramificationIndex F * P₁.inertiaDeg F) := by
    have hTC := Place.card_fiberOver_mul_ramificationIndex_mul_inertiaDeg w₁ P₁ hP₁
    have he := ramificationIndex_eq_mul_restrict (F := F) (E := F₁) P₁
    have hf := inertiaDeg_eq_mul_restrict (F := F) (E := F₁) P₁
    rw [hP₁] at he hf
    rw [← hTC, he, hf]; ring
  have hA₂ : (w₂.ramificationIndex F * w₂.inertiaDeg F) * Module.finrank F₂ M =
      (w₂.fiberOver M).card * (P₁.ramificationIndex F * P₁.inertiaDeg F) := by
    have hTC := Place.card_fiberOver_mul_ramificationIndex_mul_inertiaDeg w₂ P₂ hP₂
    have he := ramificationIndex_eq_mul_restrict (F := F) (E := F₂) P₂
    have hf := inertiaDeg_eq_mul_restrict (F := F) (E := F₂) P₂
    rw [hP₂] at he hf
    rw [← Place.ramificationIndex_eq_of_restrict_eq P₁ P₂ hP₂P₁,
      ← Place.inertiaDeg_eq_of_restrict_eq P₁ P₂ hP₂P₁, ← hTC, he, hf]; ring
  have hEpt : ∀ W ∈ T, (W.ramificationIndex F * W.inertiaDeg F) * Module.finrank E M =
      (W.fiberOver M).card * (P₁.ramificationIndex F * P₁.inertiaDeg F) := by
    intro W hW
    obtain ⟨hW₁, -⟩ := (hT W).mp hW
    obtain ⟨P, hP⟩ := Place.exists_restrict_eq (M := M) W
    have hTC := Place.card_fiberOver_mul_ramificationIndex_mul_inertiaDeg W P hP
    have he := ramificationIndex_eq_mul_restrict (F := F) (E := E) P
    have hf := inertiaDeg_eq_mul_restrict (F := F) (E := E) P
    rw [hP] at he hf
    have hPF : P.restrict F = P₁.restrict F := by
      rw [← restrict_restrict (E := F₁) P, ← restrict_restrict (F := F₁) (E := E) P, hP, hW₁,
        hw₁, hP₁F]
    rw [← Place.ramificationIndex_eq_of_restrict_eq P₁ P hPF,
      ← Place.inertiaDeg_eq_of_restrict_eq P₁ P hPF, ← hTC, he, hf]; ring
  have hbi : w₁.fiberOver M ∩ w₂.fiberOver M = T.biUnion fun W => W.fiberOver M := by
    ext P
    simp only [Finset.mem_inter, Place.mem_fiberOver, Finset.mem_biUnion, hT]
    constructor
    · rintro ⟨h₁, h₂⟩
      exact ⟨P.restrict E, ⟨(restrict_restrict P).trans h₁, (restrict_restrict P).trans h₂⟩, rfl⟩
    · rintro ⟨W, ⟨h₁, h₂⟩, rfl⟩
      exact ⟨(restrict_restrict P).symm.trans h₁, (restrict_restrict P).symm.trans h₂⟩
  have hdisjf : (↑T : Set (Place K E)).PairwiseDisjoint fun W => W.fiberOver M := by
    intro W _ W' _ hne
    change Disjoint (W.fiberOver M) (W'.fiberOver M)
    exact Finset.disjoint_left.mpr fun P h h' =>
      hne (((Place.mem_fiberOver W).mp h).symm.trans ((Place.mem_fiberOver W').mp h'))
  have hEsum : (∑ W ∈ T, W.ramificationIndex F * W.inertiaDeg F) * Module.finrank E M =
      (w₁.fiberOver M ∩ w₂.fiberOver M).card * (P₁.ramificationIndex F * P₁.inertiaDeg F) := by
    rw [hbi, Finset.card_biUnion hdisjf, Finset.sum_mul, Finset.sum_mul]
    exact Finset.sum_congr rfl hEpt
  have hx₂ : P₂ ∈ MulAction.orbit (M ≃ₐ[F] M) P₁ := by
    rw [orbit_gal_eq, Finset.mem_coe, Place.mem_fiberOver]
    exact hP₂P₁
  obtain ⟨x₁, hx₁⟩ : ∃ x : MulAction.orbit (M ≃ₐ[F] M) P₁, (x : Place K M) = P₁ :=
    ⟨⟨P₁, MulAction.mem_orbit_self P₁⟩, rfl⟩
  obtain ⟨x₂, hx₂'⟩ : ∃ x : MulAction.orbit (M ≃ₐ[F] M) P₁, (x : Place K M) = P₂ :=
    ⟨⟨P₂, hx₂⟩, rfl⟩
  have hO := ncard_orbit_inter_orbit_defect (X := MulAction.orbit (M ≃ₐ[F] M) P₁)
    (resHom F M F₁).range (resHom F M F₂).range s hconjₛ hcover hdisj x₁ x₂
  have cX : Nat.card (MulAction.orbit (M ≃ₐ[F] M) P₁) = (v.fiberOver M).card := by
    rw [Nat.card_coe_set_eq, orbit_gal_eq, hP₁F, Set.ncard_coe_finset]
  have c₁ : (MulAction.orbit (resHom F M F₁).range x₁).ncard = (w₁.fiberOver M).card := by
    rw [← Set.ncard_image_of_injective _ Subtype.val_injective, image_val_orbit, hx₁,
      orbit_range_resHom_eq, hP₁, Set.ncard_coe_finset]
  have c₂ : (MulAction.orbit (resHom F M F₂).range x₂).ncard = (w₂.fiberOver M).card := by
    rw [← Set.ncard_image_of_injective _ Subtype.val_injective, image_val_orbit, hx₂',
      orbit_range_resHom_eq, hP₂, Set.ncard_coe_finset]
  have c₁₂ : (MulAction.orbit (resHom F M F₁).range x₁ ∩
      MulAction.orbit (resHom F M F₂).range x₂).ncard
      = (w₁.fiberOver M ∩ w₂.fiberOver M).card := by
    rw [← Set.ncard_image_of_injective _ Subtype.val_injective,
      Set.image_inter Subtype.val_injective, image_val_orbit, image_val_orbit, hx₁, hx₂',
      orbit_range_resHom_eq, orbit_range_resHom_eq, hP₁, hP₂, ← Finset.coe_inter,
      Set.ncard_coe_finset]
  have hdict : ((s⁻¹ • P₁ : Place K M)).restrict F₂ = (P₁.restrict F₁).restrict F₂ := by
    apply Place.ext
    rw [Place.restrict_toValuationSubring, Place.restrict_toValuationSubring,
      Place.restrict_toValuationSubring]
    have hsmul : (s⁻¹ • P₁ : Place K M).toValuationSubring
        = SemilinearAut.ofAlgAut ((s⁻¹ : M ≃ₐ[F] M).restrictScalars K) • P₁.toValuationSubring :=
      rfl
    rw [hsmul]
    ext y
    rw [ValuationSubring.mem_comap, ValuationSubring.mem_comap, ValuationSubring.mem_comap,
      mem_smul_valuationSubring_iff]
    have hg : (SemilinearAut.ofAlgAut ((s⁻¹ : M ≃ₐ[F] M).restrictScalars K))⁻¹
        • (algebraMap F₂ M y) = s (algebraMap F₂ M y) := by
      rw [← map_inv]
      rfl
    rw [hg, hcomm y]
  have hmatch : (x₂ ∈ MulAction.orbit (resHom F M F₂).range (s⁻¹ • x₁)) ↔
      w₁.restrict F₂ = w₂ := by
    have hval : ((s⁻¹ • x₁ : MulAction.orbit (M ≃ₐ[F] M) P₁) : Place K M) = s⁻¹ • P₁ := by
      have h1 : ((s⁻¹ • x₁ : MulAction.orbit (M ≃ₐ[F] M) P₁) : Place K M)
          = s⁻¹ • (x₁ : Place K M) := rfl
      rw [h1, hx₁]
    constructor
    · rintro ⟨g, hg⟩
      have hg' : (g : M ≃ₐ[F] M) • (s⁻¹ • P₁ : Place K M) = P₂ := by
        have := congrArg Subtype.val hg
        rwa [show ((g • (s⁻¹ • x₁) : MulAction.orbit (M ≃ₐ[F] M) P₁) : Place K M)
          = (g : M ≃ₐ[F] M) • ((s⁻¹ • x₁ : MulAction.orbit (M ≃ₐ[F] M) P₁) : Place K M) from rfl,
          hval, hx₂'] at this
      have hmem : P₂ ∈ MulAction.orbit (resHom F M F₂).range (s⁻¹ • P₁ : Place K M) := ⟨g, hg'⟩
      rw [orbit_range_resHom_eq, Finset.mem_coe, Place.mem_fiberOver, hP₂, hdict, hP₁] at hmem
      exact hmem.symm
    · intro hm
      have hmem : P₂ ∈ MulAction.orbit (resHom F M F₂).range (s⁻¹ • P₁ : Place K M) := by
        rw [orbit_range_resHom_eq, Finset.mem_coe, Place.mem_fiberOver, hP₂, hdict, hP₁]
        exact hm.symm
      obtain ⟨g, hg⟩ := hmem
      refine ⟨g, ?_⟩
      apply Subtype.ext
      rw [show ((g • (s⁻¹ • x₁) : MulAction.orbit (M ≃ₐ[F] M) P₁) : Place K M)
        = (g : M ≃ₐ[F] M) • ((s⁻¹ • x₁ : MulAction.orbit (M ≃ₐ[F] M) P₁) : Place K M) from rfl,
        hval, hx₂']
      exact hg
  rw [hHE, index_range_resHom, index_range_resHom, index_range_resHom, cX, c₁, c₂, c₁₂] at hO
  have hn₁ := Module.finrank_mul_finrank F F₁ M
  have hn₂ := Module.finrank_mul_finrank F F₂ M
  have hnE := Module.finrank_mul_finrank F E M
  have hposA : 0 < (v.fiberOver M).card :=
    Finset.card_pos.mpr ⟨P₁, by rw [Place.mem_fiberOver]; exact hP₁F⟩
  have hpos1 : 0 < Module.finrank F F₁ := Module.finrank_pos
  have hpos2 : 0 < Module.finrank F F₂ := Module.finrank_pos
  have hposE : 0 < Module.finrank F E := Module.finrank_pos
  have hposM₁ : 0 < Module.finrank F₁ M := Module.finrank_pos
  have hposM₂ : 0 < Module.finrank F₂ M := Module.finrank_pos
  have hposME : 0 < Module.finrank E M := Module.finrank_pos
  by_cases hm : w₁.restrict F₂ = w₂
  · rw [ite_eq_left (hmatch.mpr hm)] at hO
    rw [ite_eq_left hm]
    have hsq : Module.finrank F M * Module.finrank F M
        = ((v.fiberOver M).card * (P₁.ramificationIndex F * P₁.inertiaDeg F))
          * (Module.finrank F E * Module.finrank E M) := by
      rw [hA, hnE]
    have key : (w₁.fiberOver M ∩ w₂.fiberOver M).card * (Module.finrank F₁ M * Module.finrank F₂ M)
        + (w₁.fiberOver M).card * (Module.finrank E M * Module.finrank F₂ M)
        = (w₁.fiberOver M).card * (w₂.fiberOver M).card
          * ((P₁.ramificationIndex F * P₁.inertiaDeg F) * Module.finrank E M) := by
      have hposmul : 0 < Module.finrank F F₁ * Module.finrank F F₂ * Module.finrank F E
          * (v.fiberOver M).card :=
        Nat.mul_pos (Nat.mul_pos (Nat.mul_pos hpos1 hpos2) hposE) hposA
      refine Nat.eq_of_mul_eq_mul_right hposmul ?_
      calc ((w₁.fiberOver M ∩ w₂.fiberOver M).card
              * (Module.finrank F₁ M * Module.finrank F₂ M)
            + (w₁.fiberOver M).card * (Module.finrank E M * Module.finrank F₂ M))
            * (Module.finrank F F₁ * Module.finrank F F₂ * Module.finrank F E
              * (v.fiberOver M).card)
          = (Module.finrank F F₁ * Module.finrank F₁ M)
              * (Module.finrank F F₂ * Module.finrank F₂ M) * Module.finrank F E
              * ((w₁.fiberOver M ∩ w₂.fiberOver M).card * (v.fiberOver M).card)
            + (Module.finrank F F₂ * Module.finrank F₂ M)
              * (Module.finrank F E * Module.finrank E M) * Module.finrank F F₁
              * ((w₁.fiberOver M).card * (v.fiberOver M).card) := by ring
        _ = Module.finrank F M * Module.finrank F M * Module.finrank F E
              * ((w₁.fiberOver M ∩ w₂.fiberOver M).card * (v.fiberOver M).card)
            + Module.finrank F M * Module.finrank F M * Module.finrank F F₁
              * ((w₁.fiberOver M).card * (v.fiberOver M).card) := by
              rw [hn₁, hn₂, hnE]
        _ = Module.finrank F M * Module.finrank F M
              * (Module.finrank F E
                  * ((w₁.fiberOver M ∩ w₂.fiberOver M).card * (v.fiberOver M).card)
                + Module.finrank F F₁
                  * ((w₁.fiberOver M).card * (v.fiberOver M).card)) := by ring
        _ = Module.finrank F M * Module.finrank F M
              * (Module.finrank F F₁ * Module.finrank F F₂
                  * ((w₁.fiberOver M).card * (w₂.fiberOver M).card)) := by rw [hO]
        _ = ((w₁.fiberOver M).card * (w₂.fiberOver M).card
              * ((P₁.ramificationIndex F * P₁.inertiaDeg F) * Module.finrank E M))
            * (Module.finrank F F₁ * Module.finrank F F₂ * Module.finrank F E
              * (v.fiberOver M).card) := by rw [hsq]; ring
    have hposμ : 0 < Module.finrank E M * (Module.finrank F₁ M * (Module.finrank F₂ M
        * (v.fiberOver M).card)) :=
      Nat.mul_pos hposME (Nat.mul_pos hposM₁ (Nat.mul_pos hposM₂ hposA))
    refine Nat.eq_of_mul_eq_mul_right hposμ ?_
    calc (∑ W ∈ T, W.ramificationIndex F * W.inertiaDeg F
            + w₁.ramificationIndex F * w₁.inertiaDeg F)
          * (Module.finrank E M * (Module.finrank F₁ M * (Module.finrank F₂ M
            * (v.fiberOver M).card)))
        = ((∑ W ∈ T, W.ramificationIndex F * W.inertiaDeg F) * Module.finrank E M)
            * (Module.finrank F₁ M * Module.finrank F₂ M) * (v.fiberOver M).card
          + ((w₁.ramificationIndex F * w₁.inertiaDeg F) * Module.finrank F₁ M)
            * (Module.finrank E M * Module.finrank F₂ M) * (v.fiberOver M).card := by ring
      _ = ((w₁.fiberOver M ∩ w₂.fiberOver M).card
            * (P₁.ramificationIndex F * P₁.inertiaDeg F))
            * (Module.finrank F₁ M * Module.finrank F₂ M) * (v.fiberOver M).card
          + ((w₁.fiberOver M).card * (P₁.ramificationIndex F * P₁.inertiaDeg F))
            * (Module.finrank E M * Module.finrank F₂ M) * (v.fiberOver M).card := by
            rw [hEsum, hA₁]
      _ = ((w₁.fiberOver M ∩ w₂.fiberOver M).card
              * (Module.finrank F₁ M * Module.finrank F₂ M)
            + (w₁.fiberOver M).card * (Module.finrank E M * Module.finrank F₂ M))
            * ((P₁.ramificationIndex F * P₁.inertiaDeg F) * (v.fiberOver M).card) := by ring
      _ = ((w₁.fiberOver M).card * (w₂.fiberOver M).card
            * ((P₁.ramificationIndex F * P₁.inertiaDeg F) * Module.finrank E M))
            * ((P₁.ramificationIndex F * P₁.inertiaDeg F) * (v.fiberOver M).card) := by
            rw [key]
      _ = ((w₁.fiberOver M).card * (P₁.ramificationIndex F * P₁.inertiaDeg F))
            * ((w₂.fiberOver M).card * (P₁.ramificationIndex F * P₁.inertiaDeg F))
            * (Module.finrank E M * (v.fiberOver M).card) := by ring
      _ = ((w₁.ramificationIndex F * w₁.inertiaDeg F) * Module.finrank F₁ M)
            * ((w₂.ramificationIndex F * w₂.inertiaDeg F) * Module.finrank F₂ M)
            * (Module.finrank E M * (v.fiberOver M).card) := by rw [hA₁, hA₂]
      _ = ((w₁.ramificationIndex F * w₁.inertiaDeg F)
            * (w₂.ramificationIndex F * w₂.inertiaDeg F))
          * (Module.finrank E M * (Module.finrank F₁ M * (Module.finrank F₂ M
            * (v.fiberOver M).card))) := by ring
  · rw [ite_eq_right (fun hc => hm (hmatch.mp hc)), add_zero] at hO
    rw [ite_eq_right hm, add_zero]
    have hposμ : 0 < Module.finrank E M * (Module.finrank F₁ M * (Module.finrank F₂ M
        * (v.fiberOver M).card)) :=
      Nat.mul_pos hposME (Nat.mul_pos hposM₁ (Nat.mul_pos hposM₂ hposA))
    refine Nat.eq_of_mul_eq_mul_right hposμ ?_
    have hsq : Module.finrank F M * Module.finrank F M
        = ((v.fiberOver M).card * (P₁.ramificationIndex F * P₁.inertiaDeg F))
          * (Module.finrank F E * Module.finrank E M) := by
      rw [hA, hnE]
    have key : (w₁.fiberOver M ∩ w₂.fiberOver M).card
        * (Module.finrank F₁ M * Module.finrank F₂ M)
        = (w₁.fiberOver M).card * (w₂.fiberOver M).card
          * ((P₁.ramificationIndex F * P₁.inertiaDeg F) * Module.finrank E M) := by
      have hposmul : 0 < Module.finrank F F₁ * Module.finrank F F₂ * Module.finrank F E
          * (v.fiberOver M).card :=
        Nat.mul_pos (Nat.mul_pos (Nat.mul_pos hpos1 hpos2) hposE) hposA
      refine Nat.eq_of_mul_eq_mul_right hposmul ?_
      calc (w₁.fiberOver M ∩ w₂.fiberOver M).card
              * (Module.finrank F₁ M * Module.finrank F₂ M)
            * (Module.finrank F F₁ * Module.finrank F F₂ * Module.finrank F E
              * (v.fiberOver M).card)
          = (Module.finrank F F₁ * Module.finrank F₁ M)
              * (Module.finrank F F₂ * Module.finrank F₂ M) * Module.finrank F E
              * ((w₁.fiberOver M ∩ w₂.fiberOver M).card * (v.fiberOver M).card) := by ring
        _ = Module.finrank F M * Module.finrank F M
              * (Module.finrank F E
                  * ((w₁.fiberOver M ∩ w₂.fiberOver M).card * (v.fiberOver M).card)) := by
              rw [hn₁, hn₂]; ring
        _ = Module.finrank F M * Module.finrank F M
              * (Module.finrank F F₁ * Module.finrank F F₂
                  * ((w₁.fiberOver M).card * (w₂.fiberOver M).card)) := by rw [hO]
        _ = ((w₁.fiberOver M).card * (w₂.fiberOver M).card
              * ((P₁.ramificationIndex F * P₁.inertiaDeg F) * Module.finrank E M))
            * (Module.finrank F F₁ * Module.finrank F F₂ * Module.finrank F E
              * (v.fiberOver M).card) := by rw [hsq]; ring
    calc (∑ W ∈ T, W.ramificationIndex F * W.inertiaDeg F)
          * (Module.finrank E M * (Module.finrank F₁ M * (Module.finrank F₂ M
            * (v.fiberOver M).card)))
        = ((∑ W ∈ T, W.ramificationIndex F * W.inertiaDeg F) * Module.finrank E M)
            * (Module.finrank F₁ M * Module.finrank F₂ M) * (v.fiberOver M).card := by ring
      _ = ((w₁.fiberOver M ∩ w₂.fiberOver M).card
            * (P₁.ramificationIndex F * P₁.inertiaDeg F))
            * (Module.finrank F₁ M * Module.finrank F₂ M) * (v.fiberOver M).card := by
            rw [hEsum]
      _ = ((w₁.fiberOver M ∩ w₂.fiberOver M).card
              * (Module.finrank F₁ M * Module.finrank F₂ M))
            * ((P₁.ramificationIndex F * P₁.inertiaDeg F) * (v.fiberOver M).card) := by ring
      _ = ((w₁.fiberOver M).card * (w₂.fiberOver M).card
            * ((P₁.ramificationIndex F * P₁.inertiaDeg F) * Module.finrank E M))
            * ((P₁.ramificationIndex F * P₁.inertiaDeg F) * (v.fiberOver M).card) := by
            rw [key]
      _ = ((w₁.fiberOver M).card * (P₁.ramificationIndex F * P₁.inertiaDeg F))
            * ((w₂.fiberOver M).card * (P₁.ramificationIndex F * P₁.inertiaDeg F))
            * (Module.finrank E M * (v.fiberOver M).card) := by ring
      _ = ((w₁.ramificationIndex F * w₁.inertiaDeg F) * Module.finrank F₁ M)
            * ((w₂.ramificationIndex F * w₂.inertiaDeg F) * Module.finrank F₂ M)
            * (Module.finrank E M * (v.fiberOver M).card) := by rw [hA₁, hA₂]
      _ = ((w₁.ramificationIndex F * w₁.inertiaDeg F)
            * (w₂.ramificationIndex F * w₂.inertiaDeg F))
          * (Module.finrank E M * (Module.finrank F₁ M * (Module.finrank F₂ M
            * (v.fiberOver M).card))) := by ring

theorem _root_.AlgebraicCurve.Place.sum_ramificationIndex_mul_inertiaDeg_bifiber_defect {K F F₁ F₂
  E : Type*} (M : Type*) [Field K] [Field F] [Field F₁] [Field F₂] [Field E] [Field M] [Algebra K
  F] [Algebra K F₁] [Algebra K F₂] [Algebra K E] [Algebra K M] [Algebra F F₁] [Algebra F F₂]
  [Algebra F E] [Algebra F M] [Algebra F₁ E] [Algebra F₂ E] [Algebra F₁ M] [Algebra F₂ M] [Algebra
  E M] [IsScalarTower K F F₁] [IsScalarTower K F F₂] [IsScalarTower K F E] [IsScalarTower K F M]
  [IsScalarTower K F₁ E] [IsScalarTower K F₂ E] [IsScalarTower K F₁ M] [IsScalarTower K F₂ M]
  [IsScalarTower K E M] [IsScalarTower F F₁ M] [IsScalarTower F F₂ M] [IsScalarTower F E M]
  [IsScalarTower F₁ E M] [IsScalarTower F₂ E M] [FiniteDimensional F F₁] [FiniteDimensional F F₂]
  [FiniteDimensional F E] [FiniteDimensional F₁ E] [FiniteDimensional F₂ E] [FiniteDimensional F M]
  [IsGalois F M] [Algebra F₂ F₁] [IsScalarTower F F₂ F₁] [IsScalarTower K F₂ F₁]
  [Algebra.IsIntegral F₂ F₁] (hθ : Function.Surjective (algebraMap F₂ F₁)) (hgen : Algebra.adjoin F
  (Set.range (algebraMap F₁ E) ∪ Set.range (algebraMap F₂ E)) = ⊤) (hLD2 : Module.finrank F E +
  Module.finrank F F₁ = Module.finrank F F₁ * Module.finrank F F₂) (hn : Module.finrank F F₂ ≠ 2)
  (v : Place K F) (w₁ : Place K F₁) (w₂ : Place K F₂) (hw₁ : w₁.restrict F = v) (hw₂ : w₂.restrict
  F = v) (T : Finset (Place K E)) (hT : ∀ W, W ∈ T ↔ W.restrict F₁ = w₁ ∧ W.restrict F₂ = w₂) : ∑ W
  ∈ T, W.ramificationIndex F * W.inertiaDeg F + (if w₁.restrict F₂ = w₂ then w₁.ramificationIndex F
  * w₁.inertiaDeg F else 0) = (w₁.ramificationIndex F * w₁.inertiaDeg F) * (w₂.ramificationIndex F
  * w₂.inertiaDeg F) :=
  WK2ADev2.bifiber_defect M hθ hgen hLD2 hn v w₁ w₂ hw₁ hw₂ T hT