Theorem: SubMulAction.OfFixingSubgroupOfSingleton.map_bijective (Jordan/SubMulActions.lean)

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ Function.Bijective ⇑(map M a)
Tactic:
constructor
State after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ Function.Injective ⇑(map M a)

case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ Function.Surjective ⇑(map M a)

State before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ Function.Injective ⇑(map M a)
Tactic:
intro _ _ hxy
State after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
a₁✝ a₂✝ : ↥(ofFixingSubgroup M {a})
hxy : (map M a) a₁✝ = (map M a) a₂✝
⊢ a₁✝ = a₂✝

State before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
a₁✝ a₂✝ : ↥(ofFixingSubgroup M {a})
hxy : (map M a) a₁✝ = (map M a) a₂✝
⊢ a₁✝ = a₂✝
Tactic:
exact hxy
State after:
no goals

State before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ Function.Surjective ⇑(map M a)
Tactic:
intro x
State after:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
x : ↥(ofStabilizer M a)
⊢ ∃ a_1, (map M a) a_1 = x

State before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
x : ↥(ofStabilizer M a)
⊢ ∃ a_1, (map M a) a_1 = x
Tactic:
use x
State after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
x : ↥(ofStabilizer M a)
⊢ (map M a) x = x

State before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
x : ↥(ofStabilizer M a)
⊢ (map M a) x = x
Tactic:
rfl
State after:
no goals