awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : CommGroup G
a b : G
rw : b * a⁻¹ * a = b
rw₁ rw₂ : b = b
⊢ a * (b * a⁻¹) = b

Tactic:
rw [mul_comm, inv_mul_cancel_right]

Premises used: mul_comm, inv_mul_cancel_right
-- Module: Mathlib.Algebra.Group.Embedding
Goal:
G : Type u_1
inst : CommMagma G
inst_1 : IsCancelMul G
g : G
h : ∀ (x : G), Eq (α := G) ((mulLeftEmbedding g : (a : G) → G) x : G) ((mulRightEmbedding g : (a : G) → G) x : G)
⊢ mulLeftEmbedding g = mulRightEmbedding g

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Embedding
Goal:
G : Type u_1
inst : CommMagma G
inst_1 : IsCancelMul G
g x : G
⊢ Eq (α := G) ((mulLeftEmbedding g : (a : G) → G) x : G) ((mulRightEmbedding g : (a : G) → G) x : G)

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.Algebra.Group.Embedding
Goal:
G : Type u_1
inst : CommMagma G
inst_1 : IsCancelMul G
g x : G
⊢ Eq (α := G) ((mulLeftEmbedding g : (a : G) → G) x : G) ((mulRightEmbedding g : (a : G) → G) x : G)

Tactic:
exact mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
⊢ Eq.{u_4 + 1} (α := Perm α) default 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
f g : Perm α
x : α
⊢ Eq (α := α) ((f * g : (a : α) → α) x : α) ((f : (a : α) → α) ((g : (a : α) → α) x : α) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
x : α
⊢ (1 : (a : α) → α) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
⊢ 1 = Equiv.refl α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
f g : Perm α
⊢ f * g = Equiv.trans g f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
f : Perm α
⊢ f⁻¹ = Equiv.symm f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
f : Perm α
⊢ Eq (α := (a : α) → α) (⇑f⁻¹ : (a : α) → α) (⇑(Equiv.symm f) : (a : α) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
⊢ Eq.{u_4 + 1} (α := (a : α) → α) (⇑1 : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
f g : Perm α
⊢ Eq (α := (a : α) → α) (⇑(f * g) : (a : α) → α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
f : Perm α
n : ℕ
⊢ Eq (α := (a : α) → α) (⇑(f ^ n) : (a : α) → α) (⇑f : (a : α) → α)^[n]

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
f : Perm α
n : ℕ
⊢ Eq (α := α → α) (⇑f : (a : α) → α)^[n] (⇑(f ^ n) : (a : α) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
f : Perm α
x y : α
⊢ x = (f⁻¹ : (a : α) → α) y ↔ (f : (a : α) → α) x = y

Tactic:
f.eq_symm_apply

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
f : Perm α
x y : α
⊢ (f⁻¹ : (a : α) → α) x = y ↔ x = (f : (a : α) → α) y

Tactic:
f.symm_apply_eq

Premises used: Equiv.symm_apply_eq
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
σ : Perm α
m n : ℤ
x : α
rw : Eq (α := α) ((σ ^ m * σ ^ n : (a : α) → α) x : α) ((σ ^ n : (a : α) → α) ((σ ^ m : (a : α) → α) x : α) : α)
rw₁ : Eq (α := α) ((σ ^ m * σ ^ n : (a : α) → α) x : α) ((σ ^ n * σ ^ m : (a : α) → α) x : α)
rw₂ rw₃ : Eq (α := α) ((σ ^ n * σ ^ m : (a : α) → α) x : α) ((σ ^ n * σ ^ m : (a : α) → α) x : α)
⊢ Eq (α := α) ((σ ^ m : (a : α) → α) ((σ ^ n : (a : α) → α) x : α) : α)
    ((σ ^ n : (a : α) → α) ((σ ^ m : (a : α) → α) x : α) : α)

Tactic:
rw [← Equiv.Perm.mul_apply, ← Equiv.Perm.mul_apply, zpow_mul_comm]

Premises used: Equiv.Perm.mul_apply, zpow_mul_comm
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Sort u_7
β : Type u_8
e : α ≃ β
⊢ e.trans 1 = e

Tactic:
Equiv.trans_refl e

Premises used: Equiv.trans_refl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
e : Perm α
⊢ e * Equiv.refl α = e

Tactic:
Equiv.trans_refl e

Premises used: Equiv.trans, Equiv.trans_refl, Equiv.refl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
⊢ Eq.{u_4 + 1} (α := α ≃ α) (Equiv.symm 1) 1

Tactic:
rfl

Premises used: Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
⊢ (Equiv.refl α)⁻¹ = 1

Tactic:
rfl

Premises used: Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : Sort u_8
e : α ≃ β
⊢ Equiv.trans 1 e = e

Tactic:
rfl

Premises used: Equiv.trans, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
e : Perm α
⊢ Equiv.refl α * e = e

Tactic:
rfl

Premises used: Equiv.trans, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
e : Perm α
⊢ Equiv.trans e⁻¹ e = 1

Tactic:
Equiv.symm_trans_self e

Premises used: Equiv.symm_trans_self
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
e : Perm α
⊢ e * Equiv.symm e = 1

Tactic:
Equiv.symm_trans_self e

Premises used: Equiv.symm_trans_self
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
e : Perm α
⊢ Equiv.trans e e⁻¹ = 1

Tactic:
Equiv.self_trans_symm e

Premises used: Equiv.self_trans_symm
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
e : Perm α
⊢ Equiv.symm e * e = 1

Tactic:
Equiv.self_trans_symm e

Premises used: Equiv.self_trans_symm
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : Type u_8
e : Perm α
f : Perm β
g : Perm α
h : Perm β
⊢ e.sumCongr f * g.sumCongr h = (e * g).sumCongr (f * h)

Tactic:
sumCongr_trans g h e f

Premises used: Equiv.Perm.sumCongr_trans
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : Type u_8
e : Perm α
f : Perm β
⊢ (e.sumCongr f)⁻¹ = e⁻¹.sumCongr f⁻¹

Tactic:
rfl

Premises used: Sum.map, Equiv.sumCongr, Equiv.symm, rfl, Sum.elim
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : Type u_8
⊢ Eq (α := Perm (α ⊕ β)) (sumCongr 1 1) 1

Tactic:
sumCongr_refl

Premises used: Equiv.Perm.sumCongr_refl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : Type u_8
fst : Perm α
snd : Perm β
fst_1 : Perm α
snd_1 : Perm β
h :
  Eq (α := Perm (α ⊕ β)) ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst, snd) : Perm (α ⊕ β))
    ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst_1, snd_1) : Perm (α ⊕ β))
rw : fst = fst_1 ∧ snd = snd_1
⊢ (fst, snd) = (fst_1, snd_1)

Tactic:
rw [Prod.mk_inj]

Premises used: Prod.mk_inj
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : Type u_8
fst : Perm α
snd : Perm β
fst_1 : Perm α
snd_1 : Perm β
h :
  Eq (α := Perm (α ⊕ β)) ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst, snd) : Perm (α ⊕ β))
    ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst_1, snd_1) : Perm (α ⊕ β))
