case intro
α : Type u_1
β : Type ?u.351988
γ : Type ?u.351991
δ : Type ?u.351994
inst✝ : CancelCommMonoidWithZero α
p b : α
hp : p ≠ 0
a : αˣ
ha : p * b * ↑a = p
⊢ IsUnit b
α : Type u_1
β : Type ?u.351988
γ : Type ?u.351991
δ : Type ?u.351994
inst✝ : CancelCommMonoidWithZero α
p b : α
h : p * b ~ᵤ p
hp : p ≠ 0
⊢ IsUnit b
cases' h with a ha
case intro
α : Type u_1
β : Type ?u.351988
γ : Type ?u.351991
δ : Type ?u.351994
inst✝ : CancelCommMonoidWithZero α
p b : α
hp : p ≠ 0
a : αˣ
ha : p * b * ↑a = p
⊢ p * (b * ↑a) = p * 1
case intro
α : Type u_1
β : Type ?u.351988
γ : Type ?u.351991
δ : Type ?u.351994
inst✝ : CancelCommMonoidWithZero α
p b : α
hp : p ≠ 0
a : αˣ
ha : p * b * ↑a = p
⊢ IsUnit b
refine' isUnit_of_mul_eq_one b a ((mul_right_inj' hp).mp _)
no goals
case intro
α : Type u_1
β : Type ?u.351988
γ : Type ?u.351991
δ : Type ?u.351994
inst✝ : CancelCommMonoidWithZero α
p b : α
hp : p ≠ 0
a : αˣ
ha : p * b * ↑a = p
⊢ p * (b * ↑a) = p * 1
rwa [← mul_assoc, mul_one]