awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
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 : CommMonoid N
f g : M →* N
x y : M
rw :
  HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
      ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x * y) : N) ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
have rw₁ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) *
    HMul.hMul (α := N) (β := N) ((g : (a : M) → N) x : N) ((g : (a : M) → N) y : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
Tactic: rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
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 : CommMonoid N
f g : M →* N
x y : M
rw :
  HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
      ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
rw₁ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) *
      HMul.hMul (α := N) (β := N) ((g : (a : M) → N) x : N) ((g : (a : M) → N) y : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x * y) : N) ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
have rw₂ : HMul.hMul (β := N)
    (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
      ((g : (a : M) → N) x : N))
    ((g : (a : M) → N) y : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
Tactic: rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
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 : CommMonoid N
f g : M →* N
x y : M
rw :
  HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
      ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
rw₁ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) *
      HMul.hMul (α := N) (β := N) ((g : (a : M) → N) x : N) ((g : (a : M) → N) y : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
rw₂ :
  HMul.hMul (β := N)
      (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
        ((g : (a : M) → N) x : N))
      ((g : (a : M) → N) y : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x * y) : N) ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
have rw₃ : HMul.hMul (β := N)
    (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
      ((g : (a : M) → N) x : N))
    ((g : (a : M) → N) y : N) =
  HMul.hMul (β := N)
    (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N))
      ((f : (a : M) → N) y : N))
    ((g : (a : M) → N) y : N)
Tactic: rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
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 : CommMonoid N
f g : M →* N
x y : M
rw :
  HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
      ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
rw₁ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) *
      HMul.hMul (α := N) (β := N) ((g : (a : M) → N) x : N) ((g : (a : M) → N) y : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
rw₂ :
  HMul.hMul (β := N)
      (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
        ((g : (a : M) → N) x : N))
      ((g : (a : M) → N) y : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
rw₃ :
  HMul.hMul (β := N)
      (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))
        ((g : (a : M) → N) x : N))
      ((g : (a : M) → N) y : N) =
    HMul.hMul (β := N)
      (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N))
        ((f : (a : M) → N) y : N))
      ((g : (a : M) → N) y : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (x * y) : N) ((g : (a : M) → N) (x * y) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N) *
      HMul.hMul (α := N) (β := N) ((f : (a : M) → N) y : N) ((g : (a : M) → N) y : N)
have rw₄ : HMul.hMul (β := N)
    (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N))
      ((f : (a : M) → N) y : N))
    ((g : (a : M) → N) y : N) =
  HMul.hMul (β := N)
    (HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N))
      ((f : (a : M) → N) y : N))
    ((g : (a : M) → N) y : N)
Tactic: rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
Goal:
M : Type u_2
N : Type u_3
P : Type u_4
inst : MulOneClass M
inst_1 : CommMonoid N
inst_2 : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
have h : ∀ (x : M), Eq.{u_4 + 1} (α := P) ((g.comp (f₁ * f₂) : (a : M) → P) x : P) ((g.comp f₁ * g.comp f₂ : (a : M) → P) x : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
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)
⊢ (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)
have simp_rw₂ : ((f : (a : M) → G) (a * b))⁻¹ = (HMul.hMul (α := G) (β := G) ((f : (a : M) → G) a : G) ((f : (a : M) → G) b : G))⁻¹
Tactic: simp_rw [← mul_inv, f.map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
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
⊢ φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹
have h : ∀ (x : M), Eq.{u_6 + 1} (α := H) ((φ.comp ψ⁻¹ : (a : M) → H) x : H) (((φ.comp ψ)⁻¹ : (a : M) → H) x : H)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
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
⊢ f.comp (g / h) = f.comp g / f.comp h
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
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)
⊢ ∀ (a b : G), a * b = b * a
have simp_rw : ∀ (a b : G), Eq.{u_6 + 1} (α := H) ((f : (a : G) → H) (a * b) : H) ((f : (a : G) → H) (b * a) : H)
Tactic: simp_rw [← hf.eq_iff, map_mul, mul_comm, implies_true]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
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)
⊢ ∀ (a b : G), a * b = b * a
have 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)
Tactic: simp_rw [← hf.eq_iff, map_mul, mul_comm, implies_true]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
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)
⊢ ∀ (a b : G), a * b = b * a
have simp_rw₂ : ∀ (a b : G), True
Tactic: simp_rw [← hf.eq_iff, map_mul, mul_comm, implies_true]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
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)
⊢ ∀ (a b : H), a * b = b * a
have 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)
Tactic: simp_rw [hf.forall₂, ← map_mul, mul_comm, implies_true]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
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)
⊢ ∀ (a b : H), a * b = b * a
have simp_rw₁ : ∀ (x₁ x₂ : G), Eq.{u_6 + 1} (α := H) ((f : (a : G) → H) (x₁ * x₂) : H) ((f : (a : G) → H) (x₂ * x₁) : H)
Tactic: simp_rw [hf.forall₂, ← map_mul, mul_comm, implies_true]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Basic (goal)
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)
⊢ ∀ (a b : H), a * b = b * a
have simp_rw₂ : ∀ (x₁ x₂ : G), True
Tactic: simp_rw [hf.forall₂, ← map_mul, mul_comm, implies_true]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.CompTypeclasses (goal)
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)
⊢ σ = id M
have h₁ : ∀ (x : M), Eq (α := M) ((σ : (a : M) → M) x : M) ((id M : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.CompTypeclasses (goal)
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 ψ χ
⊢ Eq (α := M → P) (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := N) (⇑ψ : (a : N) → P) (⇑φ : (a : M) → N))
    (⇑χ : (a : M) → P)
have rw : Eq (α := M → P) (⇑(ψ.comp φ) : (a : M) → P) (⇑χ : (a : M) → P)
Tactic: rw [← MonoidHom.coe_comp, κ.comp_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.CompTypeclasses (goal)
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)
⊢ Eq (α := M → P) (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := N) (⇑ψ : (a : N) → P) (⇑φ : (a : M) → N))
    (⇑χ : (a : M) → P)
