awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
i : R →+* ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' :
  Membership.mem (α := R[X] ⧸ I) (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
    ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y : R[X] ⧸ I)
hx :
  Membership.mem (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (γ :=
    Ideal (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
    (map (F := R[X] →+* (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
      (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I)
    ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
        (Subtype.mk (p := fun (x : R[X] ⧸ I) ↦
          Membership.mem (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) x)
          ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y) hx') :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
⊢ Eq (α := ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))
    (Subtype.mk (p := fun (x : R[X] ⧸ I) ↦
        Membership.mem (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) x)
        ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y) hx' :
      ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))
    (0 : ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))
have refine : Eq (α := R[X] ⧸ I)
  ((↑(Subtype.mk (p := fun (x : R[X] ⧸ I) ↦
          Membership.mem (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) x)
          ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y) hx') :
      R[X] ⧸ I) :
    R[X] ⧸ I)
  ((↑0 : R[X] ⧸ I) : R[X] ⧸ I)
Tactic: refine Subtype.ext ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
i : R →+* ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' :
  Membership.mem (α := R[X] ⧸ I) (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
    ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y : R[X] ⧸ I)
hx :
  Membership.mem (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (γ :=
    Ideal (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
    (map (F := R[X] →+* (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
      (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I)
    ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
        (Subtype.mk (p := fun (x : R[X] ⧸ I) ↦
          Membership.mem (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) x)
          ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y) hx') :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
⊢ Eq (α := R[X] ⧸ I)
    ((↑(Subtype.mk (p := fun (x : R[X] ⧸ I) ↦
            Membership.mem (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) x)
            ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y) hx') :
        R[X] ⧸ I) :
      R[X] ⧸ I)
    ((↑0 : R[X] ⧸ I) : R[X] ⧸ I)
have simp : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) y : R[X])
Tactic: simp only [RingHom.comp_apply, Quotient.eq_zero_iff_mem, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
i : R →+* ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' :
  Membership.mem (α := R[X] ⧸ I) (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
    ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y : R[X] ⧸ I)
hx :
  Membership.mem (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (γ :=
    Ideal (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
    (map (F := R[X] →+* (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
      (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I)
    ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
        (Subtype.mk (p := fun (x : R[X] ⧸ I) ↦
          Membership.mem (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) x)
          ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y) hx') :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
this :
  Membership.mem (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (γ :=
    Ideal (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (map (mapRingHom i) I)
    ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
        ((i : (a : R) → ↥((Quotient.mk I).comp C).range) y) :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
⊢ Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) y : R[X])
have obtain : ∀ (f : R[X])
  (hf :
    f ∈ (↑I : Set R[X]) ∧
      Eq (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
        ((mapRingHom i : (a : R[X]) → (↥((Quotient.mk I).comp C).range)[X]) f :
          (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
        ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
            ((i : (a : R) → ↥((Quotient.mk I).comp C).range) y) :
          (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])),
  Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) y : R[X])
Tactic: obtain ⟨f, hf⟩ := mem_image_of_mem_map_of_surjective (Polynomial.mapRingHom i)
      (Polynomial.map_surjective _ (RingHom.rangeRestrict_surjective ((Quotient.mk I).comp C))) this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
i : R →+* ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' :
  Membership.mem (α := R[X] ⧸ I) (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
    ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y : R[X] ⧸ I)
hx :
  Membership.mem (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (γ :=
    Ideal (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
    (map (F := R[X] →+* (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
      (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I)
    ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
        (Subtype.mk (p := fun (x : R[X] ⧸ I) ↦
          Membership.mem (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) x)
          ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y) hx') :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
this :
  Membership.mem (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (γ :=
    Ideal (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (map (mapRingHom i) I)
    ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
        ((i : (a : R) → ↥((Quotient.mk I).comp C).range) y) :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
f : R[X]
hf :
  f ∈ (↑I : Set R[X]) ∧
    Eq (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
      ((mapRingHom i : (a : R[X]) → (↥((Quotient.mk I).comp C).range)[X]) f :
        (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
      ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
          ((i : (a : R) → ↥((Quotient.mk I).comp C).range) y) :
        (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
⊢ Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) y : R[X])
have refine : Membership.mem (γ := Submodule R[X] R[X]) (RingHom.ker (mapRingHom i))
  (HSub.hSub (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) f)
Tactic: refine sub_add_cancel (C y) f ▸ I.add_mem (hi' ?_ : C y - f ∈ I) hf.1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
i : R →+* ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' :
  Membership.mem (α := R[X] ⧸ I) (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
    ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y : R[X] ⧸ I)
hx :
  Membership.mem (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (γ :=
    Ideal (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
    (map (F := R[X] →+* (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
      (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I)
    ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
        (Subtype.mk (p := fun (x : R[X] ⧸ I) ↦
          Membership.mem (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) x)
          ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y) hx') :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
this :
  Membership.mem (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (γ :=
    Ideal (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (map (mapRingHom i) I)
    ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
        ((i : (a : R) → ↥((Quotient.mk I).comp C).range) y) :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
f : R[X]
hf :
  f ∈ (↑I : Set R[X]) ∧
    Eq (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
      ((mapRingHom i : (a : R[X]) → (↥((Quotient.mk I).comp C).range)[X]) f :
        (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
      ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
          ((i : (a : R) → ↥((Quotient.mk I).comp C).range) y) :
        (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
⊢ Membership.mem (γ := Submodule R[X] R[X]) (RingHom.ker (mapRingHom i))
    (HSub.hSub (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) f)
have rw : Eq (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
  ((mapRingHom i : (a : R[X]) → (↥((Quotient.mk I).comp C).range)[X])
      (HSub.hSub (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) f) :
    (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
  (0 : (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
Tactic: rw [RingHom.mem_ker, map_sub, hf.2, sub_eq_zero, coe_mapRingHom, map_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
i : R →+* ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' :
  Membership.mem (α := R[X] ⧸ I) (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
    ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y : R[X] ⧸ I)
hx :
  Membership.mem (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (γ :=
    Ideal (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
    (map (F := R[X] →+* (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
      (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I)
    ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
        (Subtype.mk (p := fun (x : R[X] ⧸ I) ↦
          Membership.mem (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) x)
          ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y) hx') :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
⊢ Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) y : R[X])
have suffices : Membership.mem (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (γ :=
  Ideal (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (map (mapRingHom i) I)
  ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
      ((i : (a : R) → ↥((Quotient.mk I).comp C).range) y) :
    (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
Tactic: suffices C (i y) ∈ I.map (Polynomial.mapRingHom i) by
    obtain ⟨f, hf⟩ := mem_image_of_mem_map_of_surjective (Polynomial.mapRingHom i)
      (Polynomial.map_surjective _ (RingHom.rangeRestrict_surjective ((Quotient.mk I).comp C))) this
    refine sub_add_cancel (C y) f ▸ I.add_mem (hi' ?_ : C y - f ∈ I) hf.1
    rw [RingHom.mem_ker, map_sub, hf.2, sub_eq_zero, coe_mapRingHom, map_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing.{u_1} R[X]
⊢ IsField R
have apply : IsField.{u_1} (HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)}))
Tactic: apply (quotientSpanXSubCAlgEquiv 0).symm.toMulEquiv.isField
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing.{u_1} R[X]
⊢ IsField.{u_1} (HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)}))
have rw : IsMaximal (α := R[X]) (span {HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)})
Tactic: rw [← Quotient.maximal_ideal_iff_isField_quotient]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
I : Ideal R
i : R
hi : i ∈ I
⊢ Eq (α :=
    HasQuotient.Quotient (MvPolynomial σ R) (B := Ideal (MvPolynomial σ R))
      (Ideal.map (F := R →+* MvPolynomial σ R) C I))
    ((RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* MvPolynomial σ R) C I)) C :
          (a : R) → MvPolynomial σ R ⧸ Ideal.map C I)
        i :
      HasQuotient.Quotient (MvPolynomial σ R) (B := Ideal (MvPolynomial σ R))
        (Ideal.map (F := R →+* MvPolynomial σ R) C I))
    (0 :
      HasQuotient.Quotient (MvPolynomial σ R) (B := Ideal (MvPolynomial σ R))
        (Ideal.map (F := R →+* MvPolynomial σ R) C I))
have simp : Membership.mem (α := MvPolynomial σ R) (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
  ((C : (a : R) → MvPolynomial σ R) i : MvPolynomial σ R)
Tactic: simp only [Function.comp_apply, RingHom.coe_comp, Ideal.Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) a
⊢ Eq (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    ((eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X : (a : MvPolynomial σ R) → MvPolynomial σ (R ⧸ I)) a :
      MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    (0 : MvPolynomial.{u_2, u_1} σ (R ⧸ I))
have rw : Eq (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I))
  ((eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X : (a : MvPolynomial σ R) → MvPolynomial σ (R ⧸ I))
    (∑ v ∈ a.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v a)))
  0
Tactic: rw [as_sum a]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) a
⊢ Eq (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    ((eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X : (a : MvPolynomial σ R) → MvPolynomial σ (R ⧸ I))
      (∑ v ∈ a.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v a)))
    0
have rw : Eq (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I))
  (∑ x ∈ a.support,
    eval₂ (R := R) (RingHom.comp C (Ideal.Quotient.mk I)) X ((monomial x : (a : R) → MvPolynomial σ R) (coeff x a)))
  0
Tactic: rw [coe_eval₂Hom, eval₂_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) a
⊢ Eq (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    (∑ x ∈ a.support,
      eval₂ (R := R) (RingHom.comp C (Ideal.Quotient.mk I)) X ((monomial x : (a : R) → MvPolynomial σ R) (coeff x a)))
    0
have refine : ∀ n ∈ a.support,
  Eq (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    (eval₂ (R := R) (RingHom.comp C (Ideal.Quotient.mk I)) X ((monomial n : (a : R) → MvPolynomial σ R) (coeff n a))) 0
Tactic: refine Finset.sum_eq_zero fun n _ => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) a
n : σ →₀ ℕ
h : n ∈ a.support
⊢ Eq (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    (eval₂ (R := R) (RingHom.comp C (Ideal.Quotient.mk I)) X ((monomial n : (a : R) → MvPolynomial σ R) (coeff n a))) 0
have simp : HMul.hMul (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I)) (β := MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    ((C : (a : R ⧸ I) → MvPolynomial σ (R ⧸ I)) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (coeff n a)) :
      MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    (n.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I)) (X n) e :
      MvPolynomial.{u_2, u_1} σ (R ⧸ I)) =
  0
Tactic: simp only [eval₂_monomial, Function.comp_apply, RingHom.coe_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) a
n : σ →₀ ℕ
h : n ∈ a.support
⊢ HMul.hMul (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I)) (β := MvPolynomial.{u_2, u_1} σ (R ⧸ I))
      ((C : (a : R ⧸ I) → MvPolynomial σ (R ⧸ I)) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (coeff n a)) :
        MvPolynomial.{u_2, u_1} σ (R ⧸ I))
      (n.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I)) (X n) e :
        MvPolynomial.{u_2, u_1} σ (R ⧸ I)) =
    0
have refine : Eq (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I))
  ((C : (a : R ⧸ I) → MvPolynomial σ (R ⧸ I)) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (coeff n a)) :
    MvPolynomial.{u_2, u_1} σ (R ⧸ I))
  (0 : MvPolynomial.{u_2, u_1} σ (R ⧸ I))
Tactic: refine mul_eq_zero_of_left ?_ _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (hypothesis)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) a
n : σ →₀ ℕ
h : n ∈ a.support
this : coeff n a ∈ I
⊢ Eq (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    ((C : (a : R ⧸ I) → MvPolynomial σ (R ⧸ I)) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (coeff n a)) :
      MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    (0 : MvPolynomial.{u_2, u_1} σ (R ⧸ I))
have this₁ : Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (coeff n a) : R ⧸ I) (0 : R ⧸ I)
Tactic: rw [← @Ideal.mk_ker R _ I, RingHom.mem_ker] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) a
n : σ →₀ ℕ
h : n ∈ a.support
⊢ Eq (α := MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    ((C : (a : R ⧸ I) → MvPolynomial σ (R ⧸ I)) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (coeff n a)) :
      MvPolynomial.{u_2, u_1} σ (R ⧸ I))
    (0 : MvPolynomial.{u_2, u_1} σ (R ⧸ I))
have suffices : coeff n a ∈ I
Tactic: suffices coeff n a ∈ I by
    rw [← @Ideal.mk_ker R _ I, RingHom.mem_ker] at this
    simp only [this, C_0]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a : k[X]
⊢ (radical a).natDegree ≤ a.natDegree
have pos : ∀ (ha : a = 0), (radical a).natDegree ≤ a.natDegree
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a : k[X]
pos : ∀ (ha : a = 0), (radical a).natDegree ≤ a.natDegree
⊢ (radical a).natDegree ≤ a.natDegree
have neg : ∀ (ha : ¬a = 0), (radical a).natDegree ≤ a.natDegree
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a : k[X]
⊢ divRadical a ∣ (derivative : (a : k[X]) → k[X]) a
have induction : Dvd.dvd.{u_1} (α := k[X]) (divRadical 0) ((derivative : (a : k[X]) → k[X]) 0)
Tactic: induction a using induction_on_coprime
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a : k[X]
induction : Dvd.dvd.{u_1} (α := k[X]) (divRadical 0) ((derivative : (a : k[X]) → k[X]) 0)
⊢ divRadical a ∣ (derivative : (a : k[X]) → k[X]) a
have h1 : ∀ {x : k[X]}, IsUnit x → divRadical x ∣ (derivative : (a : k[X]) → k[X]) x
Tactic: induction a using induction_on_coprime
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a : k[X]
induction : Dvd.dvd.{u_1} (α := k[X]) (divRadical 0) ((derivative : (a : k[X]) → k[X]) 0)
h1 : ∀ {x : k[X]}, IsUnit x → divRadical x ∣ (derivative : (a : k[X]) → k[X]) x
⊢ divRadical a ∣ (derivative : (a : k[X]) → k[X]) a
have hpr : ∀ {p : k[X]} (i : ℕ), Prime p → divRadical (p ^ i) ∣ (derivative : (a : k[X]) → k[X]) (p ^ i)
Tactic: induction a using induction_on_coprime
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a : k[X]
induction : Dvd.dvd.{u_1} (α := k[X]) (divRadical 0) ((derivative : (a : k[X]) → k[X]) 0)
h1 : ∀ {x : k[X]}, IsUnit x → divRadical x ∣ (derivative : (a : k[X]) → k[X]) x
hpr : ∀ {p : k[X]} (i : ℕ), Prime p → divRadical (p ^ i) ∣ (derivative : (a : k[X]) → k[X]) (p ^ i)
⊢ divRadical a ∣ (derivative : (a : k[X]) → k[X]) a
have hcp : ∀ {x y : k[X]},
  IsRelPrime x y →
    divRadical x ∣ (derivative : (a : k[X]) → k[X]) x →
      divRadical y ∣ (derivative : (a : k[X]) → k[X]) y → divRadical (x * y) ∣ (derivative : (a : k[X]) → k[X]) (x * y)
Tactic: induction a using induction_on_coprime
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
⊢ Dvd.dvd.{u_1} (α := k[X]) (divRadical 0) ((derivative : (a : k[X]) → k[X]) 0)
have case : Dvd.dvd.{u_1} (α := k[X]) (divRadical 0) 0
Tactic: case h0 =>
    rw [derivative_zero]
    apply dvd_zero
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Radical (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
p : k[X]
i : ℕ
hp : Prime p
⊢ divRadical (p ^ i) ∣ (derivative : (a : k[X]) → k[X]) (p ^ i)
have zero : divRadical (HPow.hPow (β := ℕ) p 0) ∣ (derivative : (a : k[X]) → k[X]) (HPow.hPow (β := ℕ) p 0)
Tactic: cases i
Cleared hypotheses: i