On Zagier-Hoffman's conjectures in positive characteristic

Problem statement

Notes: Throughout the definitions and statements, we reindex the `i`'s so that they run from `0` to `r - 1` rather than from `1` to `r`.

Source: T. N. Dac, `On Zagier-Hoffman's conjectures in positive characteristic`, Annals of Math, 194 (1) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2021-194-1-ZagierHoffmanPositiveChar.lean

Informal solution: Unavailable.

/--
Statement of Theorem A (Brown's theorem in positive characteristic):

Let `w ∈ ℕ`, where `ℕ := {1,2,...}`. Then every MZV of weight `w` can be written as a `K`-linear
combination of MZV's in the set `𝒯_w`. In particular, `dim 𝒵_w ≤ d(w)`.
Note that `K` in the paper is `RatFunc F`.
-/
theorem declaration uses `sorry`theorem_A (w : ℕ+) :
    𝒵 F w = Submodule.span (RatFunc F) (𝒯 F w) ∧
    Module.rank (RatFunc F) (𝒵 F w) ≤ d F w := byF:Type u_1inst✝²:Field Finst✝¹:Finite Finst✝:DecidableEq F⟮X⟯w:ℕ+⊢ 𝒵 F ↑w = Submodule.span F⟮X⟯ (𝒯 F ↑w) ∧ Module.rank F⟮X⟯ ↥(𝒵 F ↑w) ≤ ↑(d F ↑w)
  sorryAll goals completed! 🐙

/--
Statement of Theorem B:

Let `w ∈ ℕ`, where `ℕ := {1,2,...}`. MZVs of weight `w` in `𝒯0 w` are all linearly independent over
`K`. In particular, `dim 𝒵 w ≥ |𝒯0 w|`. Note that `K` in the paper is `RatFunc F`.
-/
theorem declaration uses `sorry`theorem_B (w : ℕ+) :
    LinearIndependent (RatFunc F) (Subtype.val : 𝒯0 F w → CompletionAtInfty F) ∧
    Module.rank (RatFunc F) (𝒵 F w) ≥ Set.ncard (𝒯0 F w) := byF:Type u_1inst✝²:Field Finst✝¹:Finite Finst✝:DecidableEq F⟮X⟯w:ℕ+⊢ LinearIndependent F⟮X⟯ Subtype.val ∧ Module.rank F⟮X⟯ ↥(𝒵 F ↑w) ≥ ↑(𝒯0 F ↑w).ncard
  sorryAll goals completed! 🐙

/--
Statement of Theorem D:

Let `w ∈ ℕ+` with `w ≤ 2q − 2`. Then `𝒯 w` is a `K`-basis for `𝒵 w`. In particular,
`dim_K (𝒵 w) = d(w)`. Note that `K` in the paper is `RatFunc F`.

Note: Theorem A establishes that `𝒯 w` spans `𝒵 w`. So to prove `𝒯 w` is a `K`-basis for `𝒵 w`, we
only need to show that `𝒯 w` are linearly independent in `𝒵 w`.
-/
theorem declaration uses `sorry`theorem_D (w : ℕ+) (hw : w ≤ 2 * Nat.card F - 2) :
    LinearIndependent (RatFunc F) (Subtype.val : 𝒯 F w → CompletionAtInfty F) ∧
    Module.rank (RatFunc F) (𝒵 F w) = d F w := byF:Type u_1inst✝²:Field Finst✝¹:Finite Finst✝:DecidableEq F⟮X⟯w:ℕ+hw:↑w ≤ 2 * Nat.card F - 2⊢ LinearIndependent F⟮X⟯ Subtype.val ∧ Module.rank F⟮X⟯ ↥(𝒵 F ↑w) = ↑(d F ↑w)
  sorryAll goals completed! 🐙