have rw₁ : Eq (α := M → P) (⇑χ : (a : M) → P) (⇑χ : (a : M) → P)
Tactic: rw [← MonoidHom.coe_comp, κ.comp_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.CompTypeclasses (goal)
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
⊢ Eq.{u_3 + 1} (α := P) ((ψ : (a : N) → P) ((φ : (a : M) → N) x : N) : P) ((χ : (a : M) → P) x : P)
have rw : Eq.{u_3 + 1} (α := P) ((ψ : (a : N) → P) ((φ : (a : M) → N) x : N) : P) ((ψ.comp φ : (a : M) → P) x : P)
Tactic: rw [← h.comp_eq, MonoidHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.CompTypeclasses (goal)
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)
⊢ Eq.{u_3 + 1} (α := P) ((ψ : (a : N) → P) ((φ : (a : M) → N) x : N) : P) ((χ : (a : M) → P) x : P)
have rw₁ : Eq.{u_3 + 1} (α := P) ((ψ : (a : N) → P) ((φ : (a : M) → N) x : N) : P)
  ((ψ : (a : N) → P) ((φ : (a : M) → N) x : N) : P)
Tactic: rw [← h.comp_eq, MonoidHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.CompTypeclasses (goal)
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
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃ ↔ φ₁₂.CompTriple φ₃ φ₁₂₃
have mp : φ₁.CompTriple φ₂₃ φ₁₂₃ → φ₁₂.CompTriple φ₃ φ₁₂₃
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.CompTypeclasses (goal)
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 φ₃ φ₁₂₃
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃ ↔ φ₁₂.CompTriple φ₃ φ₁₂₃
have mpr : φ₁₂.CompTriple φ₃ φ₁₂₃ → φ₁.CompTriple φ₂₃ φ₁₂₃
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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
⊢ f = g
have 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
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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
⊢ { toFun := toFun, map_one' := map_one' : OneHom M N } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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
⊢ f = g
have 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
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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
⊢ { toFun := toFun, map_mul' := map_mul' : M →ₙ* N } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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
⊢ (⇑f : (a : M) → N) ∘ (g * h) = HMul.hMul (α := ι → N) ((⇑f : (a : M) → N) ∘ g) ((⇑f : (a : M) → N) ∘ h)
have h₁ : ∀ (x : ι),
  ((⇑f : (a : M) → N) ∘ (g * h)) x =
    HMul.hMul (α := ι → N) (β := ι → N) ((⇑f : (a : M) → N) ∘ g) ((⇑f : (a : M) → N) ∘ h) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ f = g
have 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
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ { toOneHom := toOneHom, map_mul' := map_mul' : M →* N } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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 })
⊢ { toOneHom := toOneHom, map_mul' := map_mul' : M →* N } = { toOneHom := toOneHom_1, map_mul' := map_mul'_1 }
have mk : toOneHom = toOneHom_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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 })
⊢ toOneHom = toOneHom_1
have mk : Eq (α := (a : M) → N) (⇑toOneHom : (a : M) → N) (⇑toOneHom_1 : (a : M) → N)
Tactic: apply DFunLike.coe_injective'
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) = 1
have rw : Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) (a * b) : N) (1 : N)
Tactic: rw [← map_mul, h, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) = 1
have rw₁ : Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) 1 : N) (1 : N)
Tactic: rw [← map_mul, h, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) = 1
have rw₂ : Eq.{u_5 + 1} (α := N) 1 1
Tactic: rw [← map_mul, h, map_one]