Theorem: OnCycleFactors.Iφ_eq_range (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ Iφ g = MonoidHom.range (φ g)
Tactic:
obtain ⟨a⟩ := g.existsBasis
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
⊢ Iφ g = MonoidHom.range (φ g)

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
⊢ Iφ g = MonoidHom.range (φ g)
Tactic:
ext τ
State after:
case intro.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ Iφ g ↔ τ ∈ MonoidHom.range (φ g)

State before:
case intro.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ Iφ g ↔ τ ∈ MonoidHom.range (φ g)
Tactic:
constructor
State after:
case intro.h.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ Iφ g → τ ∈ MonoidHom.range (φ g)

case intro.h.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ MonoidHom.range (φ g) → τ ∈ Iφ g

State before:
case intro.h.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ Iφ g → τ ∈ MonoidHom.range (φ g)
Tactic:
intro hτ
State after:
case intro.h.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ : τ ∈ Iφ g
⊢ τ ∈ MonoidHom.range (φ g)

State before:
case intro.h.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ : τ ∈ Iφ g
⊢ τ ∈ MonoidHom.range (φ g)
Tactic:
exact ⟨(φ' a) ⟨τ, hτ⟩, hφ'_is_rightInverse ⟨τ, hτ⟩⟩
State after:
no goals

State before:
case intro.h.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ MonoidHom.range (φ g) → τ ∈ Iφ g
Tactic:
rw [mem_Iφ_iff]
State after:
case intro.h.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ MonoidHom.range (φ g) →
    ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card

State before:
case intro.h.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ τ ∈ MonoidHom.range (φ g) →
    ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
      (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
Tactic:
exact hφ_eq_card_of_mem_range
State after:
no goals