R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
a b : S
hab : IsUnit (a + b)
⊢ IsUnit a ∨ IsUnit b
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
⊢ ∀ (a b : S), IsUnit (a + b) → IsUnit a ∨ IsUnit b
intro a b hab
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
b : S
a : R
hab : IsUnit (↑f a + b)
⊢ IsUnit (↑f a) ∨ IsUnit b
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
a b : S
hab : IsUnit (a + b)
⊢ IsUnit a ∨ IsUnit b
obtain ⟨a, rfl⟩ := hf a
case intro.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
a b : R
hab : IsUnit (↑f a + ↑f b)
⊢ IsUnit (↑f a) ∨ IsUnit (↑f b)
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
b : S
a : R
hab : IsUnit (↑f a + b)
⊢ IsUnit (↑f a) ∨ IsUnit b
obtain ⟨b, rfl⟩ := hf b
case intro.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
a b : R
hab : IsUnit (↑f (a + b))
⊢ IsUnit (↑f a) ∨ IsUnit (↑f b)
case intro.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
a b : R
hab : IsUnit (↑f a + ↑f b)
⊢ IsUnit (↑f a) ∨ IsUnit (↑f b)
rw [← map_add] at hab
no goals
case intro.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
a b : R
hab : IsUnit (↑f (a + b))
⊢ IsUnit (↑f a) ∨ IsUnit (↑f b)
exact
  (isUnit_or_isUnit_of_isUnit_add <| IsLocalRingHom.map_nonunit _ hab).imp f.isUnit_map
    f.isUnit_map