-- 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 α)
x : α
hx : x ∈ (↑(σ * τ).support : Set α)
hxσ : (σ : (a : α) → α) x ≠ x
intro :
  Eq (α := α)
    ((↑(((Set.union (s := (↑(f * σ * f⁻¹).support : Set α)) (t := (↑(g * τ * g⁻¹).support : Set α)) hd2'').symm :
              (a :
                  { b : α // b ∈ (↑(f * σ * f⁻¹).support : Set α) } ⊕
                    { b : α // b ∈ (↑(g * τ * g⁻¹).support : Set α) }) →
                (↑((↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)) : Type u))
            (Sum.map (α := { a : α // a ∈ (↑σ.support : Set α) }) (β := { a : α // a ∈ (↑τ.support : Set α) })
              ((⇑(subtypeEquiv (p := Membership.mem (↑σ.support : Set α)) (q :=
                      Membership.mem (↑(f * σ * f⁻¹).support : Set α)) f ⋯) :
                  (a : { a : α // a ∈ (↑σ.support : Set α) }) → { b : α // b ∈ (↑(f * σ * f⁻¹).support : Set α) }) :
                (a : { a : α // a ∈ (↑σ.support : Set α) }) → { b : α // b ∈ (↑(f * σ * f⁻¹).support : Set α) })
              (⇑(subtypeEquiv (p := Membership.mem (↑τ.support : Set α)) (q :=
                    Membership.mem (↑(g * τ * g⁻¹).support : Set α)) g ⋯) :
                (a : { a : α // a ∈ (↑τ.support : Set α) }) → { b : α // b ∈ (↑(g * τ * g⁻¹).support : Set α) })
              (Sum.inl
                  (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α))
                    (↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α))
                          ((σ * τ : (a : α) → α) x) ⋯) :
                      α)
                    ⋯) :
                (↑(↑σ.support : Set α) : Type u) ⊕ (↑(↑τ.support : Set α) : Type u)))) :
        α) :
      α)
    ((f * σ * f⁻¹ * (g * τ * g⁻¹) : (a : α) → α)
        (↑(((Set.union (s := (↑(f * σ * f⁻¹).support : Set α)) (t := (↑(g * τ * g⁻¹).support : Set α)) hd2'').symm :
                (a :
                    { b : α // b ∈ (↑(f * σ * f⁻¹).support : Set α) } ⊕
                      { b : α // b ∈ (↑(g * τ * g⁻¹).support : Set α) }) →
                  (↑((↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)) : Type u))
              (Sum.map (α := { a : α // a ∈ (↑σ.support : Set α) }) (β := { a : α // a ∈ (↑τ.support : Set α) })
                (⇑(subtypeEquiv (p := Membership.mem (↑σ.support : Set α)) (q :=
                      Membership.mem (↑(f * σ * f⁻¹).support : Set α)) f ⋯) :
                  (a : { a : α // a ∈ (↑σ.support : Set α) }) → { b : α // b ∈ (↑(f * σ * f⁻¹).support : Set α) })
                (⇑(subtypeEquiv (p := Membership.mem (↑τ.support : Set α)) (q :=
                      Membership.mem (↑(g * τ * g⁻¹).support : Set α)) g ⋯) :
                  (a : { a : α // a ∈ (↑τ.support : Set α) }) → { b : α // b ∈ (↑(g * τ * g⁻¹).support : Set α) })
                (Sum.inl
                  (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α))
                    (↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) x ⋯) : α) ⋯)))) :
          α) :
      α)
intro₁ :
  (↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) x ⋯) : α) ∈ (↑σ.support : Set α)
intro₂ :
  Membership.mem (α := α) (↑σ.support : Set α)
    ((↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) ((σ * τ : (a : α) → α) x) ⋯) :
        α) :
      α)
⊢ Eq (α := α)
    ((↑(((Set.union (s := (↑(f * σ * f⁻¹).support : Set α)) (t := (↑(g * τ * g⁻¹).support : Set α)) hd2'').symm :
              (a :
                  { b : α // b ∈ (↑(f * σ * f⁻¹).support : Set α) } ⊕
                    { b : α // b ∈ (↑(g * τ * g⁻¹).support : Set α) }) →
                (↑((↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)) : Type u))
            (Sum.map (α := { a : α // a ∈ (↑σ.support : Set α) }) (β := { a : α // a ∈ (↑τ.support : Set α) })
              (⇑(subtypeEquiv (p := Membership.mem (↑σ.support : Set α)) (q :=
                    Membership.mem (↑(f * σ * f⁻¹).support : Set α)) f ⋯) :
                (a : { a : α // a ∈ (↑σ.support : Set α) }) → { b : α // b ∈ (↑(f * σ * f⁻¹).support : Set α) })
              (⇑(subtypeEquiv (p := Membership.mem (↑τ.support : Set α)) (q :=
                    Membership.mem (↑(g * τ * g⁻¹).support : Set α)) g ⋯) :
                (a : { a : α // a ∈ (↑τ.support : Set α) }) → { b : α // b ∈ (↑(g * τ * g⁻¹).support : Set α) })
              ((Set.union (s := (↑σ.support : Set α)) (t := (↑τ.support : Set α)) hd1'' :
                  (a : (↑((↑σ.support : Set α) ∪ (↑τ.support : Set α)) : Type u)) →
                    (↑(↑σ.support : Set α) : Type u) ⊕ (↑(↑τ.support : Set α) : Type u))
                (Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α))
                    ((σ * τ : (a : α) → α) x) ⋯ :
                  { b : α // b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α) })))) :
        α) :
      α)
    ((f * σ * f⁻¹ * (g * τ * g⁻¹) : (a : α) → α)
        (↑(((Set.union (s := (↑(f * σ * f⁻¹).support : Set α)) (t := (↑(g * τ * g⁻¹).support : Set α)) hd2'').symm :
                (a :
                    { b : α // b ∈ (↑(f * σ * f⁻¹).support : Set α) } ⊕
                      { b : α // b ∈ (↑(g * τ * g⁻¹).support : Set α) }) →
                  (↑((↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)) : Type u))
              (Sum.map (α := { a : α // a ∈ (↑σ.support : Set α) }) (β := { a : α // a ∈ (↑τ.support : Set α) })
                (⇑(subtypeEquiv (p := Membership.mem (↑σ.support : Set α)) (q :=
                      Membership.mem (↑(f * σ * f⁻¹).support : Set α)) f ⋯) :
                  (a : { a : α // a ∈ (↑σ.support : Set α) }) → { b : α // b ∈ (↑(f * σ * f⁻¹).support : Set α) })
                (⇑(subtypeEquiv (p := Membership.mem (↑τ.support : Set α)) (q :=
                      Membership.mem (↑(g * τ * g⁻¹).support : Set α)) g ⋯) :
                  (a : { a : α // a ∈ (↑τ.support : Set α) }) → { b : α // b ∈ (↑(g * τ * g⁻¹).support : Set α) })
                ((Set.union (s := (↑σ.support : Set α)) (t := (↑τ.support : Set α)) hd1'' :
                    (a : (↑((↑σ.support : Set α) ∪ (↑τ.support : Set α)) : Type u)) →
                      (↑(↑σ.support : Set α) : Type u) ⊕ (↑(↑τ.support : Set α) : Type u))
                  (Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) x ⋯)))) :
          α) :
      α)

Tactic:
rw [Set.union_apply_left, Set.union_apply_left]

Premises used: Equiv.Set.union_apply_left