Theorem: SubMulAction.OfFixingSubgroupUnion.map_bijective (Jordan/SubMulActions.lean)

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

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

State before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
⊢ Function.Injective ⇑(map_ofFixingSubgroupUnion M s t)
Tactic:
intro a b h
State after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a b : ↥(ofFixingSubgroup M (s ∪ t))
h : (map_ofFixingSubgroupUnion M s t) a = (map_ofFixingSubgroupUnion M s t) b
⊢ a = b

State before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a b : ↥(ofFixingSubgroup M (s ∪ t))
h : (map_ofFixingSubgroupUnion M s t) a = (map_ofFixingSubgroupUnion M s t) b
⊢ a = b
Tactic:
simp only [← SetLike.coe_eq_coe] at h ⊢
State after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a b : ↥(ofFixingSubgroup M (s ∪ t))
h : ↑↑((map_ofFixingSubgroupUnion M s t) a) = ↑↑((map_ofFixingSubgroupUnion M s t) b)
⊢ ↑a = ↑b

State before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a b : ↥(ofFixingSubgroup M (s ∪ t))
h : ↑↑((map_ofFixingSubgroupUnion M s t) a) = ↑↑((map_ofFixingSubgroupUnion M s t) b)
⊢ ↑a = ↑b
Tactic:
exact h
State after:
no goals

State before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
⊢ Function.Surjective ⇑(map_ofFixingSubgroupUnion M s t)
Tactic:
rintro ⟨⟨a, ha⟩, ha'⟩
State after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
⊢ ∃ a_1, (map_ofFixingSubgroupUnion M s t) a_1 = { val := { val := a, property := ha }, property := ha' }

State before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
⊢ ∃ a_1, (map_ofFixingSubgroupUnion M s t) a_1 = { val := { val := a, property := ha }, property := ha' }
Tactic:
suffices a ∈ ofFixingSubgroup M (s ∪ t) by
  exact ⟨⟨a, this⟩,  rfl⟩
State after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
⊢ a ∈ ofFixingSubgroup M (s ∪ t)

State before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
⊢ a ∈ ofFixingSubgroup M (s ∪ t)
Tactic:
intro hy
State after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
⊢ False

State before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
⊢ False
Tactic:
cases' (Set.mem_union a s t).mp hy with h h
State after:
case right.mk.mk.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ s
⊢ False

case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ t
⊢ False

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
this : a ∈ ofFixingSubgroup M (s ∪ t)
⊢ ∃ a_1, (map_ofFixingSubgroupUnion M s t) a_1 = { val := { val := a, property := ha }, property := ha' }
Tactic:
exact ⟨⟨a, this⟩,  rfl⟩
State after:
no goals

State before:
case right.mk.mk.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ s
⊢ False
Tactic:
exact ha 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 α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ t
⊢ False
Tactic:
apply ha'
State after:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ t
⊢ { val := a, property := ha } ∈ Subtype.val ⁻¹' t

State before:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ t
⊢ { val := a, property := ha } ∈ Subtype.val ⁻¹' t
Tactic:
simp only [Set.mem_preimage]
State after:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ t
⊢ a ∈ t

State before:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : { val := a, property := ha } ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
hy : a ∈ s ∪ t
h : a ∈ t
⊢ a ∈ t
Tactic:
exact h
State after:
no goals