import Mathlib

set_option autoImplicit false
set_option synthInstance.maxHeartbeats 200000
set_option maxHeartbeats 1600000

section
section

open MvPowerSeries IsLocalRing

noncomputable section

namespace FormalGroup

variable {R : Type*} [CommRing R]
variable {A : Type*} [CommRing A] [UniformSpace A] [Algebra R A]

noncomputable def eval (F : FormalGroup R) (x y : A) : A :=
  letI : UniformSpace R := ⊥
  MvPowerSeries.eval₂ (algebraMap R A) ![x, y] F.toPowerSeries

theorem eval_eq_eval₂ {R : Type*} [CommRing R] [u : UniformSpace R] [DiscreteUniformity R]
    {A : Type*} [CommRing A] [UniformSpace A] [Algebra R A] (F : FormalGroup R) (x y : A) :
    F.eval x y = MvPowerSeries.eval₂ (algebraMap R A) ![x, y] F.toPowerSeries := by
  obtain rfl : u = ⊥ := DiscreteUniformity.eq_bot
  rfl

variable [IsUniformAddGroup A] [CompleteSpace A] [T2Space A]
  [IsTopologicalRing A] [IsLinearTopology A A]

end FormalGroup

end

end

end

section
section

open MvPowerSeries IsLocalRing

noncomputable section

namespace FormalGroup

variable {R : Type*} [CommRing R]
variable {A : Type*} [CommRing A] [UniformSpace A] [Algebra R A]

noncomputable def nthSeries (F : FormalGroup R) : ℕ → PowerSeries R
  | 0 => 0
  | n + 1 => MvPowerSeries.subst ![F.nthSeries n, PowerSeries.X] F.toPowerSeries

@[simp]
theorem nthSeries_zero (F : FormalGroup R) : F.nthSeries 0 = 0 := rfl

theorem nthSeries_succ (F : FormalGroup R) (n : ℕ) :
    F.nthSeries (n + 1)
      = MvPowerSeries.subst ![F.nthSeries n, PowerSeries.X] F.toPowerSeries := rfl

theorem constantCoeff_nthSeries (F : FormalGroup R) (n : ℕ) :
    PowerSeries.constantCoeff (F.nthSeries n) = 0 := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [nthSeries_succ]
    have hcc : ∀ s : Fin 2, MvPowerSeries.constantCoeff
        ((![F.nthSeries n, PowerSeries.X] : Fin 2 → PowerSeries R) s) = 0 := by
      intro s
      fin_cases s
      · exact ih
      · exact MvPowerSeries.constantCoeff_X (R := R) ()
    exact MvPowerSeries.constantCoeff_subst_eq_zero
      (MvPowerSeries.hasSubst_of_constantCoeff_zero hcc) hcc F.zero_constantCoeff

theorem hasSubst_nthSeries (F : FormalGroup R) (n : ℕ) :
    MvPowerSeries.HasSubst (![F.nthSeries n, PowerSeries.X] : Fin 2 → PowerSeries R) := by
  refine MvPowerSeries.hasSubst_of_constantCoeff_zero fun s => ?_
  fin_cases s
  · exact F.constantCoeff_nthSeries n
  · exact MvPowerSeries.constantCoeff_X (R := R) ()

noncomputable def evalSeries (f : PowerSeries R) (x : A) : A :=
  letI : UniformSpace R := ⊥
  PowerSeries.eval₂ (algebraMap R A) x f

theorem evalSeries_eq_eval₂ {R : Type*} [CommRing R] [u : UniformSpace R]
    [DiscreteUniformity R] {A : Type*} [CommRing A] [UniformSpace A] [Algebra R A]
    (f : PowerSeries R) (x : A) :
    evalSeries f x = PowerSeries.eval₂ (algebraMap R A) x f := by
  obtain rfl : u = ⊥ := DiscreteUniformity.eq_bot
  rfl

noncomputable def evalNSMul (F : FormalGroup R) : ℕ → A → A
  | 0, _ => 0
  | n + 1, x => F.eval (F.evalNSMul n x) x

@[simp]
theorem evalNSMul_zero (F : FormalGroup R) (x : A) : F.evalNSMul 0 x = 0 := rfl

theorem evalNSMul_succ (F : FormalGroup R) (n : ℕ) (x : A) :
    F.evalNSMul (n + 1) x = F.eval (F.evalNSMul n x) x := rfl

end FormalGroup

end

end

end

section
section

open scoped Classical

namespace MvPowerSeries
variable {σ : Type*} {R : Type*} [CommRing R]

