-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem kerParam_injective (g : Perm α) : Function.Injective (kerParam g)

Proof state:
case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : { x // x ∈ g.cycleFactorsFinset }
⊢ _root_.Disjoint ((fun i => ((fun c => zpowers ↑c) i).subtype.range) a)
    (⨆ j, ⨆ (_ : j ≠ a), (fun i => ((fun c => zpowers ↑c) i).subtype.range) j)

Tactic:
simp only [range_subtype, ne_eq]

Result:
case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : { x // x ∈ g.cycleFactorsFinset }
⊢ _root_.Disjoint (zpowers ↑a) (⨆ j, ⨆ (_ : ¬j = a), zpowers ↑j)

Proof state:
case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : { x // x ∈ g.cycleFactorsFinset }
⊢ _root_.Disjoint (closure {↑a}) (closure (⋃ i, ⋃ (_ : ¬i = a), {↑i}))

Tactic:
apply disjoint_closure_of_disjoint_support

Result:
case refine_1.hind.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : { x // x ∈ g.cycleFactorsFinset }
⊢ ∀ a_1 ∈ {↑a}, ∀ b ∈ ⋃ i, ⋃ (_ : ¬i = a), {↑i}, _root_.Disjoint a_1.support b.support

Proof state:
case refine_1.hind.h.refl.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a b : { x // x ∈ g.cycleFactorsFinset }
h : ¬b = a
⊢ ↑a ≠ ↑b

Tactic:
simp only [ne_eq, ← Subtype.ext_iff]

Result:
case refine_1.hind.h.refl.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a b : { x // x ∈ g.cycleFactorsFinset }
h : ¬b = a
⊢ ¬a = b

Proof state:
case refine_2.h.intro.intro.intro.intro.refl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm { x // x ∈ Function.fixedPoints ⇑g }
b : { x // x ∈ g.cycleFactorsFinset }
⊢ _root_.Disjoint (ofSubtype a).support (↑b).support

Tactic:
exact (ofSubtype_support_disjoint a).mono_right (mem_cycleFactorsFinset_support_le b.2)

Result:
no goals

Proof state:
case refine_1.hind.h.refl.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a b : { x // x ∈ g.cycleFactorsFinset }
h : ¬b = a
⊢ _root_.Disjoint (↑a).support (↑b).support

Tactic:
rw [← disjoint_iff_disjoint_support]

Result:
case refine_1.hind.h.refl.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a b : { x // x ∈ g.cycleFactorsFinset }
h : ¬b = a
⊢ (↑a).Disjoint ↑b

Proof state:
case refine_2.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∀ a ∈ ↑ofSubtype.range, ∀ b ∈ ⋃ i, {↑i}, _root_.Disjoint a.support b.support

Tactic:
rintro - ⟨a, rfl⟩ - ⟨-, ⟨b, rfl⟩, ⟨-⟩⟩

Result:
case refine_2.h.intro.intro.intro.intro.refl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm { x // x ∈ Function.fixedPoints ⇑g }
b : { x // x ∈ g.cycleFactorsFinset }
⊢ _root_.Disjoint (ofSubtype a).support (↑b).support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Function.Injective ⇑(kerParam g)

Tactic:
rw [kerParam, MonoidHom.noncommCoprod_injective]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Function.Injective ⇑ofSubtype ∧
    Function.Injective ⇑(noncommPiCoprod ⋯) ∧ _root_.Disjoint ofSubtype.range (noncommPiCoprod ⋯).range

Proof state:
case refine_1.hind.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : { x // x ∈ g.cycleFactorsFinset }
⊢ ∀ a_1 ∈ {↑a}, ∀ b ∈ ⋃ i, ⋃ (_ : ¬i = a), {↑i}, _root_.Disjoint a_1.support b.support

Tactic:
rintro - ⟨-⟩ - ⟨-, ⟨b, rfl⟩, -, ⟨h, rfl⟩, ⟨-⟩⟩

Result:
case refine_1.hind.h.refl.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a b : { x // x ∈ g.cycleFactorsFinset }
h : ¬b = a
⊢ _root_.Disjoint (↑a).support (↑b).support

Proof state:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ _root_.Disjoint (closure ↑ofSubtype.range) (⨆ i, zpowers ↑i)

Tactic:
simp only [zpowers_eq_closure, ← closure_iUnion]

Result:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ _root_.Disjoint (closure ↑ofSubtype.range) (closure (⋃ i, {↑i}))

Proof state:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ _root_.Disjoint (closure ↑ofSubtype.range) (closure (⋃ i, {↑i}))

Tactic:
apply disjoint_closure_of_disjoint_support

Result:
case refine_2.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∀ a ∈ ↑ofSubtype.range, ∀ b ∈ ⋃ i, {↑i}, _root_.Disjoint a.support b.support

Proof state:
case refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Function.Injective ⇑(noncommPiCoprod ⋯)

Tactic:
apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep

Result:
case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ iSupIndep fun i => ((fun c => zpowers ↑c) i).subtype.range

case refine_1.hinj
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∀ (i : { x // x ∈ g.cycleFactorsFinset }), Function.Injective ⇑((fun c => zpowers ↑c) i).subtype

Proof state:
case refine_1.hinj
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∀ (i : { x // x ∈ g.cycleFactorsFinset }), Function.Injective ⇑((fun c => zpowers ↑c) i).subtype

Tactic:
exact fun i ↦ subtype_injective _

Result:
no goals

Proof state:
case refine_1.hind.h.refl.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a b : { x // x ∈ g.cycleFactorsFinset }
h : ¬b = a
⊢ (↑a).Disjoint ↑b

Tactic:
apply cycleFactorsFinset_pairwise_disjoint g a.2 b.2

Result:
case refine_1.hind.h.refl.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a b : { x // x ∈ g.cycleFactorsFinset }
h : ¬b = a
⊢ ↑a ≠ ↑b

Proof state:
case refine_1.hind.h.refl.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a b : { x // x ∈ g.cycleFactorsFinset }
h : ¬b = a
⊢ ¬a = b

Tactic:
exact ne_comm.mp h

Result:
no goals

Proof state:
case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : { x // x ∈ g.cycleFactorsFinset }
⊢ _root_.Disjoint (zpowers ↑a) (⨆ j, ⨆ (_ : ¬j = a), zpowers ↑j)

Tactic:
simp only [zpowers_eq_closure, ← closure_iUnion]

Result:
case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : { x // x ∈ g.cycleFactorsFinset }
⊢ _root_.Disjoint (closure {↑a}) (closure (⋃ i, ⋃ (_ : ¬i = a), {↑i}))

Proof state:
case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ iSupIndep fun i => ((fun c => zpowers ↑c) i).subtype.range

Tactic:
intro a

Result:
case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : { x // x ∈ g.cycleFactorsFinset }
⊢ _root_.Disjoint ((fun i => ((fun c => zpowers ↑c) i).subtype.range) a)
    (⨆ j, ⨆ (_ : j ≠ a), (fun i => ((fun c => zpowers ↑c) i).subtype.range) j)

Proof state:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ _root_.Disjoint ofSubtype.range (noncommPiCoprod ⋯).range

Tactic:
rw [noncommPiCoprod_range, ← ofSubtype.range.closure_eq]

Result:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ _root_.Disjoint (closure ↑ofSubtype.range) (⨆ i, zpowers ↑i)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Function.Injective ⇑ofSubtype ∧
    Function.Injective ⇑(noncommPiCoprod ⋯) ∧ _root_.Disjoint ofSubtype.range (noncommPiCoprod ⋯).range

Tactic:
refine ⟨ofSubtype_injective, ?_, ?_⟩

Result:
case refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Function.Injective ⇑(noncommPiCoprod ⋯)

case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ _root_.Disjoint ofSubtype.range (noncommPiCoprod ⋯).range