awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
n : ℕ
⊢ ∀ (x : α), p (((f ^ (n + 1))⁻¹ : (a : α) → α) x) ↔ p x

Tactic:
pow_aux (inv_aux.1 hf)

Premises used: _private.0.Equiv.Perm.inv_aux, Nat.iterate, _private.0.Equiv.Perm.pow_aux, Iff.mp
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
n : ℕ
⊢ ∀ (x : α), p (((f ^ (n + 1))⁻¹ : (a : α) → α) x) ↔ p x

Tactic:
exact pow_aux (inv_aux.1 hf)

Premises used: _private.0.Equiv.Perm.inv_aux, _private.0.Equiv.Perm.pow_aux, Iff.mp
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
n : ℕ
⊢ f.subtypePerm (p := p) hf ^ Int.ofNat n = (f ^ Int.ofNat n).subtypePerm (p := p) ⋯

Tactic:
subtypePerm_pow _ _ _

Premises used: zpowRec, Equiv.Perm.subtypePerm_pow
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
n : ℕ
⊢ f.subtypePerm (p := p) hf ^ Int.ofNat n = (f ^ Int.ofNat n).subtypePerm (p := p) ⋯

Tactic:
exact subtypePerm_pow _ _ _

Premises used: Equiv.Perm.subtypePerm_pow
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
n : ℕ
⊢ f.subtypePerm (p := p) hf ^ Int.negSucc n = (f ^ Int.negSucc n).subtypePerm (p := p) ⋯

Tactic:
simp only [zpow_negSucc, subtypePerm_pow, subtypePerm_inv]

Premises used: Equiv.Perm.subtypePerm_inv, zpow_negSucc, Equiv.Perm.subtypePerm_pow
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
f : Perm α
n : ℤ
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
ofNat : ∀ (n : ℕ), f.subtypePerm (p := p) hf ^ Int.ofNat n = (f ^ Int.ofNat n).subtypePerm (p := p) ⋯
negSucc : ∀ (n : ℕ), f.subtypePerm (p := p) hf ^ Int.negSucc n = (f ^ Int.negSucc n).subtypePerm (p := p) ⋯
⊢ f.subtypePerm (p := p) hf ^ n = (f ^ n).subtypePerm (p := p) ⋯

Tactic:
cases n with
  | ofNat n => exact subtypePerm_pow _ _ _
  | negSucc n => simp only [zpow_negSucc, subtypePerm_pow, subtypePerm_inv]

Premises used: Equiv.Perm.subtypePerm_inv, zpow_negSucc, Equiv.Perm.subtypePerm_pow
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
x : α
pos :
  ∀ (hx : p x),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (f.subtypePerm (p := p) h₁) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((f : (a : α) → α) x : α)
neg :
  ∀ (hx : ¬p x),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (f.subtypePerm (p := p) h₁) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((f : (a : α) → α) x : α)
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (f.subtypePerm (p := p) h₁) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    ((f : (a : α) → α) x : α)

Tactic:
by_cases hx : p x
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
x : α
hx : p x
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (f.subtypePerm (p := p) h₁) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    ((f : (a : α) → α) x : α)

Tactic:
(subtypePerm f h₁).extendDomain_apply_subtype _ hx

Premises used: Equiv.Perm.extendDomain_apply_subtype, Equiv.Perm.subtypePerm
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
x : α
hx : p x
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (f.subtypePerm (p := p) h₁) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    ((f : (a : α) → α) x : α)

Tactic:
exact (subtypePerm f h₁).extendDomain_apply_subtype _ hx

Premises used: Equiv.Perm.extendDomain_apply_subtype, Equiv.Perm.subtypePerm
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
x : α
hx : ¬p x
neg : x = (f : (a : α) → α) x
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (f.subtypePerm (p := p) h₁) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    ((f : (a : α) → α) x : α)

Tactic:
rw [ofSubtype, MonoidHom.coe_mk, OneHom.coe_mk,
        Equiv.Perm.extendDomain_apply_not_subtype _ _ hx]

Premises used: OneHom.coe_mk, Equiv.Perm.extendDomain_apply_not_subtype, MonoidHom.coe_mk, Equiv.Perm.ofSubtype
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
x : α
hx : ¬p x
⊢ x = (f : (a : α) → α) x

