case inl
R : Type ?u.35696
R' : Type ?u.35699
M : Type ?u.35702
M' : Type ?u.35705
α : Type u_1
β : Type u_2
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
x : β
⊢ (0 • x)⁻¹ = 0⁻¹ • x⁻¹

case inr
R : Type ?u.35696
R' : Type ?u.35699
M : Type ?u.35702
M' : Type ?u.35705
α : Type u_1
β : Type u_2
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
R : Type ?u.35696
R' : Type ?u.35699
M : Type ?u.35702
M' : Type ?u.35705
α : Type u_1
β : Type u_2
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
obtain rfl | hc := eq_or_ne c 0
case inr.inl
R : Type ?u.35696
R' : Type ?u.35699
M : Type ?u.35702
M' : Type ?u.35705
α : Type u_1
β : Type u_2
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
hc : c ≠ 0
⊢ (c • 0)⁻¹ = c⁻¹ • 0⁻¹

case inr.inr
R : Type ?u.35696
R' : Type ?u.35699
M : Type ?u.35702
M' : Type ?u.35705
α : Type u_1
β : Type u_2
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
hx : x ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
case inr
R : Type ?u.35696
R' : Type ?u.35699
M : Type ?u.35702
M' : Type ?u.35705
α : Type u_1
β : Type u_2
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
obtain rfl | hx := eq_or_ne x 0
no goals
case inl
R : Type ?u.35696
R' : Type ?u.35699
M : Type ?u.35702
M' : Type ?u.35705
α : Type u_1
β : Type u_2
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
x : β
⊢ (0 • x)⁻¹ = 0⁻¹ • x⁻¹
simp only [inv_zero, zero_smul]
no goals
case inr.inl
R : Type ?u.35696
R' : Type ?u.35699
M : Type ?u.35702
M' : Type ?u.35705
α : Type u_1
β : Type u_2
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
hc : c ≠ 0
⊢ (c • 0)⁻¹ = c⁻¹ • 0⁻¹
simp only [inv_zero, smul_zero]
case inr.inr
R : Type ?u.35696
R' : Type ?u.35699
M : Type ?u.35702
M' : Type ?u.35705
α : Type u_1
β : Type u_2
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
hx : x ≠ 0
⊢ c⁻¹ • x⁻¹ * c • x = 1
case inr.inr
R : Type ?u.35696
R' : Type ?u.35699
M : Type ?u.35702
M' : Type ?u.35705
α : Type u_1
β : Type u_2
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
hx : x ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
refine' inv_eq_of_mul_eq_one_left _
no goals
case inr.inr
R : Type ?u.35696
R' : Type ?u.35699
M : Type ?u.35702
M' : Type ?u.35705
α : Type u_1
β : Type u_2
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
hx : x ≠ 0
⊢ c⁻¹ • x⁻¹ * c • x = 1
rw [smul_mul_smul, inv_mul_cancel hc, inv_mul_cancel hx, one_smul]