-- Mathlib/Algebra/Group/Pi/Lemmas.lean
theorem Pi.mulSingle_mul_mulSingle_eq_mulSingle_mul_mulSingle {M : Type*} [CommMonoid M]
    {k l m n : I} {u v : M} (hu : u ≠ 1) (hv : v ≠ 1) :
    (mulSingle k u : I → M) * mulSingle l v = mulSingle m u * mulSingle n v ↔
      k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n

Proof state:
case refine_1.inl
I : Type u
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle k u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = k then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if k = n then v else 1) = (if k = k then u else 1) * if k = l then v else 1
hn : ((if n = k then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
hln : l ≠ n
⊢ v = 1

Tactic:
rcases eq_or_ne k l with (rfl | hkl)

Result:
case refine_1.inl.inl
I : Type u
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle k v = mulSingle k u * mulSingle n v
hk : ((if True then u else 1) * if k = k then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hl : ((if k = k then u else 1) * if True then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hm : ((if True then u else 1) * if k = n then v else 1) = (if k = k then u else 1) * if k = k then v else 1
hn : ((if n = k then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = k then v else 1
hln : k ≠ n
⊢ v = 1

case refine_1.inl.inr
I : Type u
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle k u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = k then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if k = n then v else 1) = (if k = k then u else 1) * if k = l then v else 1
hn : ((if n = k then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
hln : l ≠ n
hkl : k ≠ l
⊢ v = 1

Proof state:
case refine_1.inr.inl
I : Type u
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle m v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = m then v else 1
hm : ((if True then u else 1) * if m = m then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if m = m then u else 1) * if True then v else 1) = (if m = k then u else 1) * if m = l then v else 1
⊢ k = m ∧ l = m ∨ u = v ∧ k = m ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = m

Tactic:
rcases eq_or_ne k l with (rfl | hkl)

Result:
case refine_1.inr.inl.inl
I : Type u
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
h : mulSingle k u * mulSingle k v = mulSingle m u * mulSingle m v
hk : ((if True then u else 1) * if k = k then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hl : ((if k = k then u else 1) * if True then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hm : ((if True then u else 1) * if m = m then v else 1) = (if m = k then u else 1) * if m = k then v else 1
hn : ((if m = m then u else 1) * if True then v else 1) = (if m = k then u else 1) * if m = k then v else 1
⊢ k = m ∧ k = m ∨ u = v ∧ k = m ∧ k = m ∨ u * v = 1 ∧ k = k ∧ m = m

case refine_1.inr.inl.inr
I : Type u
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle m v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = m then u else 1) * if k = m then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = m then v else 1
hm : ((if True then u else 1) * if m = m then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hn : ((if m = m then u else 1) * if True then v else 1) = (if m = k then u else 1) * if m = l then v else 1
hkl : k ≠ l
⊢ k = m ∧ l = m ∨ u = v ∧ k = m ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = m

Proof state:
case refine_1.inr.inr
I : Type u
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = m then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = m then u else 1) * if l = n then v else 1
hm : (if True then u else 1) = if m = l then v else 1
hn : ((if n = m then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
hkm : k ≠ m
hmn : m ≠ n
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n

Tactic:
obtain rfl := (ite_ne_right_iff.mp (ne_of_eq_of_ne hm.symm hu)).1

Result:
case refine_1.inr.inr
I : Type u
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
hkm : k ≠ m
hmn : m ≠ n
h : mulSingle k u * mulSingle m v = mulSingle m u * mulSingle n v
hk : ((if True then u else 1) * if k = m then v else 1) = (if k = m then u else 1) * if k = n then v else 1
hl : ((if m = k then u else 1) * if True then v else 1) = (if m = m then u else 1) * if m = n then v else 1
hm : (if True then u else 1) = if m = m then v else 1
hn : ((if n = m then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = m then v else 1
⊢ k = m ∧ m = n ∨ u = v ∧ k = n ∧ m = m ∨ u * v = 1 ∧ k = m ∧ m = n

Proof state:
case refine_2.inr.inr.intro.intro
I : Type u
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k m : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : u * v = 1
⊢ mulSingle k u * mulSingle k v = mulSingle m u * mulSingle m v

Tactic:
simp_rw [← Pi.mulSingle_mul, h, mulSingle_one]

Result:
no goals

Proof state:
case refine_1.inl
I : Type u
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle k u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = k then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if k = n then v else 1) = (if k = k then u else 1) * if k = l then v else 1
hn : ((if n = k then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
⊢ k = k ∧ l = n ∨ u = v ∧ k = n ∧ l = k ∨ u * v = 1 ∧ k = l ∧ k = n

Tactic:
refine Or.inl ⟨rfl, not_ne_iff.mp fun hln => (hv ?_).elim⟩

Result:
case refine_1.inl
I : Type u
inst✝¹ : DecidableEq I
M : Type u_3
inst✝ : CommMonoid M
k l n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle k u * mulSingle n v
hk : ((if True then u else 1) * if k = l then v else 1) = (if k = k then u else 1) * if k = n then v else 1
hl : ((if l = k then u else 1) * if True then v else 1) = (if l = k then u else 1) * if l = n then v else 1
hm : ((if True then u else 1) * if k = n then v else 1) = (if k = k then u else 1) * if k = l then v else 1
hn : ((if n = k then u else 1) * if True then v else 1) = (if n = k then u else 1) * if n = l then v else 1
hln : l ≠ n
⊢ v = 1