-- 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⁻¹))
⊢ 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 α)),
  IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
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