awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : CommGroup G
inst_3 : CommGroup H
f : M →* G
a b : M
simp_rw simp_rw₁ :
  ((f : (a : M) → G) (a * b))⁻¹ =
    HMul.hMul (α := G) (β := G) (((f : (a : M) → G) a)⁻¹ : G) (((f : (a : M) → G) b)⁻¹ : G)
simp_rw₂ :
  ((f : (a : M) → G) (a * b))⁻¹ = (HMul.hMul (α := G) (β := G) ((f : (a : M) → G) a : G) ((f : (a : M) → G) b : G))⁻¹
⊢ (fun (g : M) ↦ (((f : (a : M) → G) g)⁻¹ : G)) (a * b) =
    HMul.hMul (α := G) ((fun (g : M) ↦ (((f : (a : M) → G) g)⁻¹ : G)) a)
      ((fun (g : M) ↦ (((f : (a : M) → G) g)⁻¹ : G)) b)

Tactic:
simp_rw [← mul_inv, f.map_mul]

Premises used: mul_inv, MonoidHom.map_mul
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
G : Type u_5
inst : MulOneClass M
inst_1 : CommGroup G
f : M →* G
x : M
⊢ Eq.{u_5 + 1} (α := G) ((f⁻¹ : (a : M) → G) x : G) (((f : (a : M) → G) x)⁻¹ : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
N : Type u_3
G : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : CommGroup G
φ : N →* G
ψ : M →* N
⊢ φ⁻¹.comp ψ = (φ.comp ψ)⁻¹

Tactic:
rfl

Premises used: MonoidHom.mk', rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
G : Type u_5
H : Type u_6
inst : MulOneClass M
inst_1 : CommGroup G
inst_2 : CommGroup H
φ : G →* H
ψ : M →* G
h : ∀ (x : M), Eq.{u_6 + 1} (α := H) ((φ.comp ψ⁻¹ : (a : M) → H) x : H) (((φ.comp ψ)⁻¹ : (a : M) → H) x : H)
⊢ φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
G : Type u_5
H : Type u_6
inst : MulOneClass M
inst_1 : CommGroup G
inst_2 : CommGroup H
φ : G →* H
ψ : M →* G
x : M
⊢ Eq.{u_6 + 1} (α := H) ((φ.comp ψ⁻¹ : (a : M) → H) x : H) (((φ.comp ψ)⁻¹ : (a : M) → H) x : H)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : CommGroup G
inst_3 : CommGroup H
f g : M →* G
a b : M
⊢ (fun (x : M) ↦ HDiv.hDiv (α := G) (β := G) ((f : (a : M) → G) x : G) ((g : (a : M) → G) x : G)) (a * b) =
    HMul.hMul (α := G)
      ((fun (x : M) ↦ HDiv.hDiv (α := G) (β := G) ((f : (a : M) → G) x : G) ((g : (a : M) → G) x : G)) a)
      ((fun (x : M) ↦ HDiv.hDiv (α := G) (β := G) ((f : (a : M) → G) x : G) ((g : (a : M) → G) x : G)) b)

Tactic:
simp [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]

Premises used: mul_assoc, mul_left_comm, div_eq_mul_inv, mul_comm
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
G : Type u_5
inst : MulOneClass M
inst_1 : CommGroup G
f g : M →* G
x : M
⊢ (f / g : (a : M) → G) x = HDiv.hDiv (α := G) (β := G) ((f : (a : M) → G) x : G) ((g : (a : M) → G) x : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
N : Type u_3
G : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : CommGroup G
f g : N →* G
h : M →* N
⊢ (f / g).comp h = f.comp h / g.comp h

Tactic:
rfl

Premises used: MonoidHom.mk', rfl
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
G : Type u_5
H : Type u_6
inst : MulOneClass M
inst_1 : CommGroup G
inst_2 : CommGroup H
f : G →* H
g h : M →* G
h₁ : ∀ (x : M), Eq.{u_6 + 1} (α := H) ((f.comp (g / h) : (a : M) → H) x : H) ((f.comp g / f.comp h : (a : M) → H) x : H)
⊢ f.comp (g / h) = f.comp g / f.comp h

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
M : Type u_2
G : Type u_5
H : Type u_6
inst : MulOneClass M
inst_1 : CommGroup G
inst_2 : CommGroup H
f : G →* H
g h : M →* G
x : M
⊢ Eq.{u_6 + 1} (α := H) ((f.comp (g / h) : (a : M) → H) x : H) ((f.comp g / f.comp h : (a : M) → H) x : H)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst : Group G
inst_1 : CommGroup H
f : G →* H
hf : Function.Injective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
simp_rw : ∀ (a b : G), Eq.{u_6 + 1} (α := H) ((f : (a : G) → H) (a * b) : H) ((f : (a : G) → H) (b * a) : H)
simp_rw₁ :
  ∀ (a b : G),
    HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) b : H) =
      HMul.hMul (α := H) (β := H) ((f : (a : G) → H) b : H) ((f : (a : G) → H) a : H)
