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 : HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I)
f p q : R[X]
hp :
  eval₂ (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)
      (eval₂ (RingHom.comp C (Quotient.mk I)) X p) =
    (Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) p
hq :
  eval₂ (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)
      (eval₂ (RingHom.comp C (Quotient.mk I)) X q) =
    (Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) q
⊢ eval₂ (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)
        (eval₂ (RingHom.comp C (Quotient.mk I)) X p) +
      eval₂ (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)
        (eval₂ (RingHom.comp C (Quotient.mk I)) X q) =
    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))
      ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) p :
        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) q :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
have mk : HAdd.hAdd (α := 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) p :
      HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
    (eval₂ (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) sorry)
      ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X)
      (eval₂ (RingHom.comp C (Quotient.mk I)) X q)) =
  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))
    ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) p :
      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) q :
      HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
Tactic: rw [hp, hq]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : R[X]
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X f = Polynomial.map (Quotient.mk I) f
have rw : eval X (Polynomial.map (RingHom.comp C (Quotient.mk I)) f) = Polynomial.map (Quotient.mk I) f
Tactic: rw [eval₂_eq_eval_map, ← Polynomial.map_map, ← eval₂_eq_eval_map, Polynomial.eval₂_C_X]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
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
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X f = Polynomial.map (Quotient.mk I) f
have rw₁ : eval X (Polynomial.map C (Polynomial.map (Quotient.mk I) f)) = Polynomial.map (Quotient.mk I) f
Tactic: rw [eval₂_eq_eval_map, ← Polynomial.map_map, ← eval₂_eq_eval_map, Polynomial.eval₂_C_X]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
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
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X f = Polynomial.map (Quotient.mk I) f
have rw₂ : eval₂ C X (Polynomial.map (Quotient.mk I) f) = Polynomial.map (Quotient.mk I) f
Tactic: rw [eval₂_eq_eval_map, ← Polynomial.map_map, ← eval₂_eq_eval_map, Polynomial.eval₂_C_X]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
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
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X f = Polynomial.map (Quotient.mk I) f
have rw₃ : Polynomial.map (Quotient.mk I) f = Polynomial.map (Quotient.mk I) f
Tactic: rw [eval₂_eq_eval_map, ← Polynomial.map_map, ← eval₂_eq_eval_map, Polynomial.eval₂_C_X]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : R[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))
have 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])
Tactic: apply (polynomialQuotientEquivQuotientPolynomial I).symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : R[X]
⊢ 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])
have 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)
Tactic: rw [RingEquiv.symm_apply_apply, polynomialQuotientEquivQuotientPolynomial_symm_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
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)
⊢ 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])
have a₁ : Polynomial.map (Quotient.mk I) f = Polynomial.map (Quotient.mk I) f
Tactic: rw [RingEquiv.symm_apply_apply, polynomialQuotientEquivQuotientPolynomial_symm_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
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
have 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)
Tactic: refine fun f hf => polynomial_mem_ideal_of_coeff_mem_ideal I f fun n => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
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 : ℕ
⊢ Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C I) (f.coeff n)
have 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)
Tactic: rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
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 : ℕ
⊢ 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)
have 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)
Tactic: rw [RingHom.mem_ker, coe_mapRingHom] at hf
Cleared hypotheses: hf, n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (hypothesis)
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 (α := R[X] ⧸ I) ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) (f.coeff n) : R[X] ⧸ I) (0 : R[X] ⧸ I)
have 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)
Tactic: replace hf := congr_arg (fun f : Polynomial _ => f.coeff n) hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (hypothesis)
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 (α := R[X] ⧸ I) ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) (f.coeff n) : R[X] ⧸ I) (0 : R[X] ⧸ I)
have 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)))
Tactic: simp only [coeff_map, coeff_zero] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
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)))
⊢ 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)
have 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)
Tactic: rwa [Subtype.ext_iff, RingHom.coe_rangeRestrict] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
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)
⊢ 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)
have 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)
Tactic: rwa [Subtype.ext_iff, RingHom.coe_rangeRestrict] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (hypothesis)
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)
⊢ x = 0
have hi' : 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
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
⊢ x = 0
have 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
Tactic: obtain ⟨x, hx'⟩ := x
Cleared hypotheses: x, hx
-- 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
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
have 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)))
Tactic: obtain ⟨y, rfl⟩ := RingHom.mem_range.1 hx'
Cleared hypotheses: x, hx', hx