Tactic:
not_not.mp fun h => hx (h₂ x (Ne.symm h))

Premises used: Classical.not_not, Ne.symm, Iff.mp
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
x : α
hx : ¬p x
⊢ x = (f : (a : α) → α) x

Tactic:
exact not_not.mp fun h => hx (h₂ x (Ne.symm h))

Premises used: Classical.not_not, Ne.symm, Iff.mp
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
a : α
f : Perm (Subtype p)
ha : p a
⊢ Eq (α := α) ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) f : Perm α) : (a : α) → α) a : α)
    ((↑((f : (a : Subtype p) → Subtype p) (Subtype.mk (p := p) a ha)) : α) : α)

Tactic:
extendDomain_apply_subtype _ _ ha

Premises used: Equiv.Perm.extendDomain_apply_subtype
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
f : Perm (Subtype p)
x : Subtype p
⊢ Eq (α := α) ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) f : Perm α) : (a : α) → α) (↑x : α) : α)
    ((↑((f : (a : Subtype p) → Subtype p) x) : α) : α)

Tactic:
Subtype.casesOn x fun _ => ofSubtype_apply_of_mem f

Premises used: Subtype.casesOn
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
a : α
f : Perm (Subtype p)
ha : ¬p a
⊢ (((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) f : Perm α) : (a : α) → α) a = a

Tactic:
extendDomain_apply_not_subtype _ _ ha

Premises used: Equiv.Perm.extendDomain_apply_not_subtype
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
f : Perm (Subtype p)
x : α
h : p x
⊢ p ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) f : Perm α) : (a : α) → α) x) ↔ p x

Tactic:
simpa only [h, iff_true, MonoidHom.coe_mk, ofSubtype_apply_of_mem f h] using (f ⟨x, h⟩).2

Premises used: iff_true, Equiv.Perm.ofSubtype_apply_of_mem, Subtype.mk, MonoidHom.coe_mk, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
f : Perm (Subtype p)
x : α
h : ¬p x
⊢ p ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) f : Perm α) : (a : α) → α) x) ↔ p x

Tactic:
simp [h, ofSubtype_apply_of_not_mem f h]

Premises used: Equiv.Perm.ofSubtype_apply_of_not_mem
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
x y : Perm (Subtype p)
h :
  Eq (α := Perm α) ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) x : Perm α)
    ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) y : Perm α)
rw :
  ∀
    (h :
      ∀ (x_1 : α),
        Eq (α := α) ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) x : Perm α) : (a : α) → α) x_1 : α)
          ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) y : Perm α) : (a : α) → α) x_1 : α))
    (x_1 : Subtype p),
    Eq (α := Subtype p) ((x : (a : Subtype p) → Subtype p) x_1 : Subtype p)
      ((y : (a : Subtype p) → Subtype p) x_1 : Subtype p)
⊢ x = y

Tactic:
rw [Perm.ext_iff] at h ⊢

Premises used: Equiv.Perm.ext_iff
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
x y : Perm (Subtype p)
h :
  ∀ (x_1 : α),
    Eq (α := α) ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) x : Perm α) : (a : α) → α) x_1 : α)
      ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) y : Perm α) : (a : α) → α) x_1 : α)
a : Subtype p
⊢ Eq (α := α) ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) x : Perm α) : (a : α) → α) (↑a : α) : α)
    ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) y : Perm α) : (a : α) → α) (↑a : α) : α)

Tactic:
specialize h a

Premises used: Subtype.val
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
x y : Perm (Subtype p)
a : Subtype p
h :
  Eq (α := α) ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) x : Perm α) : (a : α) → α) (↑a : α) : α)
    ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) y : Perm α) : (a : α) → α) (↑a : α) : α)
rwa :
  ∀
    (h :
      Eq (α := α) ((↑((x : (a : Subtype p) → Subtype p) a) : α) : α)
        ((((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) y : Perm α) : (a : α) → α) (↑a : α) : α)),
    Eq (α := Subtype p) ((x : (a : Subtype p) → Subtype p) a : Subtype p)
      ((y : (a : Subtype p) → Subtype p) a : Subtype p)
