Theorem: Equiv.Perm.self_mem_cycle_factors_commute (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ Commute c g
Tactic:
apply Equiv.Perm.commute_of_mem_cycleFactorsFinset_commute
State after:
case hk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ ∀ c_1 ∈ cycleFactorsFinset g, Commute c c_1

State before:
case hk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
⊢ ∀ c_1 ∈ cycleFactorsFinset g, Commute c c_1
Tactic:
intro c' hc'
State after:
case hk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
⊢ Commute c c'

State before:
case hk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
⊢ Commute c c'
Tactic:
by_cases hcc' : c = c'
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : c = c'
⊢ Commute c c'

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : ¬c = c'
⊢ Commute c c'

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : c = c'
⊢ Commute c c'

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : ¬c = c'
⊢ Commute c c'
Tactic:
rw [hcc']
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : ¬c = c'
⊢ Commute c c'

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : ¬c = c'
⊢ Commute c c'
Tactic:
apply g.cycleFactorsFinset_mem_commute hc hc'
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : ¬c = c'
⊢ c ≠ c'

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
c' : Perm α
hc' : c' ∈ cycleFactorsFinset g
hcc' : ¬c = c'
⊢ c ≠ c'
Tactic:
exact hcc'
State after:
no goals