Theorem: SubMulAction.OfFixingSubgroupOfEq.map_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 ⇑(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 ⇑(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 ⇑(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 ⇑(map 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 α
hst : s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : (map M hst) { val := x, property := hx } = (map 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 α
hst : s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : (map M hst) { val := x, property := hx } = (map M hst) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
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 α
hst : s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : ↑((map M hst) { val := x, property := hx }) = ↑((map 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 α
hst : s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : ↑((map M hst) { val := x, property := hx }) = ↑((map M hst) { val := y, property := hy })
⊢ ↑{ val := x, property := hx } = ↑{ val := y, property := hy }
Tactic:
simp only [SubMulAction.OfFixingSubgroupOfEq.map_def M hst] at hxy
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
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : x = y
⊢ ↑{ 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 α
hst : s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : x = y
⊢ ↑{ val := x, property := hx } = ↑{ val := y, property := hy }
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
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : x = 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 α
hst : s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : x = y
⊢ x = y
Tactic:
rw [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 α
hst : s = t
⊢ Function.Surjective ⇑(map M hst)
Tactic:
rintro ⟨x, hxt⟩
State after:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ ∃ a, (map M hst) a = { val := x, property := hxt }

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

case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ x ∈ ofFixingSubgroup 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
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ (map M hst) { val := x, property := ?w } = { val := x, property := hxt }

case w
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
hst : s = t
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ x ∈ ofFixingSubgroup 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
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ x ∈ ofFixingSubgroup 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
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ x ∈ ofFixingSubgroup 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
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ x ∈ ofFixingSubgroup 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
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ x ∈ ofFixingSubgroup M t
Tactic:
exact hxt
State after:
no goals