Theorem: OnCycleFactors.Group.conj_class_eq_conj_orbit (Jordan/ConjClassCount.lean)

State before:
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g : G
⊢ {k | IsConj g k} = MulAction.orbit (ConjAct G) g
Tactic:
ext k
State after:
case h
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ k ∈ {k | IsConj g k} ↔ k ∈ MulAction.orbit (ConjAct G) g

State before:
case h
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ k ∈ {k | IsConj g k} ↔ k ∈ MulAction.orbit (ConjAct G) g
Tactic:
simp only [Set.mem_setOf_eq, isConj_iff, MulAction.mem_orbit_iff, ConjAct.smul_def]
State after:
case h
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ c, c * g * c⁻¹ = k) ↔ ∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k

State before:
case h
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ c, c * g * c⁻¹ = k) ↔ ∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k
Tactic:
constructor
State after:
case h.mp
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ c, c * g * c⁻¹ = k) → ∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k

case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k

State before:
case h.mp
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ c, c * g * c⁻¹ = k) → ∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k

case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k
Tactic:
rintro ⟨c, hc⟩
State after:
case h.mp.intro
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k c : G
hc : c * g * c⁻¹ = k
⊢ ∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k

case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k

State before:
case h.mp.intro
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k c : G
hc : c * g * c⁻¹ = k
⊢ ∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k

case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k
Tactic:
use ConjAct.toConjAct c
State after:
case h
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k c : G
hc : c * g * c⁻¹ = k
⊢ ConjAct.ofConjAct (ConjAct.toConjAct c) * g * (ConjAct.ofConjAct (ConjAct.toConjAct c))⁻¹ = k

case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k

State before:
case h
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k c : G
hc : c * g * c⁻¹ = k
⊢ ConjAct.ofConjAct (ConjAct.toConjAct c) * g * (ConjAct.ofConjAct (ConjAct.toConjAct c))⁻¹ = k

case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k
Tactic:
simp only [hc, ConjAct.ofConjAct_toConjAct]
State after:
case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k

State before:
case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k
Tactic:
rintro ⟨x, hx⟩
State after:
case h.mpr.intro
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
x : ConjAct G
hx : ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k
⊢ ∃ c, c * g * c⁻¹ = k

State before:
case h.mpr.intro
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
x : ConjAct G
hx : ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k
⊢ ∃ c, c * g * c⁻¹ = k
Tactic:
use ConjAct.ofConjAct x
State after:
no goals