awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
Q : Type u_10
inst : MulOne M
inst_1 : MulOne N
inst_2 : MulOne P
inst_3 : MulOne 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
-- 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₁ g₂ : OneHom N P
f : OneHom M N
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => OneHom.ext <| hf.forall.2 (DFunLike.ext_iff.1 h), fun h => h ▸ rfl⟩

Premises used: Iff.mpr, Function.Surjective.forall, Eq.rec, OneHom.ext, DFunLike.ext_iff, Iff.intro, Iff.mp, 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₁ g₂ : N →ₙ* P
f : M →ₙ* N
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => MulHom.ext <| hf.forall.2 (DFunLike.ext_iff.1 h), fun h => h ▸ rfl⟩

Premises used: Iff.mpr, Function.Surjective.forall, Eq.rec, DFunLike.ext_iff, MulHom.ext, Iff.intro, Iff.mp, 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₁ g₂ : N →* P
f : M →* N
hf : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => MonoidHom.ext <| hf.forall.2 (DFunLike.ext_iff.1 h), fun h => h ▸ rfl⟩

Premises used: Iff.mpr, Function.Surjective.forall, MonoidHom.ext, Eq.rec, DFunLike.ext_iff, Iff.intro, Iff.mp, 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₁ f₂ : OneHom M N
hg : Injective.{u_5 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : g.comp f₁ = g.comp f₂
x : M
rw : Eq.{u_6 + 1} (α := P) ((g.comp f₁ : (a : M) → P) x : P) ((g : (a : N) → P) ((f₂ : (a : M) → N) x : N) : P)
rw₁ : Eq.{u_6 + 1} (α := P) ((g.comp f₂ : (a : M) → P) x : P) ((g : (a : N) → P) ((f₂ : (a : M) → N) x : N) : P)
rw₂ rw₃ :
  Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f₂ : (a : M) → N) x : N) : P)
    ((g : (a : N) → P) ((f₂ : (a : M) → N) x : N) : P)
⊢ Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f₁ : (a : M) → N) x : N) : P)
    ((g : (a : N) → P) ((f₂ : (a : M) → N) x : N) : P)

Tactic:
rw [← OneHom.comp_apply, h, OneHom.comp_apply]

Premises used: OneHom.comp_apply
-- 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₁ f₂ : M →ₙ* N
hg : Injective.{u_5 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : g.comp f₁ = g.comp f₂
x : M
rw : Eq.{u_6 + 1} (α := P) ((g.comp f₁ : (a : M) → P) x : P) ((g : (a : N) → P) ((f₂ : (a : M) → N) x : N) : P)
rw₁ : Eq.{u_6 + 1} (α := P) ((g.comp f₂ : (a : M) → P) x : P) ((g : (a : N) → P) ((f₂ : (a : M) → N) x : N) : P)
rw₂ rw₃ :
  Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f₂ : (a : M) → N) x : N) : P)
    ((g : (a : N) → P) ((f₂ : (a : M) → N) x : N) : P)
⊢ Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f₁ : (a : M) → N) x : N) : P)
    ((g : (a : N) → P) ((f₂ : (a : M) → N) x : N) : P)

Tactic:
rw [← MulHom.comp_apply, h, MulHom.comp_apply]

Premises used: MulHom.comp_apply
-- 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₁ f₂ : M →* N
hg : Injective.{u_5 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : g.comp f₁ = g.comp f₂
x : M
rw : Eq.{u_6 + 1} (α := P) ((g.comp f₁ : (a : M) → P) x : P) ((g : (a : N) → P) ((f₂ : (a : M) → N) x : N) : P)
rw₁ : Eq.{u_6 + 1} (α := P) ((g.comp f₂ : (a : M) → P) x : P) ((g : (a : N) → P) ((f₂ : (a : M) → N) x : N) : P)
rw₂ rw₃ :
  Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f₂ : (a : M) → N) x : N) : P)
    ((g : (a : N) → P) ((f₂ : (a : M) → N) x : N) : P)