simp_rw₂ : ∀ (a b : G), True
⊢ ∀ (a b : G), a * b = b * a

Tactic:
simp_rw [← hf.eq_iff, map_mul, mul_comm, implies_true]

Premises used: Function.Injective.eq_iff, map_mul, mul_comm, implies_true
-- Module: Mathlib.Algebra.Group.Hom.Basic
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst : CommGroup G
inst_1 : Group H
f : G →* H
hf : Function.Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
simp_rw :
  ∀ (x₁ x₂ : G),
    HMul.hMul (α := H) (β := H) ((f : (a : G) → H) x₁ : H) ((f : (a : G) → H) x₂ : H) =
      HMul.hMul (α := H) (β := H) ((f : (a : G) → H) x₂ : H) ((f : (a : G) → H) x₁ : H)
simp_rw₁ : ∀ (x₁ x₂ : G), Eq.{u_6 + 1} (α := H) ((f : (a : G) → H) (x₁ * x₂) : H) ((f : (a : G) → H) (x₂ * x₁) : H)
simp_rw₂ : ∀ (x₁ x₂ : G), True
⊢ ∀ (a b : H), a * b = b * a

Tactic:
simp_rw [hf.forall₂, ← map_mul, mul_comm, implies_true]

Premises used: map_mul, mul_comm, implies_true, Function.Surjective.forall₂
-- Module: Mathlib.Algebra.Group.Hom.CompTypeclasses
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
σ : M →* M
h : _root_.CompTriple.IsId (M := M) (⇑σ : (a : M) → M)
h₁ : ∀ (x : M), Eq (α := M) ((σ : (a : M) → M) x : M) ((id M : (a : M) → M) x : M)
⊢ σ = id M

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Hom.CompTypeclasses
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
σ : M →* M
h : _root_.CompTriple.IsId (M := M) (⇑σ : (a : M) → M)
x : M
⊢ Eq (α := M) ((σ : (a : M) → M) x : M) ((id M : (a : M) → M) x : M)

Tactic:
congr_fun h.eq_id _

Premises used: congr_fun, CompTriple.IsId.eq_id
-- Module: Mathlib.Algebra.Group.Hom.CompTypeclasses
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
σ : M →* M
h : _root_.CompTriple.IsId (M := M) (⇑σ : (a : M) → M)
x : M
⊢ Eq (α := M) ((σ : (a : M) → M) x : M) ((id M : (a : M) → M) x : M)

Tactic:
exact congr_fun h.eq_id _

Premises used: congr_fun, CompTriple.IsId.eq_id
-- Module: Mathlib.Algebra.Group.Hom.CompTypeclasses
Goal:
M : Type u_1
N_1 : Type u_2
P_1 : Type u_3
inst : Monoid M
inst_1 : Monoid N_1
inst_2 : Monoid P_1
N : Type u_4
P : Type u_5
inst_3 : Monoid N
inst_4 : Monoid P
φ : N →* N
inst_5 : IsId φ
ψ : N →* P
⊢ ψ.comp φ = ψ

Tactic:
simp only [IsId.eq_id, MonoidHom.comp_id]

Premises used: MonoidHom.CompTriple.IsId.eq_id, MonoidHom.comp_id
-- Module: Mathlib.Algebra.Group.Hom.CompTypeclasses
Goal:
M_1 : Type u_1
N_1 : Type u_2
P : Type u_3
inst : Monoid M_1
inst_1 : Monoid N_1
inst_2 : Monoid P
M : Type u_4
N : Type u_5
inst_3 : Monoid M
inst_4 : Monoid N
φ : M →* N
ψ : N →* N
inst_5 : IsId ψ
⊢ ψ.comp φ = φ

Tactic:
simp only [IsId.eq_id, MonoidHom.id_comp]

