Theorem: OnCycleFactors.mem_support_iff_exists_Kf (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
⊢ x ∈ Equiv.Perm.support g ↔ ∃ c i, x = Kf a 1 (c, i)
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
⊢ x ∈ Equiv.Perm.support g → ∃ c i, x = Kf a 1 (c, i)

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
⊢ (∃ c i, x = Kf a 1 (c, i)) → x ∈ Equiv.Perm.support g

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
⊢ x ∈ Equiv.Perm.support g → ∃ c i, x = Kf a 1 (c, i)
Tactic:
intro hx
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : x ∈ Equiv.Perm.support g
⊢ ∃ c i, x = Kf a 1 (c, i)

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : x ∈ Equiv.Perm.support g
⊢ ∃ c i, x = Kf a 1 (c, i)
Tactic:
rw [← Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff] at hx
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ∃ c i, x = Kf a 1 (c, i)

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ∃ c i, x = Kf a 1 (c, i)
Tactic:
use ⟨g.cycleOf x, hx⟩
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ∃ i, x = Kf a 1 ({ val := Equiv.Perm.cycleOf g x, property := hx }, i)

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ∃ i, x = Kf a 1 ({ val := Equiv.Perm.cycleOf g x, property := hx }, i)
Tactic:
simp only [Kf_def, Equiv.Perm.coe_one, id.def]
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })
Tactic:
let ha := a.mem_support ⟨g.cycleOf x, hx⟩
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
ha : Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx } ∈
  Equiv.Perm.support ↑{ val := Equiv.Perm.cycleOf g x, property := hx } :=
  Equiv.Perm.Basis.mem_support { val := Equiv.Perm.cycleOf g x, property := hx }
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
ha : Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx } ∈
  Equiv.Perm.support ↑{ val := Equiv.Perm.cycleOf g x, property := hx } :=
  Equiv.Perm.Basis.mem_support { val := Equiv.Perm.cycleOf g x, property := hx }
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })
Tactic:
simp only [Subtype.coe_mk, Equiv.Perm.mem_support_cycleOf_iff] at ha
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
ha :
  Equiv.Perm.SameCycle g x (Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx }) ∧
    x ∈ Equiv.Perm.support g
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
ha :
  Equiv.Perm.SameCycle g x (Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx }) ∧
    x ∈ Equiv.Perm.support g
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })
Tactic:
obtain ⟨i, hi⟩ := ha.1.symm
State after:
case h.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
ha :
  Equiv.Perm.SameCycle g x (Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx }) ∧
    x ∈ Equiv.Perm.support g
i : ℤ
hi : (g ^ i) (Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx }) = x
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })

State before:
case h.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
ha :
  Equiv.Perm.SameCycle g x (Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx }) ∧
    x ∈ Equiv.Perm.support g
i : ℤ
hi : (g ^ i) (Equiv.Perm.Basis.toFun { val := Equiv.Perm.cycleOf g x, property := hx }) = x
⊢ ∃ i, x = (g ^ i) (a { val := Equiv.Perm.cycleOf g x, property := hx })
Tactic:
exact ⟨i, hi.symm⟩
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
x : α
⊢ (∃ c i, x = Kf a 1 (c, i)) → x ∈ Equiv.Perm.support g
Tactic:
rintro ⟨c, i, rfl⟩
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ Kf a 1 (c, i) ∈ Equiv.Perm.support g

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ Kf a 1 (c, i) ∈ Equiv.Perm.support g
Tactic:
simp only [Kf_def, Equiv.Perm.zpow_apply_mem_support, Equiv.Perm.coe_one, id.def]
State after:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ a c ∈ Equiv.Perm.support g

State before:
case mpr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ a c ∈ Equiv.Perm.support g
Tactic:
apply Equiv.Perm.mem_cycleFactorsFinset_support_le c.prop
State after:
case mpr.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ a c ∈ Equiv.Perm.support ↑c

State before:
case mpr.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ a c ∈ Equiv.Perm.support ↑c
Tactic:
apply a.mem_support
State after:
no goals