⊢ Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f₁ : (a : M) → N) x : N) : P)
    ((g : (a : N) → P) ((f₂ : (a : M) → N) x : N) : P)

Tactic:
rw [← MonoidHom.comp_apply, h, MonoidHom.comp_apply]

Premises used: MonoidHom.comp_apply
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOne M
inst_1 : MulOne N
⊢ Injective (α := M →* N) toOneHom

Tactic:
Function.Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Premises used: DFunLike.coe_injective, Function.Injective.of_comp
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : MulOne M
inst_1 : MulOne N
⊢ Injective (α := M →* N) toMulHom

Tactic:
Function.Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Premises used: DFunLike.coe_injective, Function.Injective.of_comp
-- 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.comp (id M) = 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
⊢ f.comp (id M) = 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
⊢ f.comp (id M) = 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
inst : One M
inst_1 : One N
f : OneHom M N
⊢ comp (id N) f = 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
⊢ comp (id N) f = 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
⊢ comp (id N) f = 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
inst : Monoid M
inst_1 : Monoid N
f : M →* N
a : M
n : ℕ
⊢ (f : (a : M) → N) (a ^ n) = HPow.hPow (α := N) ((f : (a : M) → N) a : N) n

Tactic:
map_pow f a n

Premises used: map_pow
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : DivInvMonoid M
inst_1 : DivInvMonoid N
f : M →* N
hf : ∀ (x : M), Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) x⁻¹ : N) (((f : (a : M) → N) x)⁻¹ : N)
a : M
n : ℤ
⊢ (f : (a : M) → N) (a ^ n) = HPow.hPow (α := N) ((f : (a : M) → N) a : N) n

Tactic:
map_zpow' f hf a n

Premises used: map_zpow'
-- 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
f : OneHom M N
g : N → M
h₁ : LeftInverse g (⇑f : (a : M) → N)
rw : g ((f : (a : M) → N) 1) = 1
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) 1 1
⊢ g 1 = 1

Tactic:
rw [← f.map_one, h₁]

Premises used: OneHom.map_one
-- 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
f : M →ₙ* N
g : N → M
h₁ : LeftInverse g (⇑f : (a : M) → N)
h₂ : RightInverse g (⇑f : (a : M) → N)
x y : N
rw : g (x * y) = g (HMul.hMul (β := N) x ((f : (a : M) → N) (g y) : N))
rw₁ rw₂ : g (x * y) = g (x * y)
⊢ g (x * y) = g (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (g x) : N) ((f : (a : M) → N) (g y) : N))

Tactic:
rw [h₂ x, h₂ y]
-- 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
f : M →ₙ* N
g : N → M
h₁ : LeftInverse g (⇑f : (a : M) → N)
h₂ : RightInverse g (⇑f : (a : M) → N)
x y : N
rw rw₁ :
  g (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (g x) : N) ((f : (a : M) → N) (g y) : N)) =
    g (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (g x) : N) ((f : (a : M) → N) (g y) : N))
⊢ g (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (g x) : N) ((f : (a : M) → N) (g y) : N)) =
    g ((f : (a : M) → N) (g x * g y))

Tactic:
rw [f.map_mul]

