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

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

case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
⊢ Function.Surjective ⇑(conjMap_ofFixingSubgroup M hst)

State before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
⊢ Function.Injective ⇑(conjMap_ofFixingSubgroup M hst)
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 α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy :
  (conjMap_ofFixingSubgroup M hst) { val := x, property := hx } =
    (conjMap_ofFixingSubgroup M hst) { 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 α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy :
  (conjMap_ofFixingSubgroup M hst) { val := x, property := hx } =
    (conjMap_ofFixingSubgroup M hst) { 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 α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy :
  (conjMap_ofFixingSubgroup M hst) { val := x, property := hx } =
    (conjMap_ofFixingSubgroup M hst) { 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 α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy :
  (conjMap_ofFixingSubgroup M hst) { val := x, property := hx } =
    (conjMap_ofFixingSubgroup M hst) { val := y, property := hy }
⊢ x = y
Tactic:
rw [← SetLike.coe_eq_coe] at hxy
State after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy :
  ↑((conjMap_ofFixingSubgroup M hst) { val := x, property := hx }) =
    ↑((conjMap_ofFixingSubgroup M hst) { 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 α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy :
  ↑((conjMap_ofFixingSubgroup M hst) { val := x, property := hx }) =
    ↑((conjMap_ofFixingSubgroup M hst) { val := y, property := hy })
⊢ x = y
Tactic:
change g • x = g • y at hxy
State after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : g • x = g • y
⊢ x = y

State before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : g • x = g • y
⊢ x = y
Tactic:
apply (MulAction.injective g) hxy
State after:
no goals

State before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
⊢ Function.Surjective ⇑(conjMap_ofFixingSubgroup M hst)
Tactic:
rintro ⟨x, hx⟩
State after:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ ∃ a, (conjMap_ofFixingSubgroup M hst) a = { val := x, property := hx }

State before:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ ∃ a, (conjMap_ofFixingSubgroup M hst) a = { val := x, property := hx }
Tactic:
have hst' : g⁻¹ • t = s := by
  apply symm; rw [← inv_smul_eq_iff]; rw [inv_inv]
  exact hst
State after:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ ∃ a, (conjMap_ofFixingSubgroup M hst) a = { val := x, property := hx }

State before:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ ∃ a, (conjMap_ofFixingSubgroup M hst) a = { val := x, property := hx }
Tactic:
use (SubMulAction.conjMap_ofFixingSubgroup M hst') ⟨x, hx⟩
State after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ (conjMap_ofFixingSubgroup M hst) ((conjMap_ofFixingSubgroup M hst') { val := x, property := hx }) =
    { val := x, property := hx }

State before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ (conjMap_ofFixingSubgroup M hst) ((conjMap_ofFixingSubgroup M hst') { val := x, property := hx }) =
    { val := x, property := hx }
Tactic:
rw [← SetLike.coe_eq_coe]
State after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ ↑((conjMap_ofFixingSubgroup M hst) ((conjMap_ofFixingSubgroup M hst') { val := x, property := hx })) =
    ↑{ val := x, property := hx }

State before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ ↑((conjMap_ofFixingSubgroup M hst) ((conjMap_ofFixingSubgroup M hst') { val := x, property := hx })) =
    ↑{ val := x, property := hx }
Tactic:
change g • g⁻¹ • x = x
State after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ g • g⁻¹ • x = x

State before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ g • g⁻¹ • x = x
Tactic:
rw [← mul_smul, mul_inv_self, one_smul]
State after:
no goals

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ g⁻¹ • t = s
Tactic:
apply symm
State after:
case a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ s = g⁻¹ • t

State before:
case a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ s = g⁻¹ • t
Tactic:
rw [← inv_smul_eq_iff]
State after:
case a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ g⁻¹⁻¹ • s = t

State before:
case a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ g⁻¹⁻¹ • s = t
Tactic:
rw [inv_inv]
State after:
case a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ g • s = t

State before:
case a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ g • s = t
Tactic:
exact hst
State after:
no goals