awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
F : Type u_9
inst : MulOne M
inst_1 : MulOne N
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
a b : M
h : a * b = 1
rw : Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) (a * b) : N) (1 : N)
rw₁ : Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) 1 : N) (1 : N)
rw₂ rw₃ : Eq.{u_5 + 1} (α := N) 1 1
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) = 1

Tactic:
rw [← map_mul, h, map_one]

Premises used: map_mul, map_one
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : DivInvMonoid G
inst_2 : DivInvMonoid H
inst_3 : MulHomClass F G H
f : F
hf : ∀ (a : G), Eq.{u_8 + 1} (α := H) ((f : (a : G) → H) a⁻¹ : H) (((f : (a : G) → H) a)⁻¹ : H)
a b : G
⊢ (f : (a : G) → H) (a / b) = HDiv.hDiv (α := H) (β := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) b : H)

Tactic:
grind [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : DivInvMonoid G
inst_2 : DivInvMonoid H
inst_3 : MulHomClass F G H
f : F
hf : ∀ (a : G), Eq.{u_8 + 1} (α := H) ((f : (a : G) → H) a⁻¹ : H) (((f : (a : G) → H) a)⁻¹ : H)
g h : ι → G
h₁ :
  ∀ (x : ι),
    ((⇑f : (a : G) → H) ∘ (g / h)) x =
      HDiv.hDiv (α := ι → H) (β := ι → H) ((⇑f : (a : G) → H) ∘ g) ((⇑f : (a : G) → H) ∘ h) x
⊢ (⇑f : (a : G) → H) ∘ (g / h) = HDiv.hDiv (α := ι → H) ((⇑f : (a : G) → H) ∘ g) ((⇑f : (a : G) → H) ∘ h)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : DivInvMonoid G
inst_2 : DivInvMonoid H
inst_3 : MulHomClass F G H
f : F
hf : ∀ (a : G), Eq.{u_8 + 1} (α := H) ((f : (a : G) → H) a⁻¹ : H) (((f : (a : G) → H) a)⁻¹ : H)
g h : ι → G
x : ι
⊢ ((⇑f : (a : G) → H) ∘ (g / h)) x =
    HDiv.hDiv (α := ι → H) (β := ι → H) ((⇑f : (a : G) → H) ∘ g) ((⇑f : (a : G) → H) ∘ h) x

Tactic:
simp [map_div' f hf]

Premises used: map_div'
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : Group G
inst_2 : DivisionMonoid H
inst_3 : MonoidHomClass F G H
f : F
a : G
⊢ Eq.{u_8 + 1} (α := H) ((f : (a : G) → H) a⁻¹ : H) (((f : (a : G) → H) a)⁻¹ : H)

Tactic:
eq_inv_of_mul_eq_one_left <| map_mul_eq_one f <| inv_mul_cancel _

Premises used: inv_mul_cancel, eq_inv_of_mul_eq_one_left, map_mul_eq_one
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : Group G
inst_2 : DivisionMonoid H
inst_3 : MonoidHomClass F G H
f : F
g : ι → G
h : ∀ (x : ι), Eq.{u_8 + 1} (α := H) (((⇑f : (a : G) → H) ∘ g⁻¹) x : H) (((⇑f : (a : G) → H) ∘ g)⁻¹ x : H)
⊢ Eq (α := ι → H) ((⇑f : (a : G) → H) ∘ g⁻¹) ((⇑f : (a : G) → H) ∘ g)⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : Group G
inst_2 : DivisionMonoid H
inst_3 : MonoidHomClass F G H
f : F
g : ι → G
x : ι
⊢ Eq.{u_8 + 1} (α := H) (((⇑f : (a : G) → H) ∘ g⁻¹) x : H) (((⇑f : (a : G) → H) ∘ g)⁻¹ x : H)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : Group G
inst_2 : DivisionMonoid H
inst_3 : MonoidHomClass F G H
f : F
a b : G
rw :
  HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) b⁻¹ : H) =
    HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a : H) (((f : (a : G) → H) b)⁻¹ : H)
rw₁ rw₂ :
  HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a : H) (((f : (a : G) → H) b)⁻¹ : H) =
    HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a : H) (((f : (a : G) → H) b)⁻¹ : H)
⊢ (f : (a : G) → H) (a * b⁻¹) = HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a : H) (((f : (a : G) → H) b)⁻¹ : H)

Tactic:
rw [map_mul, map_inv]

Premises used: map_inv, map_mul
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : Group G
inst_2 : DivisionMonoid H
inst_3 : MonoidHomClass F G H
f : F
g h : ι → G
⊢ (⇑f : (a : G) → H) ∘ (g * h⁻¹) = HMul.hMul (α := ι → H) ((⇑f : (a : G) → H) ∘ g) ((⇑f : (a : G) → H) ∘ h)⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : Group G
inst_2 : DivisionMonoid H
inst_3 : MonoidHomClass F G H
f : F
⊢ ∀ (a b : G),
    (f : (a : G) → H) (a / b) = HDiv.hDiv (α := H) (β := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) b : H)

Tactic:
map_div' _ <| map_inv f

Premises used: map_inv, map_div'
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : Group G
inst_2 : DivisionMonoid H
inst_3 : MonoidHomClass F G H
f : F
g h : ι → G
h₁ :
  ∀ (x : ι),
    ((⇑f : (a : G) → H) ∘ (g / h)) x =
      HDiv.hDiv (α := ι → H) (β := ι → H) ((⇑f : (a : G) → H) ∘ g) ((⇑f : (a : G) → H) ∘ h) x
⊢ (⇑f : (a : G) → H) ∘ (g / h) = HDiv.hDiv (α := ι → H) ((⇑f : (a : G) → H) ∘ g) ((⇑f : (a : G) → H) ∘ h)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : Group G
inst_2 : DivisionMonoid H
inst_3 : MonoidHomClass F G H
f : F
g h : ι → G
x : ι
⊢ ((⇑f : (a : G) → H) ∘ (g / h)) x =
    HDiv.hDiv (α := ι → H) (β := ι → H) ((⇑f : (a : G) → H) ∘ g) ((⇑f : (a : G) → H) ∘ h) x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : Monoid G
inst_2 : Monoid H
inst_3 : MonoidHomClass F G H
f : F
a : G
rw : (f : (a : G) → H) 1 = HPow.hPow (α := H) (β := ℕ) ((f : (a : G) → H) a : H) 0
rw₁ : Eq.{u_8 + 1} (α := H) ((f : (a : G) → H) 1 : H) (1 : H)
rw₂ rw₃ : Eq.{u_8 + 1} (α := H) 1 1
⊢ (f : (a : G) → H) (HPow.hPow (β := ℕ) a 0) = HPow.hPow (α := H) (β := ℕ) ((f : (a : G) → H) a : H) 0

Tactic:
rw [pow_zero, pow_zero, map_one]

Premises used: pow_zero, map_one
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : Monoid G
inst_2 : Monoid H
inst_3 : MonoidHomClass F G H
f : F
a : G
n : ℕ
rw : (f : (a : G) → H) (a ^ n * a) = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (n + 1)
rw₁ :
  (f : (a : G) → H) (a ^ n * a) =
    HMul.hMul (β := H) (HPow.hPow (α := H) ((f : (a : G) → H) a : H) n) ((f : (a : G) → H) a : H)
rw₂ :
  HMul.hMul (α := H) (β := H) ((f : (a : G) → H) (a ^ n) : H) ((f : (a : G) → H) a : H) =
    HMul.hMul (β := H) (HPow.hPow (α := H) ((f : (a : G) → H) a : H) n) ((f : (a : G) → H) a : H)
rw₃ rw₄ :
  HMul.hMul (β := H) (HPow.hPow (α := H) ((f : (a : G) → H) a : H) n) ((f : (a : G) → H) a : H) =
    HMul.hMul (β := H) (HPow.hPow (α := H) ((f : (a : G) → H) a : H) n) ((f : (a : G) → H) a : H)
⊢ (f : (a : G) → H) (a ^ (n + 1)) = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (n + 1)