Premises used: MonoidHom.CompTriple.IsId.eq_id, MonoidHom.id_comp
-- Module: Mathlib.Algebra.Group.Hom.CompTypeclasses
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
φ : M →* N
ψ : N →* M
h : Function.RightInverse.{u_2 + 1, u_1 + 1} (α := N) (β := M) (⇑φ : (a : M) → N) (⇑ψ : (a : N) → M)
χ : M →* M
inst_2 : IsId χ
⊢ ψ.comp φ = χ

Tactic:
simp only [IsId.eq_id, ← DFunLike.coe_fn_eq, coe_comp, h.id, coe_id]

Premises used: MonoidHom.coe_comp, MonoidHom.CompTriple.IsId.eq_id, Function.RightInverse.id, MonoidHom.coe_id, DFunLike.coe_fn_eq
-- Module: Mathlib.Algebra.Group.Hom.CompTypeclasses
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
φ : M →* N
ψ : N →* P
χ : M →* P
κ : φ.CompTriple ψ χ
rw : Eq (α := M → P) (⇑(ψ.comp φ) : (a : M) → P) (⇑χ : (a : M) → P)
rw₁ rw₂ : Eq (α := M → P) (⇑χ : (a : M) → P) (⇑χ : (a : M) → P)
⊢ Eq (α := M → P) (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := N) (⇑ψ : (a : N) → P) (⇑φ : (a : M) → N))
    (⇑χ : (a : M) → P)

Tactic:
rw [← MonoidHom.coe_comp, κ.comp_eq]

Premises used: MonoidHom.coe_comp, MonoidHom.CompTriple.comp_eq
-- Module: Mathlib.Algebra.Group.Hom.CompTypeclasses
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
φ : M →* N
ψ : N →* P
χ : M →* P
h : φ.CompTriple ψ χ
x : M
rw : Eq.{u_3 + 1} (α := P) ((ψ : (a : N) → P) ((φ : (a : M) → N) x : N) : P) ((ψ.comp φ : (a : M) → P) x : P)
rw₁ rw₂ :
  Eq.{u_3 + 1} (α := P) ((ψ : (a : N) → P) ((φ : (a : M) → N) x : N) : P)
    ((ψ : (a : N) → P) ((φ : (a : M) → N) x : N) : P)
⊢ Eq.{u_3 + 1} (α := P) ((ψ : (a : N) → P) ((φ : (a : M) → N) x : N) : P) ((χ : (a : M) → P) x : P)

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

Premises used: MonoidHom.CompTriple.comp_eq, MonoidHom.comp_apply
-- Module: Mathlib.Algebra.Group.Hom.CompTypeclasses
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
Q : Type u_4
inst_3 : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
mp : φ₁.CompTriple φ₂₃ φ₁₂₃ → φ₁₂.CompTriple φ₃ φ₁₂₃
mpr : φ₁₂.CompTriple φ₃ φ₁₂₃ → φ₁.CompTriple φ₂₃ φ₁₂₃
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃ ↔ φ₁₂.CompTriple φ₃ φ₁₂₃

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Hom.CompTypeclasses
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
Q : Type u_4
inst_3 : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
h : φ₂₃.comp φ₁ = φ₁₂₃
⊢ φ₃.comp φ₁₂ = φ₁₂₃

Tactic:
simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]

Premises used: MonoidHom.CompTriple.comp_eq, MonoidHom.comp_assoc
-- Module: Mathlib.Algebra.Group.Hom.CompTypeclasses
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
Q : Type u_4
inst_3 : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
h : φ₂₃.comp φ₁ = φ₁₂₃
⊢ φ₁₂.CompTriple φ₃ φ₁₂₃

Tactic:
exact ⟨by simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]⟩
-- Module: Mathlib.Algebra.Group.Hom.CompTypeclasses
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
Q : Type u_4
inst_3 : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
h : φ₃.comp φ₁₂ = φ₁₂₃
⊢ φ₂₃.comp φ₁ = φ₁₂₃

Tactic:
simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]

Premises used: MonoidHom.CompTriple.comp_eq, MonoidHom.comp_assoc
-- Module: Mathlib.Algebra.Group.Hom.CompTypeclasses
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
Q : Type u_4
inst_3 : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
h : φ₃.comp φ₁₂ = φ₁₂₃
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃

