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

State before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
⊢ Function.Surjective ⇑(Subgroup.subtype (fixingSubgroup M ∅))
Tactic:
intro g
State after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
g : M
⊢ ∃ a, (Subgroup.subtype (fixingSubgroup M ∅)) a = g

State before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
g : M
⊢ ∃ a, (Subgroup.subtype (fixingSubgroup M ∅)) a = g
Tactic:
suffices g ∈ fixingSubgroup M (∅ : Set α) by
  exact ⟨⟨g, this⟩, rfl⟩
State after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
g : M
⊢ g ∈ fixingSubgroup M ∅

State before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
g : M
⊢ g ∈ fixingSubgroup M ∅
Tactic:
rw [mem_fixingSubgroup_iff]
State after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
g : M
⊢ ∀ y ∈ ∅, g • y = y

State before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
g : M
⊢ ∀ y ∈ ∅, g • y = y
Tactic:
simp only [Set.mem_empty_iff_false, IsEmpty.forall_iff, implies_true]
State after:
no goals

State before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
g : M
this : g ∈ fixingSubgroup M ∅
⊢ ∃ a, (Subgroup.subtype (fixingSubgroup M ∅)) a = g
Tactic:
exact ⟨⟨g, this⟩, rfl⟩
State after:
no goals