Theorem: isPretransitive_of_cycle (Jordan/Jordan.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
g : Equiv.Perm α
hg : g ∈ G
hgc : Equiv.Perm.IsCycle g
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
Tactic:
obtain ⟨a, _, hgc⟩ := hgc
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
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)

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
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
Tactic:
have hs : ∀ x : α, g • x ≠ x ↔
  x ∈ SubMulAction.ofFixingSubgroup G ((↑g.support : Set α)ᶜ) := by
  intro x
  rw [SubMulAction.mem_ofFixingSubgroup_iff]
  simp only [Set.mem_compl_iff, Finset.mem_coe, Equiv.Perm.not_mem_support]
  rfl
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))ᶜ
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)

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))ᶜ
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
Tactic:
suffices ∀ x ∈ SubMulAction.ofFixingSubgroup G ((↑g.support : Set α)ᶜ),
    ∃ k : fixingSubgroup G ((↑g.support : Set α)ᶜ), x = k • a
  by
  apply IsPretransitive.mk
  rintro ⟨x, hx⟩ ⟨y, hy⟩
  obtain ⟨k, hk⟩ := this x hx
  obtain ⟨k', hk'⟩ := this y hy
  use k' * k⁻¹
  rw [← SetLike.coe_eq_coe]
  simp only [SetLike.mk_smul_mk]
  rw [hk, hk', smul_smul, inv_mul_cancel_right]
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 ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ, ∃ k, x = k • a

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
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

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
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

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'⟩
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

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)
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

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
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

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
State after:
no goals

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
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))ᶜ

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]
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))ᶜ

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]
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

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
State after:
no goals

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
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

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⟩
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 }

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
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 }

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
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 }

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⁻¹
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 }

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]
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 }

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]
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

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]
State after:
no goals

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]
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

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
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

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
State after:
no goals