internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.subtypePerm_apply_zpow_of_mem
Proof state before:
case negSucc.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ (g ^ (i + 1)) ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) = x
Tactic:
rw [← Equiv.Perm.subtypePerm_apply_pow_of_mem g s hs]
Proof state after:
case negSucc.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))
        { val := ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }), property := ?negSucc.a.hx }) =
    x

case negSucc.a.hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) ∈ s
Theorem: Equiv.Perm.subtypePerm_apply_zpow_of_mem
Proof state before:
case negSucc.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))
        { val := ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }), property := ?negSucc.a.hx }) =
    x

case negSucc.a.hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) ∈ s
Tactic:
rw [Finset.mk_coe, Equiv.Perm.apply_inv_self, Subtype.coe_mk]
Proof state after:
case negSucc.a.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) ∈ ↑s
Theorem: Equiv.Perm.subtypePerm_apply_zpow_of_mem
Proof state before:
case negSucc.a.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) ∈ ↑s
Tactic:
apply Finset.coe_mem
Proof state after:
no goals
Theorem: Equiv.Perm.isInvariant_of_support_le
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : support c ≤ s
x : α
⊢ x ∈ s ↔ c x ∈ s
Tactic:
by_cases hx' : x ∈ c.support
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : support c ≤ s
x : α
hx' : x ∈ support c
⊢ x ∈ s ↔ c x ∈ s

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : support c ≤ s
x : α
hx' : x ∉ support c
⊢ x ∈ s ↔ c x ∈ s
Theorem: Equiv.Perm.isInvariant_of_support_le
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : support c ≤ s
x : α
hx' : x ∉ support c
⊢ x ∈ s ↔ c x ∈ s
Tactic:
rw [Equiv.Perm.not_mem_support.mp hx']
Proof state after:
no goals
Theorem: Equiv.Perm.isInvariant_of_support_le
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : support c ≤ s
x : α
hx' : x ∈ support c
⊢ x ∈ s ↔ c x ∈ s
Tactic:
simp only [hcs hx', true_iff_iff]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : support c ≤ s
x : α
hx' : x ∈ support c
⊢ c x ∈ s
Theorem: Equiv.Perm.isInvariant_of_support_le
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : support c ≤ s
x : α
hx' : x ∈ support c
⊢ c x ∈ s
Tactic:
exact hcs (Equiv.Perm.apply_mem_support.mpr hx')
Proof state after:
no goals
Theorem: Equiv.Perm.IsCycle.nonempty_support
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
⊢ (support g).Nonempty
Tactic:
rw [Finset.nonempty_iff_ne_empty, Ne.def, Equiv.Perm.support_eq_empty_iff]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
⊢ ¬g = 1
Theorem: Equiv.Perm.IsCycle.nonempty_support
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
⊢ ¬g = 1
Tactic:
exact Equiv.Perm.IsCycle.ne_one hg
Proof state after:
no goals
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ Commute g c ↔
    ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ Commute g c →
    ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ (∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c),
      subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)) →
    Commute g c
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ Commute g c →
    ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
intro hgc
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
⊢ ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
⊢ ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
let hgc' := Equiv.Perm.mem_support_of_commute hgc
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
⊢ ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
⊢ ∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c), subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
use hgc'
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
obtain ⟨a, ha⟩ := Equiv.Perm.IsCycle.nonempty_support hc
Proof state after:
case h.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case h.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
suffices c.SameCycle a (g a) by
  simp only [Equiv.Perm.SameCycle] at this
  obtain ⟨i, hi⟩ := this; use i
  ext ⟨x, hx⟩
  simp only [Equiv.Perm.subtypePermOfSupport, Subtype.coe_mk, Equiv.Perm.subtypePerm_apply]
  rw [Equiv.Perm.subtypePerm_apply_zpow_of_mem]
  suffices c.SameCycle a x by
    obtain ⟨j, rfl⟩ := this
    simp only [← Equiv.Perm.mul_apply, Commute.eq (Commute.zpow_right hgc j)]
    rw [← zpow_add, add_comm i j, zpow_add]
    simp only [Equiv.Perm.mul_apply]
    simp only [EmbeddingLike.apply_eq_iff_eq]
    exact hi
  exact hc.sameCycle (mem_support.mp ha) (mem_support.mp hx)