rwa₁ :
  ∀
    (h :
      Eq.{u_4 + 1} (α := α) (↑((x : (a : Subtype p) → Subtype p) a) : α) (↑((y : (a : Subtype p) → Subtype p) a) : α)),
    Eq (α := Subtype p) ((x : (a : Subtype p) → Subtype p) a : Subtype p)
      ((y : (a : Subtype p) → Subtype p) a : Subtype p)
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (h :
      Eq (α := (↑p : Type u_4)) ((x : (a : Subtype p) → Subtype p) a : Subtype p)
        ((y : (a : Subtype p) → Subtype p) a : Subtype p)),
    Eq (α := Subtype p) ((x : (a : Subtype p) → Subtype p) a : Subtype p)
      ((y : (a : Subtype p) → Subtype p) a : Subtype p)
⊢ Eq (α := Subtype p) ((x : (a : Subtype p) → Subtype p) a : Subtype p)
    ((y : (a : Subtype p) → Subtype p) a : Subtype p)

Tactic:
rwa [ofSubtype_apply_coe, ofSubtype_apply_coe, SetCoe.ext_iff] at h

Premises used: Equiv.Perm.ofSubtype_apply_coe, SetCoe.ext_iff
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
f : Perm (Subtype p)
⊢ subtypePerm (p := p) ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) f) ⋯ = f

Tactic:
Equiv.ext fun x => Subtype.coe_injective (ofSubtype_apply_coe f x)

Premises used: Equiv.ext, Subtype.coe_injective, Equiv.Perm.ofSubtype_apply_coe
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
g : Perm α
hg : ∀ (x : α), p ((g : (a : α) → α) x) ↔ p x
a : α
ha : p a
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (g.subtypePerm (p := p) hg) :
            Perm α) :
          (a : α) → α)
        a :
      α)
    ((g : (a : α) → α) a : α)

Tactic:
ofSubtype_apply_of_mem (g.subtypePerm hg) ha

