From f7a7c27234fef797a54eb3b5b08cde13bac66f57 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Mon, 16 May 2022 09:19:03 +0000
Subject: [PATCH] chore(ring_theory/ideal/local_ring): golf some proofs, add
 missing lemma (#14157)

---
 src/algebra/group/units.lean          | 5 ++++-
 src/ring_theory/ideal/local_ring.lean | 8 ++++----
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/algebra/group/units.lean b/src/algebra/group/units.lean
index a46b542432168..eb5b3a4476dd8 100644
--- a/src/algebra/group/units.lean
+++ b/src/algebra/group/units.lean
@@ -186,11 +186,14 @@ by rw [mul_assoc, inv_mul, mul_one]
 @[to_additive] theorem mul_inv_eq_iff_eq_mul {a c : α} : a * ↑b⁻¹ = c ↔ a = c * b :=
 ⟨λ h, by rw [← h, inv_mul_cancel_right], λ h, by rw [h, mul_inv_cancel_right]⟩
 
-lemma inv_eq_of_mul_eq_one_right {u : αˣ} {a : α} (h : ↑u * a = 1) : ↑u⁻¹ = a :=
+@[to_additive] lemma inv_eq_of_mul_eq_one_right {u : αˣ} {a : α} (h : ↑u * a = 1) : ↑u⁻¹ = a :=
 calc ↑u⁻¹ = ↑u⁻¹ * 1 : by rw mul_one
       ... = ↑u⁻¹ * ↑u * a : by rw [←h, ←mul_assoc]
       ... = a : by rw [u.inv_mul, one_mul]
 
+@[to_additive] lemma eq_iff_inv_mul {u : αˣ} {a : α} : ↑u = a ↔ ↑u⁻¹ * a = 1 :=
+⟨inv_mul_of_eq, inv_inv u ▸ inv_eq_of_mul_eq_one_right⟩
+
 lemma inv_unique {u₁ u₂ : αˣ} (h : (↑u₁ : α) = ↑u₂) : (↑u₁⁻¹ : α) = ↑u₂⁻¹ :=
 inv_eq_of_mul_eq_one_right $ by rw [h, u₂.mul_inv]
 
diff --git a/src/ring_theory/ideal/local_ring.lean b/src/ring_theory/ideal/local_ring.lean
index a5fbcac43506c..5f236d028e751 100644
--- a/src/ring_theory/ideal/local_ring.lean
+++ b/src/ring_theory/ideal/local_ring.lean
@@ -84,9 +84,9 @@ lemma is_unit_or_is_unit_of_is_unit_add {a b : R} (h : is_unit (a + b)) :
   is_unit a ∨ is_unit b :=
 begin
   rcases h with ⟨u, hu⟩,
-  replace hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1, from by rw [←mul_add, ←hu, units.inv_mul],
-  cases is_unit_or_is_unit_of_add_one hu; [left, right];
-    exact (is_unit_of_mul_is_unit_right (by assumption))
+  rw [units.eq_iff_inv_mul, mul_add] at hu,
+  apply or.imp _ _ (is_unit_or_is_unit_of_add_one hu);
+    exact is_unit_of_mul_is_unit_right,
 end
 
 lemma nonunits_add {a b : R} (ha : a ∈ nonunits R) (hb : b ∈ nonunits R) : a + b ∈ nonunits R:=
@@ -302,7 +302,7 @@ begin
   intros a b hab,
   obtain ⟨a, rfl⟩ := hf a,
   obtain ⟨b, rfl⟩ := hf b,
-  replace hab : is_unit (f (a + b)), from by simpa only [map_add] using hab,
+  rw ←map_add at hab,
   exact (is_unit_or_is_unit_of_is_unit_add $ is_local_ring_hom.map_nonunit _ hab).imp
     f.is_unit_map f.is_unit_map
 end