R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
⊢ ∃ a_1, ↑(Units.map ↑f) a_1 = a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
⊢ Function.Surjective ↑(Units.map ↑f)
intro a
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ ∃ a_1, ↑(Units.map ↑f) a_1 = a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
⊢ ∃ a_1, ↑(Units.map ↑f) a_1 = a
obtain ⟨b, hb⟩ := hf (a : S)
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ ↑(Units.map ↑f) (IsUnit.unit (_ : IsUnit b)) = a
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ ∃ a_1, ↑(Units.map ↑f) a_1 = a
use (isUnit_of_map_unit f b (by rw [hb]; exact Units.isUnit _)).unit
case intro.a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ ↑(↑(Units.map ↑f) (IsUnit.unit (_ : IsUnit b))) = ↑a
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ ↑(Units.map ↑f) (IsUnit.unit (_ : IsUnit b)) = a
ext
no goals
case intro.a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ ↑(↑(Units.map ↑f) (IsUnit.unit (_ : IsUnit b))) = ↑a
exact hb
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ IsUnit ↑a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ IsUnit (↑f b)
rw [hb]
no goals
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ IsUnit ↑a
exact Units.isUnit _