Premises used: Equiv.Perm.subtypePerm, Equiv.Perm.ofSubtype_apply_of_mem
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
g : Perm α
hg : ∀ (x : α), p ((g : (a : α) → α) x) ↔ p x
a : α
ha : ¬p a
⊢ (((ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (g.subtypePerm (p := p) hg) : Perm α) :
        (a : α) → α)
      a =
    a

Tactic:
ofSubtype_apply_of_not_mem (g.subtypePerm hg) ha

Premises used: Equiv.Perm.subtypePerm, Equiv.Perm.ofSubtype_apply_of_not_mem
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
a : α
f : Perm (Subtype p)
h : p a
⊢ Eq (α := α)
    (((↑((Perm.subtypeEquivSubtypePerm p :
                  (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                f) :
            Perm α) :
          (a : α) → α)
        a :
      α)
    ((↑((f : (a : Subtype p) → Subtype p) (Subtype.mk (p := p) a h)) : α) : α)

Tactic:
f.ofSubtype_apply_of_mem h

Premises used: Equiv.Perm.ofSubtype_apply_of_mem
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
a : α
f : Perm (Subtype p)
h : ¬p a
⊢ ((↑((Perm.subtypeEquivSubtypePerm p :
                (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
              f) :
          Perm α) :
        (a : α) → α)
      a =
    a

Tactic:
f.ofSubtype_apply_of_not_mem h

Premises used: Equiv.Perm.ofSubtype_apply_of_not_mem
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
x y : α
⊢ (swap x y)⁻¹ = swap x y

Tactic:
rfl

Premises used: Equiv.swapCore, Equiv.swap, Equiv.symm, rfl, ite
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
i j : α
⊢ swap i j * swap i j = 1

Tactic:
swap_swap i j

Premises used: Equiv.swap_swap
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
simp :
  (if (f : (a : α) → α) z = x then y else if (f : (a : α) → α) z = y then x else (f : (a : α) → α) z) =
    (f : (a : α) → α)
      (if z = (f⁻¹ : (a : α) → α) x then (f⁻¹ : (a : α) → α) y
        else if z = (f⁻¹ : (a : α) → α) y then (f⁻¹ : (a : α) → α) x else z :
        α)
⊢ Eq (α := α) ((swap x y * f : (a : α) → α) z : α)
    ((HMul.hMul (β := Perm α) f (swap ((f⁻¹ : (a : α) → α) x) ((f⁻¹ : (a : α) → α) y) : Perm α) : (a : α) → α) z : α)

Tactic:
simp only [Perm.mul_apply, swap_apply_def]

Premises used: Equiv.swap_apply_def, Equiv.Perm.mul_apply
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
pos : (f : (a : α) → α) z = x → z = (f⁻¹ : (a : α) → α) x → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
pos₁ :
  (f : (a : α) → α) z = x →
    ¬z = (f⁻¹ : (a : α) → α) x → z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)
neg : (f : (a : α) → α) z = x → ¬z = (f⁻¹ : (a : α) → α) x → ¬z = (f⁻¹ : (a : α) → α) y → y = (f : (a : α) → α) z
pos₂ :
  ¬(f : (a : α) → α) z = x →
    (f : (a : α) → α) z = y → z = (f⁻¹ : (a : α) → α) x → x = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
pos₃ :
  ¬(f : (a : α) → α) z = x →
    (f : (a : α) → α) z = y →
      ¬z = (f⁻¹ : (a : α) → α) x → z = (f⁻¹ : (a : α) → α) y → x = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)
neg₁ :
  ¬(f : (a : α) → α) z = x →
    (f : (a : α) → α) z = y → ¬z = (f⁻¹ : (a : α) → α) x → ¬z = (f⁻¹ : (a : α) → α) y → x = (f : (a : α) → α) z
pos₄ :
  ¬(f : (a : α) → α) z = x →
    ¬(f : (a : α) → α) z = y →
      z = (f⁻¹ : (a : α) → α) x →
        Eq (α := α) ((f : (a : α) → α) z : α) ((f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α) : α)
pos₅ :
  ¬(f : (a : α) → α) z = x →
    ¬(f : (a : α) → α) z = y →
      ¬z = (f⁻¹ : (a : α) → α) x →
        z = (f⁻¹ : (a : α) → α) y →
          Eq (α := α) ((f : (a : α) → α) z : α) ((f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α) : α)
neg₂ :
  ¬(f : (a : α) → α) z = x →
    ¬(f : (a : α) → α) z = y →
      ¬z = (f⁻¹ : (a : α) → α) x →
        ¬z = (f⁻¹ : (a : α) → α) y → Eq (α := α) ((f : (a : α) → α) z : α) ((f : (a : α) → α) z : α)
⊢ (if (f : (a : α) → α) z = x then y else if (f : (a : α) → α) z = y then x else (f : (a : α) → α) z) =
    (f : (a : α) → α)
      (if z = (f⁻¹ : (a : α) → α) x then (f⁻¹ : (a : α) → α) y
        else if z = (f⁻¹ : (a : α) → α) y then (f⁻¹ : (a : α) → α) x else z :
        α)

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
h : (f : (a : α) → α) z = x
h_1 : z = (f⁻¹ : (a : α) → α) x
⊢ y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)

Tactic:
simp_all [eq_symm_apply]

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
h : (f : (a : α) → α) z = x
h_1 : ¬z = (f⁻¹ : (a : α) → α) x
h_2 : z = (f⁻¹ : (a : α) → α) y
⊢ y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)

Tactic:
simp_all [eq_symm_apply]

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
h : (f : (a : α) → α) z = x
h_1 : ¬z = (f⁻¹ : (a : α) → α) x
h_2 : ¬z = (f⁻¹ : (a : α) → α) y
⊢ y = (f : (a : α) → α) z

Tactic:
simp_all [eq_symm_apply]

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
h : ¬(f : (a : α) → α) z = x
h_1 : (f : (a : α) → α) z = y
h_2 : z = (f⁻¹ : (a : α) → α) x
⊢ x = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)

Tactic:
simp_all [eq_symm_apply]

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
h : ¬(f : (a : α) → α) z = x
h_1 : (f : (a : α) → α) z = y
h_2 : ¬z = (f⁻¹ : (a : α) → α) x
h_3 : z = (f⁻¹ : (a : α) → α) y
⊢ x = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)

