Theorem: Ideal.ker_lift (GlimpseOfLean/Library/Basic.lean)

State before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.16994
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)
Tactic:
have : comap ((Quotient.lift I f H).comp (Quotient.mk I)) ⊥ = ker f := rfl
State after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.16994
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : comap ((Quotient.lift I f H).comp (Quotient.mk I)) ⊥ = ker f
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)

State before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.16994
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : comap ((Quotient.lift I f H).comp (Quotient.mk I)) ⊥ = ker f
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)
Tactic:
rw [← comap_comap] at this
State after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.16994
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : comap (Quotient.mk I) (comap (Quotient.lift I f H) ⊥) = ker f
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)

State before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.16994
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : comap (Quotient.mk I) (comap (Quotient.lift I f H) ⊥) = ker f
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)
Tactic:
apply_fun map (Quotient.mk I) at this
State after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.16994
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : map (Quotient.mk I) (comap (Quotient.mk I) (comap (Quotient.lift I f H) ⊥)) = map (Quotient.mk I) (ker f)
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)

State before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.16994
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : map (Quotient.mk I) (comap (Quotient.mk I) (comap (Quotient.lift I f H) ⊥)) = map (Quotient.mk I) (ker f)
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)
Tactic:
rwa [map_comap_of_surjective _ Quotient.mk_surjective] at this
State after:
no goals