awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x : (a : R[X]) → S) p = (↑y : S)
e_f :
  ∀ (i : ℕ),
    (↑(Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            ((aeval x : (a : R[X]) → S)
              (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)))
            ⋯) :
        S) =
      (↑(HSMul.hSMul (β := ↥R[x]) (p.coeff i)
            (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
                ((aeval x : (a : R[X]) → S) (HPow.hPow (α := R[X]) X i)) ⋯ :
              ↥R[x])) :
        S)
⊢ Eq.{u_2 + 1} (α := ↥R[x])
    (∑ i ∈ p.support,
      Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
        ((aeval x : (a : R[X]) → S)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)))
        ⋯)
    (∑ i ∈ p.support,
      HSMul.hSMul (β := ↥R[x]) (p.coeff i)
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            ((aeval x : (a : R[X]) → S) (HPow.hPow (α := R[X]) X i)) ⋯ :
          ↥R[x]))

Tactic:
congr with i
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x : (a : R[X]) → S) p = (↑y : S)
i : ℕ
⊢ (↑(Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
          ((aeval x : (a : R[X]) → S)
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)))
          ⋯) :
      S) =
    (↑(HSMul.hSMul (β := ↥R[x]) (p.coeff i)
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
              ((aeval x : (a : R[X]) → S) (HPow.hPow (α := R[X]) X i)) ⋯ :
            ↥R[x])) :
      S)

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x : (a : R[X]) → S) p = (↑y : S)
⊢ y =
    ∑ i ∈ p.support,
      HSMul.hSMul (β := ↥R[x]) (p.coeff i)
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            ((aeval x : (a : R[X]) → S) (HPow.hPow (α := R[X]) X i)) ⋯ :
          ↥R[x])

Tactic:
have : y = ∑ i ∈ p.support, p.coeff i • ⟨_, (X ^ i).aeval_mem_adjoin_singleton _ x⟩ := by
      trans ∑ i ∈ p.support, ⟨_, (C (p.coeff i) * X ^ i).aeval_mem_adjoin_singleton _ x⟩
      · ext1
        simp only [AddSubmonoidClass.coe_finsetSum, ← map_sum, ← hp', ← as_sum_support_C_mul_X_pow]
      · congr with i
        simp [Algebra.smul_def]
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x : (a : R[X]) → S) p = (↑y : S)
this :
  y =
    ∑ i ∈ p.support,
      HSMul.hSMul (β := ↥R[x]) (p.coeff i)
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            ((aeval x : (a : R[X]) → S) (HPow.hPow (α := R[X]) X i)) ⋯ :
          ↥R[x])
mpr :
  Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (∑ x_1 ∈ p.support,
      HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) (p.coeff x_1) : ↥R[x])
        (Subtype.mk (p := fun (x_2 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_2)
            ((aeval x : (a : R[X]) → S) (HPow.hPow (α := R[X]) X x_1)) ⋯ :
          ↥R[x]))
⊢ Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y

Tactic:
simp_rw [this, Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x : (a : R[X]) → S) p = (↑y : S)
this :
  y =
    ∑ i ∈ p.support,
      HSMul.hSMul (β := ↥R[x]) (p.coeff i)
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            ((aeval x : (a : R[X]) → S) (HPow.hPow (α := R[X]) X i)) ⋯ :
          ↥R[x])
⊢ Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (∑ x_1 ∈ p.support,
      HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) (p.coeff x_1) : ↥R[x])
        (Subtype.mk (p := fun (x_2 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_2)
            ((aeval x : (a : R[X]) → S) (HPow.hPow (α := R[X]) X x_1)) ⋯ :
          ↥R[x]))

Tactic:
sum_mem fun i _ ↦ Ideal.mul_mem_right _ _ (Ideal.mem_map_of_mem _ (hp i))

