awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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
⊢ (⇑f : (a : G) → H) ∘ (g / h) = HDiv.hDiv (α := ι → H) ((⇑f : (a : G) → H) ∘ g) ((⇑f : (a : G) → H) ∘ h)
have h₁ : ∀ (x : ι),
  ((⇑f : (a : G) → H) ∘ (g / h)) x =
    HDiv.hDiv (α := ι → H) (β := ι → H) ((⇑f : (a : G) → H) ∘ g) ((⇑f : (a : G) → H) ∘ h) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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
⊢ Eq (α := ι → H) ((⇑f : (a : G) → H) ∘ g⁻¹) ((⇑f : (a : G) → H) ∘ g)⁻¹
have h : ∀ (x : ι), Eq.{u_8 + 1} (α := H) (((⇑f : (a : G) → H) ∘ g⁻¹) x : H) (((⇑f : (a : G) → H) ∘ g)⁻¹ x : H)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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⁻¹) = HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a : H) (((f : (a : G) → H) b)⁻¹ : H)
have 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)
Tactic: rw [map_mul, map_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ (f : (a : G) → H) (a * b⁻¹) = HMul.hMul (α := H) (β := H) ((f : (a : G) → H) a : H) (((f : (a : G) → H) b)⁻¹ : H)
have 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)
Tactic: rw [map_mul, map_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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) = HDiv.hDiv (α := ι → H) ((⇑f : (a : G) → H) ∘ g) ((⇑f : (a : G) → H) ∘ h)
have h₁ : ∀ (x : ι),
  ((⇑f : (a : G) → H) ∘ (g / h)) x =
    HDiv.hDiv (α := ι → H) (β := ι → H) ((⇑f : (a : G) → H) ∘ g) ((⇑f : (a : G) → H) ∘ h) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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
