awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ (a : α),
    a ∈ (↑σ.support : Set α) ↔ Membership.mem (α := α) (↑(f * σ * f⁻¹).support : Set α) ((f : (a : α) → α) a : α)
intro₁ :
  ∀ (a : α),
    a ∈ (↑τ.support : Set α) ↔ Membership.mem (α := α) (↑(g * τ * g⁻¹).support : Set α) ((g : (a : α) → α) a : α)
⊢ { x : α // x ∈ (↑(σ * τ).support : Set α) } ≃ { x : α // x ∈ (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) }

Tactic:
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

Premises used: Equiv.Set.union, Equiv.trans, Equiv.setCongr, Equiv.subtypeEquiv, Equiv.sumCongr, Equiv.symm
-- 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 α)
a : α
⊢ a ∈ (↑σ.support : Set α) ↔ Membership.mem (α := α) (↑(f * σ * f⁻¹).support : Set α) ((f : (a : α) → α) a : α)

Tactic:
simp only [Set.mem_image, toEmbedding_apply, exists_eq_right, support_conj, coe_map,
        apply_eq_iff_eq]

Premises used: Set.mem_image, Equiv.toEmbedding_apply, exists_eq_right, Equiv.Perm.support_conj, Finset.coe_map, Equiv.apply_eq_iff_eq
-- 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 α)
a : α
⊢ a ∈ (↑τ.support : Set α) ↔ Membership.mem (α := α) (↑(g * τ * g⁻¹).support : Set α) ((g : (a : α) → α) a : α)

Tactic:
simp only [Set.mem_image, toEmbedding_apply, exists_eq_right, support_conj, coe_map,
        apply_eq_iff_eq]

Premises used: Set.mem_image, Equiv.toEmbedding_apply, exists_eq_right, Equiv.Perm.support_conj, Finset.coe_map, Equiv.apply_eq_iff_eq
-- 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 α)
⊢ x ∈ (↑σ.support : Set α) ∨ x ∈ (↑τ.support : Set α)

