lean-eval Aristotle (Harmonic) submission for substInv_X_sub_X_sq_eq_catalan

Challenge.lean

import Mathlib

open PowerSeries

theorem substInv_X_sub_X_sq_eq_catalan (n : ℕ) :
    haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := by
      simp [coeff_X, coeff_X_pow]; exact invertibleOne
    coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) =
      (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := by
  sorry

config.json

{
  "challenge_module": "Challenge",
  "solution_module": "Solution",
  "theorem_names": [
    "substInv_X_sub_X_sq_eq_catalan"
  ],
  "permitted_axioms": [
    "propext",
    "Quot.sound",
    "Classical.choice"
  ],
  "enable_nanoda": false
}

Helpers.lean

namespace Submission.Helpers

end Submission.Helpers

lakefile.toml

name = "substInv_X_sub_X_sq_eq_catalan"
testDriver = "workspace_test"
defaultTargets = ["Challenge", "Solution", "Submission"]

[leanOptions]
autoImplicit = false

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "5450b53e5ddc"

[[lean_lib]]
name = "Challenge"

[[lean_lib]]
name = "Solution"

[[lean_lib]]
name = "Submission"

[[lean_exe]]
name = "workspace_test"
root = "WorkspaceTest"

lean-toolchain

leanprover/lean4:v4.30.0-rc2

Solution.lean

import Mathlib
import Submission

open PowerSeries

theorem substInv_X_sub_X_sq_eq_catalan (n : ℕ) :
    haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := by
      simp [coeff_X, coeff_X_pow]; exact invertibleOne
    coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) =
      (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := by
  exact Submission.substInv_X_sub_X_sq_eq_catalan n

Submission.lean

import Mathlib

open PowerSeries

namespace Submission

private noncomputable def C_rat : ℚ⟦X⟧ := PowerSeries.map (Nat.castRingHom ℚ) catalanSeries

private lemma C_rat_eq : C_rat ^ 2 * X + 1 = C_rat := by
  have := congr_arg (PowerSeries.map (Nat.castRingHom ℚ)) catalanSeries_sq_mul_X_add_one
  simp only [map_add, map_mul, map_pow, map_one, map_X] at this
  exact this

private lemma C_rat_coeff (n : ℕ) : coeff n C_rat = (catalan n : ℚ) := by
  simp [C_rat, coeff_map, catalanSeries_coeff]

private lemma hasSubst_X_mul_C_rat : HasSubst (X * C_rat : ℚ⟦X⟧) := by
  simp [HasSubst, ← constantCoeff.eq_def, map_mul, C_rat]

private lemma subst_X_sub_X_sq_eq :
    ((X : ℚ⟦X⟧) - X ^ 2).subst (X * C_rat) = X := by
  rw [subst_sub hasSubst_X_mul_C_rat, subst_X hasSubst_X_mul_C_rat,
      subst_pow hasSubst_X_mul_C_rat, subst_X hasSubst_X_mul_C_rat]
  have key : C_rat - X * C_rat ^ 2 = 1 := by linear_combination -C_rat_eq
  calc X * C_rat - (X * C_rat) ^ 2
      = X * (C_rat - X * C_rat ^ 2) := by ring
    _ = X * 1 := by rw [key]
    _ = X := mul_one X

private noncomputable instance : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := by
  simp [coeff_X, coeff_X_pow]; exact invertibleOne

private lemma substInv_eq : substInv ((X : ℚ⟦X⟧) - X ^ 2) = X * C_rat := by
  have P_const : constantCoeff ((X : ℚ⟦X⟧) - X ^ 2) = 0 := by
    simp [map_sub, map_pow]
  have hP : HasSubst ((X : ℚ⟦X⟧) - X ^ 2) := by
    simp [HasSubst, ← constantCoeff.eq_def, map_sub, map_pow]
  have hg : HasSubst (X * C_rat : ℚ⟦X⟧) := hasSubst_X_mul_C_rat
  have h1 := subst_substInv_left ((X : ℚ⟦X⟧) - X ^ 2) P_const
  have h2 := subst_comp_subst_apply hP hg (substInv ((X : ℚ⟦X⟧) - X ^ 2))
  rw [h1, subst_X hg, subst_X_sub_X_sq_eq, X_subst] at h2
  exact h2.symm

private lemma catalan_eq_choose_div (n : ℕ) :
    (catalan n : ℚ) = (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := by
  have h := succ_mul_catalan_eq_centralBinom n
  rw [Nat.centralBinom] at h
  have hn : (↑n + 1 : ℚ) ≠ 0 := by positivity
  rw [eq_div_iff hn]
  have : (↑(catalan n) : ℚ) * (↑n + 1) = ↑((n + 1) * catalan n) := by push_cast; ring
  rw [this, h]

theorem substInv_X_sub_X_sq_eq_catalan (n : ℕ) :
    haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := by
      simp [coeff_X, coeff_X_pow]; exact invertibleOne
    coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) =
      (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := by
  rw [substInv_eq, coeff_succ_X_mul, C_rat_coeff, catalan_eq_choose_div]

end Submission

WorkspaceTest.lean

import Lean

open Lean

def comparatorExists (comparatorBin : String) : IO Bool := do
  if comparatorBin.contains '/' then
    return (← System.FilePath.pathExists comparatorBin)
  try
    let child ← IO.Process.spawn {
      cmd := "sh"
      args := #["-c", "command -v \"$1\" >/dev/null 2>&1", "sh", comparatorBin]
    }
    let exitCode ← child.wait
    return exitCode == 0
  catch _ =>
    return false

def main : IO UInt32 := do
  let comparatorBin := (← IO.getEnv "COMPARATOR_BIN").getD "comparator"
  if !(← comparatorExists comparatorBin) then
    IO.eprintln s!"Failed to run comparator via `{comparatorBin}`."
    IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
    IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export."
    pure 1
  else
    try
      let child ← IO.Process.spawn {
        cmd := "lake"
        args := #["env", comparatorBin, "config.json"]
      }
      let exitCode ← child.wait
      pure exitCode
    catch err =>
      IO.eprintln s!"Failed to run comparator via `{comparatorBin}`."
      IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
      IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export."
      IO.eprintln s!"Original error: {err}"
      pure 1