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

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

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

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

State before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
x : α
hx : x ∈ ofFixingSubgroup M ∅
y : α
hy : y ∈ ofFixingSubgroup M ∅
hxy :
  (ofFixingSubgroupEmpty_equivariantMap M α) { val := x, property := hx } =
    (ofFixingSubgroupEmpty_equivariantMap M α) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
Tactic:
simp only [Subtype.mk_eq_mk]
State after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
x : α
hx : x ∈ ofFixingSubgroup M ∅
y : α
hy : y ∈ ofFixingSubgroup M ∅
hxy :
  (ofFixingSubgroupEmpty_equivariantMap M α) { val := x, property := hx } =
    (ofFixingSubgroupEmpty_equivariantMap M α) { val := y, property := hy }
⊢ x = y

State before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
x : α
hx : x ∈ ofFixingSubgroup M ∅
y : α
hy : y ∈ ofFixingSubgroup M ∅
hxy :
  (ofFixingSubgroupEmpty_equivariantMap M α) { val := x, property := hx } =
    (ofFixingSubgroupEmpty_equivariantMap M α) { val := y, property := hy }
⊢ x = y
Tactic:
exact hxy
State after:
no goals

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

State before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
x : α
⊢ ∃ a, (ofFixingSubgroupEmpty_equivariantMap M α) a = x
Tactic:
use ⟨x, (SubMulAction.mem_ofFixingSubgroup_iff M).mp (Set.not_mem_empty x)⟩
State after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
x : α
⊢ (ofFixingSubgroupEmpty_equivariantMap M α) { val := x, property := ⋯ } = x

State before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
x : α
⊢ (ofFixingSubgroupEmpty_equivariantMap M α) { val := x, property := ⋯ } = x
Tactic:
rfl
State after:
no goals