[GOAL]
β : Type u_1
M : Type ?u.36709
α : Type ?u.36708
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
⊢ ↑mk.symm c₁ • a = ↑mk.symm c₂ • a
[PROOFSTEP]
rcases exists_pair_ne β with ⟨x, y, hne⟩
[GOAL]
case intro.intro
β : Type u_1
M : Type ?u.36709
α : Type ?u.36708
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
x y : β
hne : x ≠ y
⊢ ↑mk.symm c₁ • a = ↑mk.symm c₂ • a
[PROOFSTEP]
contrapose! hne
[GOAL]
case intro.intro
β : Type u_1
M : Type ?u.36709
α : Type ?u.36708
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
x y : β
hne : ↑mk.symm c₁ • a ≠ ↑mk.symm c₂ • a
⊢ x = y
[PROOFSTEP]
haveI := Classical.decEq α
[GOAL]
case intro.intro
β : Type u_1
M : Type ?u.36709
α : Type ?u.36708
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
x y : β
hne : ↑mk.symm c₁ • a ≠ ↑mk.symm c₂ • a
this : DecidableEq α
⊢ x = y
[PROOFSTEP]
replace h := congr_fun (h (update (const α x) (mk.symm c₂ • a) y)) a
[GOAL]
case intro.intro
β : Type u_1
M : Type ?u.36709
α : Type ?u.36708
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
a : α
x y : β
hne : ↑mk.symm c₁ • a ≠ ↑mk.symm c₂ • a
this : DecidableEq α
h : (c₁ • update (const α x) (↑mk.symm c₂ • a) y) a = (c₂ • update (const α x) (↑mk.symm c₂ • a) y) a
⊢ x = y
[PROOFSTEP]
simpa [smul_apply, hne] using h