left : fst = fst_1
right : snd = snd_1
⊢ fst = fst_1 ∧ snd = snd_1

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : Type u_8
fst : Perm α
snd : Perm β
fst_1 : Perm α
snd_1 : Perm β
h :
  Eq (α := Perm (α ⊕ β)) ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst, snd) : Perm (α ⊕ β))
    ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst_1, snd_1) : Perm (α ⊕ β))
left : ∀ (i : α), Eq (α := α) ((fst : (a : α) → α) i : α) ((fst_1 : (a : α) → α) i : α)
⊢ fst = fst_1

Tactic:
ext i
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : Type u_8
fst : Perm α
snd : Perm β
fst_1 : Perm α
snd_1 : Perm β
h :
  Eq (α := Perm (α ⊕ β)) ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst, snd) : Perm (α ⊕ β))
    ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst_1, snd_1) : Perm (α ⊕ β))
right : ∀ (i : β), Eq (α := β) ((snd : (a : β) → β) i : β) ((snd_1 : (a : β) → β) i : β)
⊢ snd = snd_1

Tactic:
ext i
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : Type u_8
fst : Perm α
snd : Perm β
fst_1 : Perm α
snd_1 : Perm β
h :
  Eq (α := Perm (α ⊕ β)) ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst, snd) : Perm (α ⊕ β))
    ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst_1, snd_1) : Perm (α ⊕ β))
i : α
⊢ Eq (α := α) ((fst : (a : α) → α) i : α) ((fst_1 : (a : α) → α) i : α)

Tactic:
simpa using Equiv.congr_fun h (Sum.inl i)

