Place_inertiaDeg_pos_of_finiteDimensional.lean

theorem linearIndependent_lift (w : Place K F') {ι : Type*} [Finite ι]
    (x : ι → w.toValuationSubring)
    (hx : LinearIndependent (w.restrict F).ResidueField
      fun i => (residue w.toValuationSubring (x i) : w.ResidueField)) :
    LinearIndependent F fun i => ((x i : w.toValuationSubring) : F') := by
  classical
  let : Fintype ι := Fintype.ofFinite ι
  rw [Fintype.linearIndependent_iff]
  intro g hg
  by_contra hne
  obtain ⟨i₀, hi₀⟩ : ∃ i, g i ≠ 0 := not_forall.mp hne
  set O : ValuationSubring F := (w.restrict F).toValuationSubring
  have hne' : (Finset.univ.filter fun i => g i ≠ 0).Nonempty := ⟨i₀, by simpa using hi₀⟩
  obtain ⟨k, hk, hkmax⟩ := Finset.exists_max_image _ (fun i => O.valuation (g i)) hne'
  have hgk : g k ≠ 0 := by simpa using hk
  have hb : ∀ i, g i / g k ∈ O := by
    intro i
    by_cases hi : g i = 0
    · simp [hi]
    · apply O.mem_of_valuation_le_one
      rw [map_div₀]
      have hk0 : (0 : O.ValueGroup) < O.valuation (g k) := by
        rw [zero_lt_iff]; exact (map_ne_zero _).mpr hgk
      exact (div_le_one₀ hk0).mpr (hkmax i (by simpa using hi))
  let b : ι → O := fun i => ⟨g i / g k, hb i⟩
  have hrel : ∑ i, Place.restrictInclusion F w (b i) * x i = 0 := by
    apply Subtype.ext
    have hcoe : ((∑ i, Place.restrictInclusion F w (b i) * x i : w.toValuationSubring) : F') =
        ∑ i, algebraMap F F' (g i / g k) * (x i : F') := by
      rw [AddSubmonoidClass.coe_finsetSum]
      refine Finset.sum_congr rfl fun i _ => ?_
      rw [MulMemClass.coe_mul, Place.coe_restrictInclusion]
    rw [hcoe]
    have : ∑ i, algebraMap F F' (g i / g k) * (x i : F') =
        algebraMap F F' (g k)⁻¹ * ∑ i, g i • ((x i : w.toValuationSubring) : F') := by
      rw [Finset.mul_sum]
      refine Finset.sum_congr rfl fun i _ => ?_
      rw [Algebra.smul_def, div_eq_inv_mul, map_mul, mul_assoc]
    rw [this, hg, mul_zero]
    rfl
  have hres : ∑ i, (residue O (b i) : (w.restrict F).ResidueField) •
      (residue w.toValuationSubring (x i) : w.ResidueField) = 0 := by
    have h := congrArg (residue w.toValuationSubring) hrel
    rw [map_sum, map_zero] at h
    rw [← h]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [Algebra.smul_def, Place.algebraMap_residueField_eq, Place.restrictResidueMap_residue,
      map_mul]
  have hk1 := (Fintype.linearIndependent_iff.mp hx) _ hres k
  have hbk : b k = 1 := Subtype.ext (div_self hgk)
  rw [hbk, map_one] at hk1
  exact one_ne_zero hk1

theorem finite_residueField (w : Place K F') :
    Module.Finite (w.restrict F).ResidueField w.ResidueField

theorem _root_.AlgebraicCurve.Place.inertiaDeg_pos_of_finiteDimensional {K F F' : Type*} [Field K]
  [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] (w : Place K F') : 0 < w.inertiaDeg F