-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem ofPermHom_support :
    (ofPermHom a τ).support =
      (τ : Perm g.cycleFactorsFinset).support.biUnion (fun c ↦ c.val.support)

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

Tactic:
rw [disjoint_iff_disjoint_support, Finset.disjoint_left] at this

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

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

Tactic:
push_neg

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
H : ↑τ c = c
⊢ ∀ (a : { x // x ∈ g.cycleFactorsFinset }), ↑τ a ≠ a → ↑a x = x

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

Tactic:
exact this (by aesop) hc

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
H : ↑τ c = c
⊢ ∀ (a : { x // x ∈ g.cycleFactorsFinset }), ↑τ a ≠ a → ↑a x = x

Tactic:
intro d hd

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

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

Tactic:
by_cases H : (τ : Perm g.cycleFactorsFinset) c = c

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
H : ↑τ c = c
⊢ (¬∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x) ↔ ↑τ c = c

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

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
H : ↑τ c = c
⊢ (¬∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x) ↔ ↑τ c = c

Tactic:
simp only [H, iff_true]

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
H : ↑τ c = c
⊢ ¬∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x