Premises used: Equiv.congr_fun, Sum.inl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : Type u_8
fst : Perm α
snd : Perm β
fst_1 : Perm α
snd_1 : Perm β
h :
  Eq (α := Perm (α ⊕ β)) ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst, snd) : Perm (α ⊕ β))
    ((sumCongrHom α β : (a : Perm α × Perm β) → Perm (α ⊕ β)) (fst_1, snd_1) : Perm (α ⊕ β))
i : β
⊢ Eq (α := β) ((snd : (a : β) → β) i : β) ((snd_1 : (a : β) → β) i : β)

Tactic:
simpa using Equiv.congr_fun h (Sum.inr i)

Premises used: Equiv.congr_fun, Sum.inr
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : Type u_8
inst : DecidableEq α
inst_1 : DecidableEq β
i j : α
⊢ Eq (α := Perm (α ⊕ β)) ((swap i j).sumCongr 1) (swap (Sum.inl i) (Sum.inl j))

Tactic:
sumCongr_swap_refl i j

Premises used: Equiv.Perm.sumCongr_swap_refl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : Type u_8
inst : DecidableEq α
inst_1 : DecidableEq β
i j : β
⊢ Eq (α := Perm (α ⊕ β)) (sumCongr 1 (swap i j)) (swap (Sum.inr i) (Sum.inr j))

Tactic:
sumCongr_refl_swap i j

Premises used: Equiv.Perm.sumCongr_refl_swap
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : α → Type u_8
F G : (a : α) → Perm (β a)
⊢ sigmaCongrRight (β := β) F * sigmaCongrRight (β := β) G = sigmaCongrRight (β := β) (F * G)

Tactic:
rfl

Premises used: Equiv.trans, Equiv.sigmaCongrRight, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : α → Type u_8
F : (a : α) → Perm (β a)
⊢ (sigmaCongrRight (β := β) F)⁻¹ = sigmaCongrRight (β := β) fun (a : α) ↦ (F a)⁻¹

Tactic:
rfl

Premises used: Equiv.symm, Equiv.sigmaCongrRight, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : α → Type u_8
⊢ Eq (α := Perm ((a : α) × β a)) (sigmaCongrRight (β := β) 1) 1

Tactic:
rfl

Premises used: Equiv.sigmaCongrRight, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : α → Type u_8
x y : (a : α) → Perm (β a)
h :
  Eq (α := Perm ((a : α) × β a))
    ((sigmaCongrRightHom β : (a : (a : α) → Perm (β a)) → Perm ((a : α) × β a)) x : Perm ((a : α) × β a))
    ((sigmaCongrRightHom β : (a : (a : α) → Perm (β a)) → Perm ((a : α) × β a)) y : Perm ((a : α) × β a))
h₁ : ∀ (a : α) (b : β a), Eq (α := β a) ((x a : (a_1 : β a) → β a) b : β a) ((y a : (a_1 : β a) → β a) b : β a)
⊢ x = y

Tactic:
ext a b
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_7
β : α → Type u_8
x y : (a : α) → Perm (β a)
h :
  Eq (α := Perm ((a : α) × β a))
    ((sigmaCongrRightHom β : (a : (a : α) → Perm (β a)) → Perm ((a : α) × β a)) x : Perm ((a : α) × β a))
    ((sigmaCongrRightHom β : (a : (a : α) → Perm (β a)) → Perm ((a : α) × β a)) y : Perm ((a : α) × β a))
a : α
b : β a
⊢ Eq (α := β a) ((x a : (a_1 : β a) → β a) b : β a) ((y a : (a_1 : β a) → β a) b : β a)

Tactic:
simpa using Equiv.congr_fun h ⟨a, b⟩

