awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Quotient
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])
simp : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) y : R[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)

Tactic:
simp only [RingHom.comp_apply, Quotient.eq_zero_iff_mem, ZeroMemClass.coe_zero]

Premises used: Ideal.Quotient.eq_zero_iff_mem, ZeroMemClass.coe_zero, RingHom.comp_apply
-- Module: Mathlib.RingTheory.Polynomial.Quotient
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])
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])
⊢ 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

Premises used: Ideal.mem_image_of_mem_map_of_surjective, Polynomial.C, RingHom.rangeRestrict_surjective, Polynomial.map_surjective, Ideal.Quotient.mk, RingHom.comp, Polynomial.mapRingHom
-- Module: Mathlib.RingTheory.Polynomial.Quotient
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])

Tactic:
sub_add_cancel (C y) f ▸ I.add_mem (hi' ?_ : C y - f ∈ I) hf.1

Premises used: Polynomial.C, Set.Mem, Eq.rec, Ideal.add_mem, And.left, sub_add_cancel, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Quotient
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])
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)
⊢ Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) y : R[X])

Tactic:
refine sub_add_cancel (C y) f ▸ I.add_mem (hi' ?_ : C y - f ∈ I) hf.1
-- Module: Mathlib.RingTheory.Polynomial.Quotient
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])
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])
⊢ Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) y : R[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]
-- Module: Mathlib.RingTheory.Polynomial.Quotient
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 (α := (↥(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:
hx

Premises used: Set.Mem, setOf
-- Module: Mathlib.RingTheory.Polynomial.Quotient
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 (α := (↥(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:
exact hx
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing.{u_1} R[X]
apply :
  IsField.{u_1} (HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)}))
⊢ IsField R

Tactic:
apply (quotientSpanXSubCAlgEquiv 0).symm.toMulEquiv.isField

Premises used: AlgEquiv.symm, AlgEquiv.toMulEquiv, Polynomial.quotientSpanXSubCAlgEquiv, MulEquiv.isField, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing.{u_1} R[X]
rw : IsMaximal (α := R[X]) (span {HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)})
⊢ IsField.{u_1} (HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)}))

Tactic:
rw [← Quotient.maximal_ideal_iff_isField_quotient]

Premises used: Ideal.Quotient.maximal_ideal_iff_isField_quotient
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing.{u_1} R[X]
⊢ IsMaximal (α := R[X]) (span {HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)})

Tactic:
PrincipalIdealRing.isMaximal_of_irreducible (irreducible_X_sub_C 0)

Premises used: PrincipalIdealRing.isMaximal_of_irreducible, OfNat.ofNat, Polynomial.irreducible_X_sub_C
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing.{u_1} R[X]
⊢ IsMaximal (α := R[X]) (span {HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)})

Tactic:
exact PrincipalIdealRing.isMaximal_of_irreducible (irreducible_X_sub_C 0)

Premises used: PrincipalIdealRing.isMaximal_of_irreducible, OfNat.ofNat, Polynomial.irreducible_X_sub_C
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
I : Ideal R
i : R
hi : i ∈ I
simp :
  Membership.mem (α := MvPolynomial σ R) (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
    ((C : (a : R) → MvPolynomial σ R) i : MvPolynomial σ R)
⊢ 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))

Tactic:
simp only [Function.comp_apply, RingHom.coe_comp, Ideal.Quotient.eq_zero_iff_mem]

Premises used: Ideal.Quotient.eq_zero_iff_mem, RingHom.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
I : Ideal R
i : R
hi : i ∈ I
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
    ((C : (a : R) → MvPolynomial σ R) i : MvPolynomial σ R)

Tactic:
Ideal.mem_map_of_mem _ hi

Premises used: Ideal.mem_map_of_mem, Set.Mem
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
I : Ideal R
i : R
hi : i ∈ I
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
    ((C : (a : R) → MvPolynomial σ R) i : MvPolynomial σ R)

Tactic:
exact Ideal.mem_map_of_mem _ hi

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Polynomial.Quotient
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
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
⊢ 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))

Tactic:
rw [as_sum a]

Premises used: MvPolynomial.as_sum
-- Module: Mathlib.RingTheory.Polynomial.Quotient
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
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
⊢ 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 [coe_eval₂Hom, eval₂_sum]

Premises used: MvPolynomial.eval₂_sum, MvPolynomial.coe_eval₂Hom
-- Module: Mathlib.RingTheory.Polynomial.Quotient
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

Tactic:
Finset.sum_eq_zero fun n _ => ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Quotient
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
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
⊢ 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:
refine Finset.sum_eq_zero fun n _ => ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Quotient
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
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
⊢ 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:
simp only [eval₂_monomial, Function.comp_apply, RingHom.coe_comp]

Premises used: RingHom.coe_comp, Function.comp_apply, MvPolynomial.eval₂_monomial
-- Module: Mathlib.RingTheory.Polynomial.Quotient
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

Tactic:
mul_eq_zero_of_left ?_ _

Premises used: mul_eq_zero_of_left
-- Module: Mathlib.RingTheory.Polynomial.Quotient
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
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))
⊢ 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:
refine mul_eq_zero_of_left ?_ _

Premises used: mul_eq_zero_of_left
-- Module: Mathlib.RingTheory.Polynomial.Quotient
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 (α := 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

Premises used: RingHom.mem_ker, Ideal.mk_ker