⊢ (f : (a : G) → H) (HPow.hPow (β := ℕ) a 0) = HPow.hPow (α := H) (β := ℕ) ((f : (a : G) → H) a : H) 0
have rw : (f : (a : G) → H) 1 = HPow.hPow (α := H) (β := ℕ) ((f : (a : G) → H) a : H) 0
Tactic: rw [pow_zero, pow_zero, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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
⊢ (f : (a : G) → H) (HPow.hPow (β := ℕ) a 0) = HPow.hPow (α := H) (β := ℕ) ((f : (a : G) → H) a : H) 0
have rw₁ : Eq.{u_8 + 1} (α := H) ((f : (a : G) → H) 1 : H) (1 : H)
Tactic: rw [pow_zero, pow_zero, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ (f : (a : G) → H) (HPow.hPow (β := ℕ) a 0) = HPow.hPow (α := H) (β := ℕ) ((f : (a : G) → H) a : H) 0
have rw₂ : Eq.{u_8 + 1} (α := H) 1 1
Tactic: rw [pow_zero, pow_zero, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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 : ℕ
⊢ (f : (a : G) → H) (a ^ (n + 1)) = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (n + 1)
have rw : (f : (a : G) → H) (a ^ n * a) = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (n + 1)
Tactic: rw [pow_succ, pow_succ, map_mul, map_pow f a n]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ (f : (a : G) → H) (a ^ (n + 1)) = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (n + 1)
have 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)
Tactic: rw [pow_succ, pow_succ, map_mul, map_pow f a n]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ (f : (a : G) → H) (a ^ (n + 1)) = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (n + 1)
have 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)
Tactic: rw [pow_succ, pow_succ, map_mul, map_pow f a n]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ (f : (a : G) → H) (a ^ (n + 1)) = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (n + 1)
have 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)
Tactic: rw [pow_succ, pow_succ, map_mul, map_pow f a n]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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 : ℕ
⊢ (⇑f : (a : G) → H) ∘ (g ^ n) = HPow.hPow (α := ι → H) ((⇑f : (a : G) → H) ∘ g) n
have h : ∀ (x : ι), ((⇑f : (a : G) → H) ∘ (g ^ n)) x = HPow.hPow (α := ι → H) ((⇑f : (a : G) → H) ∘ g) n x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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 : ℕ
⊢ (f : (a : G) → H) (HPow.hPow (β := ℤ) a (↑n : ℤ)) = HPow.hPow (α := H) (β := ℤ) ((f : (a : G) → H) a : H) (↑n : ℤ)
have rw : (f : (a : G) → H) (a ^ n) = HPow.hPow (α := H) (β := ℤ) ((f : (a : G) → H) a : H) (↑n : ℤ)
Tactic: rw [zpow_natCast, map_pow, zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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 : ℤ)
⊢ (f : (a : G) → H) (HPow.hPow (β := ℤ) a (↑n : ℤ)) = HPow.hPow (α := H) (β := ℤ) ((f : (a : G) → H) a : H) (↑n : ℤ)
have rw₁ : HPow.hPow (α := H) ((f : (a : G) → H) a : H) n = HPow.hPow (α := H) (β := ℤ) ((f : (a : G) → H) a : H) (↑n : ℤ)
Tactic: rw [zpow_natCast, map_pow, zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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 : ℤ)
⊢ (f : (a : G) → H) (HPow.hPow (β := ℤ) a (↑n : ℤ)) = HPow.hPow (α := H) (β := ℤ) ((f : (a : G) → H) a : H) (↑n : ℤ)
have rw₂ : HPow.hPow (α := H) ((f : (a : G) → H) a : H) n = HPow.hPow (α := H) ((f : (a : G) → H) a : H) n
Tactic: rw [zpow_natCast, map_pow, zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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 : ℕ
⊢ (f : (a : G) → H) (a ^ Int.negSucc n) = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (Int.negSucc n)
have rw : (f : (a : G) → H) (a ^ (n + 1))⁻¹ = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (Int.negSucc n)
Tactic: rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ (f : (a : G) → H) (a ^ Int.negSucc n) = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (Int.negSucc n)
have rw₁ : ((f : (a : G) → H) (a ^ (n + 1)))⁻¹ = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (Int.negSucc n)
Tactic: rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ (f : (a : G) → H) (a ^ Int.negSucc n) = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (Int.negSucc n)
have rw₂ : (HPow.hPow (α := H) ((f : (a : G) → H) a : H) (n + 1))⁻¹ = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (Int.negSucc n)
Tactic: rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ (f : (a : G) → H) (a ^ Int.negSucc n) = HPow.hPow (α := H) ((f : (a : G) → H) a : H) (Int.negSucc n)
have 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)
Tactic: rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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 : ℤ
⊢ (⇑f : (a : G) → H) ∘ (g ^ n) = HPow.hPow (α := ι → H) ((⇑f : (a : G) → H) ∘ g) n
have h : ∀ (x : ι), ((⇑f : (a : G) → H) ∘ (g ^ n)) x = HPow.hPow (α := ι → H) ((⇑f : (a : G) → H) ∘ g) n 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 : Group G
inst_1 : MulOneClass M
f : M → G
map_mul : ∀ (a b : M), f (a * b) = f a * f b
⊢ f 1 = 1
have rw : f 1 * f 1 = 1 * f 1
Tactic: rw [← mul_right_cancel_iff, ← map_mul _ 1, one_mul, one_mul]
-- 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 : 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
⊢ f 1 = 1
have rw₁ : G
Tactic: rw [← mul_right_cancel_iff, ← map_mul _ 1, one_mul, one_mul]
-- 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 : 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
⊢ f 1 = 1
have rw₂ : f (HMul.hMul (α := M) 1 1) = 1 * f 1
Tactic: rw [← mul_right_cancel_iff, ← map_mul _ 1, one_mul, one_mul]
-- 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 : 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
⊢ f 1 = 1
have rw₃ : f 1 = 1 * f 1
Tactic: rw [← mul_right_cancel_iff, ← map_mul _ 1, one_mul, one_mul]
-- 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 : 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
⊢ f 1 = 1
have rw₄ : f 1 = f 1
Tactic: rw [← mul_right_cancel_iff, ← map_mul _ 1, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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
⊢ 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)
have 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)
Tactic: rw [← OneHom.comp_apply, h, OneHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← OneHom.comp_apply, h, OneHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← OneHom.comp_apply, h, OneHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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
⊢ 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)
have 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)
Tactic: rw [← MulHom.comp_apply, h, MulHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← MulHom.comp_apply, h, MulHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← MulHom.comp_apply, h, MulHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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
⊢ 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)
have 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)
Tactic: rw [← MonoidHom.comp_apply, h, MonoidHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← MonoidHom.comp_apply, h, MonoidHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Hom.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← MonoidHom.comp_apply, h, MonoidHom.comp_apply]
-- 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 : OneHom M N
g : N → M
h₁ : LeftInverse g (⇑f : (a : M) → N)
⊢ g 1 = 1
have rw : g ((f : (a : M) → N) 1) = 1
Tactic: rw [← f.map_one, 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
f : OneHom M N
g : N → M
h₁ : LeftInverse g (⇑f : (a : M) → N)
rw : g ((f : (a : M) → N) 1) = 1
⊢ g 1 = 1
have rw₁ : Eq.{u_4 + 1} (α := M) 1 1
Tactic: rw [← f.map_one, 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 : M →ₙ* N
g : N → M
h₁ : LeftInverse g (⇑f : (a : M) → N)
h₂ : RightInverse g (⇑f : (a : M) → N)
x y : N
⊢ g (x * y) = g (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (g x) : N) ((f : (a : M) → N) (g y) : N))
have rw : g (x * y) = g (HMul.hMul (β := N) x ((f : (a : M) → N) (g y) : N))
Tactic: rw [h₂ x, h₂ y]
-- 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 : 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))
⊢ g (x * y) = g (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (g x) : N) ((f : (a : M) → N) (g y) : N))
have rw₁ : g (x * y) = g (x * y)
Tactic: rw [h₂ x, h₂ y]
-- 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 : M →ₙ* N
g : N → M
h₁ : LeftInverse g (⇑f : (a : M) → N)
h₂ : RightInverse g (⇑f : (a : M) → N)
x 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))
have 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))
Tactic: rw [f.map_mul]