Theorem: Equiv.Perm.Basis.Kf_factorsThrough (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
⊢ Function.FactorsThrough (Kf a e') (Kf a e)
Tactic:
rintro ⟨c, i⟩ ⟨d, j⟩ He
State after:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : Kf a e (c, i) = Kf a e (d, j)
⊢ Kf a e' (c, i) = Kf a e' (d, j)

State before:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : Kf a e (c, i) = Kf a e (d, j)
⊢ Kf a e' (c, i) = Kf a e' (d, j)
Tactic:
simp only [Kf_def] at He ⊢
State after:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e c)) = (g ^ j) (a (e d))
⊢ (g ^ i) (a (e' c)) = (g ^ j) (a (e' d))

State before:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e c)) = (g ^ j) (a (e d))
⊢ c = d
Tactic:
apply Equiv.injective e
State after:
case mk.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e c)) = (g ^ j) (a (e d))
⊢ e c = e d

State before:
case mk.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e c)) = (g ^ j) (a (e d))
⊢ e c = e d
Tactic:
rw [← Subtype.coe_inj, Equiv.Perm.Basis.eq_cycleOf, Equiv.Perm.Basis.eq_cycleOf, He]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e c)) = (g ^ j) (a (e d))
hcd : c = d
⊢ (g ^ i) (a (e' c)) = (g ^ j) (a (e' d))
Tactic:
rw [hcd] at He ⊢
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ (g ^ i) (a (e' d)) = (g ^ j) (a (e' d))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ (g ^ i) (a (e' d)) = (g ^ j) (a (e' d))
Tactic:
rw [g.zpow_eq_zpow_on_iff i j,
  ← Equiv.Perm.cycle_is_cycleOf (a := a (e d)) (a.mem_support _) (e d).prop] at He
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ (g ^ i) (a (e' d)) = (g ^ j) (a (e' d))

case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ g (a (e d)) ≠ a (e d)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ (g ^ i) (a (e' d)) = (g ^ j) (a (e' d))

case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ g (a (e d)) ≠ a (e d)
Tactic:
rw [g.zpow_eq_zpow_on_iff,
  ← Equiv.Perm.cycle_is_cycleOf (a := a (e' d)) (a.mem_support _) (e' d).prop, ← hee' d]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card

case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ g (a (e' d)) ≠ a (e' d)

case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ g (a (e d)) ≠ a (e d)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card

case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ g (a (e' d)) ≠ a (e' d)

case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ g (a (e d)) ≠ a (e d)
Tactic:
exact He
State after:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ g (a (e' d)) ≠ a (e' d)

case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ g (a (e d)) ≠ a (e d)

State before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ g (a (e' d)) ≠ a (e' d)
Tactic:
rw [← Equiv.Perm.mem_support, ← Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff,
  ← Equiv.Perm.cycle_is_cycleOf (a := a (e' d)) (a.mem_support _) (e' d).prop]
State after:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ ↑(e' d) ∈ Equiv.Perm.cycleFactorsFinset g

State before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ ↑(e' d) ∈ Equiv.Perm.cycleFactorsFinset g
Tactic:
exact (e' d).prop
State after:
no goals

State before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ g (a (e d)) ≠ a (e d)
Tactic:
rw [← Equiv.Perm.mem_support, ← Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff,
  ← Equiv.Perm.cycle_is_cycleOf (a := a (e d)) (a.mem_support _) (e d).prop]
State after:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ ↑(e d) ∈ Equiv.Perm.cycleFactorsFinset g

State before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ ↑(e d) ∈ Equiv.Perm.cycleFactorsFinset g
Tactic:
exact (e d).prop
State after:
no goals