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

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

case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Surjective ⇑(equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s)

State before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Injective ⇑(equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s)
Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ h
State after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { 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 : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { 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 : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { 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 : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy }
⊢ x = y
Tactic:
rw [← SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_coe M hx]
State after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy }
⊢ ↑↑((equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx }) = y

State before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy }
⊢ ↑↑((equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx }) = y
Tactic:
rw [← SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_coe M hy]
State after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy }
⊢ ↑↑((equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx }) =
    ↑↑((equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy })

State before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h :
  (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx } =
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy }
⊢ ↑↑((equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := x, property := hx }) =
    ↑↑((equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := y, property := hy })
Tactic:
rw [h]
State after:
no goals

State before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Surjective ⇑(equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s)
Tactic:
rintro ⟨⟨x, hx1⟩, hx2⟩
State after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
⊢ ∃ a_1,
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) a_1 =
      { val := { val := x, property := hx1 }, property := hx2 }

State before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
⊢ ∃ a_1,
    (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) a_1 =
      { val := { val := x, property := hx1 }, property := hx2 }
Tactic:
refine' ⟨⟨x, _⟩, rfl⟩
State after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
⊢ x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))

State before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
⊢ x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
Tactic:
rw [SubMulAction.mem_ofFixingSubgroup_iff]
State after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
⊢ x ∉ insert a (Subtype.val '' s)

State before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
⊢ x ∉ insert a (Subtype.val '' s)
Tactic:
intro h
State after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
h : x ∈ insert a (Subtype.val '' s)
⊢ False

State before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
h : x ∈ insert a (Subtype.val '' s)
⊢ False
Tactic:
cases Set.mem_insert_iff.mp h with
| inl h' => rw [SubMulAction.mem_ofStabilizer_iff] at hx1 ; exact hx1 h'
| inr h' =>
rw [SubMulAction.mem_ofFixingSubgroup_iff] at hx2
apply hx2
obtain ⟨x1, hx1', rfl⟩ := h'
simp only [SetLike.eta]
exact hx1'
State after:
no goals

State before:
case right.mk.mk.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
h : x ∈ insert a (Subtype.val '' s)
h' : x = a
⊢ False
Tactic:
rw [SubMulAction.mem_ofStabilizer_iff] at hx1
State after:
case right.mk.mk.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1✝ : x ∈ ofStabilizer M a
hx1 : x ≠ a
hx2 : { val := x, property := hx1✝ } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
h : x ∈ insert a (Subtype.val '' s)
h' : x = a
⊢ False

State before:
case right.mk.mk.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1✝ : x ∈ ofStabilizer M a
hx1 : x ≠ a
hx2 : { val := x, property := hx1✝ } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
h : x ∈ insert a (Subtype.val '' s)
h' : x = a
⊢ False
Tactic:
exact hx1 h'
State after:
no goals

State before:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∈ ofFixingSubgroup (↥(stabilizer M a)) s
h : x ∈ insert a (Subtype.val '' s)
h' : x ∈ Subtype.val '' s
⊢ False
Tactic:
rw [SubMulAction.mem_ofFixingSubgroup_iff] at hx2
State after:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∉ s
h : x ∈ insert a (Subtype.val '' s)
h' : x ∈ Subtype.val '' s
⊢ False

State before:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∉ s
h : x ∈ insert a (Subtype.val '' s)
h' : x ∈ Subtype.val '' s
⊢ False
Tactic:
apply hx2
State after:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∉ s
h : x ∈ insert a (Subtype.val '' s)
h' : x ∈ Subtype.val '' s
⊢ { val := x, property := hx1 } ∈ s

State before:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx1 : x ∈ ofStabilizer M a
hx2 : { val := x, property := hx1 } ∉ s
h : x ∈ insert a (Subtype.val '' s)
h' : x ∈ Subtype.val '' s
⊢ { val := x, property := hx1 } ∈ s
Tactic:
obtain ⟨x1, hx1', rfl⟩ := h'
State after:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x1 : ↥(ofStabilizer M a)
hx1' : x1 ∈ s
hx1 : ↑x1 ∈ ofStabilizer M a
hx2 : { val := ↑x1, property := hx1 } ∉ s
h : ↑x1 ∈ insert a (Subtype.val '' s)
⊢ { val := ↑x1, property := hx1 } ∈ s

State before:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x1 : ↥(ofStabilizer M a)
hx1' : x1 ∈ s
hx1 : ↑x1 ∈ ofStabilizer M a
hx2 : { val := ↑x1, property := hx1 } ∉ s
h : ↑x1 ∈ insert a (Subtype.val '' s)
⊢ { val := ↑x1, property := hx1 } ∈ s
Tactic:
simp only [SetLike.eta]
State after:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x1 : ↥(ofStabilizer M a)
hx1' : x1 ∈ s
hx1 : ↑x1 ∈ ofStabilizer M a
hx2 : { val := ↑x1, property := hx1 } ∉ s
h : ↑x1 ∈ insert a (Subtype.val '' s)
⊢ x1 ∈ s

State before:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x1 : ↥(ofStabilizer M a)
hx1' : x1 ∈ s
hx1 : ↑x1 ∈ ofStabilizer M a
hx2 : { val := ↑x1, property := hx1 } ∉ s
h : ↑x1 ∈ insert a (Subtype.val '' s)
⊢ x1 ∈ s
Tactic:
exact hx1'
State after:
no goals