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τ : 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 : α) : α) : α) :
                  α) :
              α) :
          α) :
      α)
⊢ 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 : α) → α) 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 : α) : α) : α) : α) :
              α) :
          α) :
      α)
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 : α) : α) : α) : α) :
      α)
⊢ 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 : α) : α) : α)
  ((g : (a : α) → α) ((τ : (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 : α) : α) : α) : α) :
              α) :
          α) :
      α)
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 : α) : α)
⊢ 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 : α) → α) x : α) : α) ((g : (a : α) → α) ((τ : (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 : α)
⊢ ¬Eq (α := α) ((g * τ * g⁻¹ : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
      ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
have intro : ¬Eq (α := α) ((g * τ : (a : α) → α) ((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]
-- 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 :
  ¬Eq (α := α) ((g * τ : (a : α) → α) ((g⁻¹ : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α) : α)
      ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
⊢ ¬Eq (α := α) ((g * τ * g⁻¹ : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
      ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
have intro₁ : ¬Eq (α := α)
    ((g : (a : α) → α)
        ((τ : (a : α) → α) ((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]
-- 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 :
  ¬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 : α) : α)
⊢ ¬Eq (α := α) ((g * τ * g⁻¹ : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
      ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
have intro₂ : ¬Eq (α := α)
    ((g : (a : α) → α)
        ((τ : (a : α) → α) ((Equiv.symm 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]
-- 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 :
  ¬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 : α) : α)
⊢ ¬Eq (α := α) ((g * τ * g⁻¹ : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
      ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
have intro₃ : ¬Eq (α := α) ((g : (a : α) → α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
    ((g : (a : α) → α) ((τ : (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τ : 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 : α) : α)
⊢ ¬Eq (α := α) ((g * τ * g⁻¹ : (a : α) → α) ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α) : α)
      ((g : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
have intro₄ : ¬Eq (α := α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) ((τ : (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τ : Ne (α := α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) ((τ : (a : α) → α) 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, ← 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 : α)
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, ← 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 : α)
intro : x ∈ (↑τ.support : Set α)
intro₁ : x ∈ τ.support
⊢ (↑(Subtype.mk (p := fun (b : α) ↦ b ∈ (↑σ.support : Set α) ∪ (↑τ.support : Set α)) x ⋯) : α) ∈ (↑τ.support : Set α)
have intro₂ : Membership.mem (α := α) τ.support ((τ : (a : α) → α) x : α)
Tactic: rwa [Subtype.coe_mk, 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 : α)
⊢ 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_right hxτ,
        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τ : Ne (α := α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) ((τ : (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 : Set α) ((σ : (a : α) → α) ((τ : (a : α) → α) x : α) : α)
Tactic: rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 (τ x)).resolve_right hxτ,
        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τ : Ne (α := α) ((τ : (a : α) → α) ((τ : (a : α) → α) x : α) : α) ((τ : (a : α) → α) 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_right hxτ,
        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τ : 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 : α)
⊢ 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_right hxτ,
        mem_coe, mem_support]