Theorem: SubMulAction.ofStabilizer.conjMap_bijective (Jordan/SubMulActions.lean)

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
⊢ Function.Bijective ⇑(conjMap M hab)
Tactic:
constructor
State after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
⊢ Function.Injective ⇑(conjMap M hab)

case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
⊢ Function.Surjective ⇑(conjMap M hab)

State before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
⊢ Function.Injective ⇑(conjMap M hab)
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 α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
hxy : (conjMap M hab) { val := x, property := hx } = (conjMap M hab) { 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 α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
hxy : (conjMap M hab) { val := x, property := hx } = (conjMap M hab) { 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 α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
hxy : (conjMap M hab) { val := x, property := hx } = (conjMap M hab) { 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 α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
hxy : (conjMap M hab) { val := x, property := hx } = (conjMap M hab) { 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 α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
hxy : ↑((conjMap M hab) { val := x, property := hx }) = ↑((conjMap M hab) { 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 α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
hxy : ↑((conjMap M hab) { val := x, property := hx }) = ↑((conjMap M hab) { 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 α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
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 α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M a
y : α
hy : y ∈ ofStabilizer M a
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 α
a b : α
g : M
hab : g • a = b
⊢ Function.Surjective ⇑(conjMap M hab)
Tactic:
rintro ⟨x, hx⟩
State after:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ ∃ a_1, (conjMap M hab) a_1 = { val := x, property := hx }

State before:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ ∃ a_1, (conjMap M hab) a_1 = { val := x, property := hx }
Tactic:
use (SubMulAction.ofStabilizer.conjMap M (inv_smul_eq_iff.mpr hab.symm)) ⟨x, hx⟩
State after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ (conjMap M hab) ((conjMap M ⋯) { 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 α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ (conjMap M hab) ((conjMap M ⋯) { 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 α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ ↑((conjMap M hab) ((conjMap M ⋯) { 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 α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ ↑((conjMap M hab) ((conjMap M ⋯) { 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 α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ g • g⁻¹ • x = x

State before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a b : α
g : M
hab : g • a = b
x : α
hx : x ∈ ofStabilizer M b
⊢ g • g⁻¹ • x = x
Tactic:
simp only [smul_inv_smul]
State after:
no goals