Tactic:
exact ⟨by simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]⟩
-- 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 g : OneHom M N
h : f.toFun = g.toFun
mk :
  ∀ (toFun : M → N) (map_one' : toFun 1 = 1)
    (h : { toFun := toFun, map_one' := map_one' : OneHom M N }.toFun = g.toFun),
    { toFun := toFun, map_one' := map_one' : OneHom M N } = g
⊢ f = g

Tactic:
cases f
-- 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
g : OneHom M N
toFun : M → N
map_one' : toFun 1 = 1
h : { toFun := toFun, map_one' := map_one' : OneHom M N }.toFun = g.toFun
mk :
  ∀ (toFun_1 : M → N) (map_one'_1 : toFun_1 1 = 1)
    (h :
      { toFun := toFun, map_one' := map_one' : OneHom M N }.toFun =
        { toFun := toFun_1, map_one' := map_one'_1 : OneHom M N }.toFun),
    { toFun := toFun, map_one' := map_one' : OneHom M N } = { toFun := toFun_1, map_one' := map_one'_1 }
⊢ { toFun := toFun, map_one' := map_one' : OneHom M N } = g

Tactic:
cases g
-- 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
toFun : M → N
map_one' : toFun 1 = 1
toFun_1 : M → N
map_one'_1 : toFun_1 1 = 1
h :
  { toFun := toFun, map_one' := map_one' : OneHom M N }.toFun =
    { toFun := toFun_1, map_one' := map_one'_1 : OneHom M N }.toFun
⊢ { toFun := toFun, map_one' := map_one' : OneHom M N } = { toFun := toFun_1, map_one' := map_one'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
F : Type u_9
inst : One M
inst_1 : One N
inst_2 : FunLike F M N
inst_3 : OneHomClass F M N
f : F
⊢ Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) 1 : N) (1 : N)

Tactic:
OneHomClass.map_one f

Premises used: OneHomClass.map_one
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
F : Type u_9
inst : One M
inst_1 : One N
inst_2 : FunLike F M N
inst_3 : OneHomClass F M N
f : F
⊢ Eq (α := ι → N) (comp.{u_1 + 1, u_4 + 1, u_5 + 1} (β := M) (⇑f : (a : M) → N) 1) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
F : Type u_9
inst : One M
inst_1 : One N
inst_2 : FunLike F M N
inst_3 : Subsingleton M
inst_4 : OneHomClass F M N
f g : F
x : M
⊢ Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)

Tactic:
simp [Subsingleton.elim x 1]

Premises used: Subsingleton.elim, OfNat.ofNat
-- 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 : FunLike F M N
inst_3 : Subsingleton M
⊢ Subsingleton (OneHom M N)

Tactic:
.of_oneHomClass

Premises used: Subsingleton.of_oneHomClass
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
F : Type u_9
inst : One M
inst_1 : One N
inst_2 : FunLike F M N
inst_3 : OneHomClass F M N
f : F
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : M
⊢ Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N) ↔ x = 1

Tactic:
hf.eq_iff' (map_one f)

Premises used: Function.Injective.eq_iff', map_one
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
R : Type u_10
S : Type u_11
F : Type u_12
inst : One R
inst_1 : One S
inst_2 : FunLike F R S
inst_3 : OneHomClass F R S
f : F
hf : Injective.{u_10 + 1, u_11 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R
⊢ Ne.{u_11 + 1} (α := S) ((f : (a : R) → S) x : S) (1 : S) ↔ x ≠ 1

Tactic:
(map_eq_one_iff f hf).not

Premises used: Iff.not, map_eq_one_iff
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
R : Type u_10
S : Type u_11
F : Type u_12
inst : One R
inst_1 : One S
inst_2 : FunLike F R S
inst_3 : OneHomClass F R S
f : F
x : R
hx rwa rwa₁ rwa₂ rwa₃ : Ne.{u_11 + 1} (α := S) ((f : (a : R) → S) x : S) (1 : S)
⊢ Ne.{u_11 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) 1 : S)

Tactic:
rwa [(map_one f)]

