-- 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 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

Tactic:
have H' : Disjoint ((τ : Perm g.cycleFactorsFinset) c : Perm α)
  ((τ : Perm g.cycleFactorsFinset) d : Perm α) :=
  cycleFactorsFinset_pairwise_disjoint g ((τ : Perm g.cycleFactorsFinset) c).prop
    ((τ : Perm g.cycleFactorsFinset) d).prop (by
    intro h'; apply h
    simpa only [Subtype.coe_inj, EmbeddingLike.apply_eq_iff_eq] using 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
H' : (↑(↑τ c)).Disjoint ↑(↑τ d)
⊢ 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
h' : ↑(↑τ c) = ↑(↑τ d)
⊢ c = d

Tactic:
simpa only [Subtype.coe_inj, EmbeddingLike.apply_eq_iff_eq] using h'

Result:
no goals

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
⊢ a.ofPermHomFun τ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
rw [ofPermHomFun_apply_of_cycleOf_mem a τ hd hm]

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
⊢ (g ^ m) (a (↑τ d)) ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Proof state:
case pos
α : 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:
simp only [h, hd, iff_true, mem_support_self]

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 }
hx' : x ∈ (↑d).support
⊢ False

Tactic:
rw [Function.mem_fixedPoints_iff, ← not_mem_support] at 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
⊢ False

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
h' : ↑(↑τ c) = ↑(↑τ d)
⊢ False

Tactic:
apply 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)
⊢ c = d

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
⊢ a (↑τ d) ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
by_cases h : c = d

Result:
case pos
α : 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

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