awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f g : (R ⧸ I)[X]
⊢ (eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
          ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
        (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
      (f + g) =
    HAdd.hAdd (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I)) (β :=
      HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
      ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
              ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
            (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
          f :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
      ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
              ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
            (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
          g :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))

Tactic:
simp only [eval₂_add, coe_eval₂RingHom]

Premises used: Polynomial.coe_eval₂RingHom, Polynomial.eval₂_add
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : R[X]
rw : eval X (Polynomial.map (RingHom.comp C (Quotient.mk I)) f) = Polynomial.map (Quotient.mk I) f
rw₁ : eval X (Polynomial.map C (Polynomial.map (Quotient.mk I) f)) = Polynomial.map (Quotient.mk I) f
rw₂ : eval₂ C X (Polynomial.map (Quotient.mk I) f) = Polynomial.map (Quotient.mk I) f
rw₃ rw₄ : Polynomial.map (Quotient.mk I) f = Polynomial.map (Quotient.mk I) f
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X f = Polynomial.map (Quotient.mk I) f

Tactic:
rw [eval₂_eq_eval_map, ← Polynomial.map_map, ← eval₂_eq_eval_map, Polynomial.eval₂_C_X]

Premises used: Polynomial.eval₂_C_X, Polynomial.map_map, Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : R[X]
a :
  Eq (α := (R ⧸ I)[X])
    ((I.polynomialQuotientEquivQuotientPolynomial.symm : (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
        ((I.polynomialQuotientEquivQuotientPolynomial : (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
          (Polynomial.map (Quotient.mk I) f)) :
      (R ⧸ I)[X])
    ((I.polynomialQuotientEquivQuotientPolynomial.symm : (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
        ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) f) :
      (R ⧸ I)[X])
⊢ Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
    ((I.polynomialQuotientEquivQuotientPolynomial : (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
        (Polynomial.map (Quotient.mk I) f) :
      HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
    ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) f :
      HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))

Tactic:
apply (polynomialQuotientEquivQuotientPolynomial I).symm.injective

Premises used: RingEquiv.injective, Ideal.polynomialQuotientEquivQuotientPolynomial, RingEquiv.symm
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : R[X]
a :
  Polynomial.map (Quotient.mk I) f =
    (I.polynomialQuotientEquivQuotientPolynomial.symm : (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
      ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) f)
a₁ a₂ : Polynomial.map (Quotient.mk I) f = Polynomial.map (Quotient.mk I) f
⊢ Eq (α := (R ⧸ I)[X])
    ((I.polynomialQuotientEquivQuotientPolynomial.symm : (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
        ((I.polynomialQuotientEquivQuotientPolynomial : (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
          (Polynomial.map (Quotient.mk I) f)) :
      (R ⧸ I)[X])
    ((I.polynomialQuotientEquivQuotientPolynomial.symm : (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
        ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) f) :
      (R ⧸ I)[X])

Tactic:
rw [RingEquiv.symm_apply_apply, polynomialQuotientEquivQuotientPolynomial_symm_mk]

Premises used: RingEquiv.symm_apply_apply, Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
h : P.IsPrime
⊢ IsDomain.{u_1} (HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C P))

Tactic:
MulEquiv.isDomain (Polynomial (R ⧸ P)) (polynomialQuotientEquivQuotientPolynomial P).symm

Premises used: Polynomial, HasQuotient.Quotient, MulEquiv.isDomain, Ideal.polynomialQuotientEquivQuotientPolynomial, MulEquivClass.toMulEquiv, RingEquiv.symm
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
x : ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
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]) x :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
i : R →+* ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
⊢ RingHom.ker (mapRingHom i) ≤ I

Tactic:
fun f hf => polynomial_mem_ideal_of_coeff_mem_ideal I f fun n => ?_

Premises used: Set.Mem, Ideal.polynomial_mem_ideal_of_coeff_mem_ideal
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
x : ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
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]) x :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
i : R →+* ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
refine :
  ∀ (f : R[X]) (hf : Membership.mem (γ := Submodule R[X] R[X]) (RingHom.ker (mapRingHom i)) f) (n : ℕ),
    Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C I) (f.coeff n)
⊢ RingHom.ker (mapRingHom i) ≤ I

Tactic:
refine fun f hf => polynomial_mem_ideal_of_coeff_mem_ideal I f fun n => ?_

Premises used: Ideal.polynomial_mem_ideal_of_coeff_mem_ideal
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
x : ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
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]) x :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
i : R →+* ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
hf : Membership.mem (γ := Submodule R[X] R[X]) (RingHom.ker (mapRingHom i)) f
n : ℕ
rw : Eq (α := R[X] ⧸ I) ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) (f.coeff n) : R[X] ⧸ I) (0 : R[X] ⧸ I)
⊢ Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C I) (f.coeff n)

