Theorem: SubMulAction.OfFixingSubgroupOfEq.toMap_bijective (Jordan/SubMulActions.lean)

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
⊢ Function.Bijective (MulActionHom.toMap (map M hst))
Tactic:
constructor
State after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
⊢ Function.Injective (MulActionHom.toMap (map M hst))

case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
⊢ Function.Surjective (MulActionHom.toMap (map M hst))

State before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
⊢ Function.Injective (MulActionHom.toMap (map M hst))
Tactic:
rintro ⟨g, hg⟩ ⟨k, hk⟩ hgk
State after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
g : M
hg : g ∈ fixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hgk :
  MulActionHom.toMap (map M hst) { val := g, property := hg } =
    MulActionHom.toMap (map M hst) { val := k, property := hk }
⊢ { val := g, property := hg } = { val := k, property := hk }

State before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
g : M
hg : g ∈ fixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hgk :
  MulActionHom.toMap (map M hst) { val := g, property := hg } =
    MulActionHom.toMap (map M hst) { val := k, property := hk }
⊢ { val := g, property := hg } = { val := k, property := hk }
Tactic:
rw [← SetLike.coe_eq_coe] at hgk ⊢
State after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
g : M
hg : g ∈ fixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hgk :
  ↑(MulActionHom.toMap (map M hst) { val := g, property := hg }) =
    ↑(MulActionHom.toMap (map M hst) { val := k, property := hk })
⊢ ↑{ val := g, property := hg } = ↑{ val := k, property := hk }

State before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
g : M
hg : g ∈ fixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hgk :
  ↑(MulActionHom.toMap (map M hst) { val := g, property := hg }) =
    ↑(MulActionHom.toMap (map M hst) { val := k, property := hk })
⊢ ↑{ val := g, property := hg } = ↑{ val := k, property := hk }
Tactic:
simp only
State after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
g : M
hg : g ∈ fixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hgk :
  ↑(MulActionHom.toMap (map M hst) { val := g, property := hg }) =
    ↑(MulActionHom.toMap (map M hst) { val := k, property := hk })
⊢ g = k

State before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
g : M
hg : g ∈ fixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hgk :
  ↑(MulActionHom.toMap (map M hst) { val := g, property := hg }) =
    ↑(MulActionHom.toMap (map M hst) { val := k, property := hk })
⊢ g = k
Tactic:
exact hgk
State after:
no goals

State before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
⊢ Function.Surjective (MulActionHom.toMap (map M hst))
Tactic:
rintro ⟨k, hk⟩
State after:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ ∃ a, MulActionHom.toMap (map M hst) a = { val := k, property := hk }

State before:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ ∃ a, MulActionHom.toMap (map M hst) a = { val := k, property := hk }
Tactic:
use ⟨k, ?_⟩
State after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ MulActionHom.toMap (map M hst) { val := k, property := ?w } = { val := k, property := hk }

case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ k ∈ fixingSubgroup M s

State before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ MulActionHom.toMap (map M hst) { val := k, property := ?w } = { val := k, property := hk }

case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ k ∈ fixingSubgroup M s
Tactic:
rfl
State after:
case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ k ∈ fixingSubgroup M s

State before:
case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ k ∈ fixingSubgroup M s
Tactic:
rw [hst]
State after:
case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ k ∈ fixingSubgroup M t

State before:
case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
k : M
hk : k ∈ fixingSubgroup M t
⊢ k ∈ fixingSubgroup M t
Tactic:
exact hk
State after:
no goals