R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
i : ℕ
⊢ ∀ (m : { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1)) }), ↑(powQuotSuccInclusion f p P i) m = 0 → m = 0
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
i : ℕ
⊢ Function.Injective ↑(powQuotSuccInclusion f p P i)
rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
case mk
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
i : ℕ
x : S ⧸ P ^ e
hx : x ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hx0 : ↑(powQuotSuccInclusion f p P i) { val := x, property := hx } = 0
⊢ { val := x, property := hx } = 0
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
i : ℕ
⊢ ∀ (m : { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1)) }), ↑(powQuotSuccInclusion f p P i) m = 0 → m = 0
rintro ⟨x, hx⟩ hx0
case mk
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
i : ℕ
x : S ⧸ P ^ e
hx : x ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hx0 : ↑(↑(powQuotSuccInclusion f p P i) { val := x, property := hx }) = ↑0
⊢ ↑{ val := x, property := hx } = ↑0
case mk
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
i : ℕ
x : S ⧸ P ^ e
hx : x ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hx0 : ↑(powQuotSuccInclusion f p P i) { val := x, property := hx } = 0
⊢ { val := x, property := hx } = 0
rw [Subtype.ext_iff] at hx0 ⊢
no goals
case mk
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
i : ℕ
x : S ⧸ P ^ e
hx : x ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hx0 : ↑(↑(powQuotSuccInclusion f p P i) { val := x, property := hx }) = ↑0
⊢ ↑{ val := x, property := hx } = ↑0
rwa [powQuotSuccInclusion_apply_coe] at hx0