R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
⊢ x = 0
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ x = 0
let i := ((Quotient.mk I).comp C).rangeRestrict
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
⊢ x = 0
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
⊢ x = 0
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
case mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (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' : x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx : ↑C { val := x, property := hx' } ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ { val := x, property := hx' } = 0
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
⊢ x = 0
obtain ⟨x, hx'⟩ := x
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } = 0
case mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (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' : x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx : ↑C { val := x, property := hx' } ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ { val := x, property := hx' } = 0
obtain ⟨y, rfl⟩ := RingHom.mem_range.1 hx'
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ ↑{ val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } = ↑0
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } = 0
refine' Subtype.eq _
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ ↑C y ∈ I
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ ↑{ val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } = ↑0
simp only [RingHom.comp_apply, Quotient.eq_zero_iff_mem, ZeroMemClass.coe_zero]
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ ↑C (↑i y) ∈ map (mapRingHom i) I
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ ↑C y ∈ I
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, RingHom.map_sub, hf.2, sub_eq_zero, coe_mapRingHom, map_C]
no goals
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ ↑C (↑i y) ∈ map (mapRingHom i) I
exact hx
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ coeff f n ∈ comap C I
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
⊢ RingHom.ker (mapRingHom i) ≤ I
refine' fun f hf => polynomial_mem_ideal_of_coeff_mem_ideal I f fun n => _
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ coeff f n ∈ comap C I
rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
hf : Polynomial.map i f = 0
n : ℕ
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
rw [RingHom.mem_ker, coe_mapRingHom] at hf
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
n : ℕ
hf : (fun f => coeff f n) (Polynomial.map i f) = (fun f => coeff f n) 0
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
hf : Polynomial.map i f = 0
n : ℕ
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
replace hf := congr_arg (fun f : Polynomial _ => f.coeff n) hf
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
n : ℕ
hf : ↑(RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)) (coeff f n) = 0
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
n : ℕ
hf : (fun f => coeff f n) (Polynomial.map i f) = (fun f => coeff f n) 0
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
simp only [coeff_map, coeff_zero] at hf
no goals
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
n : ℕ
hf : ↑(RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)) (coeff f n) = 0
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
rwa [Subtype.ext_iff, RingHom.coe_rangeRestrict] at hf
case intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
this : ↑C (↑i y) ∈ map (mapRingHom i) I
f : R[X]
hf : f ∈ ↑I ∧ ↑(mapRingHom i) f = ↑C (↑i y)
⊢ ↑C y ∈ I
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
this : ↑C (↑i y) ∈ map (mapRingHom i) I
⊢ ↑C y ∈ I
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
case intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
this : ↑C (↑i y) ∈ map (mapRingHom i) I
f : R[X]
hf : f ∈ ↑I ∧ ↑(mapRingHom i) f = ↑C (↑i y)
⊢ ↑C y - f ∈ RingHom.ker (mapRingHom i)
case intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
this : ↑C (↑i y) ∈ map (mapRingHom i) I
f : R[X]
hf : f ∈ ↑I ∧ ↑(mapRingHom i) f = ↑C (↑i y)
⊢ ↑C y ∈ I
refine' sub_add_cancel (C y) f ▸ I.add_mem (hi' _ : C y - f ∈ I) hf.1
no goals
case intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
this : ↑C (↑i y) ∈ map (mapRingHom i) I
f : R[X]
hf : f ∈ ↑I ∧ ↑(mapRingHom i) f = ↑C (↑i y)
⊢ ↑C y - f ∈ RingHom.ker (mapRingHom i)
rw [RingHom.mem_ker, RingHom.map_sub, hf.2, sub_eq_zero, coe_mapRingHom, map_C]