internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
case pos
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ s
⊢ ∃ g, g • a = x
Tactic:
exact hs a ha x hx
Proof state after:
no goals
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
case neg
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∉ s
⊢ ∃ g, g • a = x
Tactic:
rw [← Set.mem_compl_iff] at hx
Proof state after:
case neg
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
⊢ ∃ g, g • a = x
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
case neg
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
⊢ ∃ g, g • a = x
Tactic:
obtain ⟨k, hk⟩ := hs' b hb x hx
Proof state after:
case neg.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : G
hk : k • b = x
⊢ ∃ g, g • a = x
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
case neg.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : G
hk : k • b = x
⊢ ∃ g, g • a = x
Tactic:
use k * g
Proof state after:
case h
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : G
hk : k • b = x
⊢ (k * g) • a = x
Theorem: Equiv.Perm.IsPretransitive.of_partition
Proof state before:
case h
α : Type u_1
inst✝² : DecidableEq α
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hG : stabilizer G s ≠ ⊤
a b : α
g : G
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : G
hk : k • b = x
⊢ (k * g) • a = x
Tactic:
rw [MulAction.mul_smul, hgab, hk]
Proof state after:
no goals
Theorem: Equiv.Perm.swap_mem_stabilizer
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ swap a b ∈ stabilizer (Perm α) s
Tactic:
suffices Equiv.swap a b • s ⊆ s by
  rw [mem_stabilizer_iff]
  apply Set.Subset.antisymm
  exact this
  exact Set.subset_set_smul_iff.mpr this
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ swap a b • s ⊆ s
Theorem: Equiv.Perm.swap_mem_stabilizer
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ swap a b • s ⊆ s
Tactic:
rintro _ ⟨x, hx, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
⊢ (fun x => swap a b • x) x ∈ s
Theorem: Equiv.Perm.swap_mem_stabilizer
Proof state before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
⊢ (fun x => swap a b • x) x ∈ s
Tactic:
simp only [Equiv.Perm.smul_def]
Proof state after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
⊢ (swap a b) x ∈ s
Theorem: Equiv.Perm.swap_mem_stabilizer
Proof state before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
⊢ (swap a b) x ∈ s
Tactic:
cases' em (x = a) with hxa hxa'
Proof state after:
case intro.intro.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa : x = a
⊢ (swap a b) x ∈ s

case intro.intro.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
⊢ (swap a b) x ∈ s
Theorem: Equiv.Perm.swap_mem_stabilizer
Proof state before:
case intro.intro.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa : x = a
⊢ (swap a b) x ∈ s

case intro.intro.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
⊢ (swap a b) x ∈ s
Tactic:
rw [hxa, Equiv.swap_apply_left]
Proof state after:
case intro.intro.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa : x = a
⊢ b ∈ s

case intro.intro.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
⊢ (swap a b) x ∈ s
Theorem: Equiv.Perm.swap_mem_stabilizer
Proof state before:
case intro.intro.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa : x = a
⊢ b ∈ s

case intro.intro.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
⊢ (swap a b) x ∈ s
Tactic:
exact hb
Proof state after:
case intro.intro.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
⊢ (swap a b) x ∈ s
Theorem: Equiv.Perm.swap_mem_stabilizer
Proof state before:
case intro.intro.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
⊢ (swap a b) x ∈ s
Tactic:
cases' em (x = b) with hxb hxb'
Proof state after:
case intro.intro.inr.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb : x = b
⊢ (swap a b) x ∈ s

case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ (swap a b) x ∈ s
Theorem: Equiv.Perm.swap_mem_stabilizer
Proof state before:
case intro.intro.inr.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb : x = b
⊢ (swap a b) x ∈ s

case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ (swap a b) x ∈ s
Tactic:
rw [hxb, Equiv.swap_apply_right]
Proof state after:
case intro.intro.inr.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb : x = b
⊢ a ∈ s

