internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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]
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof state after:
no goals
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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'
Proof state after:
no goals
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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'
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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'
Proof state after:
no goals
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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]
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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]
Proof 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 ≠ ∅
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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 = ⊤
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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]
Proof state after:
no goals
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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ᶜ
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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ᶜ
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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]
Proof 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ᶜ ≠ ∅
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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
Proof 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 = ⊤
Theorem: Equiv.Perm.has_swap_of_lt_stabilizer
Proof 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]
Proof state after:
no goals