R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y✝ : R
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hf : Function.Surjective ↑f
y : S
⊢ ∃ a, ↑(lift I f H) a = y
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hf : Function.Surjective ↑f
⊢ Function.Surjective ↑(lift I f H)
intro y
case intro
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y : R
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hf : Function.Surjective ↑f
x : R
⊢ ∃ a, ↑(lift I f H) a = ↑f x
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y✝ : R
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hf : Function.Surjective ↑f
y : S
⊢ ∃ a, ↑(lift I f H) a = y
obtain ⟨x, rfl⟩ := hf y
case intro
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y : R
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hf : Function.Surjective ↑f
x : R
⊢ ↑(lift I f H) (↑(mk I) x) = ↑f x
case intro
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y : R
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hf : Function.Surjective ↑f
x : R
⊢ ∃ a, ↑(lift I f H) a = ↑f x
use Ideal.Quotient.mk I x
no goals
case intro
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y : R
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hf : Function.Surjective ↑f
x : R
⊢ ↑(lift I f H) (↑(mk I) x) = ↑f x
simp only [Ideal.Quotient.lift_mk]