Proof state after:
case h.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
⊢ SameCycle c a (g a)
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case h.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
⊢ SameCycle c a (g a)
Tactic:
apply hc.sameCycle (mem_support.mp ha) (mem_support.mp ((hgc' a).mp ha))
Proof state after:
no goals
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
this : SameCycle c a (g a)
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
simp only [Equiv.Perm.SameCycle] at this
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
this : ∃ i, (c ^ i) a = g a
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
this : ∃ i, (c ^ i) a = g a
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
obtain ⟨i, hi⟩ := this
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
⊢ subtypePerm g hgc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
Tactic:
use i
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
⊢ (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hgc'
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
⊢ (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hgc'
Tactic:
ext ⟨x, hx⟩
Proof state after:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ ↑(((fun x => subtypePermOfSupport c ^ x) i) { val := x, property := hx }) =
    ↑((subtypePerm g hgc') { val := x, property := hx })
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ ↑(((fun x => subtypePermOfSupport c ^ x) i) { val := x, property := hx }) =
    ↑((subtypePerm g hgc') { val := x, property := hx })
Tactic:
simp only [Equiv.Perm.subtypePermOfSupport, Subtype.coe_mk, Equiv.Perm.subtypePerm_apply]
Proof state after:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ ↑((subtypePerm c ⋯ ^ i) { val := x, property := hx }) = g x
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ ↑((subtypePerm c ⋯ ^ i) { val := x, property := hx }) = g x
Tactic:
rw [Equiv.Perm.subtypePerm_apply_zpow_of_mem]
Proof state after:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ (c ^ i) x = g x
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ (c ^ i) x = g x
Tactic:
suffices c.SameCycle a x by
  obtain ⟨j, rfl⟩ := this
  simp only [← Equiv.Perm.mul_apply, Commute.eq (Commute.zpow_right hgc j)]
  rw [← zpow_add, add_comm i j, zpow_add]
  simp only [Equiv.Perm.mul_apply]
  simp only [EmbeddingLike.apply_eq_iff_eq]
  exact hi
Proof state after:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ SameCycle c a x
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case h.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
⊢ SameCycle c a x
Tactic:
exact hc.sameCycle (mem_support.mp ha) (mem_support.mp hx)
Proof state after:
no goals
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ support c
this : SameCycle c a x
⊢ (c ^ i) x = g x
Tactic:
obtain ⟨j, rfl⟩ := this
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ i) ((c ^ j) a) = g ((c ^ j) a)
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ i) ((c ^ j) a) = g ((c ^ j) a)
Tactic:
simp only [← Equiv.Perm.mul_apply, Commute.eq (Commute.zpow_right hgc j)]
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ i * c ^ j) a = (c ^ j * g) a
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ i * c ^ j) a = (c ^ j * g) a
Tactic:
rw [← zpow_add, add_comm i j, zpow_add]
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ j * c ^ i) a = (c ^ j * g) a
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ j * c ^ i) a = (c ^ j * g) a
Tactic:
simp only [Equiv.Perm.mul_apply]
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ j) ((c ^ i) a) = (c ^ j) (g a)
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ j) ((c ^ i) a) = (c ^ j) (g a)
Tactic:
simp only [EmbeddingLike.apply_eq_iff_eq]
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ i) a = g a
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hgc : Commute g c
hgc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c := mem_support_of_commute hgc
a : α
ha : a ∈ support c
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ support c
⊢ (c ^ i) a = g a
Tactic:
exact hi
Proof state after:
no goals
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
⊢ (∃ (hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c),
      subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)) →
    Commute g c
Tactic:
rintro ⟨hc', h⟩
Proof state after:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
h : subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
⊢ Commute g c
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
h : subtypePerm g hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)
⊢ Commute g c
Tactic:
obtain ⟨i, hi⟩ := h
Proof state after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
⊢ Commute g c
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
⊢ ∀ x ∈ support c, g x = (c ^ i) x
Tactic:
intro x hx
Proof state after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
⊢ g x = (c ^ i) x
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
⊢ g x = (c ^ i) x
Tactic:
let hix := Equiv.Perm.congr_fun hi ⟨x, hx⟩
Proof state after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
hix : ((fun x => subtypePermOfSupport c ^ x) i) { val := x, property := hx } =
  (subtypePerm g hc') { val := x, property := hx } :=
  Perm.congr_fun hi { val := x, property := hx }
⊢ g x = (c ^ i) x
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
hix : ((fun x => subtypePermOfSupport c ^ x) i) { val := x, property := hx } =
  (subtypePerm g hc') { val := x, property := hx } :=
  Perm.congr_fun hi { val := x, property := hx }
⊢ g x = (c ^ i) x
Tactic:
simp only [← Subtype.coe_inj, Equiv.Perm.subtypePermOfSupport] at hix
Proof state after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
hix : ↑((subtypePerm c ⋯ ^ i) { val := x, property := hx }) = ↑((subtypePerm g hc') { val := x, property := hx })
⊢ g x = (c ^ i) x
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
hix : ↑((subtypePerm c ⋯ ^ i) { val := x, property := hx }) = ↑((subtypePerm g hc') { val := x, property := hx })
⊢ g x = (c ^ i) x
Tactic:
simp only [Subtype.coe_mk, Equiv.Perm.subtypePerm_apply,
  Equiv.Perm.subtypePerm_apply_zpow_of_mem] at hix
Proof state after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
hix : (c ^ i) x = g x
⊢ g x = (c ^ i) x
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
x : α
hx : x ∈ support c
hix : (c ^ i) x = g x
⊢ g x = (c ^ i) x
Tactic:
exact hix.symm
Proof state after:
no goals