Tactic:
simp_all [eq_symm_apply]

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
h : ¬(f : (a : α) → α) z = x
h_1 : (f : (a : α) → α) z = y
h_2 : ¬z = (f⁻¹ : (a : α) → α) x
h_3 : ¬z = (f⁻¹ : (a : α) → α) y
⊢ x = (f : (a : α) → α) z

Tactic:
simp_all [eq_symm_apply]

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
h : ¬(f : (a : α) → α) z = x
h_1 : ¬(f : (a : α) → α) z = y
h_2 : z = (f⁻¹ : (a : α) → α) x
⊢ Eq (α := α) ((f : (a : α) → α) z : α) ((f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α) : α)

Tactic:
simp_all [eq_symm_apply]

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
h : ¬(f : (a : α) → α) z = x
h_1 : ¬(f : (a : α) → α) z = y
h_2 : ¬z = (f⁻¹ : (a : α) → α) x
h_3 : z = (f⁻¹ : (a : α) → α) y
⊢ Eq (α := α) ((f : (a : α) → α) z : α) ((f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α) : α)

Tactic:
simp_all [eq_symm_apply]

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y z : α
h : ¬(f : (a : α) → α) z = x
h_1 : ¬(f : (a : α) → α) z = y
h_2 : ¬z = (f⁻¹ : (a : α) → α) x
h_3 : ¬z = (f⁻¹ : (a : α) → α) y
⊢ Eq (α := α) ((f : (a : α) → α) z : α) ((f : (a : α) → α) z : α)

Tactic:
simp_all [eq_symm_apply]

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y : α
⊢ f * swap x y = HMul.hMul (α := Perm α) (swap ((f : (a : α) → α) x) ((f : (a : α) → α) y) : Perm α) f

Tactic:
simp [swap_mul_eq_mul_swap]

Premises used: Equiv.swap_mul_eq_mul_swap
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
x y : α
rw :
  swap ((f : (a : α) → α) x) ((f : (a : α) → α) y) =
    HMul.hMul (α := Perm α) (swap ((f : (a : α) → α) x) ((f : (a : α) → α) y) : Perm α) f * f⁻¹
rw₁ rw₂ :
  Eq (α := Perm α) (swap ((f : (a : α) → α) x) ((f : (a : α) → α) y) : Perm α)
    (swap ((f : (a : α) → α) x) ((f : (a : α) → α) y) : Perm α)
⊢ swap ((f : (a : α) → α) x) ((f : (a : α) → α) y) = f * swap x y * f⁻¹

Tactic:
rw [mul_swap_eq_swap_mul, mul_inv_cancel_right]

Premises used: mul_inv_cancel_right, Equiv.mul_swap_eq_swap_mul
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
i j : α
σ : Perm α
⊢ swap i j * (swap i j * σ) = σ

