internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ subtypePermOfSupport c ^ k = subtypePerm g hc' ↔ c ^ k = ofSubtype (subtypePerm g hc')
Tactic:
unfold subtypePermOfSupport
Proof state after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ subtypePerm c ⋯ ^ k = subtypePerm g hc' ↔ c ^ k = ofSubtype (subtypePerm g hc')
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ subtypePerm c ⋯ ^ k = subtypePerm g hc' ↔ c ^ k = ofSubtype (subtypePerm g hc')
Tactic:
rw [Equiv.Perm.subtypePerm_zpow]
Proof state after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ subtypePerm (c ^ k) ⋯ = subtypePerm g hc' ↔ c ^ k = ofSubtype (subtypePerm g hc')
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ subtypePerm (c ^ k) ⋯ = subtypePerm g hc' ↔ c ^ k = ofSubtype (subtypePerm g hc')
Tactic:
simp only [Equiv.ext_iff, subtypePerm_apply, Subtype.mk.injEq, Subtype.forall]
Proof state after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ (∀ a ∈ support c, (c ^ k) a = g a) ↔ ∀ (x : α), (c ^ k) x = (ofSubtype (subtypePerm g hc')) x
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ (∀ a ∈ support c, (c ^ k) a = g a) ↔ ∀ (x : α), (c ^ k) x = (ofSubtype (subtypePerm g hc')) x
Tactic:
apply forall_congr'
Proof state after:
case h.h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ ∀ (a : α), a ∈ support c → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case h.h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
⊢ ∀ (a : α), a ∈ support c → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a
Tactic:
intro a
Proof state after:
case h.h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
⊢ a ∈ support c → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case h.h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
⊢ a ∈ support c → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a
Tactic:
by_cases ha : a ∈ c.support
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∈ support c
⊢ a ∈ support c → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∈ support c
⊢ a ∈ support c → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a
Tactic:
rw [imp_iff_right ha]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∈ support c
⊢ (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∈ support c
⊢ (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a
Tactic:
apply Eq.congr rfl
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∈ support c
⊢ g a = (ofSubtype (subtypePerm g hc')) a
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∈ support c
⊢ g a = (ofSubtype (subtypePerm g hc')) a
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_mem]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∈ support c
⊢ g a = ↑((subtypePerm g hc') { val := a, property := ?pos.ha✝ })

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∈ support c
⊢ a ∈ support c
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∈ support c
⊢ g a = ↑((subtypePerm g hc') { val := a, property := ?pos.ha✝ })

case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∈ support c
⊢ a ∈ support c
Tactic:
rfl
Proof state after:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∈ support c
⊢ a ∈ support c
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∈ support c
⊢ a ∈ support c
Tactic:
exact ha
Proof state after:
no goals
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a
Tactic:
rw [iff_true_left _]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ (c ^ k) a = (ofSubtype (subtypePerm g hc')) a

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_not_mem]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ (c ^ k) a = a

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support c

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ (c ^ k) a = a

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support c

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
rw [←Equiv.Perm.not_mem_support]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support (c ^ k)

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support c

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support (c ^ k)

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support c

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
intro ha'
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
ha' : a ∈ support (c ^ k)
⊢ False

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support c

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
ha' : a ∈ support (c ^ k)
⊢ False

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support c

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
apply ha
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
ha' : a ∈ support (c ^ k)
⊢ a ∈ support c

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support c

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
ha' : a ∈ support (c ^ k)
⊢ a ∈ support c

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support c

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
apply Equiv.Perm.support_zpow_le
Proof state after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
ha' : a ∈ support (c ^ k)
⊢ a ∈ support (c ^ ?neg.n✝)

case neg.n
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
ha' : a ∈ support (c ^ k)
⊢ ℤ

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support c

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
ha' : a ∈ support (c ^ k)
⊢ a ∈ support (c ^ ?neg.n✝)

case neg.n
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
ha' : a ∈ support (c ^ k)
⊢ ℤ

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support c

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
exact ha'
Proof state after:
case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support c

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∉ support c

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
exact ha
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Theorem: Equiv.Perm.IsCycle.commute_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
k : ℤ
a : α
ha : a ∉ support c
⊢ a ∈ support c → (c ^ k) a = g a
Tactic:
exact fun b => False.elim (ha b)
Proof state after:
no goals
Theorem: Equiv.Perm.IsCycle.forall_commute_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Perm α
⊢ (∀ c ∈ cycleFactorsFinset g, Commute z c) ↔
    ∀ c ∈ cycleFactorsFinset g,
      ∃ (hc : ∀ (x : α), x ∈ support c ↔ z x ∈ support c), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c
Tactic:
apply forall_congr'
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Perm α
⊢ ∀ (a : Perm α),
    a ∈ cycleFactorsFinset g → Commute z a ↔
      a ∈ cycleFactorsFinset g →
        ∃ (hc : ∀ (x : α), x ∈ support a ↔ z x ∈ support a), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers a
Theorem: Equiv.Perm.IsCycle.forall_commute_iff
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Perm α
⊢ ∀ (a : Perm α),
    a ∈ cycleFactorsFinset g → Commute z a ↔
      a ∈ cycleFactorsFinset g →
        ∃ (hc : ∀ (x : α), x ∈ support a ↔ z x ∈ support a), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers a
Tactic:
intro c
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
⊢ c ∈ cycleFactorsFinset g → Commute z c ↔
    c ∈ cycleFactorsFinset g →
      ∃ (hc : ∀ (x : α), x ∈ support c ↔ z x ∈ support c), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c
Theorem: Equiv.Perm.IsCycle.forall_commute_iff
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
⊢ c ∈ cycleFactorsFinset g → Commute z c ↔
    c ∈ cycleFactorsFinset g →
      ∃ (hc : ∀ (x : α), x ∈ support c ↔ z x ∈ support c), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c
Tactic:
apply imp_congr_right
Proof state after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
⊢ c ∈ cycleFactorsFinset g →
    (Commute z c ↔
      ∃ (hc : ∀ (x : α), x ∈ support c ↔ z x ∈ support c), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c)
Theorem: Equiv.Perm.IsCycle.forall_commute_iff
Proof state before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
⊢ c ∈ cycleFactorsFinset g →
    (Commute z c ↔
      ∃ (hc : ∀ (x : α), x ∈ support c ↔ z x ∈ support c), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c)
Tactic:
intro hc
Proof state after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ Commute z c ↔ ∃ (hc : ∀ (x : α), x ∈ support c ↔ z x ∈ support c), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c
Theorem: Equiv.Perm.IsCycle.forall_commute_iff
Proof state before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ Commute z c ↔ ∃ (hc : ∀ (x : α), x ∈ support c ↔ z x ∈ support c), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c
Tactic:
exact Equiv.Perm.IsCycle.commute_iff (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).1
Proof state after:
no goals
Theorem: Equiv.Perm.subtypePerm_on_cycleFactorsFinset
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ subtypePerm g ⋯ = subtypePermOfSupport c
Tactic:
ext ⟨x, hx⟩
Proof state after:
case H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hx : x ∈ support c
⊢ ↑((subtypePerm g ⋯) { val := x, property := hx }) = ↑((subtypePermOfSupport c) { val := x, property := hx })
Theorem: Equiv.Perm.subtypePerm_on_cycleFactorsFinset
Proof state before:
case H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hx : x ∈ support c
⊢ ↑((subtypePerm g ⋯) { val := x, property := hx }) = ↑((subtypePermOfSupport c) { val := x, property := hx })
Tactic:
simp only [subtypePerm_apply, Subtype.coe_mk, subtypePermOfSupport]
Proof state after:
case H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hx : x ∈ support c
⊢ g x = c x
Theorem: Equiv.Perm.subtypePerm_on_cycleFactorsFinset
Proof state before:
case H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hx : x ∈ support c
⊢ g x = c x
Tactic:
exact ((mem_cycleFactorsFinset_iff.mp hc).2 x hx).symm
Proof state after:
no goals
Theorem: Equiv.Perm.commute_of_mem_cycleFactorsFinset_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ Commute k c ↔
    ∃ (hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c), subtypePerm k hc' ∈ Subgroup.zpowers (subtypePerm g ⋯)
Tactic:
rw [Equiv.Perm.IsCycle.commute_iff' (mem_cycleFactorsFinset_iff.mp hc).1]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ (∃ (hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c),
      subtypePerm k hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)) ↔
    ∃ (hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c), subtypePerm k hc' ∈ Subgroup.zpowers (subtypePerm g ⋯)
Theorem: Equiv.Perm.commute_of_mem_cycleFactorsFinset_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ (∃ (hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c),
      subtypePerm k hc' ∈ Subgroup.zpowers (subtypePermOfSupport c)) ↔
    ∃ (hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c), subtypePerm k hc' ∈ Subgroup.zpowers (subtypePerm g ⋯)
Tactic:
apply exists_congr
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ ∀ (a : ∀ (x : α), x ∈ support c ↔ k x ∈ support c),
    subtypePerm k a ∈ Subgroup.zpowers (subtypePermOfSupport c) ↔ subtypePerm k a ∈ Subgroup.zpowers (subtypePerm g ⋯)
Theorem: Equiv.Perm.commute_of_mem_cycleFactorsFinset_iff
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ ∀ (a : ∀ (x : α), x ∈ support c ↔ k x ∈ support c),
    subtypePerm k a ∈ Subgroup.zpowers (subtypePermOfSupport c) ↔ subtypePerm k a ∈ Subgroup.zpowers (subtypePerm g ⋯)
Tactic:
intro hc'
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
⊢ subtypePerm k hc' ∈ Subgroup.zpowers (subtypePermOfSupport c) ↔ subtypePerm k hc' ∈ Subgroup.zpowers (subtypePerm g ⋯)
Theorem: Equiv.Perm.commute_of_mem_cycleFactorsFinset_iff
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
⊢ subtypePerm k hc' ∈ Subgroup.zpowers (subtypePermOfSupport c) ↔ subtypePerm k hc' ∈ Subgroup.zpowers (subtypePerm g ⋯)
Tactic:
simp only [Subgroup.mem_zpowers_iff]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
⊢ (∃ k_1, subtypePermOfSupport c ^ k_1 = subtypePerm k hc') ↔ ∃ k_1, subtypePerm g ⋯ ^ k_1 = subtypePerm k hc'
Theorem: Equiv.Perm.commute_of_mem_cycleFactorsFinset_iff
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
⊢ (∃ k_1, subtypePermOfSupport c ^ k_1 = subtypePerm k hc') ↔ ∃ k_1, subtypePerm g ⋯ ^ k_1 = subtypePerm k hc'
Tactic:
apply exists_congr
Proof state after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
⊢ ∀ (a : ℤ), subtypePermOfSupport c ^ a = subtypePerm k hc' ↔ subtypePerm g ⋯ ^ a = subtypePerm k hc'