Tactic:
rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]

Premises used: Ideal.Quotient.eq_zero_iff_mem, RingHom.comp_apply, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
x : ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
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]) x :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
i : R →+* ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
hf : Membership.mem (γ := Submodule R[X] R[X]) (RingHom.ker (mapRingHom i)) f
n : ℕ
rw :
  ∀ (hf : Polynomial.map i f = 0) (n : ℕ),
    Eq (α := R[X] ⧸ I) ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) (f.coeff n) : R[X] ⧸ I) (0 : R[X] ⧸ I)
⊢ Eq (α := R[X] ⧸ I) ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) (f.coeff n) : R[X] ⧸ I) (0 : R[X] ⧸ I)

Tactic:
rw [RingHom.mem_ker, coe_mapRingHom] at hf

Premises used: RingHom.mem_ker, Polynomial.coe_mapRingHom
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
x : ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
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]) x :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
i : R →+* ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
hf : Polynomial.map i f = 0
n : ℕ
⊢ Eq.{u_1 + 1} (α := ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))
    ((fun (f : (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) ↦ f.coeff n) (Polynomial.map i f))
    ((fun (f : (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) ↦ f.coeff n) 0)

Tactic:
replace hf := congr_arg (fun f : Polynomial _ => f.coeff n) hf
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
x : ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
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]) x :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
i : R →+* ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
n : ℕ
hf :
  Eq.{u_1 + 1} (α := ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))
    ((fun (f : (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) ↦ f.coeff n) (Polynomial.map i f))
    ((fun (f : (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) ↦ f.coeff n) 0)
⊢ Eq (α := ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))
    ((i : (a : R) → ↥((Quotient.mk I).comp C).range) (f.coeff n) :
      ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))
    (0 : ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))

Tactic:
simp only [coeff_map, coeff_zero] at hf

Premises used: Polynomial.coeff_map, Polynomial.coeff_zero
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
x : ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
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]) x :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
i : R →+* ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
n : ℕ
hf :
  Eq (α := ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))
    ((i : (a : R) → ↥((Quotient.mk I).comp C).range) (f.coeff n) :
      ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))
    (0 : ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))
rwa :
  ∀
    (hf :
      Eq.{u_1 + 1} (α := R[X] ⧸ I) (↑((i : (a : R) → ↥((Quotient.mk I).comp C).range) (f.coeff n)) : R[X] ⧸ I)
        (↑0 : R[X] ⧸ I)),
    Eq (α := R[X] ⧸ I) ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) (f.coeff n) : R[X] ⧸ I) (0 : R[X] ⧸ I)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (hf :
      Eq (α := R[X] ⧸ I) ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) (f.coeff n) : R[X] ⧸ I)
        ((↑0 : R[X] ⧸ I) : R[X] ⧸ I)),
    Eq (α := R[X] ⧸ I) ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) (f.coeff n) : R[X] ⧸ I) (0 : R[X] ⧸ I)
⊢ Eq (α := R[X] ⧸ I) ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) (f.coeff n) : R[X] ⧸ I) (0 : R[X] ⧸ I)

Tactic:
rwa [Subtype.ext_iff, RingHom.coe_rangeRestrict] at hf

Premises used: Subtype.ext_iff, RingHom.coe_rangeRestrict
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
x : ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
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]) x :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
i : R →+* ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
⊢ RingHom.ker (mapRingHom i) ≤ I

Tactic:
have hi' : RingHom.ker (Polynomial.mapRingHom i) ≤ I := by
    refine fun f hf => polynomial_mem_ideal_of_coeff_mem_ideal I f fun n => ?_
    rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]
    rw [RingHom.mem_ker, coe_mapRingHom] at hf
    replace hf := congr_arg (fun f : Polynomial _ => f.coeff n) hf
    simp only [coeff_map, coeff_zero] at hf
    rwa [Subtype.ext_iff, RingHom.coe_rangeRestrict] at hf
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
x : ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
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]) x :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[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
obtain :
  ∀ (x : R[X] ⧸ I)
    (hx' : Membership.mem (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) x)
    (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) x
              hx') :
          (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[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) x hx' =
      0
⊢ x = 0

Tactic:
obtain ⟨x, hx'⟩ := x
-- 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
x : R[X] ⧸ I
hx' : Membership.mem (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) x
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) x hx') :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
obtain :
  ∀ (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)))
⊢ 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) x hx' =
    0

Tactic:
obtain ⟨y, rfl⟩ := RingHom.mem_range.1 hx'

Premises used: RingHom.mem_range, Iff.mp, rfl
-- 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])
⊢ 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)))

Tactic:
Subtype.ext ?_

Premises used: Subtype.ext
-- 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])
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)
⊢ 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)))

Tactic:
refine Subtype.ext ?_

Premises used: Subtype.ext