-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)
hd2' :
  (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)
hd1'' : _root_.Disjoint (↑σ.support : Set α) (↑τ.support : Set α)
hd2'' : _root_.Disjoint (↑(f * σ * f⁻¹).support : Set α) (↑(g * τ * g⁻¹).support : Set α)
intro : { x : α // x ∈ (↑(σ * τ).support : Set α) } ≃ { x : α // x ∈ (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) }
intro₁ :
  ∀ (x : α) (hx : x ∈ (↑(σ * τ).support : Set α)),
    Eq (α := α)
      ((↑((((setCongr (s := (↑(σ * τ).support : Set α)) (t := (↑σ.support : Set α) ∪ (↑τ.support : Set α)) hd1').trans
                      (Set.union (s := (↑σ.support : Set α)) (t := (↑τ.support : Set α)) hd1'')).trans
                  (Equiv.trans
                    (Equiv.sumCongr
                      (subtypeEquiv (p := Membership.mem (↑σ.support : Set α)) (q :=
                        Membership.mem (↑(f * σ * f⁻¹).support : Set α)) f ⋯)
                      (subtypeEquiv (p := Membership.mem (↑τ.support : Set α)) (q :=
                        Membership.mem (↑(g * τ * g⁻¹).support : Set α)) g ⋯))
                    ((setCongr (s := (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α)) (t :=
                            (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)) hd2').trans
                        (Set.union (s := (↑(f * σ * f⁻¹).support : Set α)) (t := (↑(g * τ * g⁻¹).support : Set α))
                          hd2'')).symm) :
                (a : { x : α // x ∈ (↑(σ * τ).support : Set α) }) →
                  { x : α // x ∈ (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑(σ * τ).support : Set α)) ((σ * τ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((f * σ * f⁻¹ * (g * τ * g⁻¹) : (a : α) → α)
          (↑((((setCongr (s := (↑(σ * τ).support : Set α)) (t := (↑σ.support : Set α) ∪ (↑τ.support : Set α))
                            hd1').trans
                        (Set.union (s := (↑σ.support : Set α)) (t := (↑τ.support : Set α)) hd1'')).trans
                    (Equiv.trans
                      (Equiv.sumCongr
                        (subtypeEquiv (p := Membership.mem (↑σ.support : Set α)) (q :=
                          Membership.mem (↑(f * σ * f⁻¹).support : Set α)) f ⋯)
                        (subtypeEquiv (p := Membership.mem (↑τ.support : Set α)) (q :=
                          Membership.mem (↑(g * τ * g⁻¹).support : Set α)) g ⋯))
                      ((setCongr (s := (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α)) (t :=
                              (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)) hd2').trans
                          (Set.union (s := (↑(f * σ * f⁻¹).support : Set α)) (t := (↑(g * τ * g⁻¹).support : Set α))
                            hd2'')).symm) :
                  (a : { x : α // x ∈ (↑(σ * τ).support : Set α) }) →
                    { x : α // x ∈ (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑(σ * τ).support : Set α)) x hx)) :
            α) :
        α)
⊢ IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))

Tactic:
refine isConj_of_support_equiv ?_ ?_

Premises used: Equiv.Perm.isConj_of_support_equiv