Theorem: SubMulAction.ofFixingSubgroup.mapOfInclusion_injective (Jordan/SubMulActions.lean)

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : t ⊆ s
⊢ Function.Injective ⇑(mapOfInclusion M hst)
Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
State after:
case mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : t ⊆ s
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : (mapOfInclusion M hst) { val := x, property := hx } = (mapOfInclusion M hst) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }

State before:
case mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : t ⊆ s
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : (mapOfInclusion M hst) { val := x, property := hx } = (mapOfInclusion M hst) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
Tactic:
rw [← SetLike.coe_eq_coe] at hxy ⊢
State after:
case mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : t ⊆ s
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : ↑((mapOfInclusion M hst) { val := x, property := hx }) = ↑((mapOfInclusion M hst) { val := y, property := hy })
⊢ ↑{ val := x, property := hx } = ↑{ val := y, property := hy }

State before:
case mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : t ⊆ s
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : ↑((mapOfInclusion M hst) { val := x, property := hx }) = ↑((mapOfInclusion M hst) { val := y, property := hy })
⊢ ↑{ val := x, property := hx } = ↑{ val := y, property := hy }
Tactic:
exact hxy
State after:
no goals