Premises used: map_one
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
F : Type u_9
inst : One M
inst_1 : One N
inst_2 : FunLike F M N
inst_3 : OneHomClass F M N
f : F
⊢ 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:
ι : 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 g : M →ₙ* N
h : f.toFun = g.toFun
mk :
  ∀ (toFun : M → N) (map_mul' : ∀ (x y : M), toFun (x * y) = toFun x * toFun y)
    (h : { toFun := toFun, map_mul' := map_mul' : M →ₙ* N }.toFun = g.toFun),
    { toFun := toFun, map_mul' := map_mul' : M →ₙ* N } = g
⊢ f = g

Tactic:
cases f
-- 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
g : M →ₙ* N
toFun : M → N
map_mul' : ∀ (x y : M), toFun (x * y) = toFun x * toFun y
h : { toFun := toFun, map_mul' := map_mul' : M →ₙ* N }.toFun = g.toFun
mk :
  ∀ (toFun_1 : M → N) (map_mul'_1 : ∀ (x y : M), toFun_1 (x * y) = toFun_1 x * toFun_1 y)
    (h :
      { toFun := toFun, map_mul' := map_mul' : M →ₙ* N }.toFun =
        { toFun := toFun_1, map_mul' := map_mul'_1 : M →ₙ* N }.toFun),
    { toFun := toFun, map_mul' := map_mul' : M →ₙ* N } = { toFun := toFun_1, map_mul' := map_mul'_1 }
⊢ { toFun := toFun, map_mul' := map_mul' : M →ₙ* N } = g

Tactic:
cases g
-- 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
toFun : M → N
map_mul' : ∀ (x y : M), toFun (x * y) = toFun x * toFun y
toFun_1 : M → N
map_mul'_1 : ∀ (x y : M), toFun_1 (x * y) = toFun_1 x * toFun_1 y
h :
  { toFun := toFun, map_mul' := map_mul' : M →ₙ* N }.toFun =
    { toFun := toFun_1, map_mul' := map_mul'_1 : M →ₙ* N }.toFun
⊢ { toFun := toFun, map_mul' := map_mul' : M →ₙ* N } = { toFun := toFun_1, map_mul' := map_mul'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
F : Type u_9
inst : Mul M
inst_1 : Mul N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
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)

Tactic:
MulHomClass.map_mul f x y

Premises used: MulHomClass.map_mul
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
F : Type u_9
inst : Mul M
inst_1 : Mul N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
g h : ι → M
h₁ :
  ∀ (x : ι),
    ((⇑f : (a : M) → N) ∘ (g * h)) x =
      HMul.hMul (α := ι → N) (β := ι → N) ((⇑f : (a : M) → N) ∘ g) ((⇑f : (a : M) → N) ∘ h) x
⊢ (⇑f : (a : M) → N) ∘ (g * h) = HMul.hMul (α := ι → N) ((⇑f : (a : M) → N) ∘ g) ((⇑f : (a : M) → N) ∘ h)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
F : Type u_9
inst : Mul M
inst_1 : Mul N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
g h : ι → M
x : ι
⊢ ((⇑f : (a : M) → N) ∘ (g * h)) x =
    HMul.hMul (α := ι → N) (β := ι → N) ((⇑f : (a : M) → N) ∘ g) ((⇑f : (a : M) → N) ∘ h) x

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Hom.Defs
Goal:
M : Type u_4
N : Type u_5
F : Type u_9
inst : Mul M
inst_1 : Mul N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
⊢ Eq (α := (a : M) → N) (⇑(↑f : M →ₙ* N) : (a : M) → N) (⇑f : (a : M) → N)

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 : MulOne M
inst_1 : MulOne N
f g : M →* N
h : Eq (α := (a : M) → N) ((fun (f : M →* N) ↦ f.toFun) f) ((fun (f : M →* N) ↦ f.toFun) g)
mk :
  ∀ (toOneHom : OneHom M N) (map_mul' : ∀ (x y : M), toOneHom.toFun (x * y) = toOneHom.toFun x * toOneHom.toFun y)
    (h :
      Eq (α := (a : M) → N) ((fun (f : M →* N) ↦ f.toFun) { toOneHom := toOneHom, map_mul' := map_mul' })
        ((fun (f : M →* N) ↦ f.toFun) g)),
    { toOneHom := toOneHom, map_mul' := map_mul' : M →* N } = g
⊢ f = g

Tactic:
cases f
-- 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
g : M →* N
toOneHom : OneHom M N
map_mul' : ∀ (x y : M), toOneHom.toFun (x * y) = toOneHom.toFun x * toOneHom.toFun y
h :
  Eq (α := (a : M) → N) ((fun (f : M →* N) ↦ f.toFun) { toOneHom := toOneHom, map_mul' := map_mul' })
    ((fun (f : M →* N) ↦ f.toFun) g)
mk :
  ∀ (toOneHom_1 : OneHom M N)
    (map_mul'_1 : ∀ (x y : M), toOneHom_1.toFun (x * y) = toOneHom_1.toFun x * toOneHom_1.toFun y)
    (h :
      Eq (α := (a : M) → N) ((fun (f : M →* N) ↦ f.toFun) { toOneHom := toOneHom, map_mul' := map_mul' })
        ((fun (f : M →* N) ↦ f.toFun) { toOneHom := toOneHom_1, map_mul' := map_mul'_1 })),
    { toOneHom := toOneHom, map_mul' := map_mul' : M →* N } = { toOneHom := toOneHom_1, map_mul' := map_mul'_1 }
⊢ { toOneHom := toOneHom, map_mul' := map_mul' : M →* N } = g

Tactic:
cases g
-- 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
toOneHom : OneHom M N
map_mul' : ∀ (x y : M), toOneHom.toFun (x * y) = toOneHom.toFun x * toOneHom.toFun y
toOneHom_1 : OneHom M N
map_mul'_1 : ∀ (x y : M), toOneHom_1.toFun (x * y) = toOneHom_1.toFun x * toOneHom_1.toFun y
h :
  Eq (α := (a : M) → N) ((fun (f : M →* N) ↦ f.toFun) { toOneHom := toOneHom, map_mul' := map_mul' })
    ((fun (f : M →* N) ↦ f.toFun) { toOneHom := toOneHom_1, map_mul' := map_mul'_1 })
mk : toOneHom = toOneHom_1
⊢ { toOneHom := toOneHom, map_mul' := map_mul' : M →* N } = { toOneHom := toOneHom_1, map_mul' := map_mul'_1 }

Tactic:
congr
-- 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
toOneHom : OneHom M N
map_mul' : ∀ (x y : M), toOneHom.toFun (x * y) = toOneHom.toFun x * toOneHom.toFun y
toOneHom_1 : OneHom M N
map_mul'_1 : ∀ (x y : M), toOneHom_1.toFun (x * y) = toOneHom_1.toFun x * toOneHom_1.toFun y
h :
  Eq (α := (a : M) → N) ((fun (f : M →* N) ↦ f.toFun) { toOneHom := toOneHom, map_mul' := map_mul' })
    ((fun (f : M →* N) ↦ f.toFun) { toOneHom := toOneHom_1, map_mul' := map_mul'_1 })
mk : Eq (α := (a : M) → N) (⇑toOneHom : (a : M) → N) (⇑toOneHom_1 : (a : M) → N)
⊢ toOneHom = toOneHom_1

Tactic:
apply DFunLike.coe_injective'

Premises used: DFunLike.coe_injective'
-- 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
toOneHom : OneHom M N
map_mul' : ∀ (x y : M), toOneHom.toFun (x * y) = toOneHom.toFun x * toOneHom.toFun y
toOneHom_1 : OneHom M N
map_mul'_1 : ∀ (x y : M), toOneHom_1.toFun (x * y) = toOneHom_1.toFun x * toOneHom_1.toFun y
h :
  Eq (α := (a : M) → N) ((fun (f : M →* N) ↦ f.toFun) { toOneHom := toOneHom, map_mul' := map_mul' })
    ((fun (f : M →* N) ↦ f.toFun) { toOneHom := toOneHom_1, map_mul' := map_mul'_1 })
⊢ Eq (α := (a : M) → N) (⇑toOneHom : (a : M) → N) (⇑toOneHom_1 : (a : M) → N)

Tactic:
h
-- 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
toOneHom : OneHom M N
map_mul' : ∀ (x y : M), toOneHom.toFun (x * y) = toOneHom.toFun x * toOneHom.toFun y
toOneHom_1 : OneHom M N
map_mul'_1 : ∀ (x y : M), toOneHom_1.toFun (x * y) = toOneHom_1.toFun x * toOneHom_1.toFun y
h :
  Eq (α := (a : M) → N) ((fun (f : M →* N) ↦ f.toFun) { toOneHom := toOneHom, map_mul' := map_mul' })
    ((fun (f : M →* N) ↦ f.toFun) { toOneHom := toOneHom_1, map_mul' := map_mul'_1 })
⊢ Eq (α := (a : M) → N) (⇑toOneHom : (a : M) → N) (⇑toOneHom_1 : (a : M) → N)

Tactic:
exact h
-- 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 : Subsingleton M
⊢ Subsingleton (M →* N)

Tactic:
.of_oneHomClass

Premises used: Subsingleton.of_oneHomClass
-- 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
⊢ Eq (α := (a : M) → N) (⇑(↑f : M →* N) : (a : M) → N) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl