awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x : α
n : ℕ
⊢ (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x : α
n : ℕ
⊢ (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
inv₁ : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
zpow₁ : ∀ (x : α) (n : ℤ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
⊢ Group α

Tactic:
apply e.injective.group _

Premises used: Function.Injective.group, Equiv.injective
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x y : α
⊢ (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x y : α
⊢ (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x : α
n : ℕ
⊢ (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x : α
n : ℕ
⊢ (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x : α
n : ℤ
⊢ (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x : α
n : ℤ
⊢ (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
one₁ : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
inv₁ : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)
div₁ :
  ∀ (x y : α),
    (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
npow₁ : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
zpow₁ : ∀ (x : α) (n : ℤ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
⊢ CommGroup α

Tactic:
apply e.injective.commGroup _

Premises used: Function.Injective.commGroup, Equiv.injective
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x y : α
⊢ (e : (a : α) → β) (x * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) x⁻¹ : β) (((e : (a : α) → β) x)⁻¹ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x y : α
⊢ (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x y : α
⊢ (e : (a : α) → β) (x / y) = HDiv.hDiv (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x : α
n : ℕ
⊢ (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x : α
n : ℕ
⊢ (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x : α
n : ℤ
⊢ (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x : α
n : ℤ
⊢ (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
obtain : ∀ (n : ℕ) (e : G ≃ Fin n), ∃ (G' : Type v) (x : Group G') (x_1 : Fintype G'), Nonempty (G ≃* G')
⊢ ∃ (G' : Type v) (x : Group G') (x_1 : Fintype G'), Nonempty (G ≃* G')

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin G

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
n : ℕ
e_1 : G ≃ Fin n
f : Fin n ≃ ULift.{v, 0} (Fin n) := Equiv.symm Equiv.ulift
e : Equiv.{u + 1, max 1 (v + 1)} G (ULift.{v, 0} (Fin n)) := e_1.trans f
groupH : Group (ULift.{v, 0} (Fin n)) := e.symm.group
⊢ ∃ (G' : Type v) (x : Group G') (x_1 : Fintype G'), Nonempty (G ≃* G')

Tactic:
⟨ULift (Fin n), groupH, inferInstance, ⟨MulEquiv.symm <| e.symm.mulEquiv⟩⟩

Premises used: ULift, inferInstance, Nonempty.intro, Equiv.mulEquiv, Exists.intro, Equiv.symm, MulEquiv.symm, Fin
-- Module: Mathlib.Algebra.Group.TransferInstance
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
n : ℕ
e_1 : G ≃ Fin n
f : Fin n ≃ ULift.{v, 0} (Fin n) := Equiv.symm Equiv.ulift
e : Equiv.{u + 1, max 1 (v + 1)} G (ULift.{v, 0} (Fin n)) := e_1.trans f
groupH : Group (ULift.{v, 0} (Fin n)) := e.symm.group
⊢ ∃ (G' : Type v) (x : Group G') (x_1 : Fintype G'), Nonempty (G ≃* G')

Tactic:
exact ⟨ULift (Fin n), groupH, inferInstance, ⟨MulEquiv.symm <| e.symm.mulEquiv⟩⟩
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a : G
f : G → α
x : G
⊢ τ a f x = f (x - a)

Tactic:
rfl

Premises used: translate, rfl
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
f : G → α
h : ∀ (x : G), τ 0 f x = f x
⊢ τ 0 f = f

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
f : G → α
x : G
⊢ τ 0 f x = f x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a b : G
f : G → α
h : ∀ (x : G), τ a (τ b f) x = τ (a + b) f x
⊢ τ a (τ b f) = τ (a + b) f

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a b : G
f : G → α
x : G
⊢ τ a (τ b f) x = τ (a + b) f x

Tactic:
simp [sub_sub]

Premises used: sub_sub
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a b : G
f : G → α
h : ∀ (x : G), τ (a + b) f x = τ a (τ b f) x
⊢ τ (a + b) f = τ a (τ b f)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a b : G
f : G → α
x : G
⊢ τ (a + b) f x = τ a (τ b f) x

Tactic:
simp [sub_sub]

Premises used: sub_sub
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a b : G
f : G → α
rw : τ (b + a) f = τ b (τ a f)
rw₁ rw₂ : τ b (τ a f) = τ b (τ a f)
⊢ τ (a + b) f = τ b (τ a f)

Tactic:
rw [add_comm, translate_add]

Premises used: add_comm, translate_add
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a b : G
f : G → α
rw : τ (a + b) f = τ b (τ a f)
rw₁ rw₂ : τ b (τ a f) = τ b (τ a f)
⊢ τ a (τ b f) = τ b (τ a f)

Tactic:
rw [← translate_add, translate_add']

Premises used: translate_add', translate_add
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
β : Type u_3
G : Type u_5
inst : AddCommGroup G
a : G
f : G → α
g : α → β
⊢ g ∘ τ a f = τ a (g ∘ f)

Tactic:
rfl

Premises used: translate, rfl
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a : G
f : G → α
h : ∀ (x : G), τ a f x = HVAdd.hVAdd (α := Gᵈᵃᵃ) ((DomAddAct.mk : (a : G) → Gᵈᵃᵃ) (-a) : Gᵈᵃᵃ) f x
⊢ τ a f = HVAdd.hVAdd (α := Gᵈᵃᵃ) ((DomAddAct.mk : (a : G) → Gᵈᵃᵃ) (-a) : Gᵈᵃᵃ) f

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
a : G
f : G → α
x : G
⊢ τ a f x = HVAdd.hVAdd (α := Gᵈᵃᵃ) ((DomAddAct.mk : (a : G) → Gᵈᵃᵃ) (-a) : Gᵈᵃᵃ) f x

Tactic:
simp [DomAddAct.vadd_apply, sub_eq_neg_add]

Premises used: sub_eq_neg_add, DomAddAct.vadd_apply
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
H : Type u_6
inst : AddCommGroup G
inst_1 : SMul H α
a : G
f : G → α
c : H
⊢ τ a (c • f) = c • τ a f

Tactic:
rfl

Premises used: translate, rfl
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
inst_1 : Zero α
a : G
⊢ Eq (α := G → α) (τ a 0) 0

Tactic:
rfl

Premises used: translate, rfl
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
inst_1 : Add α
a : G
f g : G → α
⊢ τ a (f + g) = τ a f + τ a g

Tactic:
rfl

Premises used: translate, rfl
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
inst_1 : Sub α
a : G
f g : G → α
⊢ τ a (f - g) = τ a f - τ a g

Tactic:
rfl

Premises used: translate, rfl
-- Module: Mathlib.Algebra.Group.Translate
Goal:
α : Type u_2
G : Type u_5
inst : AddCommGroup G
inst_1 : Neg α
a : G
f : G → α
⊢ τ a (-f) = -τ a f

Tactic:
rfl

Premises used: translate, rfl
-- Module: Mathlib.Algebra.Group.Translate
Goal:
ι : Type u_1
M : Type u_4
G : Type u_5
inst : AddCommGroup G
inst_1 : AddCommMonoid M
a : G
f : ι → G → M
s : Finset ι
h : ∀ (x : G), Eq.{u_4 + 1} (α := M) (τ a (∑ i ∈ s, f i) x) ((∑ i ∈ s, τ a (f i)) x)
⊢ Eq (α := G → M) (τ a (∑ i ∈ s, f i)) (∑ i ∈ s, τ a (f i))

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Translate
Goal:
ι : Type u_1
M : Type u_4
G : Type u_5
inst : AddCommGroup G
inst_1 : AddCommMonoid M
a : G
f : ι → G → M
s : Finset ι
x : G
⊢ Eq.{u_4 + 1} (α := M) (τ a (∑ i ∈ s, f i) x) ((∑ i ∈ s, τ a (f i)) x)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Translate
Goal:
M : Type u_4
G : Type u_5
inst : AddCommGroup G
inst_1 : AddCommMonoid M
inst_2 : Fintype G
a : G
f : G → M
⊢ Eq.{u_4 + 1} (α := M) (∑ b : G, τ a f b) (∑ b : G, f b)

Tactic:
Fintype.sum_equiv (Equiv.subRight _) _ _ fun _ ↦ rfl

Premises used: Equiv.subRight, Fintype.sum_equiv, rfl
-- Module: Mathlib.Algebra.Group.Translate
Goal:
G : Type u_5
H : Type u_6
inst : AddCommGroup G
inst_1 : AddCommGroup H
a : G
f : G → H
h : ∀ (x : G), x ∈ support (τ a f) ↔ x ∈ a +ᵥ support f
⊢ support (τ a f) = a +ᵥ support f

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Translate
Goal:
G : Type u_5
H : Type u_6
inst : AddCommGroup G
inst_1 : AddCommGroup H
a : G
f : G → H
x : G
⊢ x ∈ support (τ a f) ↔ x ∈ a +ᵥ support f

Tactic:
simp [mem_vadd_set_iff_neg_vadd_mem, sub_eq_neg_add]

Premises used: sub_eq_neg_add, Set.mem_vadd_set_iff_neg_vadd_mem
-- Module: Mathlib.Algebra.Group.Translate
Goal:
ι : Type u_1
M : Type u_4
G : Type u_5
inst : AddCommGroup G
inst_1 : CommMonoid M
a : G
f : ι → G → M
s : Finset ι
h : ∀ (x : G), Eq.{u_4 + 1} (α := M) (τ a (∏ i ∈ s, f i) x) ((∏ i ∈ s, τ a (f i)) x)
⊢ Eq (α := G → M) (τ a (∏ i ∈ s, f i)) (∏ i ∈ s, τ a (f i))

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Translate
Goal:
ι : Type u_1
M : Type u_4
G : Type u_5
inst : AddCommGroup G
inst_1 : CommMonoid M
a : G
f : ι → G → M
s : Finset ι
x : G
⊢ Eq.{u_4 + 1} (α := M) (τ a (∏ i ∈ s, f i) x) ((∏ i ∈ s, τ a (f i)) x)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Additive α ≃ α) (Equiv.symm ofMul) toMul

Tactic:
rfl

Premises used: Additive.toMul, rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := α ≃ Additive α) (Equiv.symm toMul) ofMul

Tactic:
rfl

Premises used: Additive.ofMul, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
a b : Additive α
hab : Eq (α := α) ((toMul : (a : Additive α) → α) a : α) ((toMul : (a : Additive α) → α) b : α)
⊢ a = b

Tactic:
hab

Premises used: Additive
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
p : Additive α → Prop
⊢ (∀ (a : Additive α), p a) ↔ ∀ (a : α), p ((ofMul : (a : α) → Additive α) a)

Tactic:
Iff.rfl

Premises used: Additive, Iff.rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
p : Additive α → Prop
⊢ (∃ (a : Additive α), p a) ↔ ∃ (a : α), p ((ofMul : (a : α) → Additive α) a)

Tactic:
Iff.rfl

Premises used: Additive, Iff.rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Multiplicative α ≃ α) (Equiv.symm ofAdd) toAdd

Tactic:
rfl

Premises used: Multiplicative.toAdd, rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := α ≃ Multiplicative α) (Equiv.symm toAdd) ofAdd

Tactic:
rfl

Premises used: Multiplicative.ofAdd, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
a b : Multiplicative α
hab : Eq (α := α) ((toAdd : (a : Multiplicative α) → α) a : α) ((toAdd : (a : Multiplicative α) → α) b : α)
⊢ a = b

Tactic:
hab

Premises used: Multiplicative
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
p : Multiplicative α → Prop
⊢ (∀ (a : Multiplicative α), p a) ↔ ∀ (a : α), p ((ofAdd : (a : α) → Multiplicative α) a)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Multiplicative
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
p : Multiplicative α → Prop
⊢ (∃ (a : Multiplicative α), p a) ↔ ∃ (a : α), p ((ofAdd : (a : α) → Multiplicative α) a)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Multiplicative
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
x : α
⊢ (toAdd : (a : Multiplicative α) → α) ((ofAdd : (a : α) → Multiplicative α) x : Multiplicative α) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
x : Multiplicative α
⊢ (ofAdd : (a : α) → Multiplicative α) ((toAdd : (a : Multiplicative α) → α) x : α) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
x : α
⊢ (toMul : (a : Additive α) → α) ((ofMul : (a : α) → Additive α) x : Additive α) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
x : Additive α
⊢ (ofMul : (a : α) → Additive α) ((toMul : (a : Additive α) → α) x : α) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
β : Type v
inst : Subsingleton α
⊢ Subsingleton.{u + 1} (Additive α)

Tactic:
toMul.injective.subsingleton

Premises used: Function.Injective.subsingleton, Additive.toMul, Equiv.injective
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
β : Type v
inst : Subsingleton α
⊢ Subsingleton.{u + 1} (Multiplicative α)

Tactic:
toAdd.injective.subsingleton

Premises used: Function.Injective.subsingleton, Multiplicative.toAdd, Equiv.injective
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
β : Type v
inst : Nontrivial α
⊢ Nontrivial.{u} (Additive α)

Tactic:
ofMul.injective.nontrivial

Premises used: Function.Injective.nontrivial, Additive.ofMul, Equiv.injective