Premises used: MulHom.map_mul
-- 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
is_surj : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
is_comm : IsMulCommutative M
a b : N
have : ∀ (a' : M) (ha' : (f : (a : M) → N) a' = a), a * b = b * a
⊢ a * b = b * a

Tactic:
have ⟨a', ha'⟩ := is_surj a
-- 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
is_surj : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
is_comm : IsMulCommutative M
a b : N
a' : M
ha' : (f : (a : M) → N) a' = a
have : ∀ (b' : M) (hb' : (f : (a : M) → N) b' = b), a * b = b * a
⊢ a * b = b * a

Tactic:
have ⟨b', hb'⟩ := is_surj b
-- 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
is_surj : Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
is_comm : IsMulCommutative M
a b : N
a' : M
ha' : (f : (a : M) → N) a' = a
b' : M
hb' : (f : (a : M) → N) b' = b
⊢ a * b = b * a

Tactic:
simp [← ha', ← hb', ← map_mul, mul_comm']

Premises used: map_mul, mul_comm'
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
inst : MulOne M
f g : Monoid.End M
h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((g : (a : M) → M) x : M)
⊢ 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 : MulOne M
⊢ MonoidHomClass (Monoid.End M) M M

Tactic:
inferInstanceAs <| MonoidHomClass (M →* M) M M

Premises used: _private.0.Monoid.End.instMonoidHomClass._proof_1
-- 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
n : ℕ
f : Monoid.End M
zero : Eq (α := M → M) (⇑f : (a : M) → M)^[0] (⇑(npowRec 0 f) : (a : M) → M)
succ :
  ∀ (n : ℕ),
    Eq (α := M → M) (⇑f : (a : M) → M)^[n] (⇑(npowRec n f) : (a : M) → M) →
      Eq (α := M → M) (⇑f : (a : M) → M)^[n + 1] (⇑(npowRec (n + 1) f) : (a : M) → M)
⊢ Eq (α := M → M) (⇑f : (a : M) → M)^[n] (⇑(npowRec n f) : (a : M) → M)

Tactic:
induction n
-- 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
f : Monoid.End M
zero : Eq.{u_4 + 1} (α := M → M) id (⇑1 : (a : M) → M)
⊢ Eq (α := M → M) (⇑f : (a : M) → M)^[0] (⇑(npowRec 0 f) : (a : M) → M)

Tactic:
simp [npowRec, *]

Premises used: npowRec
-- 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
f : Monoid.End M
n : ℕ
h : Eq (α := M → M) (⇑f : (a : M) → M)^[n] (⇑(npowRec n f) : (a : M) → M)
succ :
  Eq (α := M → M) (comp (β := M) (⇑(npowRec n f) : (a : M) → M) (⇑f : (a : M) → M)) (⇑(npowRec n f * f) : (a : M) → M)
⊢ Eq (α := M → M) (⇑f : (a : M) → M)^[n + 1] (⇑(npowRec (n + 1) f) : (a : M) → M)

Tactic:
simp [npowRec, *]

Premises used: npowRec
-- 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
f : Monoid.End M
⊢ Eq.{u_4 + 1} (α := M → M) id (⇑1 : (a : M) → M)

Tactic:
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 : MulOne M
f : Monoid.End M
n : ℕ
h : Eq (α := M → M) (⇑f : (a : M) → M)^[n] (⇑(npowRec n f) : (a : M) → M)
⊢ Eq (α := M → M) (comp (β := M) (⇑(npowRec n f) : (a : M) → M) (⇑f : (a : M) → M)) (⇑(npowRec n f * f) : (a : M) → M)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
inst : MulOne M
f : Monoid.End M
n : ℕ
⊢ Eq (α := (a : M) → M) (⇑(f ^ n) : (a : M) → M) (⇑f : (a : M) → M)^[n]

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
inst : MulOne M
f g : Monoid.End M
⊢ Eq (α := (a : M) → M) (⇑(f * g) : (a : M) → M) (comp (β := M) (⇑f : (a : M) → M) (⇑g : (a : M) → M))

Tactic:
rfl

Premises used: Monoid.End, rfl
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
inst : One M
inst_1 : One N
x : M
⊢ Eq.{u_5 + 1} (α := N) ((1 : (a : M) → N) x : N) (1 : 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 : MulOneClass N
x : M
⊢ Eq.{u_5 + 1} (α := N) ((1 : (a : M) → N) x : N) (1 : 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
f : OneHom M N
⊢ Eq (α := OneHom M P) (comp 1 f) 1

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
f : OneHom N P
h : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((f.comp 1 : (a : M) → P) x : P) ((1 : (a : M) → P) x : P)
⊢ Eq (α := OneHom M P) (f.comp 1) 1

Tactic:
ext
-- 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
f : OneHom N P
x : M
⊢ Eq.{u_6 + 1} (α := P) ((f.comp 1 : (a : M) → P) x : P) ((1 : (a : M) → P) x : P)

Tactic:
simp only [map_one, OneHom.coe_comp, Function.comp_apply, OneHom.one_apply]

Premises used: OneHom.coe_comp, OneHom.one_apply, map_one, Function.comp_apply
-- 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 : MulOneClass P
f : M →* N
⊢ Eq (α := M →* P) (comp 1 f) 1

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 : MulOneClass N
inst_2 : MulOneClass P
f : N →* P
h : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((f.comp 1 : (a : M) → P) x : P) ((1 : (a : M) → P) x : P)
⊢ Eq (α := M →* P) (f.comp 1) 1

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

Tactic:
simp only [map_one, coe_comp, Function.comp_apply, one_apply]

Premises used: MonoidHom.coe_comp, map_one, MonoidHom.one_apply, Function.comp_apply
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
f : α →* β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a⁻¹ : β) (((f : (a : α) → β) a)⁻¹ : β)

Tactic:
map_inv f _

Premises used: map_inv
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
f : α →* β
g : α
n : ℤ
⊢ (f : (a : α) → β) (g ^ n) = HPow.hPow (α := β) ((f : (a : α) → β) g : β) n

Tactic:
map_zpow f g n

Premises used: map_zpow
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
f : α →* β
g h : α
⊢ (f : (a : α) → β) (g / h) = HDiv.hDiv (α := β) (β := β) ((f : (a : α) → β) g : β) ((f : (a : α) → β) h : β)

Tactic:
map_div f g h

Premises used: map_div
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : DivisionMonoid β
f : α →* β
g h : α
⊢ (f : (a : α) → β) (g * h⁻¹) = HMul.hMul (α := β) (β := β) ((f : (a : α) → β) g : β) (((f : (a : α) → β) h)⁻¹ : β)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_10
F : Type u_11
inst : Mul M
inst_1 : FunLike F M M
inst_2 : MulHomClass F M M
f : F
n : ℕ
x y : M
⊢ (⇑f : (a : M) → M)^[n] (x * y) = (⇑f : (a : M) → M)^[n] x * (⇑f : (a : M) → M)^[n] y

Tactic:
Function.Semiconj₂.iterate (map_mul f) n x y

Premises used: map_mul, Function.Semiconj₂.iterate
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_10
F : Type u_11
inst : One M
inst_1 : FunLike F M M
inst_2 : OneHomClass F M M
f : F
n : ℕ
⊢ Eq.{u_10 + 1} (α := M) ((⇑f : (a : M) → M)^[n] 1) 1

Tactic:
iterate_fixed (map_one f) n

Premises used: map_one, Function.iterate_fixed
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_10
F : Type u_11
inst : Group M
inst_1 : FunLike F M M
inst_2 : MonoidHomClass F M M
f : F
n : ℕ
x : M
⊢ (⇑f : (a : M) → M)^[n] x⁻¹ = ((⇑f : (a : M) → M)^[n] x)⁻¹

Tactic:
Commute.iterate_left (map_inv f) n x

Premises used: map_inv, Function.Commute.iterate_left
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_10
F : Type u_11
inst : Group M
inst_1 : FunLike F M M
inst_2 : MonoidHomClass F M M
f : F
n : ℕ
x y : M
⊢ (⇑f : (a : M) → M)^[n] (x / y) = (⇑f : (a : M) → M)^[n] x / (⇑f : (a : M) → M)^[n] y

Tactic:
Semiconj₂.iterate (map_div f) n x y

Premises used: Function.Semiconj₂.iterate, map_div
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_10
F : Type u_11
inst : Monoid M
inst_1 : FunLike F M M
inst_2 : MonoidHomClass F M M
f : F
n : ℕ
x : M
k : ℕ
⊢ (⇑f : (a : M) → M)^[n] (x ^ k) = (⇑f : (a : M) → M)^[n] x ^ k

Tactic:
Commute.iterate_left (map_pow f · k) n x

Premises used: map_pow, Function.Commute.iterate_left
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_10
F : Type u_11
inst : Group M
inst_1 : FunLike F M M
inst_2 : MonoidHomClass F M M
f : F
n : ℕ
x : M
k : ℤ
⊢ (⇑f : (a : M) → M)^[n] (x ^ k) = (⇑f : (a : M) → M)^[n] x ^ k

Tactic:
Commute.iterate_left (map_zpow f · k) n x

Premises used: map_zpow, Function.Commute.iterate_left
-- Module: Mathlib.Algebra.Group.Hom.End
Goal:
M : Type uM
inst : AddCommMonoid M
n : ℕ
m : M
⊢ ((↑n : AddMonoid.End M) : (a : M) → M) m = n • m

Tactic:
rfl

Premises used: AddMonoid.End.instFunLike._aux_1, rfl
-- Module: Mathlib.Algebra.Group.Hom.End
Goal:
M : Type uM
inst : AddCommMonoid M
n : ℕ
inst_1 : n.AtLeastTwo
m : M
⊢ (OfNat.ofNat n : (a : M) → M) m = n • m

Tactic:
rfl

Premises used: AddMonoid.End.instFunLike._aux_1, rfl
-- Module: Mathlib.Algebra.Group.Hom.End
Goal:
M : Type uM
inst : AddCommGroup M
⊢ Eq.{uM + 1} (α := SubNegMonoid (AddMonoid.End M)) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Hom.End
Goal:
M : Type uM
inst : AddCommGroup M
⊢ Eq.{uM + 1} (α := SubNegMonoid (AddMonoid.End M)) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : One M
inst_1 : Monoid N
f : OneHom M N
n : ℕ
⊢ HPow.hPow (α := (a : M) → N) (⇑f : (a : M) → N) n 1 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : MulOneClass M
inst_1 : CommMonoid N
f : M →* N
n : ℕ
⊢ HPow.hPow (α := (a : M) → N) (⇑f : (a : M) → N) n 1 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : MulOneClass M
inst_1 : CommMonoid N
f : M →* N
n : ℕ
x y : M
⊢ HPow.hPow (α := (a : M) → N) (⇑f : (a : M) → N) n (x * y) =
    HPow.hPow (α := (a : M) → N) (⇑f : (a : M) → N) n x * HPow.hPow (α := (a : M) → N) (⇑f : (a : M) → N) n y

Tactic:
simp [mul_pow]

Premises used: mul_pow
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
inst : One M
inst_1 : Monoid N
f : OneHom M N
n : ℕ
x : M
⊢ (f ^ n : (a : M) → N) x = HPow.hPow (α := N) ((f : (a : M) → N) x : N) n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
inst : MulOneClass M
inst_1 : CommMonoid N
f : M →* N
n : ℕ
x : M
⊢ (f ^ n : (a : M) → N) x = HPow.hPow (α := N) ((f : (a : M) → N) x : N) n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : One M
inst_1 : Group N
f : OneHom M N
n : ℤ
⊢ HPow.hPow (α := (a : M) → N) (⇑f : (a : M) → N) n 1 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : MulOneClass M
inst_1 : CommGroup N
f : M →* N
n : ℤ
⊢ HPow.hPow (α := (a : M) → N) (⇑f : (a : M) → N) n 1 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : MulOneClass M
inst_1 : CommGroup N
f : M →* N
n : ℤ
x y : M
⊢ HPow.hPow (α := (a : M) → N) (⇑f : (a : M) → N) n (x * y) =
    HPow.hPow (α := (a : M) → N) (⇑f : (a : M) → N) n x * HPow.hPow (α := (a : M) → N) (⇑f : (a : M) → N) n y

Tactic:
simp [mul_zpow]

Premises used: mul_zpow
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
inst : One M
inst_1 : Group N
f : OneHom M N
z : ℤ
x : M
⊢ (f ^ z : (a : M) → N) x = HPow.hPow (α := N) ((f : (a : M) → N) x : N) z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
inst : MulOneClass M
inst_1 : CommGroup N
f : M →* N
z : ℤ
x : M
⊢ (f ^ z : (a : M) → N) x = HPow.hPow (α := N) ((f : (a : M) → N) x : N) z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : One M
inst_1 : MulOneClass N
inst_2 : IsLeftCancelMul N
⊢ IsLeftCancelMul (OneHom M N)

Tactic:
DFunLike.coe_injective.isLeftCancelMul _ fun _ _ => rfl

Premises used: DFunLike.coe_injective, Function.Injective.isLeftCancelMul, rfl
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : MulOneClass M
inst_1 : CommMonoid N
inst_2 : IsLeftCancelMul N
⊢ IsLeftCancelMul (M →* N)

Tactic:
DFunLike.coe_injective.isLeftCancelMul _ fun _ _ => rfl

Premises used: DFunLike.coe_injective, Function.Injective.isLeftCancelMul, rfl
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : One M
inst_1 : MulOneClass N
inst_2 : IsRightCancelMul N
⊢ IsRightCancelMul (OneHom M N)

Tactic:
DFunLike.coe_injective.isRightCancelMul _ fun _ _ => rfl

Premises used: Function.Injective.isRightCancelMul, DFunLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : MulOneClass M
inst_1 : CommMonoid N
inst_2 : IsRightCancelMul N
⊢ IsRightCancelMul (M →* N)

Tactic:
DFunLike.coe_injective.isRightCancelMul _ fun _ _ => rfl

Premises used: Function.Injective.isRightCancelMul, DFunLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
inst : AddCommMonoid M
m : M
⊢ Eq (α := M) ((0 : (a : M) → M) m : M) (0 : M)

Tactic:
rfl

Premises used: AddMonoid.End.instFunLike._aux_1, rfl
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
inst : AddZeroClass M
m : M
⊢ (1 : (a : M) → M) m = m

Tactic:
rfl

Premises used: AddMonoid.End.instFunLike._aux_1, rfl
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
inst : AddCommGroup M
z : ℤ
m : M
⊢ ((↑z : AddMonoid.End M) : (a : M) → M) m = z • m

Tactic:
rfl

Premises used: AddMonoid.End.instFunLike._aux_1, rfl
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
x : MulOneClass M
x_1 : MulOneClass N
x_2 : CommMonoid P
f g : M →* N →* P
⊢ f = g ↔
    ∀ (x_3 : M) (y : N),
      Eq.{uP + 1} (α := P) ((((f : (a : M) → N →* P) x_3 : N →* P) : (a : N) → P) y : P)
        ((((g : (a : M) → N →* P) x_3 : N →* P) : (a : N) → P) y : P)

Tactic:
DFunLike.ext_iff.trans <| forall_congr' fun _ => DFunLike.ext_iff

Premises used: DFunLike.ext_iff, forall_congr', Iff.trans
-- Module: Mathlib.Algebra.Group.Hom.Instances
Goal:
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
mM : MulOneClass M
mN : MulOneClass N
mP : CommMonoid P
f : M →* N →* P
y : N
⊢ Eq.{uP + 1} (α := P) (((f : (a : M) → N →* P) 1 : (a : N) → P) y : P) (1 : P)

Tactic:
simp [f.map_one, one_apply]

Premises used: MonoidHom.map_one, MonoidHom.one_apply