-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree →
        i ≠ j →
          P R { val := Function.update (β := fun (a : Fin n) ↦ R[X]) e.val j (e.val j %ₘ e.val i) : InductionObj R n } →
            P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            {
              val :=
                HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
                  ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
                  ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
              InductionObj (Away c) n } →
          P (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))
              {
                val :=
                  (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
                      (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
                    e.val } →
            P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n) (hv : y = e.degree), P R e
R : Type u
inst : CommRing R
e : InductionObj R n
hv : v = e.degree
h : Nontrivial R
he0 : ∃ (x : Fin n), ¬e.val x = 0
H : ¬∃ (i : Fin n), (e.val i).Monic ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
i : Fin n
hi : e.val i ≠ 0
i_min : ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
right :
  (∀ (x : Fin n),
      (HMul.hMul (α := (Away (e.val i).leadingCoeff)[X])
            ((Polynomial.C : (a : Away (e.val i).leadingCoeff) → (Away (e.val i).leadingCoeff)[X])
              (IsLocalization.Away.invSelf (e.val i).leadingCoeff))
            (Polynomial.map (algebraMap R (Away (e.val i).leadingCoeff)) (e.val x))).degree =
        (e.val x).degree) →
    ¬((ofLex : (a : Lex ((Fin n → WithBot ℕ) × Prop)) → (Fin n → WithBot ℕ) × Prop)
          {
              val :=
                HSMul.hSMul (α := (Away (e.val i).leadingCoeff)[X]) (β := Fin n → (Away (e.val i).leadingCoeff)[X])
                  ((Polynomial.C : (a : Away (e.val i).leadingCoeff) → (Away (e.val i).leadingCoeff)[X])
                    (IsLocalization.Away.invSelf (e.val i).leadingCoeff))
                  (Polynomial.map (algebraMap R (Away (e.val i).leadingCoeff)) ∘ e.val) :
              InductionObj (Away (e.val i).leadingCoeff) n }.degree).2
⊢ Eq (α := Fin n → WithBot ℕ)
      ((ofLex : (a : Lex ((Fin n → WithBot ℕ) × Prop)) → (Fin n → WithBot ℕ) × Prop)
          {
              val :=
                HSMul.hSMul (α := (Away (e.val i).leadingCoeff)[X]) (β := Fin n → (Away (e.val i).leadingCoeff)[X])
                  ((Polynomial.C : (a : Away (e.val i).leadingCoeff) → (Away (e.val i).leadingCoeff)[X])
                    (IsLocalization.Away.invSelf (e.val i).leadingCoeff))
                  ((⇑(mapRingHom (algebraMap R (Away (e.val i).leadingCoeff))) :
                      (a : R[X]) → (Away (e.val i).leadingCoeff)[X]) ∘
                    e.val) :
              InductionObj (Away (e.val i).leadingCoeff) n }.degree).1
      ((ofLex : (a : Lex ((Fin n → WithBot ℕ) × Prop)) → (Fin n → WithBot ℕ) × Prop) e.degree).1 →
    LE.le (α := Prop)
        ((ofLex : (a : Lex ((Fin n → WithBot ℕ) × Prop)) → (Fin n → WithBot ℕ) × Prop)
            {
                val :=
                  HSMul.hSMul (α := (Away (e.val i).leadingCoeff)[X]) (β := Fin n → (Away (e.val i).leadingCoeff)[X])
                    ((Polynomial.C : (a : Away (e.val i).leadingCoeff) → (Away (e.val i).leadingCoeff)[X])
                      (IsLocalization.Away.invSelf (e.val i).leadingCoeff))
                    ((⇑(mapRingHom (algebraMap R (Away (e.val i).leadingCoeff))) :
                        (a : R[X]) → (Away (e.val i).leadingCoeff)[X]) ∘
                      e.val) :
                InductionObj (Away (e.val i).leadingCoeff) n }.degree).2
        ((ofLex : (a : Lex ((Fin n → WithBot ℕ) × Prop)) → (Fin n → WithBot ℕ) × Prop) e.degree).2 ∧
      ¬LE.le (α := Prop) ((ofLex : (a : Lex ((Fin n → WithBot ℕ) × Prop)) → (Fin n → WithBot ℕ) × Prop) e.degree).2
          ((ofLex : (a : Lex ((Fin n → WithBot ℕ) × Prop)) → (Fin n → WithBot ℕ) × Prop)
              {
                  val :=
                    HSMul.hSMul (α := (Away (e.val i).leadingCoeff)[X]) (β := Fin n → (Away (e.val i).leadingCoeff)[X])
                      ((Polynomial.C : (a : Away (e.val i).leadingCoeff) → (Away (e.val i).leadingCoeff)[X])
                        (IsLocalization.Away.invSelf (e.val i).leadingCoeff))
                      ((⇑(mapRingHom (algebraMap R (Away (e.val i).leadingCoeff))) :
                          (a : R[X]) → (Away (e.val i).leadingCoeff)[X]) ∘
                        e.val) :
                  InductionObj (Away (e.val i).leadingCoeff) n }.degree).2

Tactic:
simp only [coe_mapRingHom, funext_iff, InductionObj.ofLex_degree_fst, Pi.smul_apply,
        comp_apply, smul_eq_mul, show (ofLex e.degree).2 from H,
        le_Prop_eq, implies_true, true_implies, true_and]

Premises used: funext_iff, _private.0.ChevalleyThm.PolynomialC.InductionObj.ofLex_degree_fst, Polynomial.coe_mapRingHom, le_Prop_eq, true_implies, Function.comp_apply, implies_true, smul_eq_mul, true_and, Pi.smul_apply