-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : Finite α
σ τ π ρ : Perm α
hc1 : IsConj σ π
hc2 : IsConj τ ρ
hd1 : σ.Disjoint τ
hd2 : π.Disjoint ρ
intro : ∀ (val : Fintype α), IsConj (σ * τ) (π * ρ)
intro₁ :
  ∀ (val : Fintype α) (f : Perm α) (hc1 : IsConj σ (f * σ * f⁻¹)) (hd2 : (f * σ * f⁻¹).Disjoint ρ),
    IsConj (σ * τ) (f * σ * f⁻¹ * ρ)
intro₂ :
  ∀ (val : Fintype α) (f : Perm α) (hc1 : IsConj σ (f * σ * f⁻¹)) (g : Perm α) (hc2 : IsConj τ (g * τ * g⁻¹))
    (hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)), IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
intro₃ :
  ∀ (val : Fintype α) (f : Perm α) (hc1 : IsConj σ (f * σ * f⁻¹)) (g : Perm α) (hc2 : IsConj τ (g * τ * g⁻¹))
    (hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹))
    (hd1' : (↑(σ * τ).support : Set α) = (↑(σ.support ∪ τ.support) : Set α)),
    IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
intro₄ :
  ∀ (val : Fintype α) (f : Perm α) (hc1 : IsConj σ (f * σ * f⁻¹)) (g : Perm α) (hc2 : IsConj τ (g * τ * g⁻¹))
    (hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹))
    (hd1' : (↑(σ * τ).support : Set α) = (↑(σ.support ∪ τ.support) : Set α))
    (hd2' :
      (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑((f * σ * f⁻¹).support ∪ (g * τ * g⁻¹).support) : Set α)),
    IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
intro₅ :
  ∀ (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 α)),
    IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
intro₆ :
  ∀ (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 α)), IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
intro₇ :
  ∀ (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 α)),
    IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
intro₈ :
  (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 α)) →
                      { x : α // x ∈ (↑(σ * τ).support : Set α) } ≃
                        { x : α // x ∈ (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) }
⊢ IsConj (σ * τ) (π * ρ)
have intro₉ : ∀ (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 α)) (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 sorry)
                    (subtypeEquiv (p := Membership.mem (↑τ.support : Set α)) (q :=
                      Membership.mem (↑(g * τ * g⁻¹).support : Set α)) g sorry))
                  ((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) sorry)) :
        α) :
      α)
    ((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 sorry)
                      (subtypeEquiv (p := Membership.mem (↑τ.support : Set α)) (q :=
                        Membership.mem (↑(g * τ * g⁻¹).support : Set α)) g sorry))
                    ((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)) :
          α) :
      α)
Tactic: classical
  cases nonempty_fintype α
  obtain ⟨f, rfl⟩ := isConj_iff.1 hc1
  obtain ⟨g, rfl⟩ := isConj_iff.1 hc2
  have hd1' := coe_inj.2 hd1.support_mul
  have hd2' := coe_inj.2 hd2.support_mul
  rw [coe_union] at *
  have hd1'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd1)
  have hd2'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd2)
  refine isConj_of_support_equiv ?_ ?_
  · refine ((Equiv.setCongr hd1').trans (Equiv.Set.union hd1'')).trans <|
      (Equiv.sumCongr (subtypeEquiv f fun a => ?_) <| subtypeEquiv g fun a => ?_).trans
        ((Equiv.setCongr hd2').trans (Equiv.Set.union hd2'')).symm <;>
      simp only [Set.mem_image, toEmbedding_apply, exists_eq_right, support_conj, coe_map,
        apply_eq_iff_eq]
  intro x hx
  simp only [trans_apply, symm_trans_apply, Equiv.setCongr_apply, Equiv.setCongr_symm_apply,
    Equiv.sumCongr_apply]
  rw [hd1', Set.mem_union] at hx
  rcases hx with hxσ | hxτ
  · rw [mem_coe, mem_support] at hxσ
    rw [Set.union_apply_left, Set.union_apply_left]
    · simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inl, comp_apply,
        Set.union_symm_apply_left, Subtype.coe_mk, apply_eq_iff_eq, coe_inv]
      have h := (hd2 (f x)).resolve_left ?_
      · rw [mul_apply, mul_apply, coe_inv] at h
        rw [h, symm_apply_apply, (hd1 x).resolve_left hxσ]
      · rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]
    · rwa [Subtype.coe_mk, mem_coe, mem_support]
    · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
        apply_mem_support, mem_support]
  · rw [mem_coe, ← apply_mem_support, mem_support] at hxτ
    rw [Set.union_apply_right, Set.union_apply_right]
    · simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inr, comp_apply,
        Set.union_symm_apply_right, Subtype.coe_mk]
      have h := (hd2 (g (τ x))).resolve_right ?_
      · rw [mul_apply, mul_apply, coe_inv] at h
        rw [coe_inv, coe_inv, symm_apply_apply, h, (hd1 (τ x)).resolve_right hxτ]
      · rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]
    · rwa [Subtype.coe_mk, mem_coe, ← apply_mem_support, mem_support]
    · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 (τ x)).resolve_right hxτ,
        mem_coe, mem_support]
Cleared hypotheses: π, ρ, hc1, hc2, hd2