Premises used: Algebra.algebraMap, Ideal.mem_map_of_mem, Algebra.adjoin, Membership.mem, Subtype, Ideal.map, Subtype.mk, HPow.hPow, Ideal.mul_mem_right, Polynomial.aeval, Polynomial.aeval_mem_adjoin_singleton, Singleton.singleton, Polynomial.X, DFunLike.coe, sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x : (a : R[X]) → S) p = (↑y : S)
this :
  y =
    ∑ i ∈ p.support,
      HSMul.hSMul (β := ↥R[x]) (p.coeff i)
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            ((aeval x : (a : R[X]) → S) (HPow.hPow (α := R[X]) X i)) ⋯ :
          ↥R[x])
⊢ Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (∑ x_1 ∈ p.support,
      HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) (p.coeff x_1) : ↥R[x])
        (Subtype.mk (p := fun (x_2 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_2)
            ((aeval x : (a : R[X]) → S) (HPow.hPow (α := R[X]) X x_1)) ⋯ :
          ↥R[x]))

Tactic:
exact sum_mem fun i _ ↦ Ideal.mul_mem_right _ _ (Ideal.mem_map_of_mem _ (hp i))

Premises used: Ideal.mem_map_of_mem, Ideal.map, Ideal.mul_mem_right, sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst_3 : Invertible x
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← Ideal.one_eq_top, ← Ideal.add_eq_sup, Ideal.add_eq_one_iff] at h

Premises used: Ideal.one_eq_top, Ideal.add_eq_one_iff, Ideal.add_eq_sup
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst_3 : Invertible x
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∃ (p : R[X]),
    p.leadingCoeff - 1 ∈ I ∧
      Eq.{u_2 + 1} (α := S)
        ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) : (a : R[X]) → S) p : S) (0 : S)

Tactic:
have ⟨y, hy, z, hz, eq⟩ := h
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst_3 : Invertible x
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : ↥R[x]
hy : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
z : ↥R[x]
hz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq : y + z = 1
have :
  ∀ (p : R[X]) (hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)),
    ∃ (p : R[X]),
      p.leadingCoeff - 1 ∈ I ∧
        Eq.{u_2 + 1} (α := S)
          ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) : (a : R[X]) → S) p : S) (0 : S)
⊢ ∃ (p : R[X]),
    p.leadingCoeff - 1 ∈ I ∧
      Eq.{u_2 + 1} (α := S)
        ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) : (a : R[X]) → S) p : S) (0 : S)

Tactic:
have ⟨p, hp⟩ := (mem_ideal_map_adjoin ..).mp hy
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst_3 : Invertible x
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : ↥R[x]
hy : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
z : ↥R[x]
hz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq : y + z = 1
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
have : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∃ (p : R[X]),
    p.leadingCoeff - 1 ∈ I ∧
      Eq.{u_2 + 1} (α := S)
        ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) : (a : R[X]) → S) p : S) (0 : S)

Tactic:
have ⟨w, hw⟩ := Ideal.mem_span_singleton.mp hz
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst_3 : Invertible x
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : ↥R[x]
hy : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
z : ↥R[x]
hz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq : y + z = 1
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
w : ↥R[x]
hw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have :
  ∀ (q : R[X]) (hq : (aeval x : (a : R[X]) → S) q = (↑w : S)),
    ∃ (p : R[X]),
      p.leadingCoeff - 1 ∈ I ∧
        Eq.{u_2 + 1} (α := S)
          ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) : (a : R[X]) → S) p : S) (0 : S)
⊢ ∃ (p : R[X]),
    p.leadingCoeff - 1 ∈ I ∧
      Eq.{u_2 + 1} (α := S)
        ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) : (a : R[X]) → S) p : S) (0 : S)

Tactic:
have ⟨q, hq⟩ := adjoin_eq_exists_aeval R x w
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst_3 : Invertible x
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : ↥R[x]
hy : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
z : ↥R[x]
hz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq : y + z = 1
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
w : ↥R[x]
hw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : R[X]
hq : (aeval x : (a : R[X]) → S) q = (↑w : S)
h₁ :
  (1 - p - X * q).reverse.leadingCoeff - 1 ∈ I ∧
    Eq.{u_2 + 1} (α := S)
      ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) : (a : R[X]) → S) (1 - p - X * q).reverse :
        S)
      (0 : S)
