awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : Group α
a : α
n : ℕ
⊢ Equiv.mulLeft a ^ Int.negSucc n = Equiv.mulLeft (a ^ Int.negSucc n)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : Group α
a : α
n : ℕ
⊢ Equiv.mulRight a ^ Int.ofNat n = Equiv.mulRight (a ^ Int.ofNat n)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.End
Goal:
α : Type u_4
inst : Group α
a : α
n : ℕ
⊢ Equiv.mulRight a ^ Int.negSucc n = Equiv.mulRight (a ^ Int.negSucc n)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.End
Goal:
M : Type u_2
inst : Mul M
e₁ e₂ : MulAut M
⊢ Eq (α := (a : M) → M) (⇑(e₁ * e₂) : (a : M) → M) (Function.comp (β := M) (⇑e₁ : (a : M) → M) (⇑e₂ : (a : M) → M))

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
M : Type u_2
inst : Mul M
e : MulAut M
⊢ Eq (α := (a : M) → M) (⇑e⁻¹ : (a : M) → M) (⇑(MulEquiv.symm e) : (a : M) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
M : Type u_2
inst : Mul M
e₁ e₂ : MulAut M
⊢ e₁ * e₂ = MulEquiv.trans e₂ e₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
M : Type u_2
inst : Mul M
⊢ Eq (α := MulAut M) 1 (MulEquiv.refl M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
M : Type u_2
inst : Mul M
e₁ : MulAut M
⊢ e₁⁻¹ = MulEquiv.symm e₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
M : Type u_2
inst : Mul M
e : MulAut M
⊢ MulEquiv.symm e⁻¹ = e

Tactic:
rfl

Premises used: Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
M : Type u_2
inst : Mul M
e : MulAut M
⊢ (MulEquiv.symm e)⁻¹ = e

Tactic:
rfl

Premises used: Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
M : Type u_2
inst : Mul M
e : MulAut M
m : M
rw rw₁ : Eq (α := M) ((MulEquiv.symm e : (a : M) → M) m : M) ((MulEquiv.symm e : (a : M) → M) m : M)
⊢ Eq (α := M) ((e⁻¹ : (a : M) → M) m : M) ((MulEquiv.symm e : (a : M) → M) m : M)

Tactic:
rw [inv_def]

Premises used: MulAut.inv_def
-- Module: Mathlib.Algebra.Group.End
Goal:
M : Type u_2
inst : Mul M
e₁ e₂ : MulAut M
m : M
⊢ Eq (α := M) ((e₁ * e₂ : (a : M) → M) m : M) ((e₁ : (a : M) → M) ((e₂ : (a : M) → M) m : M) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
M : Type u_2
inst : Mul M
m : M
⊢ (1 : (a : M) → M) m = m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
M : Type u_2
inst : Mul M
e : MulAut M
m : M
⊢ (e : (a : M) → M) ((e⁻¹ : (a : M) → M) m : M) = m

Tactic:
MulEquiv.apply_symm_apply _ _

Premises used: MulEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.End
Goal:
M : Type u_2
inst : Mul M
e : MulAut M
m : M
⊢ (e⁻¹ : (a : M) → M) ((e : (a : M) → M) m : M) = m

Tactic:
MulEquiv.apply_symm_apply _ _

Premises used: MulEquiv.apply_symm_apply
-- 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
inst : Mul M
inst_1 : Group G
g x : G
⊢ (fun (h : G) ↦ g⁻¹ * h * g) ((fun (h : G) ↦ g * h * g⁻¹) x) = x

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- 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
inst : Mul M
inst_1 : Group G
g x : G
⊢ (fun (h : G) ↦ g * h * g⁻¹) ((fun (h : G) ↦ g⁻¹ * h * g) x) = x

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- 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
inst : Mul M
inst_1 : Group G
g : G
⊢ ∀ (x y : G), g * (x * y) * g⁻¹ = g * x * g⁻¹ * (g * y * g⁻¹)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- 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
inst : Mul M
inst_1 : Group G
h :
  ∀ (x : G),
    Eq (α := G)
      (({ toFun := fun (h : G) ↦ 1 * h * 1⁻¹, invFun := fun (h : G) ↦ 1⁻¹ * h * 1, left_inv := ⋯, right_inv := ⋯,
              map_mul' := ⋯ } :
            (a : G) → G)
          x :
        G)
      ((1 : (a : G) → G) x : G)
⊢ Eq.{u_3 + 1} (α := MulAut G)
    { toFun := fun (h : G) ↦ 1 * h * 1⁻¹, invFun := fun (h : G) ↦ 1⁻¹ * h * 1, left_inv := ⋯, right_inv := ⋯,
      map_mul' := ⋯ }
    1

Tactic:
ext
-- 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
inst : Mul M
inst_1 : Group G
x : G
⊢ Eq (α := G)
    (({ toFun := fun (h : G) ↦ 1 * h * 1⁻¹, invFun := fun (h : G) ↦ 1⁻¹ * h * 1, left_inv := ⋯, right_inv := ⋯,
            map_mul' := ⋯ } :
          (a : G) → G)
        x :
      G)
    ((1 : (a : G) → G) x : G)

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
inst : Mul M
inst_1 : Group G
x x_1 : G
h :
  ∀ (x_2 : G),
    Eq (α := G)
      (({ toFun := fun (h : G) ↦ x * x_1 * h * (x * x_1)⁻¹, invFun := fun (h : G) ↦ (x * x_1)⁻¹ * h * (x * x_1),
              left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ } :
            (a : G) → G)
          x_2 :
        G)
      ((HMul.hMul (α := MulAut G)
              { toFun := fun (h : G) ↦ x * h * x⁻¹, invFun := fun (h : G) ↦ x⁻¹ * h * x, left_inv := ⋯, right_inv := ⋯,
                map_mul' := ⋯ : G ≃* G }
              { toFun := fun (h : G) ↦ x_1 * h * x_1⁻¹, invFun := fun (h : G) ↦ x_1⁻¹ * h * x_1, left_inv := ⋯,
                right_inv := ⋯, map_mul' := ⋯ : G ≃* G } :
            (a : G) → G)
          x_2 :
        G)
⊢ { toFun := fun (h : G) ↦ x * x_1 * h * (x * x_1)⁻¹, invFun := fun (h : G) ↦ (x * x_1)⁻¹ * h * (x * x_1),
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ } =
    HMul.hMul (α := MulAut G)
      { toFun := fun (h : G) ↦ x * h * x⁻¹, invFun := fun (h : G) ↦ x⁻¹ * h * x, left_inv := ⋯, right_inv := ⋯,
        map_mul' := ⋯ : G ≃* G }
      { toFun := fun (h : G) ↦ x_1 * h * x_1⁻¹, invFun := fun (h : G) ↦ x_1⁻¹ * h * x_1, left_inv := ⋯, right_inv := ⋯,
        map_mul' := ⋯ : G ≃* G }

Tactic:
ext
-- 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
inst : Mul M
inst_1 : Group G
x x_1 x_2 : G
⊢ Eq (α := G)
    (({ toFun := fun (h : G) ↦ x * x_1 * h * (x * x_1)⁻¹, invFun := fun (h : G) ↦ (x * x_1)⁻¹ * h * (x * x_1),
            left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ } :
          (a : G) → G)
        x_2 :
      G)
    ((HMul.hMul (α := MulAut G)
            { toFun := fun (h : G) ↦ x * h * x⁻¹, invFun := fun (h : G) ↦ x⁻¹ * h * x, left_inv := ⋯, right_inv := ⋯,
              map_mul' := ⋯ : G ≃* G }
            { toFun := fun (h : G) ↦ x_1 * h * x_1⁻¹, invFun := fun (h : G) ↦ x_1⁻¹ * h * x_1, left_inv := ⋯,
              right_inv := ⋯, map_mul' := ⋯ : G ≃* G } :
          (a : G) → G)
        x_2 :
      G)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.End
Goal:
G : Type u_3
inst : Group G
g h : G
⊢ (((conj : (a : G) → MulAut G) g : MulAut G) : (a : G) → G) h = g * h * g⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
G : Type u_3
inst : Group G
g h : G
⊢ (MulEquiv.symm ((conj : (a : G) → MulAut G) g) : (a : G) → G) h = g⁻¹ * h * g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
G : Type u_3
inst : Group G
g h : G
⊢ ((((conj : (a : G) → MulAut G) g)⁻¹ : MulAut G) : (a : G) → G) h = g⁻¹ * h * g

Tactic:
rfl

Premises used: rfl
-- 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
inst : Mul M
inst_1 : Group G
H : Type u_7
inst_2 : Group H
ϕ : G ≃* H
x : MulAut G
⊢ (fun (f : MulAut H) ↦ ϕ.trans (MulEquiv.trans f ϕ.symm))
      ((fun (f : MulAut G) ↦ ϕ.symm.trans (MulEquiv.trans f ϕ)) x) =
    x

Tactic:
simp [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- 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
inst : Mul M
inst_1 : Group G
H : Type u_7
inst_2 : Group H
ϕ : G ≃* H
x : MulAut H
⊢ (fun (f : MulAut G) ↦ ϕ.symm.trans (MulEquiv.trans f ϕ))
      ((fun (f : MulAut H) ↦ ϕ.trans (MulEquiv.trans f ϕ.symm)) x) =
    x

Tactic:
simp [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- 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
inst : Mul M
inst_1 : Group G
H : Type u_7
inst_2 : Group H
ϕ : G ≃* H
⊢ ∀ (x y : MulAut G),
    ϕ.symm.trans (MulEquiv.trans (x * y) ϕ) = ϕ.symm.trans (MulEquiv.trans x ϕ) * ϕ.symm.trans (MulEquiv.trans y ϕ)

Tactic:
simp [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- Module: Mathlib.Algebra.Group.End
Goal:
A : Type u_1
inst : Add A
e₁ e₂ : AddAut A
⊢ Eq (α := (a : A) → A) (⇑(e₁ * e₂) : (a : A) → A) (Function.comp (β := A) (⇑e₁ : (a : A) → A) (⇑e₂ : (a : A) → A))

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
A : Type u_1
inst : Add A
e : AddAut A
⊢ Eq (α := (a : A) → A) (⇑e⁻¹ : (a : A) → A) (⇑(AddEquiv.symm e) : (a : A) → A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
A : Type u_1
inst : Add A
e₁ e₂ : AddAut A
⊢ e₁ * e₂ = AddEquiv.trans e₂ e₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
A : Type u_1
inst : Add A
⊢ Eq (α := AddAut A) 1 (AddEquiv.refl A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
A : Type u_1
inst : Add A
e₁ : AddAut A
⊢ e₁⁻¹ = AddEquiv.symm e₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
A : Type u_1
inst : Add A
e₁ e₂ : AddAut A
a : A
⊢ Eq (α := A) ((e₁ * e₂ : (a : A) → A) a : A) ((e₁ : (a : A) → A) ((e₂ : (a : A) → A) a : A) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
A : Type u_1
inst : Add A
a : A
⊢ (1 : (a : A) → A) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
A : Type u_1
inst : Add A
e : AddAut A
⊢ AddEquiv.symm e⁻¹ = e

Tactic:
rfl

Premises used: Equiv.symm, rfl, AddEquiv.symm
-- Module: Mathlib.Algebra.Group.End
Goal:
A : Type u_1
inst : Add A
e : AddAut A
⊢ (AddEquiv.symm e)⁻¹ = e

Tactic:
rfl

Premises used: Equiv.symm, rfl, AddEquiv.symm
-- Module: Mathlib.Algebra.Group.End
Goal:
A : Type u_1
inst : Add A
e : AddAut A
a : A
⊢ Eq (α := A) ((e⁻¹ : (a : A) → A) a : A) ((AddEquiv.symm e : (a : A) → A) a : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
A : Type u_1
inst : Add A
e : AddAut A
a : A
⊢ (e⁻¹ : (a : A) → A) ((e : (a : A) → A) a : A) = a

Tactic:
AddEquiv.apply_symm_apply _ _

Premises used: AddEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.End
Goal:
A : Type u_1
inst : Add A
e : AddAut A
a : A
⊢ (e : (a : A) → A) ((e⁻¹ : (a : A) → A) a : A) = a

Tactic:
AddEquiv.apply_symm_apply _ _

Premises used: AddEquiv.apply_symm_apply
-- 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
inst : Add A
inst_1 : AddGroup G
g x : G
⊢ (fun (h : G) ↦ -g + h + g) ((fun (h : G) ↦ g + h + -g) x) = x

Tactic:
simp only [add_assoc, neg_add_cancel_left, neg_add_cancel, add_zero]

Premises used: add_assoc, neg_add_cancel, add_zero, neg_add_cancel_left
-- 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
inst : Add A
inst_1 : AddGroup G
g x : G
⊢ (fun (h : G) ↦ g + h + -g) ((fun (h : G) ↦ -g + h + g) x) = x

Tactic:
simp only [add_assoc, add_neg_cancel_left, add_neg_cancel, add_zero]

Premises used: add_neg_cancel, add_neg_cancel_left, add_assoc, add_zero
-- 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
inst : Add A
inst_1 : AddGroup G
g : G
⊢ ∀ (x y : G), g + (x + y) + -g = g + x + -g + (g + y + -g)

Tactic:
simp only [add_assoc, neg_add_cancel_left, forall_const]

Premises used: add_assoc, forall_const, neg_add_cancel_left
-- 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
inst : Add A
inst_1 : AddGroup G
a :
  ∀ (x : G),
    Eq (α := G)
      ((((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                  { toFun := fun (h : G) ↦ 0 + h + -0, invFun := fun (h : G) ↦ -0 + h + 0, left_inv := ⋯,
                    right_inv := ⋯, map_add' := ⋯ }) :
              AddAut G) :
            (a : G) → G)
          x :
        G)
      (((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) 0 : (a : G) → G) x : G)
⊢ Eq.{u_3 + 1} (α := AddAut G)
    ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
        ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
          { toFun := fun (h : G) ↦ 0 + h + -0, invFun := fun (h : G) ↦ -0 + h + 0, left_inv := ⋯, right_inv := ⋯,
            map_add' := ⋯ }) :
      AddAut G)
    ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) 0 : AddAut G)

Tactic:
ext
-- 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
inst : Add A
inst_1 : AddGroup G
x : G
a :
  ({ toFun := fun (h : G) ↦ h, invFun := fun (h : G) ↦ h, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ } : (a : G) → G)
      x =
    x
⊢ Eq (α := G)
    ((((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
              ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                { toFun := fun (h : G) ↦ 0 + h + -0, invFun := fun (h : G) ↦ -0 + h + 0, left_inv := ⋯, right_inv := ⋯,
                  map_add' := ⋯ }) :
            AddAut G) :
          (a : G) → G)
        x :
      G)
    (((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) 0 : (a : G) → G) x : G)

Tactic:
simp only [zero_add, neg_zero, add_zero, toMul_ofMul, toMul_zero, one_apply]

Premises used: toMul_ofMul, toMul_zero, zero_add, AddAut.one_apply, add_zero, neg_zero
-- 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
inst : Add A
inst_1 : AddGroup G
x : G
⊢ ({ toFun := fun (h : G) ↦ h, invFun := fun (h : G) ↦ h, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ } : (a : G) → G)
      x =
    x

Tactic:
rfl
-- 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
inst : Add A
inst_1 : AddGroup G
g₁ g₂ : G
a :
  ∀ (h : G),
    Eq (α := G)
      ((((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                  { toFun := fun (h : G) ↦ g₁ + g₂ + h + -(g₁ + g₂), invFun := fun (h : G) ↦ -(g₁ + g₂) + h + (g₁ + g₂),
                    left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }) :
              AddAut G) :
            (a : G) → G)
          h :
        G)
      ((((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                (HAdd.hAdd (α := Additive (AddAut G)) (β := Additive (AddAut G))
                  ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                      { toFun := fun (h : G) ↦ g₁ + h + -g₁, invFun := fun (h : G) ↦ -g₁ + h + g₁, left_inv := ⋯,
                        right_inv := ⋯, map_add' := ⋯ } :
                    Additive (AddAut G))
                  ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                      { toFun := fun (h : G) ↦ g₂ + h + -g₂, invFun := fun (h : G) ↦ -g₂ + h + g₂, left_inv := ⋯,
                        right_inv := ⋯, map_add' := ⋯ } :
                    Additive (AddAut G))) :
              AddAut G) :
            (a : G) → G)
          h :
        G)
⊢ Eq.{u_3 + 1} (α := AddAut G)
    ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
        ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
          { toFun := fun (h : G) ↦ g₁ + g₂ + h + -(g₁ + g₂), invFun := fun (h : G) ↦ -(g₁ + g₂) + h + (g₁ + g₂),
            left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }) :
      AddAut G)
    ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
        (HAdd.hAdd (α := Additive (AddAut G)) (β := Additive (AddAut G))
          ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
              { toFun := fun (h : G) ↦ g₁ + h + -g₁, invFun := fun (h : G) ↦ -g₁ + h + g₁, left_inv := ⋯,
                right_inv := ⋯, map_add' := ⋯ } :
            Additive (AddAut G))
          ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
              { toFun := fun (h : G) ↦ g₂ + h + -g₂, invFun := fun (h : G) ↦ -g₂ + h + g₂, left_inv := ⋯,
                right_inv := ⋯, map_add' := ⋯ } :
            Additive (AddAut G))) :
      AddAut G)

Tactic:
ext h
-- 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
inst : Add A
inst_1 : AddGroup G
g₁ g₂ h : G
a : g₁ + g₂ + h + -(g₁ + g₂) = g₁ + (g₂ + h + -g₂) + -g₁
⊢ Eq (α := G)
    ((((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
              ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                { toFun := fun (h : G) ↦ g₁ + g₂ + h + -(g₁ + g₂), invFun := fun (h : G) ↦ -(g₁ + g₂) + h + (g₁ + g₂),
                  left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }) :
            AddAut G) :
          (a : G) → G)
        h :
      G)
    ((((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
              (HAdd.hAdd (α := Additive (AddAut G)) (β := Additive (AddAut G))
                ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                    { toFun := fun (h : G) ↦ g₁ + h + -g₁, invFun := fun (h : G) ↦ -g₁ + h + g₁, left_inv := ⋯,
                      right_inv := ⋯, map_add' := ⋯ } :
                  Additive (AddAut G))
                ((Additive.ofMul : (a : AddAut G) → Additive (AddAut G))
                    { toFun := fun (h : G) ↦ g₂ + h + -g₂, invFun := fun (h : G) ↦ -g₂ + h + g₂, left_inv := ⋯,
                      right_inv := ⋯, map_add' := ⋯ } :
                  Additive (AddAut G))) :
            AddAut G) :
          (a : G) → G)
        h :
      G)

Tactic:
change g₁ + g₂ + h + -(g₁ + g₂) = g₁ + (g₂ + h + -g₂) + -g₁

Premises used: HAdd.hAdd, Neg.neg
-- 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
inst : Add A
inst_1 : AddGroup G
g₁ g₂ h : G
⊢ g₁ + g₂ + h + -(g₁ + g₂) = g₁ + (g₂ + h + -g₂) + -g₁

Tactic:
simp only [add_assoc, neg_add_rev]

Premises used: neg_add_rev, add_assoc
-- Module: Mathlib.Algebra.Group.End
Goal:
G : Type u_3
inst : AddGroup G
g h : G
⊢ (((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((conj : (a : G) → Additive (AddAut G)) g) : AddAut G) :
        (a : G) → G)
      h =
    g + h + -g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
G : Type u_3
inst : AddGroup G
g h : G
⊢ (AddEquiv.symm ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((conj : (a : G) → Additive (AddAut G)) g)) :
        (a : G) → G)
      h =
    -g + h + g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
G : Type u_3
inst : AddGroup G
g h : G
⊢ ((((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((conj : (a : G) → Additive (AddAut G)) g))⁻¹ : AddAut G) :
        (a : G) → G)
      h =
    -g + h + g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.End
Goal:
G : Type u_3
inst : AddGroup G
g h : G
⊢ (((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) (-(conj : (a : G) → Additive (AddAut G)) g) : AddAut G) :
        (a : G) → G)
      h =
    -g + h + g

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
inst : Add A
inst_1 : AddGroup G
H : Type u_7
inst_2 : AddGroup H
ϕ : G ≃+ H
x : AddAut G
⊢ (fun (f : AddAut H) ↦ ϕ.trans (AddEquiv.trans f ϕ.symm))
      ((fun (f : AddAut G) ↦ ϕ.symm.trans (AddEquiv.trans f ϕ)) x) =
    x

Tactic:
simp [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- 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
inst : Add A
inst_1 : AddGroup G
H : Type u_7
inst_2 : AddGroup H
ϕ : G ≃+ H
x : AddAut H
⊢ (fun (f : AddAut G) ↦ ϕ.symm.trans (AddEquiv.trans f ϕ))
      ((fun (f : AddAut H) ↦ ϕ.trans (AddEquiv.trans f ϕ.symm)) x) =
    x

Tactic:
simp [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- 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
inst : Add A
inst_1 : AddGroup G
H : Type u_7
inst_2 : AddGroup H
ϕ : G ≃+ H
⊢ ∀ (x y : AddAut G),
    ϕ.symm.trans (AddEquiv.trans (x * y) ϕ) = ϕ.symm.trans (AddEquiv.trans x ϕ) * ϕ.symm.trans (AddEquiv.trans y ϕ)

Tactic:
simp [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : EquivLike F α β
inst_1 : Mul α
inst_2 : Mul β
inst_3 : MulEquivClass F α β
⊢ Injective (α := F) (β := α ≃* β) toMulEquiv

Tactic:
fun _ _ e ↦ DFunLike.ext _ _ fun a ↦ congr_arg (fun e : α ≃* β ↦ e.toFun a) e

Premises used: DFunLike.ext, MulEquiv.toEquiv, Equiv.toFun, congr_arg, Function.Injective
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul P
inst_4 : Unique α
⊢ ∀ (x y : α → M), (Equiv.funUnique α M).toFun (x * y) = (Equiv.funUnique α M).toFun x * (Equiv.funUnique α M).toFun y

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M_1 : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N_1 : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P_1 : Type u_12
Q_1 : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst_1 : Mul P
inst_2 : Mul Q
f : M ≃ N
g : P ≃* Q
h : M → P
h₁ :
  ∀ (x : M),
    (fun (k : N → Q) (m : M) ↦ ((g.symm : (a : Q) → P) (k ((f : (a : M) → N) m)) : P))
        ((fun (h : M → P) (n : N) ↦ ((g : (a : P) → Q) (h ((f.symm : (a : N) → M) n)) : Q)) h) x =
      h x
⊢ (fun (k : N → Q) (m : M) ↦ ((g.symm : (a : Q) → P) (k ((f : (a : M) → N) m)) : P))
      ((fun (h : M → P) (n : N) ↦ ((g : (a : P) → Q) (h ((f.symm : (a : N) → M) n)) : Q)) h) =
    h

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M_1 : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N_1 : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P_1 : Type u_12
Q_1 : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst_1 : Mul P
inst_2 : Mul Q
f : M ≃ N
g : P ≃* Q
h : M → P
x : M
⊢ (fun (k : N → Q) (m : M) ↦ ((g.symm : (a : Q) → P) (k ((f : (a : M) → N) m)) : P))
      ((fun (h : M → P) (n : N) ↦ ((g : (a : P) → Q) (h ((f.symm : (a : N) → M) n)) : Q)) h) x =
    h x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Equiv.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
M_1 : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N_1 : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P_1 : Type u_12
Q_1 : Type u_13
G : Type u_14
H : Type u_15
inst : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst_1 : Mul P
inst_2 : Mul Q
f : M ≃ N
g : P ≃* Q
k : N → Q
h :
  ∀ (x : N),
    (fun (h : M → P) (n : N) ↦ ((g : (a : P) → Q) (h ((f.symm : (a : N) → M) n)) : Q))
        ((fun (k : N → Q) (m : M) ↦ ((g.symm : (a : Q) → P) (k ((f : (a : M) → N) m)) : P)) k) x =
      k x
⊢ (fun (h : M → P) (n : N) ↦ ((g : (a : P) → Q) (h ((f.symm : (a : N) → M) n)) : Q))
      ((fun (k : N → Q) (m : M) ↦ ((g.symm : (a : Q) → P) (k ((f : (a : M) → N) m)) : P)) k) =
    k

Tactic:
ext