Theorem: Nat.combination.mulAction_faithful (Jordan/MulActionCombination.lean)

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
⊢ ∃ s, g • s ≠ s
Tactic:
have zob : ∃ (a : α), (g • a : α) ≠ a := by
  by_contra h
  push_neg at h
  apply hg
  ext a
  simpa only using h a
State after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
zob : ∃ a, g • a ≠ a
⊢ ∃ s, g • s ≠ s

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
zob : ∃ a, g • a ≠ a
⊢ ∃ s, g • s ≠ s
Tactic:
obtain ⟨a, ha⟩ := zob
State after:
case intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
⊢ ∃ s, g • s ≠ s

State before:
case intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
⊢ ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
Tactic:
have : ({a} : Set α) ⊆ {g • a}ᶜ := by
  simp only [Set.subset_compl_singleton_iff, Set.mem_singleton_iff]
  exact ha
State after:
case intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
⊢ ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s

State before:
case intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
⊢ ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
Tactic:
have hα' : n ≤ Set.encard ({g • a}ᶜ) := by
  rw [← not_lt, ← WithTop.add_one_lt_coe_succ_iff, not_lt, add_comm,
    ← Set.encard_singleton (g • a), Set.encard_add_encard_compl, Set.encard_univ]
  rw [← PartENat.withTopEquiv_natCast, PartENat.withTopEquiv_le]
  exact hα
State after:
case intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
⊢ ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s

State before:
case intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
⊢ ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
Tactic:
obtain ⟨s, has, has', hs⟩ := Set.exists_superset_subset_encard_eq this (by
  rw [Set.encard_singleton, ← Nat.cast_one, Nat.cast_le]
  exact hn) hα'
State after:
case intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s

State before:
case intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
Tactic:
use s
State after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s

State before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
Tactic:
constructor
State after:
case h.left
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ Set.encard s = ↑n

case h.right
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ a ∈ s ∧ g • a ∉ s

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
⊢ ∃ a, g • a ≠ a
Tactic:
by_contra h
State after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ¬∃ a, g • a ≠ a
⊢ False

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ¬∃ a, g • a ≠ a
⊢ False
Tactic:
push_neg at h
State after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ∀ (a : α), g • a = a
⊢ False

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ∀ (a : α), g • a = a
⊢ False
Tactic:
apply hg
State after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ∀ (a : α), g • a = a
⊢ toPerm g = 1

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ∀ (a : α), g • a = a
⊢ toPerm g = 1
Tactic:
ext a
State after:
case H
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ∀ (a : α), g • a = a
a : α
⊢ (toPerm g) a = 1 a

State before:
case H
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
h : ∀ (a : α), g • a = a
a : α
⊢ (toPerm g) a = 1 a
Tactic:
simpa only using h a
State after:
no goals

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : ∃ s, Set.encard s = ↑n ∧ a ∈ s ∧ g • a ∉ s
⊢ ∃ s, g • s ≠ s
Tactic:
obtain ⟨s, hs, has, has'⟩ := this
State after:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
has' : g • a ∉ s
⊢ ∃ s, g • s ≠ s

State before:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
has' : g • a ∉ s
⊢ ∃ s, g • s ≠ s
Tactic:
have : Set.Finite s := Set.finite_of_encard_eq_coe hs
State after:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
⊢ ∃ s, g • s ≠ s

State before:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
⊢ ∃ s, g • s ≠ s
Tactic:
rw [Set.Finite.encard_eq_coe_toFinset_card this, cast_inj] at hs
State after:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ ∃ s, g • s ≠ s

State before:
case intro.intro.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ ∃ s, g • s ≠ s
Tactic:
use ⟨Set.Finite.toFinset this, hs⟩
State after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ g • { val := Set.Finite.toFinset this, property := hs } ≠ { val := Set.Finite.toFinset this, property := hs }

State before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ g • { val := Set.Finite.toFinset this, property := hs } ≠ { val := Set.Finite.toFinset this, property := hs }
Tactic:
simp only [ne_eq]
State after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ ¬g • { val := Set.Finite.toFinset this, property := hs } = { val := Set.Finite.toFinset this, property := hs }

State before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ ¬g • { val := Set.Finite.toFinset this, property := hs } = { val := Set.Finite.toFinset this, property := hs }
Tactic:
rw [Nat.Combination.eq_iff, ← Finset.coe_inj, combination_mulAction.coe_apply', Finset.coe_smul_finset, Set.Finite.coe_toFinset]
State after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ ¬g • s = s

State before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ ¬g • s = s
Tactic:
intro h
State after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
h : g • s = s
⊢ False

State before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
h : g • s = s
⊢ False
Tactic:
apply has'
State after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
h : g • s = s
⊢ g • a ∈ s

State before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
h : g • s = s
⊢ g • a ∈ s
Tactic:
rw [← h]
State after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
h : g • s = s
⊢ g • a ∈ g • s

State before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
h : g • s = s
⊢ g • a ∈ g • s
Tactic:
exact Set.smul_mem_smul_set has
State after:
no goals

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
⊢ {a} ⊆ {g • a}ᶜ
Tactic:
simp only [Set.subset_compl_singleton_iff, Set.mem_singleton_iff]
State after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
⊢ ¬g • a = a

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
⊢ ¬g • a = a
Tactic:
exact ha
State after:
no goals

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
⊢ ↑n ≤ Set.encard {g • a}ᶜ
Tactic:
rw [← not_lt, ← WithTop.add_one_lt_coe_succ_iff, not_lt, add_comm,
  ← Set.encard_singleton (g • a), Set.encard_add_encard_compl, Set.encard_univ]
State after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
⊢ ↑(succ n) ≤ PartENat.withTopEquiv (PartENat.card α)

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
⊢ ↑(succ n) ≤ PartENat.withTopEquiv (PartENat.card α)
Tactic:
rw [← PartENat.withTopEquiv_natCast, PartENat.withTopEquiv_le]
State after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
⊢ ↑(succ n) ≤ PartENat.card α

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
⊢ ↑(succ n) ≤ PartENat.card α
Tactic:
exact hα
State after:
no goals

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
⊢ Set.encard {a} ≤ ↑n
Tactic:
rw [Set.encard_singleton, ← Nat.cast_one, Nat.cast_le]
State after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
⊢ 1 ≤ n

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
⊢ 1 ≤ n
Tactic:
exact hn
State after:
no goals

State before:
case h.left
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ Set.encard s = ↑n
Tactic:
exact hs
State after:
no goals

State before:
case h.right
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ a ∈ s ∧ g • a ∉ s
Tactic:
simp only [Set.singleton_subset_iff, Set.subset_compl_singleton_iff] at has has'
State after:
case h.right
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
has' : g • a ∉ s
⊢ a ∈ s ∧ g • a ∉ s

State before:
case h.right
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
has' : g • a ∉ s
⊢ a ∈ s ∧ g • a ∉ s
Tactic:
exact ⟨has, has'⟩
State after:
no goals