Theorem: OnCycleFactors.hθ_single (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ (θ g) (1, Pi.mulSingle c { val := ↑c, property := ⋯ }) = ↑c
Tactic:
ext x
State after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
⊢ ((θ g) (1, Pi.mulSingle c { val := ↑c, property := ⋯ })) x = ↑c x

State before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
⊢ ((θ g) (1, Pi.mulSingle c { val := ↑c, property := ⋯ })) x = ↑c x
Tactic:
by_cases hx : x ∈ Function.fixedPoints g
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ((θ g) (1, Pi.mulSingle c { val := ↑c, property := ⋯ })) x = ↑c x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
⊢ ((θ g) (1, Pi.mulSingle c { val := ↑c, property := ⋯ })) x = ↑c x

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
⊢ Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
Tactic:
rw [← Equiv.Perm.cycleOf_ne_one_iff_mem, ne_eq, Equiv.Perm.cycleOf_eq_one_iff]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
⊢ ¬g x = x

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
⊢ ¬g x = x
Tactic:
simpa [Function.mem_fixedPoints_iff] using hx
State after:
no goals

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ((θ g) (1, Pi.mulSingle c { val := ↑c, property := ⋯ })) x = ↑c x
Tactic:
simp only [hθ_1 _ x hx, Equiv.Perm.coe_one, id_eq]
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ x = ↑c x

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ x = ↑c x
Tactic:
apply symm
State after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ↑c x = x

State before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ↑c x = x
Tactic:
rw [← Equiv.Perm.not_mem_support]
State after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ x ∉ Equiv.Perm.support ↑c

State before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ x ∉ Equiv.Perm.support ↑c
Tactic:
simp only [Function.mem_fixedPoints, Function.IsFixedPt, ← Equiv.Perm.not_mem_support] at hx
State after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ x ∉ Equiv.Perm.support ↑c

State before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ x ∉ Equiv.Perm.support ↑c
Tactic:
intro hx'
State after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support ↑c
⊢ False

State before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support ↑c
⊢ False
Tactic:
apply hx
State after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support ↑c
⊢ x ∈ Equiv.Perm.support g

State before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support ↑c
⊢ x ∈ Equiv.Perm.support g
Tactic:
apply Equiv.Perm.mem_cycleFactorsFinset_support_le c.prop hx'
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (1, Pi.mulSingle c { val := ↑c, property := ⋯ })) x = ↑c x
Tactic:
rw [hθ_2 _ x ⟨g.cycleOf x, hx'⟩ rfl]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑((1, Pi.mulSingle c { val := ↑c, property := ⋯ }).2 { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑((1, Pi.mulSingle c { val := ↑c, property := ⋯ }).2 { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x
Tactic:
dsimp only
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(Pi.mulSingle c { val := ↑c, property := ⋯ } { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(Pi.mulSingle c { val := ↑c, property := ⋯ } { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x
Tactic:
by_cases hc : c = ⟨Equiv.Perm.cycleOf g x, hx'⟩
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑(Pi.mulSingle c { val := ↑c, property := ⋯ } { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑(Pi.mulSingle c { val := ↑c, property := ⋯ } { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑(Pi.mulSingle c { val := ↑c, property := ⋯ } { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x
Tactic:
rw [hc, Pi.mulSingle_eq_same, Equiv.Perm.cycleOf_apply_self]
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑(Pi.mulSingle c { val := ↑c, property := ⋯ } { val := Equiv.Perm.cycleOf g x, property := hx' }) x = ↑c x
Tactic:
rw [Pi.mulSingle_eq_of_ne' hc]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑1 x = ↑c x

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑1 x = ↑c x
Tactic:
simp only [OneMemClass.coe_one, Equiv.Perm.coe_one, id_eq]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ x = ↑c x

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ x = ↑c x
Tactic:
apply symm
State after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑c x = x

State before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ ↑c x = x
Tactic:
rw [← Equiv.Perm.not_mem_support]
State after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ x ∉ Equiv.Perm.support ↑c

State before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
⊢ x ∉ Equiv.Perm.support ↑c
Tactic:
intro hxc
State after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
hxc : x ∈ Equiv.Perm.support ↑c
⊢ False

State before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
hxc : x ∈ Equiv.Perm.support ↑c
⊢ False
Tactic:
apply hc
State after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
hxc : x ∈ Equiv.Perm.support ↑c
⊢ c = { val := Equiv.Perm.cycleOf g x, property := hx' }

State before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
hxc : x ∈ Equiv.Perm.support ↑c
⊢ c = { val := Equiv.Perm.cycleOf g x, property := hx' }
Tactic:
rw [← Subtype.coe_inj]
State after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
hxc : x ∈ Equiv.Perm.support ↑c
⊢ ↑c = ↑{ val := Equiv.Perm.cycleOf g x, property := hx' }

State before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Function.fixedPoints ⇑g
hx' : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬c = { val := Equiv.Perm.cycleOf g x, property := hx' }
hxc : x ∈ Equiv.Perm.support ↑c
⊢ ↑c = ↑{ val := Equiv.Perm.cycleOf g x, property := hx' }
Tactic:
exact Equiv.Perm.cycle_is_cycleOf hxc c.prop
State after:
no goals