Tactic:
rw [hd1', Set.mem_union] at hx

Premises used: Set.mem_union
-- 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σ : x ∈ (↑σ.support : Set α)
⊢ (σ : (a : α) → α) x ≠ x

Tactic:
rw [mem_coe, mem_support] at hxσ

Premises used: Equiv.Perm.mem_support, Finset.mem_coe
-- 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 :
  ∀ (h : Eq (α := α) ((g * τ * g⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)),
    Eq (α := α) ((τ : (a : α) → α) x : α)
      ((Equiv.symm f : (a : α) → α)
          ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α) :
        α)
intro₁ : ¬Eq (α := α) ((f * σ * f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
⊢ Eq (α := α) ((τ : (a : α) → α) x : α)
    ((Equiv.symm f : (a : α) → α)
        ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α) :
      α)

Tactic:
have h := (hd2 (f x)).resolve_left ?_
-- 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
h : Eq (α := α) ((g * τ * g⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
⊢ Eq (α := α)
    ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α)
    ((f : (a : α) → α) x : α)

Tactic:
rw [mul_apply, mul_apply, coe_inv] at h

Premises used: Equiv.Perm.coe_inv, Equiv.Perm.mul_apply
-- 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
h :
  Eq (α := α)
    ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α)
    ((f : (a : α) → α) x : α)
intro : Eq (α := α) ((τ : (a : α) → α) x : α) ((Equiv.symm f : (a : α) → α) ((f : (a : α) → α) x : α) : α)
intro₁ : (τ : (a : α) → α) x = x
intro₂ intro₃ : x = x
⊢ Eq (α := α) ((τ : (a : α) → α) x : α)
    ((Equiv.symm f : (a : α) → α)
        ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α) :
      α)

Tactic:
rw [h, symm_apply_apply, (hd1 x).resolve_left hxσ]

Premises used: Equiv.symm_apply_apply, Or.resolve_left
-- 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 (α := α) ((f * σ : (a : α) → α) ((f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) ((f : (a : α) → α) x : α)
intro₁ :
  ¬Eq (α := α) ((f : (a : α) → α) ((σ : (a : α) → α) ((f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α)
      ((f : (a : α) → α) x : α)
intro₂ :
  ¬Eq (α := α)
      ((f : (a : α) → α) ((σ : (a : α) → α) ((Equiv.symm f : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α)
      ((f : (a : α) → α) x : α)
intro₃ : ¬Eq (α := α) ((f : (a : α) → α) ((σ : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
intro₄ intro₅ intro₆ intro₇ : ¬(σ : (a : α) → α) x = x
⊢ ¬Eq (α := α) ((f * σ * f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)

Tactic:
rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]

Premises used: Equiv.symm_apply_apply, Equiv.Perm.coe_inv, Equiv.Perm.mul_apply, Equiv.apply_eq_iff_eq
-- 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 : x ∈ (↑σ.support : Set α)
intro₁ : x ∈ σ.support
intro₂ intro₃ intro₄ intro₅ : (σ : (a : α) → α) x ≠ x
⊢ (↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) x ⋯) : α) ∈ (↑σ.support : Set α)

Tactic:
rwa [Subtype.coe_mk, mem_coe, mem_support]

Premises used: Subtype.coe_mk, Equiv.Perm.mem_support, Finset.mem_coe
-- 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 : Membership.mem (α := α) (↑σ.support : Set α) ((σ * τ : (a : α) → α) x : α)
intro₁ : Membership.mem (α := α) (↑σ.support : Set α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
intro₂ : Membership.mem (α := α) (↑σ.support : Set α) ((σ : (a : α) → α) x : α)
intro₃ : Membership.mem (α := α) σ.support ((σ : (a : α) → α) x : α)
intro₄ : x ∈ σ.support
intro₅ intro₆ intro₇ intro₈ : (σ : (a : α) → α) x ≠ x
⊢ Membership.mem (α := α) (↑σ.support : Set α)
    ((↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) ((σ * τ : (a : α) → α) x) ⋯) :
        α) :
      α)

Tactic:
rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
        apply_mem_support, mem_support]

Premises used: Subtype.coe_mk, Equiv.Perm.mem_support, Or.resolve_left, Equiv.Perm.apply_mem_support, Equiv.Perm.mul_apply, Finset.mem_coe
-- 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τ : x ∈ (↑τ.support : Set α)
⊢ Ne (α := α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) ((τ : (a : α) → α) x : α)

Tactic:
rw [mem_coe, ← apply_mem_support, mem_support] at hxτ

Premises used: Equiv.Perm.mem_support, Equiv.Perm.apply_mem_support, Finset.mem_coe
-- 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τ : Ne (α := α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) ((τ : (a : α) → α) x : α)
intro :
  ∀
    (h :
      Eq (α := α) ((f * σ * f⁻¹ : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
        ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)),
    Eq (α := α) ((g : (a : α) → α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
      ((f : (a : α) → α)
          ((σ : (a : α) → α)
              ((f⁻¹ : (a : α) → α)
                  ((g : (a : α) → α) ((τ : (a : α) → α) ((g⁻¹ : (a : α) → α) ((g : (a : α) → α) x : α) : α) : α) : α) :
                α) :
            α) :
        α)
intro₁ :
  ¬Eq (α := α) ((g * τ * g⁻¹ : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
      ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
⊢ Eq (α := α) ((g : (a : α) → α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
    ((f : (a : α) → α)
        ((σ : (a : α) → α)
            ((f⁻¹ : (a : α) → α)
                ((g : (a : α) → α) ((τ : (a : α) → α) ((g⁻¹ : (a : α) → α) ((g : (a : α) → α) x : α) : α) : α) : α) :
              α) :
          α) :
      α)

Tactic:
have h := (hd2 (g (τ x))).resolve_right ?_
-- 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τ : Ne (α := α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) ((τ : (a : α) → α) x : α)
h :
  Eq (α := α) ((f * σ * f⁻¹ : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
    ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
⊢ Eq (α := α)
    ((f : (a : α) → α)
        ((σ : (a : α) → α) ((Equiv.symm f : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α) : α) :
      α)
    ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)

Tactic:
rw [mul_apply, mul_apply, coe_inv] at h

Premises used: Equiv.Perm.coe_inv, Equiv.Perm.mul_apply
-- 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τ : Ne (α := α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) ((τ : (a : α) → α) x : α)
h :
  Eq (α := α)
    ((f : (a : α) → α)
        ((σ : (a : α) → α) ((Equiv.symm f : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α) : α) :
      α)
    ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
intro :
  Eq (α := α) ((g : (a : α) → α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
    ((f : (a : α) → α)
        ((σ : (a : α) → α)
            ((Equiv.symm f : (a : α) → α)
                ((g : (a : α) → α) ((τ : (a : α) → α) ((g⁻¹ : (a : α) → α) ((g : (a : α) → α) x : α) : α) : α) : α) :
              α) :
          α) :
      α)
intro₁ :
  Eq (α := α) ((g : (a : α) → α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
    ((f : (a : α) → α)
        ((σ : (a : α) → α)
            ((Equiv.symm f : (a : α) → α)
                ((g : (a : α) → α)
                    ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((g : (a : α) → α) x : α) : α) : α) :
                  α) :
              α) :
          α) :
      α)
intro₂ :
  Eq (α := α) ((g : (a : α) → α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
    ((f : (a : α) → α)
        ((σ : (a : α) → α) ((Equiv.symm f : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α) : α) :
      α)
intro₃ :
  Eq (α := α) ((g : (a : α) → α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
    ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
intro₄ intro₅ :
  Eq (α := α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
⊢ Eq (α := α) ((g : (a : α) → α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
    ((f : (a : α) → α)
        ((σ : (a : α) → α)
            ((f⁻¹ : (a : α) → α)
                ((g : (a : α) → α) ((τ : (a : α) → α) ((g⁻¹ : (a : α) → α) ((g : (a : α) → α) x : α) : α) : α) : α) :
              α) :
          α) :
      α)

Tactic:
rw [coe_inv, coe_inv, symm_apply_apply, h, (hd1 (τ x)).resolve_right hxτ]

Premises used: Equiv.symm_apply_apply, Equiv.Perm.coe_inv, Or.resolve_right, DFunLike.coe
-- 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τ : Ne (α := α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) ((τ : (a : α) → α) x : α)
intro :
  ¬Eq (α := α) ((g * τ : (a : α) → α) ((g⁻¹ : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α) : α)
      ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
intro₁ :
  ¬Eq (α := α)
      ((g : (a : α) → α)
          ((τ : (a : α) → α) ((g⁻¹ : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α) : α) :
        α)
      ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
intro₂ :
  ¬Eq (α := α)
      ((g : (a : α) → α)
          ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α) : α) :
        α)
      ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
intro₃ :
  ¬Eq (α := α) ((g : (a : α) → α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
      ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
intro₄ intro₅ intro₆ intro₇ : ¬Eq (α := α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) ((τ : (a : α) → α) x : α)
⊢ ¬Eq (α := α) ((g * τ * g⁻¹ : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
      ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)

Tactic:
rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]

Premises used: Equiv.symm_apply_apply, Equiv.Perm.coe_inv, Equiv.Perm.mul_apply, Equiv.apply_eq_iff_eq
-- 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τ : Ne (α := α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) ((τ : (a : α) → α) x : α)
intro : x ∈ (↑τ.support : Set α)
intro₁ : x ∈ τ.support
intro₂ : Membership.mem (α := α) τ.support ((τ : (a : α) → α) x : α)
intro₃ intro₄ intro₅ intro₆ : Ne (α := α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) ((τ : (a : α) → α) x : α)
⊢ (↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) x ⋯) : α) ∈ (↑τ.support : Set α)

Tactic:
rwa [Subtype.coe_mk, mem_coe, ← apply_mem_support, mem_support]

Premises used: Subtype.coe_mk, Equiv.Perm.mem_support, Equiv.Perm.apply_mem_support, Finset.mem_coe
-- 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τ : Ne (α := α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) ((τ : (a : α) → α) x : α)
intro : Membership.mem (α := α) (↑τ.support : Set α) ((σ * τ : (a : α) → α) x : α)
intro₁ : Membership.mem (α := α) (↑τ.support : Set α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
intro₂ : Membership.mem (α := α) (↑τ.support : Set α) ((τ : (a : α) → α) x : α)
intro₃ : Membership.mem (α := α) τ.support ((τ : (a : α) → α) x : α)
intro₄ intro₅ intro₆ intro₇ : Ne (α := α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) ((τ : (a : α) → α) x : α)
⊢ Membership.mem (α := α) (↑τ.support : Set α)
    ((↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) ((σ * τ : (a : α) → α) x) ⋯) :
        α) :
      α)

Tactic:
rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 (τ x)).resolve_right hxτ,
        mem_coe, mem_support]

Premises used: Subtype.coe_mk, Equiv.Perm.mem_support, Equiv.Perm.mul_apply, Or.resolve_right, DFunLike.coe, Finset.mem_coe