case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ (swap a b) x ∈ s
Theorem: Equiv.Perm.swap_mem_stabilizer
Proof state before:
case intro.intro.inr.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb : x = b
⊢ a ∈ s

case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ (swap a b) x ∈ s
Tactic:
exact ha
Proof state after:
case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ (swap a b) x ∈ s
Theorem: Equiv.Perm.swap_mem_stabilizer
Proof state before:
case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ (swap a b) x ∈ s
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne hxa' hxb']
Proof state after:
case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ x ∈ s
Theorem: Equiv.Perm.swap_mem_stabilizer
Proof state before:
case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ x ∈ s
Tactic:
exact hx
Proof state after:
no goals
Theorem: Equiv.Perm.swap_mem_stabilizer
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ swap a b ∈ stabilizer (Perm α) s
Tactic:
rw [mem_stabilizer_iff]
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ swap a b • s = s
Theorem: Equiv.Perm.swap_mem_stabilizer
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ swap a b • s = s
Tactic:
apply Set.Subset.antisymm
Proof state after:
case h₁
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ swap a b • s ⊆ s

case h₂
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ s ⊆ swap a b • s
Theorem: Equiv.Perm.swap_mem_stabilizer
Proof state before:
case h₁
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ swap a b • s ⊆ s

case h₂
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ s ⊆ swap a b • s
Tactic:
exact this
Proof state after:
case h₂
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ s ⊆ swap a b • s
Theorem: Equiv.Perm.swap_mem_stabilizer
Proof state before:
case h₂
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ s ⊆ swap a b • s
Tactic:
exact Set.subset_set_smul_iff.mpr this
Proof state after:
no goals
Theorem: Equiv.Perm.ne_one_of_isSwap
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
hf : IsSwap f
⊢ f ≠ 1
Tactic:
intro h1
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
hf : IsSwap f
h1 : f = 1
⊢ False
Theorem: Equiv.Perm.ne_one_of_isSwap
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
hf : IsSwap f
h1 : f = 1
⊢ False
Tactic:
obtain ⟨x, y, hxy, h⟩ := hf
Proof state after:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : f = swap x y
⊢ False
Theorem: Equiv.Perm.ne_one_of_isSwap
Proof state before:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : f = swap x y
⊢ False
Tactic:
rw [h1] at h
Proof state after:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ False
Theorem: Equiv.Perm.ne_one_of_isSwap
Proof state before:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ False
Tactic:
apply hxy
Proof state after:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ x = y
Theorem: Equiv.Perm.ne_one_of_isSwap
Proof state before:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ x = y
Tactic:
rw [← Equiv.swap_apply_left x y]
Proof state after:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ x = (swap x y) x
Theorem: Equiv.Perm.ne_one_of_isSwap
Proof state before:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ x = (swap x y) x
Tactic:
rw [← h]
Proof state after:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ x = 1 x
Theorem: Equiv.Perm.ne_one_of_isSwap
Proof state before:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ x = 1 x
Tactic:
simp only [Equiv.Perm.coe_one, id.def]
Proof state after:
no goals
Theorem: Equiv.Perm.swap_isSwap_iff
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
⊢ IsSwap (swap a b) ↔ a ≠ b
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
⊢ IsSwap (swap a b) → a ≠ b