noncomputable def pderivLin (i : σ) : MvPowerSeries σ R →ₗ[R] MvPowerSeries σ R where
  toFun F := (fun d => (d i + 1 : ℕ) • MvPowerSeries.coeff (d + Finsupp.single i 1) F :
              MvPowerSeries σ R)
  map_add' F G := by
    funext d
    show (d i + 1 : ℕ) • MvPowerSeries.coeff (d + Finsupp.single i 1) (F + G)
       = (d i + 1 : ℕ) • MvPowerSeries.coeff (d + Finsupp.single i 1) F
       + (d i + 1 : ℕ) • MvPowerSeries.coeff (d + Finsupp.single i 1) G
    rw [map_add, smul_add]
  map_smul' r F := by
    funext d
    show (d i + 1 : ℕ) • MvPowerSeries.coeff (d + Finsupp.single i 1) (r • F)
       = r • ((d i + 1 : ℕ) • MvPowerSeries.coeff (d + Finsupp.single i 1) F)
    rw [map_smul, smul_comm]

@[simp] theorem kw_coeff_pderiv (i : σ) (d : σ →₀ ℕ) (F : MvPowerSeries σ R) :
    MvPowerSeries.coeff d (pderivLin i F)
      = (d i + 1 : ℕ) • MvPowerSeries.coeff (d + Finsupp.single i 1) F := rfl

end MvPowerSeries

end

end

section
section

noncomputable section

open PowerSeries MvPowerSeries

namespace FormalGroup

variable {R : Type*} [CommRing R] (F : FormalGroup R)

noncomputable def partialX : MvPowerSeries (Fin 2) R :=
  MvPowerSeries.pderivLin (0 : Fin 2) F.toPowerSeries

theorem constantCoeff_partialX : MvPowerSeries.constantCoeff F.partialX = 1 := by
  unfold partialX
  rw [← MvPowerSeries.coeff_zero_eq_constantCoeff, MvPowerSeries.kw_coeff_pderiv]
  simpa using F.lin_coeff_X

noncomputable def invDiffDenom : PowerSeries R :=
  MvPowerSeries.subst ![(0 : PowerSeries R), PowerSeries.X] F.partialX

theorem hasSubst_invDiff :
    MvPowerSeries.HasSubst (![(0 : PowerSeries R), PowerSeries.X] : Fin 2 → PowerSeries R) :=
  MvPowerSeries.hasSubst_of_constantCoeff_zero (by
    intro s; fin_cases s
    · simp
    · exact MvPowerSeries.constantCoeff_X _)

theorem constantCoeff_invDiffDenom : PowerSeries.constantCoeff F.invDiffDenom = 1 := by
  unfold invDiffDenom
  rw [show (PowerSeries.constantCoeff : PowerSeries R →+* R)
      = MvPowerSeries.constantCoeff (σ := Unit) from rfl,
    MvPowerSeries.constantCoeff_subst hasSubst_invDiff]
  rw [finsum_eq_single _ (0 : Fin 2 →₀ ℕ) (fun d hd => ?_)]
  · simp [F.constantCoeff_partialX, MvPowerSeries.coeff_zero_eq_constantCoeff]
  · rcases Finsupp.ne_iff.mp hd with ⟨i, hi⟩
    rw [Finsupp.prod, map_prod]
    refine smul_eq_zero_of_right _ (Finset.prod_eq_zero (i := i) (Finsupp.mem_support_iff.mpr hi) ?_)
    have hcc : MvPowerSeries.constantCoeff
        ((![(0 : PowerSeries R), PowerSeries.X] : Fin 2 → PowerSeries R) i) = 0 := by
      fin_cases i
      · simp
      · exact MvPowerSeries.constantCoeff_X _
    rw [map_pow, hcc]
    exact zero_pow (by simpa using hi)

noncomputable def invDiff : PowerSeries R :=
  PowerSeries.invOfUnit F.invDiffDenom (1 : Rˣ)

theorem invDiffDenom_mul_invDiff : F.invDiffDenom * F.invDiff = 1 := by
  unfold invDiff
  exact PowerSeries.mul_invOfUnit F.invDiffDenom 1 (by simp [F.constantCoeff_invDiffDenom])

theorem constantCoeff_invDiff : PowerSeries.constantCoeff F.invDiff = 1 := by
  unfold invDiff
  simp [PowerSeries.constantCoeff_invOfUnit]

end FormalGroup

end

end

end

section
section

set_option maxHeartbeats 1200000

noncomputable section
open PowerSeries MvPowerSeries

namespace FormalGroup

variable {R : Type*} [CommRing R] (F : FormalGroup R)

noncomputable def qFoldSeriesB (q : ℕ) : PowerSeries R :=
  PowerSeries.mk fun k => if q ∣ k ∧ q ≤ k then PowerSeries.coeff k (F.nthSeries q) else 0

theorem coeff_qFoldSeriesB (q k : ℕ) :
    PowerSeries.coeff k (F.qFoldSeriesB q)
      = if q ∣ k ∧ q ≤ k then PowerSeries.coeff k (F.nthSeries q) else 0 :=
  PowerSeries.coeff_mk _ _

end FormalGroup

end

end

end