internlm/Lean-Github huggingface dataset:
Theorem: isPretransitive_of_cycle
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
⊢ ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
Tactic:
intro x hx
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
⊢ ∃ k, x = k • a
Theorem: isPretransitive_of_cycle
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
⊢ ∃ k, x = k • a
Tactic:
have hg' : (⟨g, hg⟩ : ↥G) ∈ fixingSubgroup G ((↑g.support : Set α)ᶜ) :=
  by
  simp_rw [mem_fixingSubgroup_iff G]
  intro y hy
  simpa only [Set.mem_compl_iff, Finset.mem_coe, Equiv.Perm.not_mem_support] using hy
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
hg' : { val := g, property := hg } ∈ fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
⊢ ∃ k, x = k • a
Theorem: isPretransitive_of_cycle
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
hg' : { val := g, property := hg } ∈ fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
⊢ ∃ k, x = k • a
Tactic:
let g' : fixingSubgroup (↥G) ((↑g.support : Set α)ᶜ) := ⟨(⟨g, hg⟩ : ↥G), hg'⟩
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
hg' : { val := g, property := hg } ∈ fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
g' : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) := { val := { val := g, property := hg }, property := hg' }
⊢ ∃ k, x = k • a
Theorem: isPretransitive_of_cycle
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
hg' : { val := g, property := hg } ∈ fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
g' : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) := { val := { val := g, property := hg }, property := hg' }
⊢ ∃ k, x = k • a
Tactic:
obtain ⟨i, hi⟩ := hgc ((hs x).mpr hx)
Proof state after:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
hg' : { val := g, property := hg } ∈ fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
g' : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) := { val := { val := g, property := hg }, property := hg' }
i : ℤ
hi : (g ^ i) a = x
⊢ ∃ k, x = k • a
Theorem: isPretransitive_of_cycle
Proof state before:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
hg' : { val := g, property := hg } ∈ fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
g' : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) := { val := { val := g, property := hg }, property := hg' }
i : ℤ
hi : (g ^ i) a = x
⊢ ∃ k, x = k • a
Tactic:
use g' ^ i
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
hg' : { val := g, property := hg } ∈ fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
g' : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) := { val := { val := g, property := hg }, property := hg' }
i : ℤ
hi : (g ^ i) a = x
⊢ x = g' ^ i • a
Theorem: isPretransitive_of_cycle
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
hg' : { val := g, property := hg } ∈ fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
g' : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) := { val := { val := g, property := hg }, property := hg' }
i : ℤ
hi : (g ^ i) a = x
⊢ x = g' ^ i • a
Tactic:
exact hi.symm
Proof state after:
no goals
Theorem: isPretransitive_of_cycle
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
⊢ ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
Tactic:
intro x
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
x : α
⊢ g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
Theorem: isPretransitive_of_cycle
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
x : α
⊢ g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
Tactic:
rw [SubMulAction.mem_ofFixingSubgroup_iff]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
x : α
⊢ g • x ≠ x ↔ x ∉ (↑(Equiv.Perm.support g))ᶜ
Theorem: isPretransitive_of_cycle
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
x : α
⊢ g • x ≠ x ↔ x ∉ (↑(Equiv.Perm.support g))ᶜ
Tactic:
simp only [Set.mem_compl_iff, Finset.mem_coe, Equiv.Perm.not_mem_support]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
x : α
⊢ g • x ≠ x ↔ ¬g x = x
Theorem: isPretransitive_of_cycle
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
x : α
⊢ g • x ≠ x ↔ ¬g x = x
Tactic:
rfl
Proof state after:
no goals
Theorem: isPretransitive_of_cycle
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
this : ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
Tactic:
apply IsPretransitive.mk
Proof state after:
case exists_smul_eq
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
this : ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
⊢ ∀ (x y : ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)), ∃ g_1, g_1 • x = y
Theorem: isPretransitive_of_cycle
Proof state before:
case exists_smul_eq
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
this : ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
⊢ ∀ (x y : ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)), ∃ g_1, g_1 • x = y
Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩
Proof state after:
case exists_smul_eq.mk.mk
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
this : ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
y : α
hy : y ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
⊢ ∃ g_1, g_1 • { val := x, property := hx } = { val := y, property := hy }
Theorem: isPretransitive_of_cycle
Proof state before:
case exists_smul_eq.mk.mk
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
this : ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
y : α
hy : y ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
⊢ ∃ g_1, g_1 • { val := x, property := hx } = { val := y, property := hy }
Tactic:
obtain ⟨k, hk⟩ := this x hx
Proof state after:
case exists_smul_eq.mk.mk.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
this : ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
y : α
hy : y ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
k : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk : x = k • a
⊢ ∃ g_1, g_1 • { val := x, property := hx } = { val := y, property := hy }
Theorem: isPretransitive_of_cycle
Proof state before:
case exists_smul_eq.mk.mk.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
this : ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
y : α
hy : y ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
k : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk : x = k • a
⊢ ∃ g_1, g_1 • { val := x, property := hx } = { val := y, property := hy }
Tactic:
obtain ⟨k', hk'⟩ := this y hy
Proof state after:
case exists_smul_eq.mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
this : ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
y : α
hy : y ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
k : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk' : y = k' • a
⊢ ∃ g_1, g_1 • { val := x, property := hx } = { val := y, property := hy }
Theorem: isPretransitive_of_cycle
Proof state before:
case exists_smul_eq.mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
this : ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
y : α
hy : y ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
k : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk' : y = k' • a
⊢ ∃ g_1, g_1 • { val := x, property := hx } = { val := y, property := hy }
Tactic:
use k' * k⁻¹
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
this : ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
y : α
hy : y ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
k : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk' : y = k' • a
⊢ (k' * k⁻¹) • { val := x, property := hx } = { val := y, property := hy }
Theorem: isPretransitive_of_cycle
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
this : ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
y : α
hy : y ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
k : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk' : y = k' • a
⊢ (k' * k⁻¹) • { val := x, property := hx } = { val := y, property := hy }
Tactic:
rw [← SetLike.coe_eq_coe]
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
this : ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
y : α
hy : y ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
k : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk' : y = k' • a
⊢ ↑((k' * k⁻¹) • { val := x, property := hx }) = ↑{ val := y, property := hy }
Theorem: isPretransitive_of_cycle
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
this : ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
y : α
hy : y ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
k : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk' : y = k' • a
⊢ ↑((k' * k⁻¹) • { val := x, property := hx }) = ↑{ val := y, property := hy }
Tactic:
simp only [SetLike.mk_smul_mk]
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
this : ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
y : α
hy : y ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
k : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk' : y = k' • a
⊢ (k' * k⁻¹) • x = y
Theorem: isPretransitive_of_cycle
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
this : ∀ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
y : α
hy : y ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
k : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
hk' : y = k' • a
⊢ (k' * k⁻¹) • x = y
Tactic:
rw [hk, hk', smul_smul, inv_mul_cancel_right]
Proof state after:
no goals
Theorem: isPretransitive_of_cycle
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
⊢ { val := g, property := hg } ∈ fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
Tactic:
simp_rw [mem_fixingSubgroup_iff G]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
⊢ ∀ y ∈ (↑(Equiv.Perm.support g))ᶜ, { val := g, property := hg } • y = y
Theorem: isPretransitive_of_cycle
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
⊢ ∀ y ∈ (↑(Equiv.Perm.support g))ᶜ, { val := g, property := hg } • y = y
Tactic:
intro y hy
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
y : α
hy : y ∈ (↑(Equiv.Perm.support g))ᶜ
⊢ { val := g, property := hg } • y = y
Theorem: isPretransitive_of_cycle
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → Equiv.Perm.SameCycle g a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ
y : α
hy : y ∈ (↑(Equiv.Perm.support g))ᶜ
⊢ { val := g, property := hg } • y = y
Tactic:
simpa only [Set.mem_compl_iff, Finset.mem_coe, Equiv.Perm.not_mem_support] using hy
Proof state after:
no goals
Theorem: Equiv.Perm.IsSwap.cycleType
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Perm α)
inst✝ : DecidableEq α
σ : Perm α
h : IsSwap σ
⊢ Perm.cycleType σ = {2}
Tactic:
simp only [h.isCycle.cycleType, Equiv.Perm.card_support_eq_two.mpr h]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Perm α)
inst✝ : DecidableEq α
σ : Perm α
h : IsSwap σ
⊢ ↑[2] = {2}
Theorem: Equiv.Perm.IsSwap.cycleType
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Perm α)
inst✝ : DecidableEq α
σ : Perm α
h : IsSwap σ
⊢ ↑[2] = {2}
Tactic:
simp only [Multiset.coe_singleton]
Proof state after:
no goals
Theorem: Equiv.Perm.IsSwap.orderOf
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Perm α)
inst✝ : DecidableEq α
σ : Perm α
h : IsSwap σ
⊢ _root_.orderOf σ = 2
Tactic:
rw [← Equiv.Perm.lcm_cycleType, h.cycleType, Multiset.lcm_singleton, normalize_eq]
Proof state after:
no goals
Theorem: jordan_swap
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
⊢ G = ⊤
Tactic:
cases' Nat.lt_or_ge (Fintype.card α) 3 with hα3 hα3
Proof state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
hα3 : Fintype.card α < 3
⊢ G = ⊤

case inr
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
hα3 : Fintype.card α ≥ 3
⊢ G = ⊤