⊢ ∃ (p : R[X]),
    p.leadingCoeff - 1 ∈ I ∧
      Eq.{u_2 + 1} (α := S)
        ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) : (a : R[X]) → S) p : S) (0 : S)

Tactic:
use (1 - p - X * q).reverse
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst_3 : Invertible x
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : ↥R[x]
hy : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
z : ↥R[x]
hz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq : y + z = 1
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
w : ↥R[x]
hw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : R[X]
hq : (aeval x : (a : R[X]) → S) q = (↑w : S)
⊢ (1 - p - X * q).coeff 0 - 1 ∈ I

Tactic:
simpa using hp.1 0

Premises used: And.left, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst_3 : Invertible x
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : ↥R[x]
hy : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
z : ↥R[x]
hz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq : y + z = 1
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
w : ↥R[x]
hw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : R[X]
hq : (aeval x : (a : R[X]) → S) q = (↑w : S)
⊢ (1 - p - X * q).coeff 0 - 1 ∈ I

Tactic:
have : (1 - p - X * q).coeff 0 - 1 ∈ I := by simpa using hp.1 0
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst_3 : Invertible x
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : ↥R[x]
hy : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
z : ↥R[x]
hz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq : y + z = 1
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
w : ↥R[x]
hw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : R[X]
hq : (aeval x : (a : R[X]) → S) q = (↑w : S)
this : (1 - p - X * q).coeff 0 - 1 ∈ I
⊢ (↑(y + z) : S) = (↑1 : S)

Tactic:
apply_fun (·.1) at eq hw
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst_3 : Invertible x
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : ↥R[x]
hy : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
z : ↥R[x]
hz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq : y + z = 1
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
w : ↥R[x]
hw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : R[X]
hq : (aeval x : (a : R[X]) → S) q = (↑w : S)
this : (1 - p - X * q).coeff 0 - 1 ∈ I
eq₁ : (↑(y + z) : S) = (↑1 : S)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply_fun (·.1) at eq hw
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst_3 : Invertible x
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : ↥R[x]
hy : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
z : ↥R[x]
hz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
w : ↥R[x]
q : R[X]
hq : (aeval x : (a : R[X]) → S) q = (↑w : S)
this : (1 - p - X * q).coeff 0 - 1 ∈ I
eq : (↑y : S) + (↑z : S) = 1
hw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ eval₂ (↑(ofId R S) : R →+* S) x (1 - p - X * q) = 0

Tactic:
simp [← aeval_def, hp.2, hq, ← eq, hw]

Premises used: Polynomial.aeval_def, And.right
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst_3 : Invertible x
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : ↥R[x]
hy : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
z : ↥R[x]
hz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
w : ↥R[x]
q : R[X]
hq : (aeval x : (a : R[X]) → S) q = (↑w : S)
this : (1 - p - X * q).coeff 0 - 1 ∈ I
eq : (↑y : S) + (↑z : S) = 1
hw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (1 - p - X * q).coeff 0 - 1 ∈ I ∧
    Eq.{u_2 + 1} (α := S)
      ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) : (a : R[X]) → S) (1 - p - X * q).reverse :
        S)
      (0 : S)

Tactic:
exact ⟨this, (eval₂_reverse_eq_zero_iff ..).mpr <| by simp [← aeval_def, hp.2, hq, ← eq, hw]⟩
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst_3 : Invertible x
h_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : ↥R[x]
hy : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
z : ↥R[x]
hz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
w : ↥R[x]
q : R[X]
hq : (aeval x : (a : R[X]) → S) q = (↑w : S)
this : (1 - p - X * q).coeff 0 - 1 ∈ I
eq : (↑y : S) + (↑z : S) = 1
hw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : (1 - p - X * q).coeff 0 = 0
⊢ I = ⊤

Tactic:
simpa [h, Ideal.eq_top_iff_one]