Premises used: Equiv.congr_fun, Sigma.mk
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
fst : Perm { a : α // p a }
snd : Perm { a : α // ¬p a }
fst_1 : Perm { a : α // p a }
snd_1 : Perm { a : α // ¬p a }
h :
  Eq (α := Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst, snd) : Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst_1, snd_1) : Perm α)
rw : fst = fst_1 ∧ snd = snd_1
⊢ (fst, snd) = (fst_1, snd_1)

Tactic:
rw [Prod.mk_inj]

Premises used: Prod.mk_inj
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
fst : Perm { a : α // p a }
snd : Perm { a : α // ¬p a }
fst_1 : Perm { a : α // p a }
snd_1 : Perm { a : α // ¬p a }
h :
  Eq (α := Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst, snd) : Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst_1, snd_1) : Perm α)
left : fst = fst_1
right : snd = snd_1
⊢ fst = fst_1 ∧ snd = snd_1

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
fst : Perm { a : α // p a }
snd : Perm { a : α // ¬p a }
fst_1 : Perm { a : α // p a }
snd_1 : Perm { a : α // ¬p a }
h :
  Eq (α := Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst, snd) : Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst_1, snd_1) : Perm α)
left :
  ∀ (i : { a : α // p a }),
    Eq.{u_4 + 1} (α := α) (↑((fst : (a : { a : α // p a }) → { a : α // p a }) i) : α)
      (↑((fst_1 : (a : { a : α // p a }) → { a : α // p a }) i) : α)
⊢ fst = fst_1

Tactic:
ext i
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
fst : Perm { a : α // p a }
snd : Perm { a : α // ¬p a }
fst_1 : Perm { a : α // p a }
snd_1 : Perm { a : α // ¬p a }
h :
  Eq (α := Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst, snd) : Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst_1, snd_1) : Perm α)
right :
  ∀ (i : { a : α // ¬p a }),
    Eq.{u_4 + 1} (α := α) (↑((snd : (a : { a : α // ¬p a }) → { a : α // ¬p a }) i) : α)
      (↑((snd_1 : (a : { a : α // ¬p a }) → { a : α // ¬p a }) i) : α)
⊢ snd = snd_1

Tactic:
ext i
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
fst : Perm { a : α // p a }
snd : Perm { a : α // ¬p a }
fst_1 : Perm { a : α // p a }
snd_1 : Perm { a : α // ¬p a }
h :
  Eq (α := Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst, snd) : Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst_1, snd_1) : Perm α)
i : { a : α // p a }
⊢ Eq.{u_4 + 1} (α := α) (↑((fst : (a : { a : α // p a }) → { a : α // p a }) i) : α)
    (↑((fst_1 : (a : { a : α // p a }) → { a : α // p a }) i) : α)

Tactic:
simpa using Equiv.congr_fun h i

Premises used: Equiv.congr_fun, Subtype.val
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
inst : DecidablePred p
fst : Perm { a : α // p a }
snd : Perm { a : α // ¬p a }
fst_1 : Perm { a : α // p a }
snd_1 : Perm { a : α // ¬p a }
h :
  Eq (α := Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst, snd) : Perm α)
    ((subtypeCongrHom p : (a : Perm { a : α // p a } × Perm { a : α // ¬p a }) → Perm α) (fst_1, snd_1) : Perm α)
i : { a : α // ¬p a }
⊢ Eq.{u_4 + 1} (α := α) (↑((snd : (a : { a : α // ¬p a }) → { a : α // ¬p a }) i) : α)
    (↑((snd_1 : (a : { a : α // ¬p a }) → { a : α // ¬p a }) i) : α)

Tactic:
simpa using Equiv.congr_fun h i

Premises used: Equiv.congr_fun, Subtype.val
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
e p : Perm α
⊢ (permCongr e : (a : Perm α) → Perm α) p = e * p * e⁻¹

Tactic:
rfl

Premises used: Equiv.trans, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
β : Type u_5
e : α ≃ β
p q : Perm α
⊢ (e.permCongr : (a : Perm α) → Perm β) (p * q) =
    HMul.hMul (α := Perm β) (β := Perm β) ((e.permCongr : (a : Perm α) → Perm β) p : Perm β)
      ((e.permCongr : (a : Perm α) → Perm β) q : Perm β)

Tactic:
permCongr_trans e q p |>.symm

Premises used: Equiv.permCongr_trans, Eq.symm
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
β : Type u_5
e : α ≃ β
⊢ e.permCongrHom.symm = e.symm.permCongrHom

Tactic:
rfl

Premises used: Equiv.equivCongr, Equiv.trans, Equiv.permCongr, Equiv.permCongrHom, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
e : α ≃ β
e' : β ≃ γ
⊢ e.permCongrHom.trans e'.permCongrHom = (e.trans e').permCongrHom

Tactic:
rfl

Premises used: Equiv.equivCongr, Equiv.trans, MulEquiv.trans, Equiv.permCongr, Equiv.permCongrHom, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
β : Type u_5
e : α ≃ β
⊢ (↑e.permCongrHom : Perm α ≃ Perm β) = e.permCongr

Tactic:
rfl

Premises used: Equiv.equivCongr, Equiv.trans, Equiv.permCongr, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
β : Type u_5
e : α ≃ β
⊢ Eq (α := (a : Perm α) → Perm β) (⇑e.permCongrHom : (a : Perm α) → Perm β) (⇑e.permCongr : (a : Perm α) → Perm β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
β : Type u_5
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_4 + 1, max 1 (u_5 + 1)} α (Subtype p)
⊢ extendDomain 1 (p := p) f = 1

Tactic:
extendDomain_refl f

Premises used: Equiv.Perm.extendDomain_refl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
β : Type u_5
e : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_4 + 1, max 1 (u_5 + 1)} α (Subtype p)
⊢ (e.extendDomain (p := p) f)⁻¹ = e⁻¹.extendDomain (p := p) f

Tactic:
rfl

Premises used: Equiv.Perm.extendDomain, Sum.map, Equiv.trans, Equiv.Perm.subtypeCongr, Equiv.symm, rfl, Sum.elim
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
β : Type u_5
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_4 + 1, max 1 (u_5 + 1)} α (Subtype p)
e e' : Perm α
⊢ e.extendDomain (p := p) f * e'.extendDomain (p := p) f = (e * e').extendDomain (p := p) f

Tactic:
extendDomain_trans _ _ _

Premises used: Equiv.Perm.extendDomain_trans
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
β : Type u_5
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_4 + 1, max 1 (u_5 + 1)} α (Subtype p)
⊢ Function.Injective.{u_4 + 1, u_5 + 1} (α := Perm α) (β := Perm β)
    (⇑(extendDomainHom (p := p) f) : (a : Perm α) → Perm β)

Tactic:
(injective_iff_map_eq_one (extendDomainHom f)).mpr fun e he =>
    ext fun x => f.injective <|
      Subtype.ext ((extendDomain_apply_image e f x).symm.trans (Perm.ext_iff.mp he (f x)))

Premises used: Iff.mpr, Equiv.Perm.extendDomainHom, Equiv.Perm.extendDomain_apply_image, Equiv.Perm.ext_iff, Iff.mp, Equiv.injective, Eq.symm, Subtype.val, DFunLike.coe, Equiv.Perm.ext, Eq.trans, Subtype.ext, injective_iff_map_eq_one
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
β : Type u_5
p : β → Prop
inst : DecidablePred p
e : Perm α
f : Equiv.{u_4 + 1, max 1 (u_5 + 1)} α (Subtype p)
⊢ e.extendDomain (p := p) f = 1 ↔ e = 1

Tactic:
(injective_iff_map_eq_one' (extendDomainHom f)).mp (extendDomainHom_injective f) e

Premises used: Equiv.Perm.extendDomain, Equiv.Perm.extendDomainHom, injective_iff_map_eq_one', Iff.mp, Equiv.Perm.subtypeCongr, Equiv.Perm.extendDomainHom_injective
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
β : Type u_5
e : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_4 + 1, max 1 (u_5 + 1)} α (Subtype p)
n : ℕ
⊢ (e ^ n).extendDomain (p := p) f = e.extendDomain (p := p) f ^ n

Tactic:
map_pow (extendDomainHom f) _ _

Premises used: Equiv.Perm.extendDomain, Equiv.Perm.extendDomainHom, map_pow, Equiv.Perm.subtypeCongr
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
β : Type u_5
e : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_4 + 1, max 1 (u_5 + 1)} α (Subtype p)
n : ℤ
⊢ (e ^ n).extendDomain (p := p) f = e.extendDomain (p := p) f ^ n

Tactic:
map_zpow (extendDomainHom f) _ _

Premises used: Equiv.Perm.extendDomain, Equiv.Perm.extendDomainHom, map_zpow, Equiv.Perm.subtypeCongr
-- Module: Mathlib.Algebra.Group.End
Goal:
A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
p : α → Prop
f_1 f : Perm α
h : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
x : { x : α // p x }
⊢ p ((f : (a : α) → α) ((f⁻¹ : (a : α) → α) (↑x : α) : α))

Tactic:
simpa using x.2

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Group.End
Goal:
A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
p : α → Prop
f_1 f : Perm α
h : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
x : { x : α // p x }
⊢ (fun (x : { x : α // p x }) ↦
        (Subtype.mk (p := fun (x : α) ↦ p x) ((f⁻¹ : (a : α) → α) (↑x : α)) ⋯ : { x : α // p x }))
      ((fun (x : { x : α // p x }) ↦
          (Subtype.mk (p := fun (x : α) ↦ p x) ((f : (a : α) → α) (↑x : α)) ⋯ : { x : α // p x }))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.End
Goal:
A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
p : α → Prop
f_1 f : Perm α
h : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
x : { x : α // p x }
⊢ (fun (x : { x : α // p x }) ↦ (Subtype.mk (p := fun (x : α) ↦ p x) ((f : (a : α) → α) (↑x : α)) ⋯ : { x : α // p x }))
      ((fun (x : { x : α // p x }) ↦
          (Subtype.mk (p := fun (x : α) ↦ p x) ((f⁻¹ : (a : α) → α) (↑x : α)) ⋯ : { x : α // p x }))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
f : Perm α
h : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
x : { x : α // p x }
⊢ Eq (α := { x : α // p x })
    ((f.subtypePerm (p := p) h : (a : { x : α // p x }) → { x : α // p x }) x : { x : α // p x })
    (Subtype.mk (p := fun (x : α) ↦ p x) ((f : (a : α) → α) (↑x : α)) ⋯ : { x : α // p x })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
h : ∀ (x : α), p ((1 : (a : α) → α) x) ↔ p ((1 : (a : α) → α) x)
⊢ subtypePerm (p := p) 1 h = 1

Tactic:
rfl

Premises used: Equiv.Perm.subtypePerm, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
f g : Perm α
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
hg : ∀ (x : α), p ((g : (a : α) → α) x) ↔ p x
⊢ f.subtypePerm (p := p) hf * g.subtypePerm (p := p) hg = (f * g).subtypePerm (p := p) ⋯

Tactic:
rfl

Premises used: Equiv.trans, Equiv.Perm.subtypePerm, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
f : Perm α
⊢ (∀ (x : α), p ((f : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α)) ↔ p ((f⁻¹ : (a : α) → α) x)) ↔
    ∀ (x : α), p ((f⁻¹ : (a : α) → α) x) ↔ p x

Tactic:
simp [Iff.comm]

Premises used: Iff.comm
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p ((f⁻¹ : (a : α) → α) x) ↔ p x
⊢ f⁻¹.subtypePerm (p := p) hf = (f.subtypePerm (p := p) ⋯)⁻¹

Tactic:
rfl

Premises used: Equiv.Perm.subtypePerm, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
⊢ (f.subtypePerm (p := p) hf)⁻¹ = f⁻¹.subtypePerm (p := p) ⋯

Tactic:
rfl

Premises used: Equiv.Perm.subtypePerm, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
⊢ HPow.hPow (β := ℕ) (f.subtypePerm (p := p) hf) 0 = (HPow.hPow (β := ℕ) f 0).subtypePerm (p := p) ⋯

Tactic:
simp
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
n : ℕ
ih : f.subtypePerm (p := p) hf ^ n = (f ^ n).subtypePerm (p := p) ⋯
succ : f.subtypePerm (p := p) hf * f.subtypePerm (p := p) hf ^ n = (f * f ^ n).subtypePerm (p := p) ⋯
succ₁ : f.subtypePerm (p := p) hf * (f ^ n).subtypePerm (p := p) ⋯ = (f * f ^ n).subtypePerm (p := p) ⋯
⊢ f.subtypePerm (p := p) hf ^ (n + 1) = (f ^ (n + 1)).subtypePerm (p := p) ⋯

Tactic:
simp_rw [pow_succ', ih, subtypePerm_mul]

Premises used: Equiv.Perm.subtypePerm_mul, pow_succ'
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
f : Perm α
n : ℕ
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
zero : HPow.hPow (β := ℕ) (f.subtypePerm (p := p) hf) 0 = (HPow.hPow (β := ℕ) f 0).subtypePerm (p := p) ⋯
succ :
  ∀ (n : ℕ) (ih : f.subtypePerm (p := p) hf ^ n = (f ^ n).subtypePerm (p := p) ⋯),
    f.subtypePerm (p := p) hf ^ (n + 1) = (f ^ (n + 1)).subtypePerm (p := p) ⋯
⊢ f.subtypePerm (p := p) hf ^ n = (f ^ n).subtypePerm (p := p) ⋯

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp_rw [pow_succ', ih, subtypePerm_mul]

Premises used: Equiv.Perm.subtypePerm_mul, pow_succ'
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
n : ℕ
rw : ∀ (x : α), p (((f ^ (n + 1))⁻¹ : (a : α) → α) x) ↔ p x
⊢ ∀ (x : α), p ((f ^ Int.negSucc n : (a : α) → α) x) ↔ p x

Tactic:
rw [zpow_negSucc]

Premises used: zpow_negSucc