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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ k a τ x = x
Tactic:
simp only [k]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ Function.extend (Kf a 1) (Kf a τ) id x = x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ Function.extend (Kf a 1) (Kf a τ) id x = x
Tactic:
rw [Function.extend_apply']
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ id x = x

case hb
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ¬∃ a_1, Kf a 1 a_1 = x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ id x = x

case hb
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ¬∃ a_1, Kf a 1 a_1 = x
Tactic:
simp only [id.def]
State after:
case hb
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ¬∃ a_1, Kf a 1 a_1 = x

State before:
case hb
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ¬∃ a_1, Kf a 1 a_1 = x
Tactic:
intro hyp
State after:
case hb
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
hyp : ∃ a_1, Kf a 1 a_1 = x
⊢ False

State before:
case hb
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
hyp : ∃ a_1, Kf a 1 a_1 = x
⊢ False
Tactic:
obtain ⟨⟨c, i⟩, rfl⟩ := hyp
State after:
case hb.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hx : Kf a 1 (c, i) ∉ Equiv.Perm.support g
⊢ False

State before:
case hb.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hx : Kf a 1 (c, i) ∉ Equiv.Perm.support g
⊢ False
Tactic:
apply hx
State after:
case hb.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hx : Kf a 1 (c, i) ∉ Equiv.Perm.support g
⊢ Kf a 1 (c, i) ∈ Equiv.Perm.support g

State before:
case hb.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hx : Kf a 1 (c, i) ∉ Equiv.Perm.support g
⊢ Kf a 1 (c, i) ∈ Equiv.Perm.support g
Tactic:
rw [Kf_def, Equiv.Perm.zpow_apply_mem_support]
State after:
case hb.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hx : Kf a 1 (c, i) ∉ Equiv.Perm.support g
⊢ a (1 c) ∈ Equiv.Perm.support g

State before:
case hb.intro.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hx : Kf a 1 (c, i) ∉ Equiv.Perm.support g
⊢ a (1 c) ∈ Equiv.Perm.support g
Tactic:
apply Equiv.Perm.Basis.mem_support'
State after:
no goals