Theorem: OnCycleFactors.θ_apply_fst (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
⊢ (θ g) (k, 1) = Equiv.Perm.ofSubtype k
Tactic:
ext x
State after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x

State before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x
Tactic:
by_cases hx : g.cycleOf x ∈ g.cycleFactorsFinset
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x
Tactic:
rw [hθ_2 _ x ⟨g.cycleOf x, hx⟩ rfl]
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑((k, 1).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = (Equiv.Perm.ofSubtype k) x

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑((k, 1).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = (Equiv.Perm.ofSubtype k) x
Tactic:
simp only [Pi.one_apply, OneMemClass.coe_one, Equiv.Perm.coe_one, id_eq]
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ x = (Equiv.Perm.ofSubtype k) x

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ x = (Equiv.Perm.ofSubtype k) x
Tactic:
rw [Equiv.Perm.ofSubtype_apply_of_not_mem]
State after:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ x ∉ MulAction.fixedBy α g

State before:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ x ∉ MulAction.fixedBy α g
Tactic:
simp only [MulAction.mem_fixedBy, Equiv.Perm.smul_def, ← Equiv.Perm.mem_support, ← Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff]
State after:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g

State before:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
Tactic:
exact hx
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x
Tactic:
rw [Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff, Equiv.Perm.not_mem_support] at hx
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : g x = x
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : g x = x
⊢ ((θ g) (k, 1)) x = (Equiv.Perm.ofSubtype k) x
Tactic:
rw [hθ_1 _ x hx, Equiv.Perm.ofSubtype_apply_of_mem]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : g x = x
⊢ ↑((k, 1).1 { val := x, property := hx }) = ↑(k { val := x, property := ?neg.ha✝ })

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : g x = x
⊢ x ∈ MulAction.fixedBy α g

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : g x = x
⊢ ↑((k, 1).1 { val := x, property := hx }) = ↑(k { val := x, property := ?neg.ha✝ })

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
x : α
hx : g x = x
⊢ x ∈ MulAction.fixedBy α g
Tactic:
rfl
State after:
no goals