Tactic:
simp [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
i j : α
σ : Perm α
rw : σ * (swap i j * swap i j) = σ
rw₁ : σ * 1 = σ
rw₂ rw₃ : σ = σ
⊢ σ * swap i j * swap i j = σ

Tactic:
rw [mul_assoc, swap_mul_self, mul_one]

Premises used: Equiv.swap_mul_self, mul_assoc, mul_one
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
i j : α
⊢ Function.Involutive fun (x : Perm α) ↦ swap i j * x

Tactic:
swap_mul_self_mul i j

Premises used: Equiv.swap_mul_self_mul, Function.Involutive
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
i j : α
⊢ Function.Involutive fun (x : Perm α) ↦ x * swap i j

Tactic:
mul_swap_mul_self i j

Premises used: Equiv.mul_swap_mul_self, Function.Involutive
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
i j : α
⊢ swap i j = 1 ↔ i = j

Tactic:
swap_eq_refl_iff

Premises used: Equiv.swap_eq_refl_iff
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
i j : α
σ : Perm α
rw : swap i j = 1 ↔ i = j
rw₁ rw₂ : i = j ↔ i = j
⊢ swap i j * σ = σ ↔ i = j

Tactic:
rw [mul_eq_right, swap_eq_one_iff]

Premises used: mul_eq_right, Equiv.swap_eq_one_iff
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
i j : α
σ : Perm α
rw : swap i j = 1 ↔ i = j
rw₁ rw₂ : i = j ↔ i = j
⊢ σ * swap i j = σ ↔ i = j

Tactic:
rw [mul_eq_left, swap_eq_one_iff]

Premises used: Equiv.swap_eq_one_iff, mul_eq_left
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
nth_rewrite : swap y z * swap x y * (swap y z)⁻¹ = swap z x
⊢ swap y z * swap x y * swap y z = swap z x

Tactic:
nth_rewrite 3 [← swap_inv]

Premises used: Equiv.swap_inv
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
rw : swap ((swap y z : (a : α) → α) x) ((swap y z : (a : α) → α) y) = swap z x
rw₁ : swap ((swap y z : (a : α) → α) x) z = swap z x
rw₂ : swap x z = swap z x
rw₃ rw₄ : swap z x = swap z x
⊢ swap y z * swap x y * (swap y z)⁻¹ = swap z x

Tactic:
rw [← swap_apply_apply, swap_apply_left, swap_apply_of_ne_of_ne hxy hxz, swap_comm]

Premises used: Equiv.swap_apply_apply, Equiv.swap_comm, Equiv.swap_apply_of_ne_of_ne, Equiv.swap_apply_left
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : Group α
⊢ Eq.{u_4 + 1} (α := Perm α) (Equiv.mulLeft 1) 1

Tactic:
ext one_mul

Premises used: Equiv.ext, one_mul
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : Group α
⊢ Eq.{u_4 + 1} (α := Perm α) (Equiv.mulRight 1) 1

Tactic:
ext mul_one

Premises used: Equiv.ext, mul_one
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : Group α
a b : α
⊢ Equiv.mulLeft (a * b) = Equiv.mulLeft a * Equiv.mulLeft b

Tactic:
ext <| mul_assoc _ _

Premises used: mul_assoc, Equiv.ext
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : Group α
a b : α
⊢ Equiv.mulRight (a * b) = Equiv.mulRight b * Equiv.mulRight a

Tactic:
ext fun _ ↦ (mul_assoc _ _ _).symm

Premises used: mul_assoc, Equiv.ext, Eq.symm
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : Group α
a : α
⊢ (Equiv.mulLeft a)⁻¹ = Equiv.mulLeft a⁻¹

Tactic:
Equiv.coe_inj.1 rfl

Premises used: Equiv.coe_inj, Iff.mp, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : Group α
a : α
⊢ (Equiv.mulRight a)⁻¹ = Equiv.mulRight a⁻¹

Tactic:
Equiv.coe_inj.1 rfl

Premises used: Equiv.coe_inj, Iff.mp, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : Group α
a : α
n : ℕ
H : ∀ (x : α), Eq (α := α) ((Equiv.mulLeft a ^ n : (a : α) → α) x : α) ((Equiv.mulLeft (a ^ n) : (a : α) → α) x : α)
⊢ Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : Group α
a : α
n : ℕ
x : α
⊢ Eq (α := α) ((Equiv.mulLeft a ^ n : (a : α) → α) x : α) ((Equiv.mulLeft (a ^ n) : (a : α) → α) x : α)

Tactic:
simp [Perm.coe_pow]

Premises used: Equiv.Perm.coe_pow
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : Group α
a : α
n : ℕ
H : ∀ (x : α), Eq (α := α) ((Equiv.mulRight a ^ n : (a : α) → α) x : α) ((Equiv.mulRight (a ^ n) : (a : α) → α) x : α)
⊢ Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : Group α
a : α
n : ℕ
x : α
⊢ Eq (α := α) ((Equiv.mulRight a ^ n : (a : α) → α) x : α) ((Equiv.mulRight (a ^ n) : (a : α) → α) x : α)

Tactic:
simp [Perm.coe_pow]

Premises used: Equiv.Perm.coe_pow
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : Group α
a : α
n : ℕ
⊢ Equiv.mulLeft a ^ Int.ofNat n = Equiv.mulLeft (a ^ Int.ofNat n)

Tactic:
simp