Theorem: isnontrivial_of_nontrivial_action (Jordan/Primitive.lean)

State before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
⊢ Nontrivial α
Tactic:
apply Or.resolve_left (subsingleton_or_nontrivial α)
State after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
⊢ ¬Subsingleton α

State before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
⊢ ¬Subsingleton α
Tactic:
intro hα
State after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
⊢ False

State before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
⊢ False
Tactic:
apply h
State after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
⊢ fixedPoints (↥N) α = ⊤

State before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
⊢ fixedPoints (↥N) α = ⊤
Tactic:
rw [eq_top_iff]
State after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
⊢ ⊤ ≤ fixedPoints (↥N) α

State before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
⊢ ⊤ ≤ fixedPoints (↥N) α
Tactic:
intro x hx
State after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
x : α
hx : x ∈ ⊤
⊢ x ∈ fixedPoints (↥N) α

State before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
x : α
hx : x ∈ ⊤
⊢ x ∈ fixedPoints (↥N) α
Tactic:
rw [mem_fixedPoints]
State after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
x : α
hx : x ∈ ⊤
⊢ ∀ (m : ↥N), m • x = x

State before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
x : α
hx : x ∈ ⊤
⊢ ∀ (m : ↥N), m • x = x
Tactic:
intro g
State after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
x : α
hx : x ∈ ⊤
g : ↥N
⊢ g • x = x

State before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : Subsingleton α
x : α
hx : x ∈ ⊤
g : ↥N
⊢ g • x = x
Tactic:
rw [subsingleton_iff] at hα
State after:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : ∀ (x y : α), x = y
x : α
hx : x ∈ ⊤
g : ↥N
⊢ g • x = x

State before:
M : Type u_1
inst✝¹ : Group M
α : Type u_2
inst✝ : MulAction M α
N : Subgroup M
h : fixedPoints (↥N) α ≠ ⊤
hα : ∀ (x y : α), x = y
x : α
hx : x ∈ ⊤
g : ↥N
⊢ g • x = x
Tactic:
apply hα
State after:
no goals