awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
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]
H : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
mp :
  ∀ (a : ↥R[x]) (ha : Membership.mem (γ := Set ↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R)) a),
    ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑a : S)
mp₁ : ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) ((↑0 : S) : S)
mp₂ :
  ∀ (a b : ↥R[x])
    (ha :
      Membership.mem (γ := Submodule ↥R[x] ↥R[x])
        (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) a)
    (hb :
      Membership.mem (γ := Submodule ↥R[x] ↥R[x])
        (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) b)
    (ha' : ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑a : S))
    (hb' : ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑b : S)),
    ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a + b) : S)
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
have mp₃ : ∀ (a b : ↥R[x])
  (hb :
    Membership.mem (γ := Submodule ↥R[x] ↥R[x])
      (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) b)
  (hb' : ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑b : S)),
  ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a • b) : S)
Tactic: induction H using Submodule.span_induction with
    | mem a ha =>
      obtain ⟨a, ha, rfl⟩ := ha
      exact ⟨C a, fun i ↦ by rw [coeff_C]; aesop, aeval_C _ _⟩
    | zero => exact ⟨0, by simp, aeval_zero _⟩
    | add a b ha hb ha' hb' =>
      obtain ⟨a, ha, ha'⟩ := ha'
      obtain ⟨b, hb, hb'⟩ := hb'
      exact ⟨a + b, fun i ↦ by simpa using add_mem (ha i) (hb i), by simp [ha', hb']⟩
    | smul a b hb hb' =>
      obtain ⟨b', hb, hb'⟩ := hb'
      have ⟨p, hp⟩ := adjoin_eq_exists_aeval R x a
      refine ⟨p * b', fun i ↦ ?_, by simp [hp, hb']⟩
      rw [coeff_mul]
      exact sum_mem fun i hi ↦ Ideal.mul_mem_left _ _ (hb _)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
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])
have trans : y =
  ∑ 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)))
      sorry
Tactic: trans ∑ i ∈ p.support, ⟨_, (C (p.coeff i) * X ^ i).aeval_mem_adjoin_singleton _ x⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
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)
trans :
  y =
    ∑ 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)))
        ⋯
⊢ 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])
have trans₁ : 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)))
      sorry)
  (∑ 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)) sorry :
        ↥R[x]))
Tactic: trans ∑ i ∈ p.support, ⟨_, (C (p.coeff i) * X ^ i).aeval_mem_adjoin_singleton _ x⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
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,
      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)))
        ⋯
have a : (↑y : S) =
  (↑(∑ 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)))
          sorry) :
    S)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
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)
⊢ 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]))
have 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)))
          sorry) :
      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)) sorry :
            ↥R[x])) :
      S)
Tactic: congr with i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (hypothesis)
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)
⊢ Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
have 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)) sorry :
        ↥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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
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) y
have 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)) sorry :
        ↥R[x]))
Tactic: simp_rw [this, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (hypothesis)
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)
⊢ ∃ (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)
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
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)
⊢ ∃ (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)
have have : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: have ⟨y, hy, z, hz, eq⟩ := h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
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]),
    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)
have 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)
Tactic: have ⟨p, hp⟩ := (mem_ideal_map_adjoin ..).mp hy
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
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)
⊢ ∃ (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)
have have : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: have ⟨w, hw⟩ := Ideal.mem_span_singleton.mp hz
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: have ⟨q, hq⟩ := adjoin_eq_exists_aeval R x w
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: use (1 - p - X * q).reverse
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (hypothesis)
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).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)
have this : (1 - p - X * q).coeff 0 - 1 ∈ I
Tactic: have : (1 - p - X * q).coeff 0 - 1 ∈ I := by simpa using hp.1 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (hypothesis)
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
⊢ (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)
have eq₁ : (↑(y + z) : S) = (↑1 : S)
Tactic: apply_fun (·.1) at eq hw
Cleared hypotheses: eq, hw
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (hypothesis)
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)
⊢ (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)
have hw₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply_fun (·.1) at eq hw
Cleared hypotheses: eq, hw
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
⊢ p.integralNormalization.coeff i =
    if p.degree = (↑i : WithBot ℕ) then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : p.degree = (↑i : WithBot ℕ)
⊢ p.integralNormalization.coeff i = 1
have rw : (if p.degree = (↑i : WithBot ℕ) then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) = 1
Tactic: rw [integralNormalization_coeff, if_pos hi]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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
⊢ p.integralNormalization.coeff i = 1
have rw₁ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [integralNormalization_coeff, if_pos hi]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : p.degree ≠ (↑i : WithBot ℕ)
⊢ p.integralNormalization.coeff i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
have 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)
Tactic: rw [integralNormalization_coeff, if_neg hi]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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)
⊢ p.integralNormalization.coeff i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
have rw₁ : p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
Tactic: rw [integralNormalization_coeff, if_neg hi]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.integralNormalization.degree = p.degree
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
⊢ p.integralNormalization.degree = p.degree
have pos : ∀ (hp : p = 0), p.integralNormalization.degree = p.degree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
pos : ∀ (hp : p = 0), p.integralNormalization.degree = p.degree
⊢ p.integralNormalization.degree = p.degree
have neg : ∀ (hp : ¬p = 0), p.integralNormalization.degree = p.degree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
hp : ¬p = 0
⊢ p.integralNormalization.degree = p.degree
have neg : p.integralNormalization.degree = (↑p.natDegree : WithBot ℕ)
Tactic: rw [degree_eq_natDegree hp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
hp : ¬p = 0
⊢ p.integralNormalization.degree = (↑p.natDegree : WithBot ℕ)
have neg : p.integralNormalization.degree ≤ (↑p.natDegree : WithBot ℕ)
Tactic: refine degree_eq_of_le_of_coeff_ne_zero ?_ (by simp [integralNormalization_coeff_natDegree, *])
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.integralNormalization.natDegree = p.natDegree
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
⊢ p.integralNormalization.natDegree = p.natDegree
have pos : ∀ (hp : p = 0), p.integralNormalization.natDegree = p.natDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Nontrivial R
pos : ∀ (hp : p = 0), p.integralNormalization.natDegree = p.natDegree
⊢ p.integralNormalization.natDegree = p.natDegree
have neg : ∀ (hp : ¬p = 0), p.integralNormalization.natDegree = p.natDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
⊢ p.integralNormalization.coeff i * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
have rw : (if p.degree = (↑i : WithBot ℕ) then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) * p.leadingCoeff ^ i =
  p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
Tactic: rw [integralNormalization_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
⊢ (if p.degree = (↑i : WithBot ℕ) then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) * p.leadingCoeff ^ i =
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
have pos : ∀ (h : p.degree = (↑i : WithBot ℕ)), 1 * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
Tactic: split_ifs with h