awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MulDistribMulAction R M
inst_4 : MulDistribMulAction R N
x : R
⊢ HSMul.hSMul (β := M × N) x 1 = 1
have fst : (HSMul.hSMul (β := M × N) x 1).1 = 1.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MulDistribMulAction R M
inst_4 : MulDistribMulAction R N
x : R
fst : (HSMul.hSMul (β := M × N) x 1).1 = 1.1
⊢ HSMul.hSMul (β := M × N) x 1 = 1
have snd : (HSMul.hSMul (β := M × N) x 1).2 = 1.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MulDistribMulAction R M
inst_4 : MulDistribMulAction R N
x : R
x_1 x_2 : M × N
⊢ x • (x_1 * x_2) = x • x_1 * x • x_2
have fst : (x • (x_1 * x_2)).1 = (x • x_1 * x • x_2).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Monoid R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : MulDistribMulAction R M
inst_4 : MulDistribMulAction R N
x : R
x_1 x_2 : M × N
fst : (x • (x_1 * x_2)).1 = (x • x_1 * x • x_2).1
⊢ x • (x_1 * x_2) = x • x_1 * x • x_2
have snd : (x • (x_1 * x_2)).2 = (x • x_1 * x • x_2).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Zero R
inst_1 : Zero M
inst_2 : Zero N
inst_3 : SMulWithZero R M
inst_4 : SMulWithZero R N
x : M × N
⊢ HSMul.hSMul (α := R) 0 x = 0
have fst : (HSMul.hSMul (α := R) 0 x).1 = 0.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst : Zero R
inst_1 : Zero M
inst_2 : Zero N
inst_3 : SMulWithZero R M
inst_4 : SMulWithZero R N
x : M × N
fst : (HSMul.hSMul (α := R) 0 x).1 = 0.1
⊢ HSMul.hSMul (α := R) 0 x = 0
have snd : (HSMul.hSMul (α := R) 0 x).2 = 0.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
inst_3 : DistribMulAction M α
inst_4 : DistribMulAction N α
inst_5 : SMulCommClass M N α
mn : M × N
⊢ HSMul.hSMul (β := α) mn 0 = 0
have change : mn.1 • HSMul.hSMul (β := α) mn.2 0 = 0
Tactic: change mn.1 • mn.2 • 0 = (0 : α)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
inst_3 : DistribMulAction M α
inst_4 : DistribMulAction N α
inst_5 : SMulCommClass M N α
mn : M × N
⊢ mn.1 • HSMul.hSMul (β := α) mn.2 0 = 0
have rw : HSMul.hSMul (β := α) mn.1 0 = 0
Tactic: rw [smul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
inst_3 : DistribMulAction M α
inst_4 : DistribMulAction N α
inst_5 : SMulCommClass M N α
mn : M × N
rw : HSMul.hSMul (β := α) mn.1 0 = 0
⊢ mn.1 • HSMul.hSMul (β := α) mn.2 0 = 0
have rw₁ : Eq.{u_3 + 1} (α := α) 0 0
Tactic: rw [smul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
inst_3 : DistribMulAction M α
inst_4 : DistribMulAction N α
inst_5 : SMulCommClass M N α
mn : M × N
a a' : α
⊢ mn • (a + a') = mn • a + mn • a'
have change : mn.1 • mn.2 • (a + a') = mn • a + mn • a'
Tactic: change mn.1 • mn.2 • _ = (_ : α)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
inst_3 : DistribMulAction M α
inst_4 : DistribMulAction N α
inst_5 : SMulCommClass M N α
mn : M × N
a a' : α
⊢ mn.1 • mn.2 • (a + a') = mn • a + mn • a'
have rw : mn.1 • mn.2 • a + mn.1 • mn.2 • a' = mn • a + mn • a'
Tactic: rw [smul_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
x : DistribMulAction (M × N) α
⊢ prodOfSMulCommClass M N α = x
have smul : ∀ (m : M) (n : N) (a : α), SMul.smul (m, n) a = SMul.smul (m, n) a
Tactic: ext ⟨m, n⟩ a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
x : DistribMulAction (M × N) α
m : M
n : N
a : α
⊢ SMul.smul (m, n) a = SMul.smul (m, n) a
have smul : HSMul.hSMul (α := M × N) (m, 1) (HSMul.hSMul (α := M × N) (1, n) a) = SMul.smul (m, n) a
Tactic: change (m, (1 : N)) • ((1 : M), n) • a = _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
x : DistribMulAction (M × N) α
m : M
n : N
a : α
⊢ HSMul.hSMul (α := M × N) (m, 1) (HSMul.hSMul (α := M × N) (1, n) a) = SMul.smul (m, n) a
have smul : (m, n) • a = SMul.smul (m, n) a
Tactic: rw [smul_smul, Prod.mk_mul_mk, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
⊢ Eq (α := (x : DistribMulAction M α) ×' (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : DistribMulAction M α) ↦ (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
      (compHom (M := M × N) α (MonoidHom.inl M N))
      (PSigma.mk (β := fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
        (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯))
    (PSigma.mk (β := fun (x : DistribMulAction M α) ↦ (x_1 : DistribMulAction N α) ×' SMulCommClass M N α) fst
      (PSigma.mk (β := fun (x : DistribMulAction N α) ↦ SMulCommClass M N α) x snd))
have h : compHom (M := M × N) α (MonoidHom.inl M N) = fst
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
h : compHom (M := M × N) α (MonoidHom.inl M N) = fst
⊢ Eq (α := (x : DistribMulAction M α) ×' (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : DistribMulAction M α) ↦ (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
      (compHom (M := M × N) α (MonoidHom.inl M N))
      (PSigma.mk (β := fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
        (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯))
    (PSigma.mk (β := fun (x : DistribMulAction M α) ↦ (x_1 : DistribMulAction N α) ×' SMulCommClass M N α) fst
      (PSigma.mk (β := fun (x : DistribMulAction N α) ↦ SMulCommClass M N α) x snd))
have h₁ : HEq (α := (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
  (PSigma.mk (β := fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α) (compHom (M := M × N) α (MonoidHom.inr M N))
      sorry :
    (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
  (β := (x : DistribMulAction N α) ×' SMulCommClass M N α)
  (PSigma.mk (β := fun (x : DistribMulAction N α) ↦ SMulCommClass M N α) x snd)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
⊢ compHom (M := M × N) α (MonoidHom.inl M N) = fst
have h : ∀ (m : M) (a : α), SMul.smul m a = SMul.smul m a
Tactic: ext m a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
m : M
a : α
| SMul.smul m a
have rw : SMul.smul m (HSMul.hSMul.{u_2, u_3, u_3} (α := N) 1 a)
Tactic: rw [← one_smul N a]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m a
have h : SMul.smul m a = SMul.smul m (HSMul.hSMul.{u_2, u_3, u_3} (α := N) 1 a)
Tactic: conv_rhs => rw [← one_smul N a]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
⊢ HEq (α := (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
        (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯ :
      (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
    (β := (x : DistribMulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : DistribMulAction N α) ↦ SMulCommClass M N α) x snd)
have h : Eq (α := DistribMulAction N α → Prop) (fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
  fun (x : DistribMulAction N α) ↦ SMulCommClass M N α
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
h :
  Eq (α := DistribMulAction N α → Prop) (fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
    fun (x : DistribMulAction N α) ↦ SMulCommClass M N α
⊢ HEq (α := (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
        (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯ :
      (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
    (β := (x : DistribMulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : DistribMulAction N α) ↦ SMulCommClass M N α) x snd)
have h₁ : compHom (M := M × N) α (MonoidHom.inr M N) = x
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
h :
  Eq (α := DistribMulAction N α → Prop) (fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
    fun (x : DistribMulAction N α) ↦ SMulCommClass M N α
h₁ : compHom (M := M × N) α (MonoidHom.inr M N) = x
⊢ HEq (α := (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
        (compHom (M := M × N) α (MonoidHom.inr M N)) ⋯ :
      (x_1 : DistribMulAction N α) ×' SMulCommClass M N α)
    (β := (x : DistribMulAction N α) ×' SMulCommClass M N α)
    (PSigma.mk (β := fun (x : DistribMulAction N α) ↦ SMulCommClass M N α) x snd)
have h₂ : HEq (α := SMulCommClass M N α) sorry snd
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
⊢ Eq (α := DistribMulAction N α → Prop) (fun (x_1 : DistribMulAction N α) ↦ SMulCommClass M N α)
    fun (x : DistribMulAction N α) ↦ SMulCommClass M N α
have h : ∀ (i : DistribMulAction N α), SMulCommClass M N α = SMulCommClass M N α
Tactic: funext i
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
i : DistribMulAction N α
⊢ SMulCommClass M N α = SMulCommClass M N α
have h : compHom (M := M × N) α (MonoidHom.inl M N) = fst
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
i : DistribMulAction N α
⊢ compHom (M := M × N) α (MonoidHom.inl M N) = fst
have h : ∀ (m : M) (a : α), SMul.smul m a = SMul.smul m a
Tactic: ext m a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
⊢ compHom (M := M × N) α (MonoidHom.inr M N) = x
have h : ∀ (n : N) (a : α), SMul.smul n a = SMul.smul n a
Tactic: ext n a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
n : N
a : α
| SMul.smul n a
have rw : HSMul.hSMul.{u_1, u_3, u_3} (α := M) 1 (SMul.smul n a)
Tactic: rw [← one_smul M (SMul.smul n a)]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Prod (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : AddMonoid α
fst : DistribMulAction M α
x : DistribMulAction N α
snd : SMulCommClass M N α
n : N
a : α
⊢ SMul.smul n a = SMul.smul n a
have h : SMul.smul n a = HSMul.hSMul.{u_1, u_3, u_3} (α := M) 1 (SMul.smul n a)
Tactic: conv_rhs => rw [← one_smul M (SMul.smul n a)]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
x : M
u : Mˣ
⊢ x * (↑u : M) * (↑u⁻¹ : M) = x
have rw : x * ((↑u : M) * (↑u⁻¹ : M)) = x
Tactic: rw [mul_assoc, Units.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
x : M
u : Mˣ
rw : x * ((↑u : M) * (↑u⁻¹ : M)) = x
⊢ x * (↑u : M) * (↑u⁻¹ : M) = x
have rw₁ : x * 1 = x
Tactic: rw [mul_assoc, Units.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
x : M
u : Mˣ
rw : x * ((↑u : M) * (↑u⁻¹ : M)) = x
rw₁ : x * 1 = x
⊢ x * (↑u : M) * (↑u⁻¹ : M) = x
have rw₂ : x = x
Tactic: rw [mul_assoc, Units.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
x : M
u v : Mˣ
⊢ x * (↑(u * v) : M) = x * (↑u : M) * (↑v : M)
have rw : x * ((↑u : M) * (↑v : M)) = x * (↑u : M) * (↑v : M)
Tactic: rw [Units.val_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
x : M
u v : Mˣ
rw : x * ((↑u : M) * (↑v : M)) = x * (↑u : M) * (↑v : M)
⊢ x * (↑(u * v) : M) = x * (↑u : M) * (↑v : M)
have rw₁ : x * ((↑u : M) * (↑v : M)) = x * ((↑u : M) * (↑v : M))
Tactic: rw [Units.val_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_2
N : Type u_3
inst : Monoid M
inst_1 : Monoid N
F : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
x y : M
ha : x ~ᵤ y
⊢ Associated.{u_3} (M := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
have obtain : ∀ (u : Mˣ) (ha : x * (↑u : M) = y), Associated.{u_3} (M := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
Tactic: obtain ⟨u, ha⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_2
N : Type u_3
inst : Monoid M
inst_1 : Monoid N
F : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
x y : M
u : Mˣ
ha : x * (↑u : M) = y
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
      ((↑(((Units.map (↑f : M →* N) : MonoidHom.{u_2, u_3} Mˣ Nˣ) : (a : Mˣ) → Nˣ) u) : N) : N) =
    (f : (a : M) → N) y
have rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
    ((↑(((Units.map (↑f : M →* N) : MonoidHom.{u_2, u_3} Mˣ Nˣ) : (a : Mˣ) → Nˣ) u) : N) : N) =
  (f : (a : M) → N) (x * (↑u : M))
Tactic: rw [← ha, map_mul, Units.coe_map, MonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_2
N : Type u_3
inst : Monoid M
inst_1 : Monoid N
F : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
x y : M
u : Mˣ
ha : x * (↑u : M) = y
rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
      ((↑(((Units.map (↑f : M →* N) : MonoidHom.{u_2, u_3} Mˣ Nˣ) : (a : Mˣ) → Nˣ) u) : N) : N) =
    (f : (a : M) → N) (x * (↑u : M))
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
      ((↑(((Units.map (↑f : M →* N) : MonoidHom.{u_2, u_3} Mˣ Nˣ) : (a : Mˣ) → Nˣ) u) : N) : N) =
    (f : (a : M) → N) y
have rw₁ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
    ((↑(((Units.map (↑f : M →* N) : MonoidHom.{u_2, u_3} Mˣ Nˣ) : (a : Mˣ) → Nˣ) u) : N) : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑u : M) : N)
Tactic: rw [← ha, map_mul, Units.coe_map, MonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_2
N : Type u_3
inst : Monoid M
inst_1 : Monoid N
F : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
x y : M
u : Mˣ
ha : x * (↑u : M) = y
rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
      ((↑(((Units.map (↑f : M →* N) : MonoidHom.{u_2, u_3} Mˣ Nˣ) : (a : Mˣ) → Nˣ) u) : N) : N) =
    (f : (a : M) → N) (x * (↑u : M))
rw₁ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
      ((↑(((Units.map (↑f : M →* N) : MonoidHom.{u_2, u_3} Mˣ Nˣ) : (a : Mˣ) → Nˣ) u) : N) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑u : M) : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
      ((↑(((Units.map (↑f : M →* N) : MonoidHom.{u_2, u_3} Mˣ Nˣ) : (a : Mˣ) → Nˣ) u) : N) : N) =
    (f : (a : M) → N) y
have rw₂ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) (((↑f : M →* N) : (a : M) → N) (↑u : M) : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑u : M) : N)
Tactic: rw [← ha, map_mul, Units.coe_map, MonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_2
N : Type u_3
inst : Monoid M
inst_1 : Monoid N
F : Type u_4
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
x y : M
u : Mˣ
ha : x * (↑u : M) = y
rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
      ((↑(((Units.map (↑f : M →* N) : MonoidHom.{u_2, u_3} Mˣ Nˣ) : (a : Mˣ) → Nˣ) u) : N) : N) =
    (f : (a : M) → N) (x * (↑u : M))
rw₁ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
      ((↑(((Units.map (↑f : M →* N) : MonoidHom.{u_2, u_3} Mˣ Nˣ) : (a : Mˣ) → Nˣ) u) : N) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑u : M) : N)
rw₂ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) (((↑f : M →* N) : (a : M) → N) (↑u : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑u : M) : N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N)
      ((↑(((Units.map (↑f : M →* N) : MonoidHom.{u_2, u_3} Mˣ Nˣ) : (a : Mˣ) → Nˣ) u) : N) : N) =
    (f : (a : M) → N) y
have rw₃ : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑u : M) : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑u : M) : N)
Tactic: rw [← ha, map_mul, Units.coe_map, MonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
a b : M
h : a = b
⊢ a * (↑1 : M) = b
have rwa : a * 1 = b
Tactic: rwa [Units.val_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
a : M
h : a ~ᵤ 0
⊢ a = 0
have let : ∀ (u : Mˣ) (h : 0 * (↑u : M) = a), a = 0
Tactic: let ⟨u, h⟩ := h.symm
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
N : Type u_2
inst : CommMonoid N
a u : N
hu : IsUnit u
⊢ u * a ~ᵤ a
have rw : a * u ~ᵤ a
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
N : Type u_2
inst : CommMonoid N
u a b : N
hu : IsUnit u
⊢ u * a ~ᵤ b ↔ a ~ᵤ b
have rw : a * u ~ᵤ b ↔ a ~ᵤ b
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
a b c : M
h : b ~ᵤ c
⊢ a * b ~ᵤ a * c
have obtain : ∀ (d : Mˣ), a * b ~ᵤ a * (b * (↑d : M))
Tactic: obtain ⟨d, rfl⟩ := h
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
h : a ~ᵤ b
c : M
⊢ a * c ~ᵤ b * c
have obtain : ∀ (d : Mˣ), a * c ~ᵤ a * (↑d : M) * c
Tactic: obtain ⟨d, rfl⟩ := h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ a ^ (n + 1) ~ᵤ b ^ (n + 1)
have h₁ : a ^ (n + 1) = a * a ^ n
Tactic: convert! h.mul_mul ih
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
h₁ : a ^ (n + 1) = a * a ^ n
⊢ a ^ (n + 1) ~ᵤ b ^ (n + 1)
have h₂ : b ^ (n + 1) = b * b ^ n
Tactic: convert! h.mul_mul ih
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ a ^ (n + 1) = a * a ^ n
have h₁ : a * a ^ n = a * a ^ n
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ b ^ (n + 1) = b * b ^ n
have h₁ : b * b ^ n = b * b ^ n
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
n : ℕ
h : a ~ᵤ b
⊢ a ^ n ~ᵤ b ^ n
have zero : HPow.hPow (β := ℕ) a 0 ~ᵤ HPow.hPow (β := ℕ) b 0
Tactic: induction n with
  | zero => simp [Associated.refl]
  | succ n ih => convert! h.mul_mul ih <;> rw [pow_succ']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
n : ℕ
h : a ~ᵤ b
zero : HPow.hPow (β := ℕ) a 0 ~ᵤ HPow.hPow (β := ℕ) b 0
⊢ a ^ n ~ᵤ b ^ n
have succ : ∀ (n : ℕ) (ih : a ^ n ~ᵤ b ^ n), a ^ (n + 1) ~ᵤ b ^ (n + 1)
Tactic: induction n with
  | zero => simp [Associated.refl]
  | succ n ih => convert! h.mul_mul ih <;> rw [pow_succ']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a b : M
hab : a ∣ b
hba : b ∣ a
⊢ a ~ᵤ b
have rcases : ∀ (c : M) (hba : a * c ∣ a), a ~ᵤ a * c
Tactic: rcases hab with ⟨c, rfl⟩
Cleared hypotheses: b, hab, hba
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c : M
hba : a * c ∣ a
⊢ a ~ᵤ a * c
have rcases : ∀ (d : M) (a_eq : a = a * c * d), a ~ᵤ a * c
Tactic: rcases hba with ⟨d, a_eq⟩
Cleared hypotheses: hba
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
⊢ a ~ᵤ a * c
have pos : ∀ (ha0 : a = 0), a ~ᵤ a * c
Tactic: by_cases ha0 : a = 0