Tactic:
rw [pow_succ, pow_succ, map_mul, map_pow f a n]

Premises used: pow_succ, map_mul
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : Monoid G
inst_2 : Monoid H
inst_3 : MonoidHomClass F G H
f : F
g : ι → G
n : ℕ
h : ∀ (x : ι), ((⇑f : (a : G) → H) ∘ (g ^ n)) x = HPow.hPow (α := ι → H) ((⇑f : (a : G) → H) ∘ g) n x
⊢ (⇑f : (a : G) → H) ∘ (g ^ n) = HPow.hPow (α := ι → H) ((⇑f : (a : G) → H) ∘ g) n

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : Monoid G
inst_2 : Monoid H
inst_3 : MonoidHomClass F G H
f : F
g : ι → G
n : ℕ
x : ι
⊢ ((⇑f : (a : G) → H) ∘ (g ^ n)) x = HPow.hPow (α := ι → H) ((⇑f : (a : G) → H) ∘ g) n x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : DivInvMonoid G
inst_2 : DivInvMonoid H
inst_3 : MonoidHomClass F G H
f : F
hf : ∀ (x : G), Eq.{u_8 + 1} (α := H) ((f : (a : G) → H) x⁻¹ : H) (((f : (a : G) → H) x)⁻¹ : H)
a : G
n : ℕ
rw : (f : (a : G) → H) (a ^ n) = HPow.hPow (α := H) (β := ℤ) ((f : (a : G) → H) a : H) (↑n : ℤ)
rw₁ : HPow.hPow (α := H) ((f : (a : G) → H) a : H) n = HPow.hPow (α := H) (β := ℤ) ((f : (a : G) → H) a : H) (↑n : ℤ)
rw₂ rw₃ : HPow.hPow (α := H) ((f : (a : G) → H) a : H) n = HPow.hPow (α := H) ((f : (a : G) → H) a : H) n
⊢ (f : (a : G) → H) (HPow.hPow (β := ℤ) a (↑n : ℤ)) = HPow.hPow (α := H) (β := ℤ) ((f : (a : G) → H) a : H) (↑n : ℤ)

Tactic:
rw [zpow_natCast, map_pow, zpow_natCast]

Premises used: zpow_natCast, map_pow
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : DivInvMonoid G
inst_2 : DivInvMonoid H
inst_3 : MonoidHomClass F G H
f : F
hf : ∀ (x : G), Eq.{u_8 + 1} (α := H) ((f : (a : G) → H) x⁻¹ : H) (((f : (a : G) → H) x)⁻¹ : H)
a : G
n : ℕ
rw : (f : (a : G) → H) (a ^ (n + 1))⁻¹ = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (Int.negSucc n)
rw₁ : ((f : (a : G) → H) (a ^ (n + 1)))⁻¹ = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (Int.negSucc n)
rw₂ :
  (HPow.hPow (α := H) ((f : (a : G) → H) a : H) (n + 1))⁻¹ =
    HPow.hPow (α := H) ((f : (a : G) → H) a : H) (Int.negSucc n)
rw₃ rw₄ :
  HPow.hPow (α := H) ((f : (a : G) → H) a : H) (Int.negSucc n) =
    HPow.hPow (α := H) ((f : (a : G) → H) a : H) (Int.negSucc n)
⊢ (f : (a : G) → H) (a ^ Int.negSucc n) = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (Int.negSucc n)

Tactic:
rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc]

Premises used: zpow_negSucc, map_pow
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : DivInvMonoid G
inst_2 : DivInvMonoid H
inst_3 : MonoidHomClass F G H
f : F
hf : ∀ (x : G), Eq.{u_8 + 1} (α := H) ((f : (a : G) → H) x⁻¹ : H) (((f : (a : G) → H) x)⁻¹ : H)
g : ι → G
n : ℤ
h : ∀ (x : ι), ((⇑f : (a : G) → H) ∘ (g ^ n)) x = HPow.hPow (α := ι → H) ((⇑f : (a : G) → H) ∘ g) n x
⊢ (⇑f : (a : G) → H) ∘ (g ^ n) = HPow.hPow (α := ι → H) ((⇑f : (a : G) → H) ∘ g) n

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : DivInvMonoid G
inst_2 : DivInvMonoid H
inst_3 : MonoidHomClass F G H
f : F
hf : ∀ (x : G), Eq.{u_8 + 1} (α := H) ((f : (a : G) → H) x⁻¹ : H) (((f : (a : G) → H) x)⁻¹ : H)
g : ι → G
n : ℤ
x : ι
⊢ ((⇑f : (a : G) → H) ∘ (g ^ n)) x = HPow.hPow (α := ι → H) ((⇑f : (a : G) → H) ∘ g) n x

