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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
⊢ (φ g) ((φ' a) τ) = ↑τ
Tactic:
apply Equiv.Perm.ext
State after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
⊢ ∀ (x : ↑↑(Equiv.Perm.cycleFactorsFinset g)), ((φ g) ((φ' a) τ)) x = ↑τ x

State before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
⊢ ∀ (x : ↑↑(Equiv.Perm.cycleFactorsFinset g)), ((φ g) ((φ' a) τ)) x = ↑τ x
Tactic:
rintro ⟨c, hc⟩
State after:
case H.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ((φ g) ((φ' a) τ)) { val := c, property := hc } = ↑τ { val := c, property := hc }

State before:
case H.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ((φ g) ((φ' a) τ)) { val := c, property := hc } = ↑τ { val := c, property := hc }
Tactic:
rw [← Subtype.coe_inj]
State after:
case H.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ↑(((φ g) ((φ' a) τ)) { val := c, property := hc }) = ↑(↑τ { val := c, property := hc })

State before:
case H.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ↑(((φ g) ((φ' a) τ)) { val := c, property := hc }) = ↑(↑τ { val := c, property := hc })
Tactic:
convert φ_eq'2 g ((φ' a τ)) ⟨c, hc⟩
State after:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ↑(↑τ { val := c, property := hc }) =
    ConjAct.ofConjAct ↑((φ' a) τ) * ↑{ val := c, property := hc } * (ConjAct.ofConjAct ↑((φ' a) τ))⁻¹

State before:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ↑(↑τ { val := c, property := hc }) =
    ConjAct.ofConjAct ↑((φ' a) τ) * ↑{ val := c, property := hc } * (ConjAct.ofConjAct ↑((φ' a) τ))⁻¹
Tactic:
rw [eq_mul_inv_iff_mul_eq]
State after:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ↑(↑τ { val := c, property := hc }) * ConjAct.ofConjAct ↑((φ' a) τ) =
    ConjAct.ofConjAct ↑((φ' a) τ) * ↑{ val := c, property := hc }

State before:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
⊢ ↑(↑τ { val := c, property := hc }) * ConjAct.ofConjAct ↑((φ' a) τ) =
    ConjAct.ofConjAct ↑((φ' a) τ) * ↑{ val := c, property := hc }
Tactic:
ext x
State after:
case h.e'_3.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x : α
⊢ (↑(↑τ { val := c, property := hc }) * ConjAct.ofConjAct ↑((φ' a) τ)) x =
    (ConjAct.ofConjAct ↑((φ' a) τ) * ↑{ val := c, property := hc }) x

State before:
case h.e'_3.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x : α
⊢ (↑(↑τ { val := c, property := hc }) * ConjAct.ofConjAct ↑((φ' a) τ)) x =
    (ConjAct.ofConjAct ↑((φ' a) τ) * ↑{ val := c, property := hc }) x
Tactic:
simp only [Finset.coe_sort_coe, Equiv.Perm.coe_mul, Function.comp_apply]
State after:
case h.e'_3.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x : α
⊢ ↑(↑τ { val := c, property := hc }) ((ConjAct.ofConjAct ↑((φ' a) τ)) x) = (ConjAct.ofConjAct ↑((φ' a) τ)) (c x)

State before:
case h.e'_3.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x : α
⊢ ↑(↑τ { val := c, property := hc }) ((ConjAct.ofConjAct ↑((φ' a) τ)) x) = (ConjAct.ofConjAct ↑((φ' a) τ)) (c x)
Tactic:
apply symm
State after:
case h.e'_3.H.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x : α
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) (c x) = ↑(↑τ { val := c, property := hc }) ((ConjAct.ofConjAct ↑((φ' a) τ)) x)

State before:
case h.e'_3.H.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : Equiv.Perm α
hc : c ∈ ↑(Equiv.Perm.cycleFactorsFinset g)
x : α
⊢ (ConjAct.ofConjAct ↑((φ' a) τ)) (c x) = ↑(↑τ { val := c, property := hc }) ((ConjAct.ofConjAct ↑((φ' a) τ)) x)
Tactic:
exact (k_cycle_apply τ.prop ⟨c, hc⟩ x)
State after:
no goals