awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw :
  InductionObj.degree (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff}))
      {
        val :=
          (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff})))) :
              (a : R[X]) → (R ⧸ Ideal.span {(e.val i).leadingCoeff})[X]) ∘
            e.val :
        InductionObj (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff})) n } <
    e.degree
⊢ InductionObj.degree (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff}))
      {
        val :=
          (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff})))) :
              (a : R[X]) → (R ⧸ Ideal.span {(e.val i).leadingCoeff})[X]) ∘
            e.val :
        InductionObj (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff})) n } <
    v

Tactic:
rw [hv]
-- 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
⊢ InductionObj.degree (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff}))
      {
        val :=
          (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff})))) :
              (a : R[X]) → (R ⧸ Ideal.span {(e.val i).leadingCoeff})[X]) ∘
            e.val :
        InductionObj (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff})) n } <
    e.degree

Tactic:
.left _ _ (lt_of_le_of_ne ?_ ?_)

Premises used: _private.0.ChevalleyThm.PolynomialC.InductionObj.degree, Prod.Lex.left, lt_of_le_of_ne
-- 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
j : Fin n
⊢ Function.comp (β := (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff}))[X])
      Polynomial.degree
      (val
        {
          val :=
            (⇑(mapRingHom
                    (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff})))) :
                (a : R[X]) → (R ⧸ Ideal.span {(e.val i).leadingCoeff})[X]) ∘
              e.val :
          InductionObj (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff})) n })
      j ≤
    (Polynomial.degree ∘ e.val) j

Tactic:
simpa using degree_map_le

Premises used: Polynomial.degree_map_le
-- 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
h_eq :
  Function.comp (β := (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff}))[X])
      Polynomial.degree
      (Polynomial.map (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff}))) ∘
        e.val) =
    Polynomial.degree ∘ e.val
⊢ Function.comp (β := (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff}))[X])
      Polynomial.degree
      (Polynomial.map (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff}))) ∘
        e.val)
      i =
    (Polynomial.degree ∘ e.val) i

Tactic:
replace h_eq := congr_fun h_eq i
-- 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
h_eq :
  Function.comp (β := (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff}))[X])
      Polynomial.degree
      (Polynomial.map (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(e.val i).leadingCoeff}))) ∘
        e.val)
      i =
    (Polynomial.degree ∘ e.val) i
⊢ e.val i = 0

Tactic:
simp only [Ideal.Quotient.algebraMap_eq, comp_apply, degree_map_eq_iff,
        Ideal.Quotient.mk_singleton_self, ne_eq, not_true_eq_false, false_or] at h_eq

Premises used: Ideal.Quotient.algebraMap_eq, Ideal.Quotient.mk_singleton_self, not_true_eq_false, false_or, ne_eq, Polynomial.degree_map_eq_iff, Function.comp_apply
-- 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
h_eq : e.val i = 0
⊢ False

Tactic:
hi h_eq
-- 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
h_eq : e.val i = 0
⊢ False

Tactic:
exact hi h_eq
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R₀ : Type u_1
inst : CommRing R₀
n : ℕ
R : Type u_6
inst_1 : CommRing R
inst_2 : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}) := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
⊢ Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) (⇑q₂ : (a : R) → R ⧸ Ideal.span {c})

Tactic:
have q₂_surjective : Surjective q₂ := Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R₀ : Type u_1
inst : CommRing R₀
n : ℕ
R : Type u_6
inst_1 : CommRing R
inst_2 : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}) := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective :
  Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) (⇑q₂ : (a : R) → R ⧸ Ideal.span {c})
e₁ : InductionObj (Localization.Away c) n :=
  {
    val :=
      HSMul.hSMul (α := (Localization.Away c)[X]) (β := Fin n → (Localization.Away c)[X])
        ((Polynomial.C : (a : Localization.Away c) → (Localization.Away c)[X]) (IsLocalization.Away.invSelf c))
        ((⇑(mapRingHom (↑q₁ : R →+* Localization.Away c)) : (a : R[X]) → (Localization.Away c)[X]) ∘ e.val) }
