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

State before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
have : ∀ (t : Set α) (_ : 1 < t.ncard), ∃ (g : Equiv.Perm α),
    g.IsSwap ∧ g ∈ stabilizer (Equiv.Perm α) t := by
  intro t ht
  rw [Set.one_lt_ncard_iff] at ht
  obtain ⟨a, b, ha, hb, h⟩ := ht
  simp only [Ne.def, Subtype.mk_eq_mk] at h
  use Equiv.swap a b
  constructor
  rw [swap_isSwap_iff]; exact h
  apply swap_mem_stabilizer ha hb
State after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
⊢ ∃ g, IsSwap g ∧ g ∈ G

State before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
cases' lt_or_le 1 (s.ncard) with h1 h1'
State after:
case inl
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1 : 1 < Set.ncard s
⊢ ∃ g, IsSwap g ∧ g ∈ G

case inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
⊢ ∃ g, IsSwap g ∧ g ∈ G

State before:
case inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
cases' lt_or_le 1 sᶜ.ncard with h1c h1c'
State after:
case inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c : 1 < Set.ncard sᶜ
⊢ ∃ g, IsSwap g ∧ g ∈ G

case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ ∃ g, IsSwap g ∧ g ∈ G

State before:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
cases subgroup_of_group_of_order_two (by
  rw [Fintype.card_perm, ← Nat.card_eq_fintype_card, hα]
  simp) G with
| inl h =>
  exfalso; exact ne_bot_of_gt hG h
| inr h =>
  rw [h]
  rw [← stabilizer_univ_eq_top (Equiv.Perm α) α]
  apply this
  rw [Set.ncard_univ, hα]
  norm_num
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
⊢ ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
Tactic:
intro t ht
State after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
ht : 1 < Set.ncard t
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t

State before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
ht : 1 < Set.ncard t
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
Tactic:
rw [Set.one_lt_ncard_iff] at ht
State after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
ht : ∃ a b, a ∈ t ∧ b ∈ t ∧ a ≠ b
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t

State before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
ht : ∃ a b, a ∈ t ∧ b ∈ t ∧ a ≠ b
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
Tactic:
obtain ⟨a, b, ha, hb, h⟩ := ht
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : a ≠ b
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : a ≠ b
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
Tactic:
simp only [Ne.def, Subtype.mk_eq_mk] at h
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : ¬a = b
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : ¬a = b
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
Tactic:
use Equiv.swap a b
State after:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : ¬a = b
⊢ IsSwap (swap a b) ∧ swap a b ∈ stabilizer (Perm α) t

State before:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : ¬a = b
⊢ IsSwap (swap a b) ∧ swap a b ∈ stabilizer (Perm α) t
Tactic:
constructor
State after:
case h.left
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : ¬a = b
⊢ IsSwap (swap a b)

case h.right
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : ¬a = b
⊢ swap a b ∈ stabilizer (Perm α) t

State before:
case h.left
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : ¬a = b
⊢ IsSwap (swap a b)

case h.right
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : ¬a = b
⊢ swap a b ∈ stabilizer (Perm α) t
Tactic:
rw [swap_isSwap_iff]
State after:
case h.left
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : ¬a = b
⊢ a ≠ b

case h.right
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : ¬a = b
⊢ swap a b ∈ stabilizer (Perm α) t

State before:
case h.left
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : ¬a = b
⊢ a ≠ b

case h.right
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : ¬a = b
⊢ swap a b ∈ stabilizer (Perm α) t
Tactic:
exact h
State after:
case h.right
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : ¬a = b
⊢ swap a b ∈ stabilizer (Perm α) t

State before:
case h.right
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : ¬a = b
⊢ swap a b ∈ stabilizer (Perm α) t
Tactic:
apply swap_mem_stabilizer ha hb
State after:
no goals

State before:
case inl
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1 : 1 < Set.ncard s
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
obtain ⟨g, hg, hg'⟩ := this s h1
State after:
case inl.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1 : 1 < Set.ncard s
g : Perm α
hg : IsSwap g
hg' : g ∈ stabilizer (Perm α) s
⊢ ∃ g, IsSwap g ∧ g ∈ G

