Theorem: SubMulAction.inclusion_injective (Jordan/SubMulActions.lean)

State before:
M : Type u_1
N : Type ?u.3198
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
⊢ Function.Injective ⇑(inclusion s)
Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩ h
State after:
case mk.mk
M : Type u_1
N : Type ?u.3198
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h : (inclusion s) { val := a, property := ha } = (inclusion s) { val := b, property := hb }
⊢ { val := a, property := ha } = { val := b, property := hb }

State before:
case mk.mk
M : Type u_1
N : Type ?u.3198
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h : (inclusion s) { val := a, property := ha } = (inclusion s) { val := b, property := hb }
⊢ { val := a, property := ha } = { val := b, property := hb }
Tactic:
simp only [Subtype.mk.injEq]
State after:
case mk.mk
M : Type u_1
N : Type ?u.3198
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h : (inclusion s) { val := a, property := ha } = (inclusion s) { val := b, property := hb }
⊢ a = b

State before:
case mk.mk
M : Type u_1
N : Type ?u.3198
α : Type u_2
inst✝ : SMul M α
s : SubMulAction M α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h : (inclusion s) { val := a, property := ha } = (inclusion s) { val := b, property := hb }
⊢ a = b
Tactic:
exact h
State after:
no goals