e₂ : InductionObj (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n :=
  { val := (⇑(mapRingHom (↑q₂ : R →+* R ⧸ Ideal.span {c})) : (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘ e.val }
h : ∀ (j : Fin n), Membership.mem (γ := Finset (Fin n)) Finset.univ j → (e₁.val j).degree ≤ (e.val j).degree
⊢ LE.le (α := ℕ) (∑ i : Fin n, (e₁.val i).degree.succ) (∑ i : Fin n, (e.val i).degree.succ)

Tactic:
gcongr with j
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R₀ : Type u_1
inst : CommRing R₀
n : ℕ
R : Type u_6
inst_1 : CommRing R
inst_2 : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}) := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective :
  Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) (⇑q₂ : (a : R) → R ⧸ Ideal.span {c})
e₁ : InductionObj (Localization.Away c) n :=
  {
    val :=
      HSMul.hSMul (α := (Localization.Away c)[X]) (β := Fin n → (Localization.Away c)[X])
        ((Polynomial.C : (a : Localization.Away c) → (Localization.Away c)[X]) (IsLocalization.Away.invSelf c))
        ((⇑(mapRingHom (↑q₁ : R →+* Localization.Away c)) : (a : R[X]) → (Localization.Away c)[X]) ∘ e.val) }
e₂ : InductionObj (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n :=
  { val := (⇑(mapRingHom (↑q₂ : R →+* R ⧸ Ideal.span {c})) : (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘ e.val }
j : Fin n
h : Membership.mem (γ := Finset (Fin n)) Finset.univ j
⊢ (e₁.val j).degree ≤ (e.val j).degree

Tactic:
(degree_mul_le _ _).trans <| (add_le_of_nonpos_left degree_C_le).trans degree_map_le

Premises used: Polynomial.degree_map_le, Polynomial.degree_mul_le, add_le_of_nonpos_left, LE.le.trans, Polynomial.degree_C_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R₀ : Type u_1
inst : CommRing R₀
n : ℕ
R : Type u_6
inst_1 : CommRing R
inst_2 : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}) := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective :
  Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) (⇑q₂ : (a : R) → R ⧸ Ideal.span {c})
e₁ : InductionObj (Localization.Away c) n :=
  {
    val :=
      HSMul.hSMul (α := (Localization.Away c)[X]) (β := Fin n → (Localization.Away c)[X])
        ((Polynomial.C : (a : Localization.Away c) → (Localization.Away c)[X]) (IsLocalization.Away.invSelf c))
        ((⇑(mapRingHom (↑q₁ : R →+* Localization.Away c)) : (a : R[X]) → (Localization.Away c)[X]) ∘ e.val) }
e₂ : InductionObj (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n :=
  { val := (⇑(mapRingHom (↑q₂ : R →+* R ⧸ Ideal.span {c})) : (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘ e.val }
j : Fin n
h : Membership.mem (γ := Finset (Fin n)) Finset.univ j
⊢ (e₁.val j).degree ≤ (e.val j).degree

Tactic:
exact (degree_mul_le _ _).trans <| (add_le_of_nonpos_left degree_C_le).trans degree_map_le

Premises used: Polynomial.degree_map_le, Polynomial.degree_mul_le, add_le_of_nonpos_left, LE.le.trans, Polynomial.degree_C_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R₀ : Type u_1
inst : CommRing R₀
n : ℕ
R : Type u_6
inst_1 : CommRing R
inst_2 : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}) := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective :
  Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) (⇑q₂ : (a : R) → R ⧸ Ideal.span {c})
e₁ : InductionObj (Localization.Away c) n :=
  {
    val :=
      HSMul.hSMul (α := (Localization.Away c)[X]) (β := Fin n → (Localization.Away c)[X])
        ((Polynomial.C : (a : Localization.Away c) → (Localization.Away c)[X]) (IsLocalization.Away.invSelf c))
        ((⇑(mapRingHom (↑q₁ : R →+* Localization.Away c)) : (a : R[X]) → (Localization.Away c)[X]) ∘ e.val) }
e₂ : InductionObj (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n :=
  { val := (⇑(mapRingHom (↑q₂ : R →+* R ⧸ Ideal.span {c})) : (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘ e.val }
⊢ e₁.degBound ≤ e.degBound

Tactic:
have degBound_e₁_le : e₁.degBound ≤ e.degBound := by
    unfold degBound
    gcongr with j
    exact (degree_mul_le _ _).trans <| (add_le_of_nonpos_left degree_C_le).trans degree_map_le