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
obtain : ∀ (i : Fin n) (hi : ¬e.val i = 0), ∃ (n_1 : ℕ) (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0
⊢ ∃ (n_1 : ℕ) (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0

Tactic:
obtain ⟨i, hi⟩ := he0
-- 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
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
⊢ ∃ (n_1 : ℕ) (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0

Tactic:
⟨(e.1 i).natDegree, i, degree_eq_natDegree hi, hi⟩

Premises used: _private.0.ChevalleyThm.PolynomialC.InductionObj.val, Polynomial.degree_eq_natDegree, And.intro, Exists.intro, Polynomial.natDegree
-- 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
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
⊢ ∃ (n_1 : ℕ) (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0

Tactic:
exact ⟨(e.1 i).natDegree, i, degree_eq_natDegree hi, hi⟩
-- 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
⊢ ∃ (n_1 : ℕ) (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0

Tactic:
have : ∃ n : ℕ, ∃ i, (e.1 i).degree = n ∧ (e.1 i) ≠ 0 := by
        obtain ⟨i, hi⟩ := he0; exact ⟨(e.1 i).natDegree, i, degree_eq_natDegree hi, hi⟩
-- 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
this : ∃ (n_1 : ℕ) (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0) this
⊢ ∃ (i : Fin n), (e.val i).degree = (↑m : WithBot ℕ) ∧ e.val i ≠ 0

Tactic:
Nat.find_spec this

Premises used: Nat.find_spec
-- 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
this : ∃ (n_1 : ℕ) (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0) this
obtain :
  ∀ (i : Fin n) (hi : (e.val i).degree = (↑m : WithBot ℕ)) (hi' : e.val i ≠ 0),
    ∃ (i : Fin n), e.val i ≠ 0 ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
⊢ ∃ (i : Fin n), e.val i ≠ 0 ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree

Tactic:
obtain ⟨i, hi, hi'⟩ : ∃ i, (e.1 i).degree = m ∧ (e.1 i) ≠ 0 := Nat.find_spec this

Premises used: Nat.find_spec
-- 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
this : ∃ (n_1 : ℕ) (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0) this
i : Fin n
hi : (e.val i).degree = (↑m : WithBot ℕ)
hi' : e.val i ≠ 0
⊢ ∃ (i : Fin n), e.val i ≠ 0 ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree

Tactic:
⟨i, hi', fun j hj ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- 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
this : ∃ (n_1 : ℕ) (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0) this
i : Fin n
hi : (e.val i).degree = (↑m : WithBot ℕ)
hi' : e.val i ≠ 0
refine : ∀ (j : Fin n) (hj : e.val j ≠ 0), (e.val i).degree ≤ (e.val j).degree
⊢ ∃ (i : Fin n), e.val i ≠ 0 ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree

Tactic:
refine ⟨i, hi', fun j hj ↦ ?_⟩
-- 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
this : ∃ (n_1 : ℕ) (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0) this
i : Fin n
hi : (e.val i).degree = (↑m : WithBot ℕ)
hi' : e.val i ≠ 0
j : Fin n
hj : e.val j ≠ 0
⊢ (e.val i).degree ≤ (e.val j).degree

Tactic:
hi.le.trans ?_

Premises used: Eq.le, LE.le.trans
-- 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
this : ∃ (n_1 : ℕ) (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0) this
i : Fin n
hi : (e.val i).degree = (↑m : WithBot ℕ)
hi' : e.val i ≠ 0
j : Fin n
hj : e.val j ≠ 0
refine : (↑m : WithBot ℕ) ≤ (e.val j).degree
⊢ (e.val i).degree ≤ (e.val j).degree

Tactic:
refine hi.le.trans ?_

Premises used: Eq.le, LE.le.trans
-- 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
this : ∃ (n_1 : ℕ) (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (i : Fin n), (e.val i).degree = (↑n_1 : WithBot ℕ) ∧ e.val i ≠ 0) this
i : Fin n
hi : (e.val i).degree = (↑m : WithBot ℕ)
hi' : e.val i ≠ 0
j : Fin n
hj : e.val j ≠ 0
rw : m ≤ (e.val j).natDegree
⊢ (↑m : WithBot ℕ) ≤ (e.val j).degree

Tactic:
rw [degree_eq_natDegree hj, Nat.cast_le]

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_le