-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem ofPermHomFun_apply_mem_support_cycle_iff {x : α} {c : g.cycleFactorsFinset} :
    ofPermHomFun a τ x ∈ ((τ : Perm g.cycleFactorsFinset) c : Perm α).support ↔
      x ∈ c.val.support

Proof state:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∉ g.support
d : { x // x ∈ g.cycleFactorsFinset }
hx' : x ∈ (↑d).support
⊢ x ∈ g.support

Tactic:
exact mem_cycleFactorsFinset_support_le d.prop hx'

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun τ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
simp only [ofPermHomFun_apply_of_mem_fixedPoints a τ hx]

Result:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ Function.fixedPoints ⇑g
⊢ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : { x // x ∈ g.cycleFactorsFinset }
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
h : ¬c = d
H : ∀ ⦃a : α⦄, a ∈ (↑d).support → a ∉ (↑c).support
H' : ∀ ⦃a : α⦄, a ∈ (↑(↑τ d)).support → a ∉ (↑(↑τ c)).support
⊢ a (↑τ d) ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
simp only [H hd, H' (mem_support_self a _)]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : { x // x ∈ g.cycleFactorsFinset }
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
h : ¬c = d
⊢ a (↑τ d) ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
have H : Disjoint c.val d.val :=
  cycleFactorsFinset_pairwise_disjoint g c.prop d.prop (Subtype.coe_ne_coe.mpr h)

Result:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : { x // x ∈ g.cycleFactorsFinset }
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
h : ¬c = d
H : (↑c).Disjoint ↑d
⊢ a (↑τ d) ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : { x // x ∈ g.cycleFactorsFinset }
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
h : ¬c = d
H : (↑c).Disjoint ↑d
H' : (↑(↑τ c)).Disjoint ↑(↑τ d)
⊢ a (↑τ d) ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
rw [disjoint_iff_disjoint_support, Finset.disjoint_right] at H H'

Result:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : { x // x ∈ g.cycleFactorsFinset }
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
h : ¬c = d
H : ∀ ⦃a : α⦄, a ∈ (↑d).support → a ∉ (↑c).support
H' : ∀ ⦃a : α⦄, a ∈ (↑(↑τ d)).support → a ∉ (↑(↑τ c)).support
⊢ a (↑τ d) ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : { x // x ∈ g.cycleFactorsFinset }
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
h : ¬c = d
H : (↑c).Disjoint ↑d
⊢ ↑(↑τ c) ≠ ↑(↑τ d)

Tactic:
intro h'

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : { x // x ∈ g.cycleFactorsFinset }
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
h : ¬c = d
H : (↑c).Disjoint ↑d
h' : ↑(↑τ c) = ↑(↑τ d)
⊢ False

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ Function.fixedPoints ⇑g
this : ∀ (d : { x // x ∈ g.cycleFactorsFinset }), x ∉ (↑d).support
⊢ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
simp only [this]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ Function.fixedPoints ⇑g
⊢ ∀ (d : { x // x ∈ g.cycleFactorsFinset }), x ∉ (↑d).support

Tactic:
intro d hx'

Result:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ Function.fixedPoints ⇑g
d : { x // x ∈ g.cycleFactorsFinset }
hx' : x ∈ (↑d).support
⊢ False

Proof state:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ Function.fixedPoints ⇑g
⊢ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
suffices ∀ (d : g.cycleFactorsFinset), x ∉ (d : Perm α).support by
  simp only [this]

Result:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ Function.fixedPoints ⇑g
⊢ ∀ (d : { x // x ∈ g.cycleFactorsFinset }), x ∉ (↑d).support

Proof state:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∉ g.support
d : { x // x ∈ g.cycleFactorsFinset }
hx' : x ∈ (↑d).support
⊢ False

Tactic:
apply hx

Result:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∉ g.support
d : { x // x ∈ g.cycleFactorsFinset }
hx' : x ∈ (↑d).support
⊢ x ∈ g.support

Proof state:
case inr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : { x // x ∈ g.cycleFactorsFinset }
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
⊢ (g ^ m) (a (↑τ d)) ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
rw [zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff]

Result:
case inr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : { x // x ∈ g.cycleFactorsFinset }
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
⊢ a (↑τ d) ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
⊢ a.ofPermHomFun τ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | ⟨d, hd, m, hm⟩)

Result:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun τ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

case inr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : { x // x ∈ g.cycleFactorsFinset }
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
⊢ a.ofPermHomFun τ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support