Tactic:
simp [map_zpow' f hf]

Premises used: map_zpow'
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : Group G
inst_2 : DivisionMonoid H
inst_3 : MonoidHomClass F G H
f : F
g : G
n : ℤ
⊢ (f : (a : G) → H) (g ^ n) = HPow.hPow (α := H) ((f : (a : G) → H) g : H) n

Tactic:
map_zpow' f (map_inv f) g n

Premises used: map_inv, map_zpow'
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst : FunLike F G H
inst_1 : Group G
inst_2 : DivisionMonoid H
inst_3 : MonoidHomClass F G H
f : F
g : ι → G
n : ℤ
⊢ (⇑f : (a : G) → H) ∘ (g ^ n) = HPow.hPow (α := ι → H) ((⇑f : (a : G) → H) ∘ g) n

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : IsMulTorsionFree N
f : M →* N
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
n : ℕ
hn : n ≠ 0
x y : M
hxy : Eq.{u_4 + 1} (α := M) ((fun (a : M) ↦ a ^ n) x) ((fun (a : M) ↦ a ^ n) y)
⊢ Eq.{u_5 + 1} (α := N) ((fun (a : N) ↦ a ^ n) ((f : (a : M) → N) x)) ((fun (a : N) ↦ a ^ n) ((f : (a : M) → N) y))

Tactic:
simpa using congrArg f hxy

Premises used: congrArg, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : One M
inst_1 : One N
f : M → N
h1 : f 1 = 1
⊢ (⇑{ toFun := f, map_one' := h1 : OneHom M N } : (a : M) → N) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : One M
inst_1 : One N
f : OneHom M N
⊢ f.toFun = (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M → N
hmul : ∀ (x y : M), f (x * y) = f x * f y
⊢ (⇑{ toFun := f, map_mul' := hmul : M →ₙ* N } : (a : M) → N) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
⊢ f.toFun = (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOne M
inst_1 : MulOne N
f : OneHom M N
hmul : ∀ (x y : M), f.toFun (x * y) = f.toFun x * f.toFun y
⊢ Eq (α := (a : M) → N) (⇑{ toOneHom := f, map_mul' := hmul : M →* N } : (a : M) → N) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOne M
inst_1 : MulOne N
f : M →* N
⊢ Eq (α := (a : M) → N) (⇑(↑f : OneHom M N) : (a : M) → N) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOne M
inst_1 : MulOne N
f : M →* N
⊢ (↑f : M →ₙ* N).toFun = (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOne M
inst_1 : MulOne N
f : M →* N
⊢ (↑f : OneHom M N).toFun = (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : One M
inst_1 : One N
f g : OneHom M N
h : ∀ (x : M), Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f g : M →ₙ* N
h : ∀ (x : M), Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOne M
inst_1 : MulOne N
f g : M →* N
h : ∀ (x : M), Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst : Group G
inst_1 : MulOneClass M
f : M → G
map_mul : ∀ (a b : M), f (a * b) = f a * f b
rw : f 1 * f 1 = 1 * f 1
rw₁ : G
rw₂ : f (HMul.hMul (α := M) 1 1) = 1 * f 1
rw₃ : f 1 = 1 * f 1
rw₄ rw₅ : f 1 = f 1
⊢ f 1 = 1

Tactic:
rw [← mul_right_cancel_iff, ← map_mul _ 1, one_mul, one_mul]

Premises used: mul_right_cancel_iff, OfNat.ofNat, one_mul
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : One M
inst_1 : One N
f : OneHom M N
h1 : Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) 1 : N) (1 : N)
⊢ { toFun := (⇑f : (a : M) → N), map_one' := h1 : OneHom M N } = f

Tactic:
OneHom.ext fun _ => rfl

Premises used: OneHom.ext, rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
hmul :
  ∀ (x y : M),
    (f : (a : M) → N) (x * y) = HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
⊢ { toFun := (⇑f : (a : M) → N), map_mul' := hmul : M →ₙ* N } = f

Tactic:
MulHom.ext fun _ => rfl

Premises used: MulHom.ext, rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOne M
inst_1 : MulOne N
f : M →* N
hmul :
  ∀ (x y : M),
    OneHom.toFun (↑f : OneHom M N) (x * y) = OneHom.toFun (↑f : OneHom M N) x * OneHom.toFun (↑f : OneHom M N) y
⊢ { toOneHom := (↑f : OneHom M N), map_mul' := hmul : M →* N } = f

Tactic:
MonoidHom.ext fun _ => rfl

Premises used: MonoidHom.ext, rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
x : One M
x_1 : One N
f : OneHom M N
f' : M → N
h : f' = (⇑f : (a : M) → N)
⊢ (⇑(f.copy f' h) : (a : M) → N) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
x : One M
x_1 : One N
f : OneHom M N
f' : M → N
h : f' = (⇑f : (a : M) → N)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
x : Mul M
x_1 : Mul N
f : M →ₙ* N
f' : M → N
h : f' = (⇑f : (a : M) → N)
⊢ (⇑(f.copy f' h) : (a : M) → N) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
x : Mul M
x_1 : Mul N
f : M →ₙ* N
f' : M → N
h : f' = (⇑f : (a : M) → N)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
x : MulOne M
x_1 : MulOne N
f : M →* N
f' : M → N
h : f' = (⇑f : (a : M) → N)
⊢ (⇑(f.copy f' h) : (a : M) → N) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
x : MulOne M
x_1 : MulOne N
f : M →* N
f' : M → N
h : f' = (⇑f : (a : M) → N)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : One M
inst_1 : One N
f : OneHom M N
⊢ Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) 1 : N) (1 : N)

Tactic:
f.map_one'

Premises used: OneHom.map_one'
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOne M
inst_1 : MulOne N
f : M →* N
⊢ Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) 1 : N) (1 : N)

Tactic:
f.map_one'

Premises used: OneHom.map_one', MonoidHom.toOneHom
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
a b : M
⊢ (f : (a : M) → N) (a * b) = HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)

Tactic:
f.map_mul' a b

Premises used: MulHom.map_mul'
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOne M
inst_1 : MulOne N
f : M →* N
a b : M
⊢ (f : (a : M) → N) (a * b) = HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)

Tactic:
f.map_mul' a b

Premises used: MonoidHom.map_mul'
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
F : Type u_9
inst : MulOne M
inst_1 : MulOne N
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
x : M
hx : ∃ (y : M), x * y = 1
⊢ ∃ (y : N), HMul.hMul (α := N) ((f : (a : M) → N) x : N) y = 1

Tactic:
let ⟨y, hy⟩ := hx
  ⟨f y, map_mul_eq_one f hy⟩

Premises used: HMul.hMul, Exists, Exists.intro, map_mul_eq_one, OfNat.ofNat, Eq, DFunLike.coe, _private.0.MonoidHom.map_exists_right_inv.match_1
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
F : Type u_9
inst : MulOne M
inst_1 : MulOne N
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
x : M
hx : ∃ (y : M), y * x = 1
⊢ ∃ (y : N), HMul.hMul (β := N) y ((f : (a : M) → N) x : N) = 1

Tactic:
let ⟨y, hy⟩ := hx
  ⟨f y, map_mul_eq_one f hy⟩

Premises used: HMul.hMul, Exists, _private.0.MonoidHom.map_exists_left_inv.match_1, Exists.intro, map_mul_eq_one, OfNat.ofNat, Eq, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
F : Type u_9
inst : MulOne M
inst_1 : MulOne N
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
inst_4 : IsDedekindFiniteMonoid N
a b : M
eq : a * b = 1
⊢ Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) (b * a) : N) ((f : (a : M) → N) 1 : N)

Tactic:
simpa [mul_eq_one_comm] using congr_arg f eq

Premises used: congr_arg, mul_eq_one_comm, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_10
inst : One M
⊢ Eq (α := (a : M) → M) (⇑(id M) : (a : M) → M) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_10
inst : Mul M
⊢ Eq (α := (a : M) → M) (⇑(id M) : (a : M) → M) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_10
inst : MulOne M
⊢ Eq (α := (a : M) → M) (⇑(id M) : (a : M) → M) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst : One M
inst_1 : One N
inst_2 : One P
hnp : OneHom N P
hmn : OneHom M N
⊢ Eq.{u_6 + 1} (α := P) ((hnp : (a : N) → P) ((hmn : (a : M) → N) 1 : N) : P) (1 : P)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
hnp : N →ₙ* P
hmn : M →ₙ* N
x y : M
⊢ (hnp : (a : N) → P) ((hmn : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := P) (β := P) ((hnp : (a : N) → P) ((hmn : (a : M) → N) x : N) : P)
      ((hnp : (a : N) → P) ((hmn : (a : M) → N) y : N) : P)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst : MulOne M
inst_1 : MulOne N
inst_2 : MulOne P
hnp : N →* P
hmn : M →* N
⊢ Eq.{u_6 + 1} (α := P) ((hnp : (a : N) → P) ((hmn : (a : M) → N) 1 : N) : P) (1 : P)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst : MulOne M
inst_1 : MulOne N
inst_2 : MulOne P
hnp : N →* P
hmn : M →* N
⊢ ∀ (x y : M),
    (hnp : (a : N) → P) ((hmn : (a : M) → N) (x * y) : N) =
      HMul.hMul (α := P) (β := P) ((hnp : (a : N) → P) ((hmn : (a : M) → N) x : N) : P)
        ((hnp : (a : N) → P) ((hmn : (a : M) → N) y : N) : P)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : One M
inst_1 : One N
inst_2 : One P
g : OneHom N P
f : OneHom M N
⊢ Eq (α := M → P) (⇑(g.comp f) : (a : M) → P)
    (Function.comp.{u_4 + 1, u_5 + 1, u_6 + 1} (β := N) (⇑g : (a : N) → P) (⇑f : (a : M) → N))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
g : N →ₙ* P
f : M →ₙ* N
⊢ Eq (α := M → P) (⇑(g.comp f) : (a : M) → P)
    (Function.comp.{u_4 + 1, u_5 + 1, u_6 + 1} (β := N) (⇑g : (a : N) → P) (⇑f : (a : M) → N))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : MulOne M
inst_1 : MulOne N
inst_2 : MulOne P
g : N →* P
f : M →* N
⊢ Eq (α := M → P) (⇑(g.comp f) : (a : M) → P)
    (Function.comp.{u_4 + 1, u_5 + 1, u_6 + 1} (β := N) (⇑g : (a : N) → P) (⇑f : (a : M) → N))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : One M
inst_1 : One N
inst_2 : One P
g : OneHom N P
f : OneHom M N
x : M
⊢ Eq.{u_6 + 1} (α := P) ((g.comp f : (a : M) → P) x : P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
g : N →ₙ* P
f : M →ₙ* N
x : M
⊢ Eq.{u_6 + 1} (α := P) ((g.comp f : (a : M) → P) x : P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : MulOne M
inst_1 : MulOne N
inst_2 : MulOne P
g : N →* P
f : M →* N
x : M
⊢ Eq.{u_6 + 1} (α := P) ((g.comp f : (a : M) → P) x : P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
Q : Type u_10
inst : One M
inst_1 : One N
inst_2 : One P
inst_3 : One Q
f : OneHom M N
g : OneHom N P
h : OneHom P Q
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
Q : Type u_10
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : Mul Q
f : M →ₙ* N
g : N →ₙ* P
h : P →ₙ* Q
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
rfl

Premises used: rfl