State before:
case inl.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1 : 1 < Set.ncard s
g : Perm α
hg : IsSwap g
hg' : g ∈ stabilizer (Perm α) s
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
use g
State after:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1 : 1 < Set.ncard s
g : Perm α
hg : IsSwap g
hg' : g ∈ stabilizer (Perm α) s
⊢ IsSwap g ∧ g ∈ G

State before:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1 : 1 < Set.ncard s
g : Perm α
hg : IsSwap g
hg' : g ∈ stabilizer (Perm α) s
⊢ IsSwap g ∧ g ∈ G
Tactic:
apply And.intro hg
State after:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1 : 1 < Set.ncard s
g : Perm α
hg : IsSwap g
hg' : g ∈ stabilizer (Perm α) s
⊢ g ∈ G

State before:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1 : 1 < Set.ncard s
g : Perm α
hg : IsSwap g
hg' : g ∈ stabilizer (Perm α) s
⊢ g ∈ G
Tactic:
exact le_of_lt hG hg'
State after:
no goals

State before:
case inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c : 1 < Set.ncard sᶜ
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
obtain ⟨g, hg, hg'⟩ := this sᶜ h1c
State after:
case inr.inl.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c : 1 < Set.ncard sᶜ
g : Perm α
hg : IsSwap g
hg' : g ∈ stabilizer (Perm α) sᶜ
⊢ ∃ g, IsSwap g ∧ g ∈ G

State before:
case inr.inl.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c : 1 < Set.ncard sᶜ
g : Perm α
hg : IsSwap g
hg' : g ∈ stabilizer (Perm α) sᶜ
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
use g
State after:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c : 1 < Set.ncard sᶜ
g : Perm α
hg : IsSwap g
hg' : g ∈ stabilizer (Perm α) sᶜ
⊢ IsSwap g ∧ g ∈ G

State before:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c : 1 < Set.ncard sᶜ
g : Perm α
hg : IsSwap g
hg' : g ∈ stabilizer (Perm α) sᶜ
⊢ IsSwap g ∧ g ∈ G
Tactic:
apply And.intro hg
State after:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c : 1 < Set.ncard sᶜ
g : Perm α
hg : IsSwap g
hg' : g ∈ stabilizer (Perm α) sᶜ
⊢ g ∈ G

State before:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c : 1 < Set.ncard sᶜ
g : Perm α
hg : IsSwap g
hg' : g ∈ stabilizer (Perm α) sᶜ
⊢ g ∈ G
Tactic:
rw [stabilizer_compl] at hg'
State after:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c : 1 < Set.ncard sᶜ
g : Perm α
hg : IsSwap g
hg' : g ∈ stabilizer (Perm α) s
⊢ g ∈ G

State before:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c : 1 < Set.ncard sᶜ
g : Perm α
hg : IsSwap g
hg' : g ∈ stabilizer (Perm α) s
⊢ g ∈ G
Tactic:
exact le_of_lt hG hg'
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ Nat.card α = 2
Tactic:
rw [← Set.ncard_add_ncard_compl s]
State after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ Set.ncard s + Set.ncard sᶜ = 2

State before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ Set.ncard s + Set.ncard sᶜ = 2
Tactic:
convert Nat.one_add 1
State after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ Set.ncard s = 1

case h.e'_2.h.e'_6
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ Set.ncard sᶜ = 1

State before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ Set.ncard s = 1
Tactic:
apply le_antisymm
State after:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ Set.ncard s ≤ 1

case h.e'_2.h.e'_5.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ 1 ≤ Set.ncard s

State before:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ Set.ncard s ≤ 1

case h.e'_2.h.e'_5.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ 1 ≤ Set.ncard s
Tactic:
assumption
State after:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ 1 ≤ Set.ncard s

