Theorem: Ideal.Quotient.rel_le_ker (DividedPowers/DPAlgebra/Misc.lean)

State before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R → R → Prop
hr : I = ofRel r
f : R →+* S
hf : ∀ {a b : R}, r a b → f a = f b
⊢ I ≤ RingHom.ker f
Tactic:
rw [hr, ofRel, Submodule.span_le]
State after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R → R → Prop
hr : I = ofRel r
f : R →+* S
hf : ∀ {a b : R}, r a b → f a = f b
⊢ {x | ∃ a b, r a b ∧ x + b = a} ⊆ ↑(RingHom.ker f)

State before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R → R → Prop
hr : I = ofRel r
f : R →+* S
hf : ∀ {a b : R}, r a b → f a = f b
⊢ {x | ∃ a b, r a b ∧ x + b = a} ⊆ ↑(RingHom.ker f)
Tactic:
rintro x ⟨a, b, hx, hab⟩
State after:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R → R → Prop
hr : I = ofRel r
f : R →+* S
hf : ∀ {a b : R}, r a b → f a = f b
x a b : R
hx : r a b
hab : x + b = a
⊢ x ∈ ↑(RingHom.ker f)

State before:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R → R → Prop
hr : I = ofRel r
f : R →+* S
hf : ∀ {a b : R}, r a b → f a = f b
x a b : R
hx : r a b
hab : x + b = a
⊢ x ∈ ↑(RingHom.ker f)
Tactic:
rw [eq_sub_iff_add_eq.mpr hab, SetLike.mem_coe, RingHom.mem_ker, map_sub, sub_eq_zero, hf hx]
State after:
no goals