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

Proof state:
α : 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
⊢ ↑c ≠ ↑d

Tactic:
aesop

Result:
no goals

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

Tactic:
exact mem_support.mp ((mem_cycleFactorsFinset_support_le c.prop) hc) hx

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ a.ofPermHomFun τ x ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

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

Result:
case h.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun τ x ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

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.ofPermHomFun τ x ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

Proof state:
case h.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ¬∃ a ∈ (↑τ).support, x ∈ (↑a).support

Tactic:
rintro ⟨c, -, hc⟩

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

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
⊢ (g ^ m) (a (↑τ c)) ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

Tactic:
conv_lhs => rw [← hm]

Result:
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
⊢ (g ^ m) (a (↑τ c)) ≠ (g ^ m) (a c) ↔ ∃ a, ↑τ a ≠ a ∧ ↑a 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
⊢ (g ^ m) (a (↑τ c)) ≠ (g ^ m) (a c) ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

Tactic:
rw [(g ^ m).injective.ne_iff, a.injective.ne_iff, not_iff_comm]

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

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
⊢ x ∉ (↑d).support

Tactic:
have := g.cycleFactorsFinset_pairwise_disjoint c.prop d.prop

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 → (↑c).Disjoint ↑d
⊢ x ∉ (↑d).support

Proof state:
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

Tactic:
simpa only [H, iff_false, not_not] using ⟨c, H, mem_support.mp hc⟩

Result:
no goals

Proof state:
case h.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun τ x ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

Tactic:
simp only [ofPermHomFun_apply_of_mem_fixedPoints a τ hx, ne_eq, not_true_eq_false, false_iff,
  ← mem_support]

Result:
case h.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ¬∃ a ∈ (↑τ).support, x ∈ (↑a).support

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.ofPermHomFun τ x ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

Tactic:
rw [ofPermHomFun_apply_of_cycleOf_mem a τ hc hm]

Result:
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
⊢ (g ^ m) (a (↑τ c)) ≠ x ↔ ∃ a, ↑τ 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
⊢ ↑d x = x

Tactic:
rw [← not_mem_support]

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
⊢ x ∉ (↑d).support

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ x ∈ (a.ofPermHom τ).support ↔ x ∈ (↑τ).support.biUnion fun c => (↑c).support

Tactic:
simp only [mem_support, Finset.mem_biUnion, ofPermHom_apply]

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ a.ofPermHomFun τ x ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

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

Tactic:
rw [Function.mem_fixedPoints_iff] at hx

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

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ (a.ofPermHom τ).support = (↑τ).support.biUnion fun c => (↑c).support

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ x ∈ (a.ofPermHom τ).support ↔ x ∈ (↑τ).support.biUnion fun c => (↑c).support