State before:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ 1 ≤ Set.ncard s
Tactic:
rw [Nat.succ_le_iff, Set.ncard_pos, Set.nonempty_iff_ne_empty]
State after:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ s ≠ ∅

State before:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ s ≠ ∅
Tactic:
intro h
State after:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
h : s = ∅
⊢ False

State before:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
h : s = ∅
⊢ False
Tactic:
apply ne_top_of_lt hG
State after:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
h : s = ∅
⊢ stabilizer (Perm α) s = ⊤

State before:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
h : s = ∅
⊢ stabilizer (Perm α) s = ⊤
Tactic:
rw [h, stabilizer_empty_eq_top]
State after:
no goals

State before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ Set.ncard sᶜ = 1
Tactic:
apply le_antisymm
State after:
case h.e'_2.h.e'_6.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ Set.ncard sᶜ ≤ 1

case h.e'_2.h.e'_6.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ 1 ≤ Set.ncard sᶜ

State before:
case h.e'_2.h.e'_6.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ Set.ncard sᶜ ≤ 1

case h.e'_2.h.e'_6.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ 1 ≤ Set.ncard sᶜ
Tactic:
assumption
State after:
case h.e'_2.h.e'_6.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ 1 ≤ Set.ncard sᶜ

State before:
case h.e'_2.h.e'_6.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ 1 ≤ Set.ncard sᶜ
Tactic:
rw [Nat.succ_le_iff, Set.ncard_pos, Set.nonempty_iff_ne_empty]
State after:
case h.e'_2.h.e'_6.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ sᶜ ≠ ∅

State before:
case h.e'_2.h.e'_6.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
⊢ sᶜ ≠ ∅
Tactic:
intro h
State after:
case h.e'_2.h.e'_6.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
h : sᶜ = ∅
⊢ False

State before:
case h.e'_2.h.e'_6.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
h : sᶜ = ∅
⊢ False
Tactic:
apply ne_top_of_lt hG
State after:
case h.e'_2.h.e'_6.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
h : sᶜ = ∅
⊢ stabilizer (Perm α) s = ⊤

State before:
case h.e'_2.h.e'_6.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
h : sᶜ = ∅
⊢ stabilizer (Perm α) s = ⊤
Tactic:
rw [← stabilizer_compl, h, stabilizer_empty_eq_top]
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
⊢ Fintype.card (Perm α) = 2
Tactic:
rw [Fintype.card_perm, ← Nat.card_eq_fintype_card, hα]
State after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
⊢ Nat.factorial 2 = 2

State before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
⊢ Nat.factorial 2 = 2
Tactic:
simp
State after:
no goals

State before:
case inr.inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊥
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
exfalso
State after:
case inr.inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊥
⊢ False

State before:
case inr.inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊥
⊢ False
Tactic:
exact ne_bot_of_gt hG h
State after:
no goals

State before:
case inr.inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ ∃ g, IsSwap g ∧ g ∈ G
Tactic:
rw [h]
State after:
case inr.inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ ∃ g, IsSwap g ∧ g ∈ ⊤

State before:
case inr.inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ ∃ g, IsSwap g ∧ g ∈ ⊤
Tactic:
rw [← stabilizer_univ_eq_top (Equiv.Perm α) α]
State after:
case inr.inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) _root_.Set.univ

State before:
case inr.inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) _root_.Set.univ
Tactic:
apply this
State after:
case inr.inr.inr.x
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ 1 < Set.ncard _root_.Set.univ

State before:
case inr.inr.inr.x
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ 1 < Set.ncard _root_.Set.univ
Tactic:
rw [Set.ncard_univ, hα]
State after:
case inr.inr.inr.x
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ 1 < 2

State before:
case inr.inr.inr.x
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.29759
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < Set.ncard t → ∃ g, IsSwap g ∧ g ∈ stabilizer (Perm α) t
h1' : Set.ncard s ≤ 1
h1c' : Set.ncard sᶜ ≤ 1
hα : Nat.card α = 2
h : G = ⊤
⊢ 1 < 2
Tactic:
norm_num
State after:
no goals