-- Mathlib/GroupTheory/SpecificGroups/Alternating.lean
theorem isConj_of {σ τ : alternatingGroup α} (hc : IsConj (σ : Perm α) (τ : Perm α))
    (hσ : (σ : Perm α).support.card + 2 ≤ Fintype.card α) : IsConj σ τ

Proof state:
case mk.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * ↑⟨σ, hσ✝⟩ * π⁻¹ = ↑⟨τ, hτ⟩
⊢ IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩

Tactic:
rw [Subtype.coe_mk, Subtype.coe_mk] at hπ

Result:
case mk.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
⊢ IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩

Proof state:
case mk.mk.intro.inr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩

Tactic:
refine isConj_iff.2 ⟨⟨π * swap a b, ?_⟩, Subtype.val_injective ?_⟩

Result:
case mk.mk.intro.inr.intro.intro.intro.intro.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ π * swap a b ∈ alternatingGroup α

case mk.mk.intro.inr.intro.intro.intro.intro.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ ↑(⟨π * swap a b, ?mk.mk.intro.inr.intro.intro.intro.intro.refine_1⟩ * ⟨σ, hσ✝⟩ *
        ⟨π * swap a b, ?mk.mk.intro.inr.intro.intro.intro.intro.refine_1⟩⁻¹) =
    ↑⟨τ, hτ⟩

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
⊢ 2 ≤ σ.supportᶜ.card

Tactic:
rw [Finset.card_compl, le_tsub_iff_left σ.support.card_le_univ]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
⊢ σ.support.card + 2 ≤ card α

Proof state:
case mk.mk.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = 1
⊢ ∃ c, c * ⟨σ, hσ✝⟩ * c⁻¹ = ⟨τ, hτ⟩

Tactic:
refine ⟨⟨π, mem_alternatingGroup.mp h⟩, Subtype.val_injective ?_⟩

Result:
case mk.mk.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = 1
⊢ ↑(⟨π, ⋯⟩ * ⟨σ, hσ✝⟩ * ⟨π, ⋯⟩⁻¹) = ↑⟨τ, hτ⟩

Proof state:
case mk.mk.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = 1
⊢ ↑(⟨π, ⋯⟩ * ⟨σ, hσ✝⟩ * ⟨π, ⋯⟩⁻¹) = ↑⟨τ, hτ⟩

Tactic:
simpa only [Subtype.val, Subgroup.coe_mul, coe_inv, coe_mk] using hπ

Result:
no goals

Proof state:
case mk.mk.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = 1
⊢ IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩

Tactic:
rw [isConj_iff]

Result:
case mk.mk.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = 1
⊢ ∃ c, c * ⟨σ, hσ✝⟩ * c⁻¹ = ⟨τ, hτ⟩

Proof state:
case mk.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
⊢ IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩

Tactic:
obtain ⟨π, hπ⟩ := isConj_iff.1 hc

Result:
case mk.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * ↑⟨σ, hσ✝⟩ * π⁻¹ = ↑⟨τ, hτ⟩
⊢ IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩

Proof state:
case mk.mk.intro.inr.intro.intro.intro.intro.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
hd : (swap a b).Disjoint σ
⊢ π * swap a b * σ * ↑⟨π * swap a b, ⋯⟩⁻¹ = π * σ * π⁻¹

Tactic:
rw [mul_assoc π _ σ, hd.commute.eq, coe_inv, coe_mk]

Result:
case mk.mk.intro.inr.intro.intro.intro.intro.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
hd : (swap a b).Disjoint σ
⊢ π * (σ * swap a b) * (π * swap a b)⁻¹ = π * σ * π⁻¹

Proof state:
case mk.mk.intro.inr.intro.intro.intro.intro.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ π * swap a b * σ * ↑⟨π * swap a b, ⋯⟩⁻¹ = π * σ * π⁻¹

Tactic:
have hd : Disjoint (swap a b) σ := by
  rw [disjoint_iff_disjoint_support, support_swap ab, Finset.disjoint_insert_left,
    Finset.disjoint_singleton_left]
  exact ⟨Finset.mem_compl.1 ha, Finset.mem_compl.1 hb⟩

Result:
case mk.mk.intro.inr.intro.intro.intro.intro.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
hd : (swap a b).Disjoint σ
⊢ π * swap a b * σ * ↑⟨π * swap a b, ⋯⟩⁻¹ = π * σ * π⁻¹