-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R : Type u_2
inst : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf :
  ∀ (i : Fin n),
    degrees.{u_2, 0} (R := R) ((f : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R) (MvPolynomial.X i)) ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg :
  Eq (α := MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
    (g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))))
    (↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
hσ' :
  ∀ (x : MvPolynomial (Fin m) R),
    (g : (a : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) → MvPolynomial (Fin m) R)
        ((σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) x) =
      x
hg' :
  Surjective (α := MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) (β := MvPolynomial (Fin m) R)
    (⇑g : (a : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) → MvPolynomial (Fin m) R)
S' : ConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Finset.image
    (fun (x : BasicConstructibleSetData (MvPolynomial (Fin m) R)) ↦
      match (motive :=
        BasicConstructibleSetData (MvPolynomial (Fin m) R) →
          BasicConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)))
        x with
      | { f := fk, n := k, g := gk } =>
        { f := (σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) fk, n := k + n,
          g := fun (s : Fin (k + n)) ↦
            Sum.elim ((⇑σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) ∘ gk)
              (fun (i : Fin n) ↦
                HSub.hSub (α := MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) (β :=
                  MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
                  ((MvPolynomial.C : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
                      (MvPolynomial.X i) :
                    MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
                  ((σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
                      ((f : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R) (MvPolynomial.X i)) :
                    MvPolynomial (Fin m) (MvPolynomial (Fin n) R)))
              ((Equiv.symm finSumFinEquiv : (a : Fin (k + n)) → Fin k ⊕ Fin n) s) })
    S
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Set.range fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) (β := MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
      ((MvPolynomial.C : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
          (MvPolynomial.X i) :
        MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
      ((σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
          ((f : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R) (MvPolynomial.X i)) :
        MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
H : LE.le (α := Ideal (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) (Ideal.span s₀) (RingHom.ker g)
p : MvPolynomial (Fin n) (MvPolynomial (Fin m) R)
C :
  ∀ (q : MvPolynomial (Fin m) R),
    ∃ (q₁ : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) (q₂ : MvPolynomial (Fin m) R),
      Membership.mem (γ := Ideal (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) (Ideal.span s₀) q₁ ∧
        Eq (α := MvPolynomial (Fin n) (MvPolynomial (Fin m) R))
          ((MvPolynomial.C : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin n) (MvPolynomial (Fin m) R)) q :
            MvPolynomial (Fin n) (MvPolynomial (Fin m) R))
          ((AlgEquiv.symm (commAlgEquiv R (Fin n) (Fin m)) :
                (a : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) → MvPolynomial (Fin n) (MvPolynomial (Fin m) R))
              (HAdd.hAdd (β := MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) q₁
                ((σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) q₂ :
                  MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) :
            MvPolynomial (Fin n) (MvPolynomial (Fin m) R))
add :
  ∀ (p q : MvPolynomial (Fin n) (MvPolynomial (Fin m) R))
    (hp :
      ∃ (q₁ : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) (q₂ : MvPolynomial (Fin m) R),
        Membership.mem (γ := Ideal (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) (Ideal.span s₀) q₁ ∧
          p =
            (AlgEquiv.symm (commAlgEquiv R (Fin n) (Fin m)) :
                (a : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) → MvPolynomial (Fin n) (MvPolynomial (Fin m) R))
              (HAdd.hAdd (β := MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) q₁
                ((σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) q₂ :
                  MvPolynomial (Fin m) (MvPolynomial (Fin n) R))))
    (hq :
      ∃ (q₁ : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) (q₂ : MvPolynomial (Fin m) R),
        Membership.mem (γ := Ideal (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) (Ideal.span s₀) q₁ ∧
          q =
            (AlgEquiv.symm (commAlgEquiv R (Fin n) (Fin m)) :
                (a : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) → MvPolynomial (Fin n) (MvPolynomial (Fin m) R))
              (HAdd.hAdd (β := MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) q₁
                ((σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) q₂ :
                  MvPolynomial (Fin m) (MvPolynomial (Fin n) R)))),
    ∃ (q₁ : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) (q₂ : MvPolynomial (Fin m) R),
      Membership.mem (γ := Ideal (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) (Ideal.span s₀) q₁ ∧
        p + q =
          (AlgEquiv.symm (commAlgEquiv R (Fin n) (Fin m)) :
              (a : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) → MvPolynomial (Fin n) (MvPolynomial (Fin m) R))
            (HAdd.hAdd (β := MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) q₁
              ((σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) q₂ :
                MvPolynomial (Fin m) (MvPolynomial (Fin n) R)))
mul_X :
  ∀ (p : MvPolynomial (Fin n) (MvPolynomial (Fin m) R)) (i : Fin n)
    (hp :
      ∃ (q₁ : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) (q₂ : MvPolynomial (Fin m) R),
        Membership.mem (γ := Ideal (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) (Ideal.span s₀) q₁ ∧
          p =
            (AlgEquiv.symm (commAlgEquiv R (Fin n) (Fin m)) :
                (a : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) → MvPolynomial (Fin n) (MvPolynomial (Fin m) R))
              (HAdd.hAdd (β := MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) q₁
                ((σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) q₂ :
                  MvPolynomial (Fin m) (MvPolynomial (Fin n) R)))),
    ∃ (q₁ : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) (q₂ : MvPolynomial (Fin m) R),
      Membership.mem (γ := Ideal (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) (Ideal.span s₀) q₁ ∧
        p * MvPolynomial.X i =
          (AlgEquiv.symm (commAlgEquiv R (Fin n) (Fin m)) :
              (a : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) → MvPolynomial (Fin n) (MvPolynomial (Fin m) R))
            (HAdd.hAdd (β := MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) q₁
              ((σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) q₂ :
                MvPolynomial (Fin m) (MvPolynomial (Fin n) R)))
⊢ ∃ (q₁ : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) (q₂ : MvPolynomial (Fin m) R),
    Membership.mem (γ := Ideal (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) (Ideal.span s₀) q₁ ∧
      p =
        (AlgEquiv.symm (commAlgEquiv R (Fin n) (Fin m)) :
            (a : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) → MvPolynomial (Fin n) (MvPolynomial (Fin m) R))
          (HAdd.hAdd (β := MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) q₁
            ((σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) q₂ :
              MvPolynomial (Fin m) (MvPolynomial (Fin n) R)))

Tactic:
induction p using MvPolynomial.induction_on with
      | C q =>
        exact ⟨0, q, by simp, (commAlgEquiv _ _ _).injective <|
          by simp [commAlgEquiv_C, σ]⟩
      | add p q hp hq =>
        obtain ⟨q₁, q₂, hq₁, rfl⟩ := hp
        obtain ⟨q₃, q₄, hq₃, rfl⟩ := hq
        refine ⟨q₁ + q₃, q₂ + q₄, add_mem hq₁ hq₃, by simp only [map_add, add_add_add_comm]⟩
      | mul_X p i hp =>
        obtain ⟨q₁, q₂, hq₁, rfl⟩ := hp
        simp only [← (commAlgEquiv R (Fin n) (Fin m)).injective.eq_iff,
          map_mul, AlgEquiv.apply_symm_apply, commAlgEquiv_X]
        refine ⟨q₁ * .C (.X i) + σ q₂ * (.C (.X i) - σ (f (.X i))), q₂ * f (.X i), ?_, ?_⟩
        · exact add_mem (Ideal.mul_mem_right _ _ hq₁)
            (Ideal.mul_mem_left _ _ (Ideal.subset_span (Set.mem_range_self _)))
        · simp; ring

Premises used: Function.Injective.eq_iff, MvPolynomial.commAlgEquiv_X, AlgEquiv.apply_symm_apply, MvPolynomial.induction_on, map_mul, AlgEquiv.injective, MvPolynomial.commAlgEquiv, Fin, rfl