Premises used: Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst_3 : Invertible x
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : ↥R[x]
hy : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
z : ↥R[x]
hz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
w : ↥R[x]
q : R[X]
hq : (aeval x : (a : R[X]) → S) q = (↑w : S)
this : (1 - p - X * q).coeff 0 - 1 ∈ I
eq : (↑y : S) + (↑z : S) = 1
hw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (1 - p - X * q).coeff 0 ≠ 0

Tactic:
exact fun h ↦ hI <| by simpa [h, Ideal.eq_top_iff_one]
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R[X]) (integralNormalization 0) 0

Tactic:
simp [integralNormalization]

Premises used: Polynomial.integralNormalization
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
x : R
hx : x ≠ 0
⊢ Eq.{u + 1} (α := R[X]) (integralNormalization ((C : (a : R) → R[X]) x)) 1

Tactic:
simp [integralNormalization, sum_def, support_C hx, degree_C hx]

Premises used: Polynomial.integralNormalization, Polynomial.degree_C, Polynomial.support_C, Polynomial.sum_def
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
⊢ p.coeff i = 0 → p.degree ≠ (↑i : WithBot ℕ)

Tactic:
have : p.coeff i = 0 → p.degree ≠ i := fun hc hd => coeff_ne_zero_of_eq_degree hd hc
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
this : p.coeff i = 0 → p.degree ≠ (↑i : WithBot ℕ)
⊢ p.integralNormalization.coeff i =
    if p.degree = (↑i : WithBot ℕ) then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Tactic:
simp +contextual [sum_def, integralNormalization, coeff_monomial, this,
    mem_support_iff]

Premises used: Polynomial.integralNormalization, Polynomial.mem_support_iff, Polynomial.coeff_monomial, Polynomial.sum_def
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : ℕ
⊢ a ∈ p.integralNormalization.support → a ∈ p.support

Tactic:
simp +contextual [sum_def, integralNormalization, coeff_monomial, mem_support_iff]

Premises used: Polynomial.integralNormalization, Polynomial.mem_support_iff, Polynomial.coeff_monomial, Polynomial.sum_def
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : p.degree = (↑i : WithBot ℕ)
rw : (if p.degree = (↑i : WithBot ℕ) then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) = 1
rw₁ rw₂ : Eq.{u + 1} (α := R) 1 1
⊢ p.integralNormalization.coeff i = 1

Tactic:
rw [integralNormalization_coeff, if_pos hi]

Premises used: if_pos, Polynomial.integralNormalization_coeff
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
⊢ p.integralNormalization.coeff p.natDegree = 1

Tactic:
integralNormalization_coeff_degree (degree_eq_natDegree hp)

Premises used: Polynomial.degree_eq_natDegree, Polynomial.integralNormalization_coeff_degree
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : p.degree ≠ (↑i : WithBot ℕ)
rw :
  (if p.degree = (↑i : WithBot ℕ) then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) =
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
rw₁ rw₂ : p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
⊢ p.integralNormalization.coeff i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Tactic:
rw [integralNormalization_coeff, if_neg hi]

Premises used: Polynomial.integralNormalization_coeff, if_neg
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : i ≠ p.natDegree
⊢ p.integralNormalization.coeff i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Tactic:
integralNormalization_coeff_degree_ne (degree_ne_of_natDegree_ne hi.symm)

Premises used: Polynomial.degree_ne_of_natDegree_ne, Ne.symm, Polynomial.integralNormalization_coeff_degree_ne
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
pos : ∀ (hp : p = 0), p.integralNormalization.degree = p.degree
neg : ∀ (hp : ¬p = 0), p.integralNormalization.degree = p.degree
⊢ p.integralNormalization.degree = p.degree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
hp : p = 0
⊢ p.integralNormalization.degree = p.degree

Tactic:
simp [hp]
-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
hp : ¬p = 0
neg : p.integralNormalization.degree = (↑p.natDegree : WithBot ℕ)
⊢ p.integralNormalization.degree = p.degree

Tactic:
rw [degree_eq_natDegree hp]

Premises used: Polynomial.degree_eq_natDegree