case mpr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
⊢ a ≠ b → IsSwap (swap a b)
Theorem: Equiv.Perm.swap_isSwap_iff
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
⊢ IsSwap (swap a b) → a ≠ b
Tactic:
intro h hab
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
⊢ False
Theorem: Equiv.Perm.swap_isSwap_iff
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
⊢ False
Tactic:
suffices Equiv.swap a b ≠ 1 by
  apply this
  rw [← hab, Equiv.swap_self]
  ext x; simp only [Equiv.coe_refl, Equiv.Perm.coe_one]
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
⊢ swap a b ≠ 1
Theorem: Equiv.Perm.swap_isSwap_iff
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
⊢ swap a b ≠ 1
Tactic:
exact ne_one_of_isSwap h
Proof state after:
no goals
Theorem: Equiv.Perm.swap_isSwap_iff
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
this : swap a b ≠ 1
⊢ False
Tactic:
apply this
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
this : swap a b ≠ 1
⊢ swap a b = 1
Theorem: Equiv.Perm.swap_isSwap_iff
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
this : swap a b ≠ 1
⊢ swap a b = 1
Tactic:
rw [← hab, Equiv.swap_self]
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
this : swap a b ≠ 1
⊢ Equiv.refl α = 1
Theorem: Equiv.Perm.swap_isSwap_iff
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
this : swap a b ≠ 1
⊢ Equiv.refl α = 1
Tactic:
ext x
Proof state after:
case H
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
this : swap a b ≠ 1
x : α
⊢ (Equiv.refl α) x = 1 x
Theorem: Equiv.Perm.swap_isSwap_iff
Proof state before:
case H
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
this : swap a b ≠ 1
x : α
⊢ (Equiv.refl α) x = 1 x
Tactic:
simp only [Equiv.coe_refl, Equiv.Perm.coe_one]
Proof state after:
no goals
Theorem: Equiv.Perm.swap_isSwap_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
⊢ a ≠ b → IsSwap (swap a b)
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : a ≠ b
⊢ IsSwap (swap a b)
Theorem: Equiv.Perm.swap_isSwap_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : a ≠ b
⊢ IsSwap (swap a b)
Tactic:
use a
Proof state after:
case h
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : a ≠ b
⊢ ∃ y, a ≠ y ∧ swap a b = swap a y
Theorem: Equiv.Perm.swap_isSwap_iff
Proof state before:
case h
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : a ≠ b
⊢ ∃ y, a ≠ y ∧ swap a b = swap a y
Tactic:
use b
Proof state after:
no goals
Theorem: Equiv.Perm.moves_in
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
⊢ ∀ a ∈ t, ∀ b ∈ t, ∃ g, g • a = b
Tactic:
intro a ha b hb
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ ∃ g, g • a = b
Theorem: Equiv.Perm.moves_in
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ ∃ g, g • a = b
Tactic:
use ⟨Equiv.swap a b, ?_⟩
Proof state after:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ { val := swap a b, property := ?w } • a = b

case w
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ swap a b ∈ G
Theorem: Equiv.Perm.moves_in
Proof state before:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ { val := swap a b, property := ?w } • a = b
Tactic:
change Equiv.swap a b • a = b
Proof state after:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ swap a b • a = b
Theorem: Equiv.Perm.moves_in
Proof state before:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ swap a b • a = b
Tactic:
simp only [Equiv.Perm.smul_def, Equiv.swap_apply_left]
Proof state after:
no goals
Theorem: Equiv.Perm.moves_in
Proof state before:
case w
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ swap a b ∈ G
Tactic:
apply le_of_lt hGt
Proof state after:
case w.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ swap a b ∈ stabilizer (Perm α) t
Theorem: Equiv.Perm.moves_in
Proof state before:
case w.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ swap a b ∈ stabilizer (Perm α) t
Tactic:
apply swap_mem_stabilizer ha hb
Proof state after:
no goals
Theorem: Equiv.Perm.stabilizer_ne_top
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nonempty sᶜ
⊢ stabilizer (Perm α) s ≠ ⊤
Tactic:
obtain ⟨a, ha⟩ := hs
Proof state after:
case intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
hsc : Set.Nonempty sᶜ
a : α
ha : a ∈ s
⊢ stabilizer (Perm α) s ≠ ⊤
Theorem: Equiv.Perm.stabilizer_ne_top
Proof state before:
case intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
hsc : Set.Nonempty sᶜ
a : α
ha : a ∈ s
⊢ stabilizer (Perm α) s ≠ ⊤
Tactic:
obtain ⟨b, hb⟩ := hsc
Proof state after:
case intro.intro
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.20454
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
⊢ stabilizer (Perm α) s ≠ ⊤