Theorem: Equiv.Perm.isMaximalStab (Jordan/PermMaximal.lean)

State before:
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)
Tactic:
cases' Nat.lt_trichotomy s.ncard sᶜ.ncard with hs hs'
State after:
case inl
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard s < Set.ncard sᶜ
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)

case inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs' : Set.ncard s = Set.ncard sᶜ ∨ Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)

State before:
case inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs' : Set.ncard s = Set.ncard sᶜ ∨ Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)
Tactic:
cases' hs' with hs hs
State after:
case inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard s = Set.ncard sᶜ
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)

case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)

State before:
case inl
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard s < Set.ncard sᶜ
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)
Tactic:
exact Equiv.Perm.isMaximalStab' s h0 h1 hs
State after:
no goals

State before:
case inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard s = Set.ncard sᶜ
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)
Tactic:
exfalso
State after:
case inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard s = Set.ncard sᶜ
⊢ False

State before:
case inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard s = Set.ncard sᶜ
⊢ False
Tactic:
apply hα
State after:
case inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard s = Set.ncard sᶜ
⊢ Fintype.card α = 2 * Set.ncard s

State before:
case inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard s = Set.ncard sᶜ
⊢ Fintype.card α = 2 * Set.ncard s
Tactic:
rw [← Nat.card_eq_fintype_card, ← Set.ncard_add_ncard_compl s, two_mul, ← hs]
State after:
no goals

State before:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)
Tactic:
rw [← compl_compl s] at h0
State after:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)

State before:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)
Tactic:
rw [← stabilizer_compl]
State after:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (Perm α) sᶜ)

State before:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (Perm α) sᶜ)
Tactic:
apply Equiv.Perm.isMaximalStab' (sᶜ) h1 h0
State after:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Set.ncard sᶜ < Set.ncard sᶜᶜ

State before:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Set.ncard sᶜ < Set.ncard sᶜᶜ
Tactic:
rw [compl_compl]
State after:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Set.ncard sᶜ < Set.ncard s

State before:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Set.ncard sᶜ < Set.ncard s
Tactic:
exact hs
State after:
no goals