R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
b : S
⊢ IsUnit b ∨ IsUnit (1 - b)
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
⊢ ∀ (a : S), IsUnit a ∨ IsUnit (1 - a)
intro b
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
a : R
⊢ IsUnit (↑f a) ∨ IsUnit (1 - ↑f a)
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
b : S
⊢ IsUnit b ∨ IsUnit (1 - b)
obtain ⟨a, rfl⟩ := hf b
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
a : R
⊢ IsUnit (1 - a) → IsUnit (1 - ↑f a)
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
a : R
⊢ IsUnit (↑f a) ∨ IsUnit (1 - ↑f a)
apply (isUnit_or_isUnit_one_sub_self a).imp <| RingHom.isUnit_map _
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
a : R
⊢ IsUnit (1 - a) → IsUnit (↑f (1 - a))
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
a : R
⊢ IsUnit (1 - a) → IsUnit (1 - ↑f a)
rw [← f.map_one, ← f.map_sub]
no goals
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
a : R
⊢ IsUnit (1 - a) → IsUnit (↑f (1 - a))
apply f.isUnit_map