awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
h3 : ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)
σ₁' : Perm { x : m ⊕ n // ∃ (a : m), Sum.inl a = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (a : m), Sum.inl a = x) h1
σ₂' : Perm { x : m ⊕ n // ∃ (b : n), Sum.inr b = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (b : n), Sum.inr b = x) h3
σ₁ : Perm m :=
  (permCongr (Equiv.symm (ofInjective Sum.inl ⋯)) : (a : Perm (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → Perm m) σ₁'
σ₂ : Perm n :=
  (permCongr (Equiv.symm (ofInjective Sum.inr ⋯)) : (a : Perm (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → Perm n) σ₂'
h₁ :
  ∀ (a : m),
    Eq (α := m ⊕ n) (((σ₁, σ₂).1.sumCongr (σ₁, σ₂).2 : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
      ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
h₂ :
  ∀ (b : n),
    Eq (α := m ⊕ n) (((σ₁, σ₂).1.sumCongr (σ₁, σ₂).2 : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)
      ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)
⊢ (σ₁, σ₂).1.sumCongr (σ₁, σ₂).2 = σ

Tactic:
ext (a | b)
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
h3 : ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)
σ₁' : Perm { x : m ⊕ n // ∃ (a : m), Sum.inl a = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (a : m), Sum.inl a = x) h1
σ₂' : Perm { x : m ⊕ n // ∃ (b : n), Sum.inr b = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (b : n), Sum.inr b = x) h3
σ₁ : Perm m :=
  (permCongr (Equiv.symm (ofInjective Sum.inl ⋯)) : (a : Perm (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → Perm m) σ₁'
σ₂ : Perm n :=
  (permCongr (Equiv.symm (ofInjective Sum.inr ⋯)) : (a : Perm (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → Perm n) σ₂'
a : m
h₁ :
  Eq (α := m ⊕ n)
    ((↑((σ₁' : (a : (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → (↑(Set.range Sum.inl) : Type (max u_2 u_1)))
            ((ofInjective Sum.inl ⋯ : (a : m) → (↑(Set.range Sum.inl) : Type (max u_2 u_1))) a)) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
⊢ Eq (α := m ⊕ n) (((σ₁, σ₂).1.sumCongr (σ₁, σ₂).2 : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)

Tactic:
rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inl_injective]

Premises used: Sum.map_inl, Sum.inl_injective, Equiv.symm_symm, Equiv.sumCongr_apply, Equiv.permCongr_apply, Equiv.apply_ofInjective_symm
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
h3 : ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)
σ₁' : Perm { x : m ⊕ n // ∃ (a : m), Sum.inl a = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (a : m), Sum.inl a = x) h1
σ₂' : Perm { x : m ⊕ n // ∃ (b : n), Sum.inr b = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (b : n), Sum.inr b = x) h3
σ₁ : Perm m :=
  (permCongr (Equiv.symm (ofInjective Sum.inl ⋯)) : (a : Perm (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → Perm m) σ₁'
σ₂ : Perm n :=
  (permCongr (Equiv.symm (ofInjective Sum.inr ⋯)) : (a : Perm (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → Perm n) σ₂'
a : m
h₁ :
  Eq (α := m ⊕ n)
    ((↑((σ₁' : (a : (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → (↑(Set.range Sum.inl) : Type (max u_2 u_1)))
            (Subtype.mk (p := fun (x : m ⊕ n) ↦ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) x) (Sum.inl a)
              ⋯)) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
⊢ Eq (α := m ⊕ n)
    ((↑((σ₁' : (a : (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → (↑(Set.range Sum.inl) : Type (max u_2 u_1)))
            ((ofInjective Sum.inl ⋯ : (a : m) → (↑(Set.range Sum.inl) : Type (max u_2 u_1))) a)) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)

Tactic:
rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]

Premises used: Subtype.coe_mk, Equiv.ofInjective_apply
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
h3 : ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)
σ₁' : Perm { x : m ⊕ n // ∃ (a : m), Sum.inl a = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (a : m), Sum.inl a = x) h1
σ₂' : Perm { x : m ⊕ n // ∃ (b : n), Sum.inr b = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (b : n), Sum.inr b = x) h3
σ₁ : Perm m :=
  (permCongr (Equiv.symm (ofInjective Sum.inl ⋯)) : (a : Perm (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → Perm m) σ₁'
σ₂ : Perm n :=
  (permCongr (Equiv.symm (ofInjective Sum.inr ⋯)) : (a : Perm (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → Perm n) σ₂'
a : m
h₁ :
  Eq (α := m ⊕ n)
    ((↑((σ₁' : (a : { x : m ⊕ n // ∃ (y : m), Sum.inl y = x }) → { x : m ⊕ n // ∃ (y : m), Sum.inl y = x })
            (Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (y : m), Sum.inl y = x) (Sum.inl a) ⋯)) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
⊢ Eq (α := m ⊕ n)
    ((↑((σ₁' : (a : (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → (↑(Set.range Sum.inl) : Type (max u_2 u_1)))
            (Subtype.mk (p := fun (x : m ⊕ n) ↦ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) x) (Sum.inl a)
              ⋯)) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)

Tactic:
dsimp [Set.range]

Premises used: Set.range
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
h3 : ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)
σ₁' : Perm { x : m ⊕ n // ∃ (a : m), Sum.inl a = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (a : m), Sum.inl a = x) h1
σ₂' : Perm { x : m ⊕ n // ∃ (b : n), Sum.inr b = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (b : n), Sum.inr b = x) h3
σ₁ : Perm m :=
  (permCongr (Equiv.symm (ofInjective Sum.inl ⋯)) : (a : Perm (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → Perm m) σ₁'
σ₂ : Perm n :=
  (permCongr (Equiv.symm (ofInjective Sum.inr ⋯)) : (a : Perm (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → Perm n) σ₂'
a : m
h₁ h₂ :
  Eq (α := m ⊕ n)
    ((↑(Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (a : m), Sum.inl a = x)
            ((σ : (a : m ⊕ n) → m ⊕ n)
              (↑(Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (y : m), Sum.inl y = x) (Sum.inl a) ⋯) : m ⊕ n))
            ⋯) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
⊢ Eq (α := m ⊕ n)
    ((↑((σ₁' : (a : { x : m ⊕ n // ∃ (y : m), Sum.inl y = x }) → { x : m ⊕ n // ∃ (y : m), Sum.inl y = x })
            (Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (y : m), Sum.inl y = x) (Sum.inl a) ⋯)) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)

Tactic:
rw [subtypePerm_apply]

Premises used: Equiv.Perm.subtypePerm_apply
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
h3 : ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)
σ₁' : Perm { x : m ⊕ n // ∃ (a : m), Sum.inl a = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (a : m), Sum.inl a = x) h1
σ₂' : Perm { x : m ⊕ n // ∃ (b : n), Sum.inr b = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (b : n), Sum.inr b = x) h3
σ₁ : Perm m :=
  (permCongr (Equiv.symm (ofInjective Sum.inl ⋯)) : (a : Perm (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → Perm m) σ₁'
σ₂ : Perm n :=
  (permCongr (Equiv.symm (ofInjective Sum.inr ⋯)) : (a : Perm (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → Perm n) σ₂'
b : n
h₁ :
  Eq (α := m ⊕ n)
    ((↑((σ₂' : (a : (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → (↑(Set.range Sum.inr) : Type (max u_2 u_1)))
            (Subtype.mk (p := fun (x : m ⊕ n) ↦ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) x) (Sum.inr b)
              ⋯)) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)
⊢ Eq (α := m ⊕ n) (((σ₁, σ₂).1.sumCongr (σ₁, σ₂).2 : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)

Tactic:
rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inr_injective, ofInjective_apply]

Premises used: Sum.inr_injective, Equiv.symm_symm, Equiv.sumCongr_apply, Equiv.permCongr_apply, Equiv.ofInjective_apply, Sum.map_inr, Equiv.apply_ofInjective_symm
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
h3 : ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)
σ₁' : Perm { x : m ⊕ n // ∃ (a : m), Sum.inl a = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (a : m), Sum.inl a = x) h1
σ₂' : Perm { x : m ⊕ n // ∃ (b : n), Sum.inr b = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (b : n), Sum.inr b = x) h3
σ₁ : Perm m :=
  (permCongr (Equiv.symm (ofInjective Sum.inl ⋯)) : (a : Perm (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → Perm m) σ₁'
σ₂ : Perm n :=
  (permCongr (Equiv.symm (ofInjective Sum.inr ⋯)) : (a : Perm (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → Perm n) σ₂'
b : n
h₁ :
  Eq (α := m ⊕ n)
    ((↑((σ₂' : (a : { x : m ⊕ n // ∃ (y : n), Sum.inr y = x }) → { x : m ⊕ n // ∃ (y : n), Sum.inr y = x })
            (Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (y : n), Sum.inr y = x) (Sum.inr b) ⋯)) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)
⊢ Eq (α := m ⊕ n)
    ((↑((σ₂' : (a : (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → (↑(Set.range Sum.inr) : Type (max u_2 u_1)))
            (Subtype.mk (p := fun (x : m ⊕ n) ↦ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) x) (Sum.inr b)
              ⋯)) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)

Tactic:
dsimp [Set.range]

Premises used: Set.range
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
h3 : ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)
σ₁' : Perm { x : m ⊕ n // ∃ (a : m), Sum.inl a = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (a : m), Sum.inl a = x) h1
σ₂' : Perm { x : m ⊕ n // ∃ (b : n), Sum.inr b = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (b : n), Sum.inr b = x) h3
σ₁ : Perm m :=
  (permCongr (Equiv.symm (ofInjective Sum.inl ⋯)) : (a : Perm (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → Perm m) σ₁'
σ₂ : Perm n :=
  (permCongr (Equiv.symm (ofInjective Sum.inr ⋯)) : (a : Perm (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → Perm n) σ₂'
b : n
h₁ h₂ :
  Eq (α := m ⊕ n)
    ((↑(Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (b : n), Sum.inr b = x)
            ((σ : (a : m ⊕ n) → m ⊕ n)
              (↑(Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (y : n), Sum.inr y = x) (Sum.inr b) ⋯) : m ⊕ n))
            ⋯) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)
⊢ Eq (α := m ⊕ n)
    ((↑((σ₂' : (a : { x : m ⊕ n // ∃ (y : n), Sum.inr y = x }) → { x : m ⊕ n // ∃ (y : n), Sum.inr y = x })
            (Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (y : n), Sum.inr y = x) (Sum.inr b) ⋯)) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)

Tactic:
rw [subtypePerm_apply]

Premises used: Equiv.Perm.subtypePerm_apply
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
σ τ : Perm α
hστ : σ.Disjoint τ
n : ℕ
rw : σ ^ n * τ ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1
rw₁ rw₂ : σ ^ n = 1 ∧ τ ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1
⊢ (σ * τ) ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1

Tactic:
rw [hστ.commute.mul_pow, Disjoint.mul_eq_one_iff (hστ.pow_disjoint_pow n n)]

Premises used: Equiv.Perm.Disjoint.commute, Equiv.Perm.Disjoint.pow_disjoint_pow, Commute.mul_pow, Equiv.Perm.Disjoint.mul_eq_one_iff
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h : σ.Disjoint τ
b : β
pos : ∀ (pb : p b), (σ.extendDomain (p := p) f : (a : β) → β) b = b ∨ (τ.extendDomain (p := p) f : (a : β) → β) b = b
neg : ∀ (pb : ¬p b), (σ.extendDomain (p := p) f : (a : β) → β) b = b ∨ (τ.extendDomain (p := p) f : (a : β) → β) b = b
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b ∨ (τ.extendDomain (p := p) f : (a : β) → β) b = b

Tactic:
by_cases pb : p b
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : p b
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b ∨ (τ.extendDomain (p := p) f : (a : β) → β) b = b

Tactic:
(h (f.symm ⟨b, pb⟩)).imp ?_ ?_

Premises used: Subtype.mk, Equiv.symm, Or.imp, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : p b
pos :
  Eq (α := α) ((σ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) : α)
      ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) →
    (σ.extendDomain (p := p) f : (a : β) → β) b = b
pos₁ :
  Eq (α := α) ((τ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) : α)
      ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) →
    (τ.extendDomain (p := p) f : (a : β) → β) b = b
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b ∨ (τ.extendDomain (p := p) f : (a : β) → β) b = b

Tactic:
refine (h (f.symm ⟨b, pb⟩)).imp ?_ ?_

Premises used: Subtype.mk, Equiv.symm, Or.imp, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h_1 : σ.Disjoint τ
b : β
pb : p b
h :
  Eq (α := α) ((σ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) : α)
    ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α)
pos :
  (↑((f : (a : α) → Subtype p) ((σ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α))) :
      β) =
    b
pos₁ : (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb))) : β) = b
pos₂ : (↑(Subtype.mk (p := p) b pb) : β) = b
pos₃ pos₄ : b = b
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b

Tactic:
rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]

Premises used: Subtype.coe_mk, Equiv.apply_symm_apply, Equiv.Perm.extendDomain_apply_subtype
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h_1 : σ.Disjoint τ
b : β
pb : p b
h :
  Eq (α := α) ((τ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) : α)
    ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α)
pos :
  (↑((f : (a : α) → Subtype p) ((τ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α))) :
      β) =
    b
pos₁ : (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb))) : β) = b
pos₂ : (↑(Subtype.mk (p := p) b pb) : β) = b
pos₃ pos₄ : b = b
⊢ (τ.extendDomain (p := p) f : (a : β) → β) b = b

Tactic:
rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]

Premises used: Subtype.coe_mk, Equiv.apply_symm_apply, Equiv.Perm.extendDomain_apply_subtype
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : ¬p b
neg : (σ.extendDomain (p := p) f : (a : β) → β) b = b
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b ∨ (τ.extendDomain (p := p) f : (a : β) → β) b = b

Tactic:
left
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : ¬p b
neg neg₁ : b = b
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b

Tactic:
rw [extendDomain_apply_not_subtype _ _ pb]

Premises used: Equiv.Perm.extendDomain_apply_not_subtype
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : Finite α
σ τ π ρ : Perm α
hc1 : IsConj σ π
hc2 : IsConj τ ρ
hd1 : σ.Disjoint τ
hd2 : π.Disjoint ρ
intro : ∀ (val : Fintype α), IsConj (σ * τ) (π * ρ)
⊢ IsConj (σ * τ) (π * ρ)

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : Finite α
σ τ π ρ : Perm α
hc1 : IsConj σ π
hc2 : IsConj τ ρ
hd1 : σ.Disjoint τ
hd2 : π.Disjoint ρ
val : Fintype α
intro : ∀ (f : Perm α) (hc1 : IsConj σ (f * σ * f⁻¹)) (hd2 : (f * σ * f⁻¹).Disjoint ρ), IsConj (σ * τ) (f * σ * f⁻¹ * ρ)
⊢ IsConj (σ * τ) (π * ρ)

Tactic:
obtain ⟨f, rfl⟩ := isConj_iff.1 hc1

Premises used: isConj_iff, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : Finite α
σ τ ρ : Perm α
hc2 : IsConj τ ρ
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint ρ
intro :
  ∀ (g : Perm α) (hc2 : IsConj τ (g * τ * g⁻¹)) (hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)),
    IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
⊢ IsConj (σ * τ) (f * σ * f⁻¹ * ρ)

Tactic:
obtain ⟨g, rfl⟩ := isConj_iff.1 hc2

Premises used: isConj_iff, Iff.mp, rfl
-- 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⁻¹)
⊢ (↑(σ * τ).support : Set α) = (↑(σ.support ∪ τ.support) : Set α)

Tactic:
have hd1' := coe_inj.2 hd1.support_mul
-- 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 ∪ τ.support) : Set α)
⊢ (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑((f * σ * f⁻¹).support ∪ (g * τ * g⁻¹).support) : Set α)

Tactic:
have hd2' := coe_inj.2 hd2.support_mul
-- 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 ∪ τ.support) : Set α)
hd2' : (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑((f * σ * f⁻¹).support ∪ (g * τ * g⁻¹).support) : Set α)
⊢ (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)

Tactic:
rw [coe_union] at *

Premises used: Finset.coe_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 ∪ τ.support) : Set α)
hd2' : (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑((f * σ * f⁻¹).support ∪ (g * τ * g⁻¹).support) : Set α)
hd1'₁ : (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)
⊢ (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)

Tactic:
rw [coe_union] at *

Premises used: Finset.coe_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 α)
⊢ _root_.Disjoint (↑σ.support : Set α) (↑τ.support : Set α)

Tactic:
have hd1'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd1)
-- 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 α)
⊢ _root_.Disjoint (↑(f * σ * f⁻¹).support : Set α) (↑(g * τ * g⁻¹).support : Set α)

Tactic:
have hd2'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd2)
-- 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 α)
⊢ IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))

Tactic:
isConj_of_support_equiv ?_ ?_

Premises used: Equiv.Perm.isConj_of_support_equiv