awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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
⊢ ¬Eq (α := α) ((f * σ * f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
have intro : ¬Eq (α := α) ((f * σ : (a : α) → α) ((f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) ((f : (a : α) → α) x : α)
Tactic: rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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 : α)
⊢ ¬Eq (α := α) ((f * σ * f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
have intro₁ : ¬Eq (α := α) ((f : (a : α) → α) ((σ : (a : α) → α) ((f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α)
    ((f : (a : α) → α) x : α)
Tactic: rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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 : α)
⊢ ¬Eq (α := α) ((f * σ * f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
have intro₂ : ¬Eq (α := α)
    ((f : (a : α) → α) ((σ : (a : α) → α) ((Equiv.symm f : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α)
    ((f : (a : α) → α) x : α)
Tactic: rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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 : α)
⊢ ¬Eq (α := α) ((f * σ * f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
have intro₃ : ¬Eq (α := α) ((f : (a : α) → α) ((σ : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
Tactic: rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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 : α)
⊢ ¬Eq (α := α) ((f * σ * f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
have intro₄ : ¬(σ : (a : α) → α) x = x
Tactic: rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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
⊢ (↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) x ⋯) : α) ∈ (↑σ.support : Set α)
have intro : x ∈ (↑σ.support : Set α)
Tactic: rwa [Subtype.coe_mk, mem_coe, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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 α)
⊢ (↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) x ⋯) : α) ∈ (↑σ.support : Set α)
have intro₁ : x ∈ σ.support
Tactic: rwa [Subtype.coe_mk, mem_coe, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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
⊢ Membership.mem (α := α) (↑σ.support : Set α)
    ((↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) ((σ * τ : (a : α) → α) x) ⋯) :
        α) :
      α)
have intro : Membership.mem (α := α) (↑σ.support : Set α) ((σ * τ : (a : α) → α) x : α)
Tactic: rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
        apply_mem_support, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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 : α)
⊢ Membership.mem (α := α) (↑σ.support : Set α)
    ((↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) ((σ * τ : (a : α) → α) x) ⋯) :
        α) :
      α)
have intro₁ : Membership.mem (α := α) (↑σ.support : Set α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
Tactic: rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
        apply_mem_support, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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 : α) : α)
⊢ Membership.mem (α := α) (↑σ.support : Set α)
    ((↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) ((σ * τ : (a : α) → α) x) ⋯) :
        α) :
      α)
have intro₂ : Membership.mem (α := α) (↑σ.support : Set α) ((σ : (a : α) → α) x : α)
Tactic: rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
        apply_mem_support, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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 : α)
⊢ Membership.mem (α := α) (↑σ.support : Set α)
    ((↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) ((σ * τ : (a : α) → α) x) ⋯) :
        α) :
      α)
have intro₃ : Membership.mem (α := α) σ.support ((σ : (a : α) → α) x : α)
Tactic: rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
        apply_mem_support, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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 : α)
⊢ Membership.mem (α := α) (↑σ.support : Set α)
    ((↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) ((σ * τ : (a : α) → α) x) ⋯) :
        α) :
      α)
have intro₄ : x ∈ σ.support
Tactic: rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
        apply_mem_support, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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 : α)
⊢ Eq (α := α) ((g : (a : α) → α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
    ((f : (a : α) → α)
        ((σ : (a : α) → α)
            ((f⁻¹ : (a : α) → α)
                ((g : (a : α) → α) ((τ : (a : α) → α) ((g⁻¹ : (a : α) → α) ((g : (a : α) → α) x : α) : α) : α) : α) :
              α) :
          α) :
      α)
have 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 : α) : α) : α) : α) :
              α) :
          α) :
      α)
Tactic: have h := (hd2 (g (τ x))).resolve_right ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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 : α) : α) : α) : α) :
                α) :
            α) :
        α)
⊢ Eq (α := α) ((g : (a : α) → α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
    ((f : (a : α) → α)
        ((σ : (a : α) → α)
            ((f⁻¹ : (a : α) → α)
                ((g : (a : α) → α) ((τ : (a : α) → α) ((g⁻¹ : (a : α) → α) ((g : (a : α) → α) x : α) : α) : α) : α) :
              α) :
          α) :
      α)
have intro₁ : ¬Eq (α := α) ((g * τ * g⁻¹ : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
    ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
Tactic: have h := (hd2 (g (τ x))).resolve_right ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
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 (α := α) ((g : (a : α) → α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
    ((f : (a : α) → α)
        ((σ : (a : α) → α)
            ((f⁻¹ : (a : α) → α)
                ((g : (a : α) → α) ((τ : (a : α) → α) ((g⁻¹ : (a : α) → α) ((g : (a : α) → α) x : α) : α) : α) : α) :
              α) :
          α) :
      α)
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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 : α) : α)
⊢ Eq (α := α) ((g : (a : α) → α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
    ((f : (a : α) → α)
        ((σ : (a : α) → α)
            ((f⁻¹ : (a : α) → α)
                ((g : (a : α) → α) ((τ : (a : α) → α) ((g⁻¹ : (a : α) → α) ((g : (a : α) → α) x : α) : α) : α) : α) :
              α) :
          α) :
      α)
have intro : Eq (α := α) ((g : (a : α) → α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
  ((f : (a : α) → α)
      ((σ : (a : α) → α)
          ((Equiv.symm 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τ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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 : α) : α) : α) : α) :
              α) :
          α) :
      α)
⊢ Eq (α := α) ((g : (a : α) → α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
    ((f : (a : α) → α)
        ((σ : (a : α) → α)
            ((f⁻¹ : (a : α) → α)
                ((g : (a : α) → α) ((τ : (a : α) → α) ((g⁻¹ : (a : α) → α) ((g : (a : α) → α) x : α) : α) : α) : α) :
              α) :
          α) :
      α)
have intro₁ : Eq (α := α) ((g : (a : α) → α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
  ((f : (a : α) → α)
      ((σ : (a : α) → α)
          ((Equiv.symm f : (a : α) → α)
              ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((g : (a : α) → α) x : α) : α) : α) :
                α) :
            α) :
        α) :
    α)
Tactic: rw [coe_inv, coe_inv, symm_apply_apply, h, (hd1 (τ x)).resolve_right hxτ]