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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
⊢ ∀ (x : α), x ∈ support c ↔ d x ∈ support c
Tactic:
intro x
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
⊢ x ∈ support c ↔ d x ∈ support c

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
⊢ x ∈ support c ↔ d x ∈ support c
Tactic:
simp only [Equiv.Perm.mem_support, not_iff_not]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
⊢ c x = x ↔ c (d x) = d x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
⊢ c x = x ↔ c (d x) = d x
Tactic:
by_cases h : c = d
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
h : c = d
⊢ c x = x ↔ c (d x) = d x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
h : ¬c = d
⊢ c x = x ↔ c (d x) = d x

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
h : c = d
⊢ c x = x ↔ c (d x) = d x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
h : ¬c = d
⊢ c x = x ↔ c (d x) = d x
Tactic:
rw [← h, EmbeddingLike.apply_eq_iff_eq]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
h : ¬c = d
⊢ c x = x ↔ c (d x) = d x

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ cycleFactorsFinset g
hd : d ∈ cycleFactorsFinset g
x : α
h : ¬c = d
⊢ c x = x ↔ c (d x) = d x
Tactic:
rw [← Equiv.Perm.mul_apply,
    Commute.eq (Equiv.Perm.cycleFactorsFinset_mem_commute g hc hd h),
    Equiv.Perm.mul_apply, EmbeddingLike.apply_eq_iff_eq]
State after:
no goals