Theorem: OnCycleFactors.φ'_support_le (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
⊢ Equiv.Perm.support (ConjAct.ofConjAct ↑((φ' a) τ)) ≤ Equiv.Perm.support g
Tactic:
intro x
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
⊢ x ∈ Equiv.Perm.support (ConjAct.ofConjAct ↑((φ' a) τ)) → x ∈ Equiv.Perm.support g

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
⊢ x ∈ Equiv.Perm.support (ConjAct.ofConjAct ↑((φ' a) τ)) → x ∈ Equiv.Perm.support g
Tactic:
simp only [Equiv.Perm.mem_support]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x → g x ≠ x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x → g x ≠ x
Tactic:
intro hx' hx
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
hx' : (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x
hx : g x = x
⊢ False

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
hx' : (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x
hx : g x = x
⊢ False
Tactic:
apply hx'
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
hx' : (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x
hx : g x = x
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) x = x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
hx' : (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x
hx : g x = x
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) x = x
Tactic:
rw [← Equiv.Perm.not_mem_support] at hx
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
hx' : (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x
hx : x ∉ Equiv.Perm.support g
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) x = x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
x : α
hx' : (ConjAct.ofConjAct ↑((φ' a) τ)) x ≠ x
hx : x ∉ Equiv.Perm.support g
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) x = x
Tactic:
exact OnCycleFactors.k_apply_of_not_mem_support x hx
State after:
no goals