awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : Zero A
inst_1 : SMulZeroClass M A
inst_2 : Zero B
inst_3 : SMul M B
f : ZeroHom A B
smul : ∀ (c : M) (x : A), (f : (a : A) → B) (c • x) = HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B)
c : M
⊢ HSMul.hSMul (β := B) c 0 = 0
have rw : HSMul.hSMul (β := B) c ((f : (a : A) → B) 0 : B) = (f : (a : A) → B) 0
Tactic: rw [← map_zero f, ← smul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : Zero A
inst_1 : SMulZeroClass M A
inst_2 : Zero B
inst_3 : SMul M B
f : ZeroHom A B
smul : ∀ (c : M) (x : A), (f : (a : A) → B) (c • x) = HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B)
c : M
rw : HSMul.hSMul (β := B) c ((f : (a : A) → B) 0 : B) = (f : (a : A) → B) 0
⊢ HSMul.hSMul (β := B) c 0 = 0
have rw₁ : Eq.{u_9 + 1} (α := B) ((f : (a : A) → B) (HSMul.hSMul (β := A) c 0) : B) ((f : (a : A) → B) 0 : B)
Tactic: rw [← map_zero f, ← smul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : Zero A
inst_1 : SMulZeroClass M A
inst_2 : Zero B
inst_3 : SMul M B
f : ZeroHom A B
smul : ∀ (c : M) (x : A), (f : (a : A) → B) (c • x) = HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B)
c : M
rw : HSMul.hSMul (β := B) c ((f : (a : A) → B) 0 : B) = (f : (a : A) → B) 0
rw₁ : Eq.{u_9 + 1} (α := B) ((f : (a : A) → B) (HSMul.hSMul (β := A) c 0) : B) ((f : (a : A) → B) 0 : B)
⊢ HSMul.hSMul (β := B) c 0 = 0
have rw₂ : Eq.{u_9 + 1} (α := B) ((f : (a : A) → B) 0 : B) ((f : (a : A) → B) 0 : B)
Tactic: rw [← map_zero f, ← smul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M_1 : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : Zero A
inst_1 : SMulZeroClass M_1 A
R : Type u_12
S : Type u_13
M : Type u_14
inst_2 : Zero M
inst_3 : SMulZeroClass R M
inst_4 : SMul S M
f : R → S
hf : Surjective f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
c : R
⊢ HSMul.hSMul (β := M) (f c) 0 = 0
have rw : HSMul.hSMul (β := M) c 0 = 0
Tactic: rw [hsmul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M_1 : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : Zero A
inst_1 : SMulZeroClass M_1 A
R : Type u_12
S : Type u_13
M : Type u_14
inst_2 : Zero M
inst_3 : SMulZeroClass R M
inst_4 : SMul S M
f : R → S
hf : Surjective f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
c : R
rw : HSMul.hSMul (β := M) c 0 = 0
⊢ HSMul.hSMul (β := M) (f c) 0 = 0
have rw₁ : Eq.{u_14 + 1} (α := M) 0 0
Tactic: rw [hsmul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : Zero M₀
inst_1 : Zero A
inst_2 : SMulWithZero M₀ A
a : M₀
b : A
inst_3 : Zero M₀'
inst_4 : Zero A'
inst_5 : SMul M₀ A'
f : ZeroHom A A'
hf : Surjective.{u_7 + 1, u_8 + 1} (α := A) (β := A') (⇑f : (a : A) → A')
smul : ∀ (a : M₀) (b : A), (f : (a : A) → A') (a • b) = HSMul.hSMul (β := A') a ((f : (a : A) → A') b : A')
c : M₀
⊢ HSMul.hSMul (β := A') c 0 = 0
have rw : HSMul.hSMul (β := A') c ((f : (a : A) → A') 0 : A') = (f : (a : A) → A') 0
Tactic: rw [← f.map_zero, ← smul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : Zero M₀
inst_1 : Zero A
inst_2 : SMulWithZero M₀ A
a : M₀
b : A
inst_3 : Zero M₀'
inst_4 : Zero A'
inst_5 : SMul M₀ A'
f : ZeroHom A A'
hf : Surjective.{u_7 + 1, u_8 + 1} (α := A) (β := A') (⇑f : (a : A) → A')
smul : ∀ (a : M₀) (b : A), (f : (a : A) → A') (a • b) = HSMul.hSMul (β := A') a ((f : (a : A) → A') b : A')
c : M₀
rw : HSMul.hSMul (β := A') c ((f : (a : A) → A') 0 : A') = (f : (a : A) → A') 0
⊢ HSMul.hSMul (β := A') c 0 = 0
have rw₁ : Eq.{u_8 + 1} (α := A') ((f : (a : A) → A') (HSMul.hSMul (β := A) c 0) : A') ((f : (a : A) → A') 0 : A')
Tactic: rw [← f.map_zero, ← smul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : Zero M₀
inst_1 : Zero A
inst_2 : SMulWithZero M₀ A
a : M₀
b : A
inst_3 : Zero M₀'
inst_4 : Zero A'
inst_5 : SMul M₀ A'
f : ZeroHom A A'
hf : Surjective.{u_7 + 1, u_8 + 1} (α := A) (β := A') (⇑f : (a : A) → A')
smul : ∀ (a : M₀) (b : A), (f : (a : A) → A') (a • b) = HSMul.hSMul (β := A') a ((f : (a : A) → A') b : A')
c : M₀
rw : HSMul.hSMul (β := A') c ((f : (a : A) → A') 0 : A') = (f : (a : A) → A') 0
rw₁ : Eq.{u_8 + 1} (α := A') ((f : (a : A) → A') (HSMul.hSMul (β := A) c 0) : A') ((f : (a : A) → A') 0 : A')
⊢ HSMul.hSMul (β := A') c 0 = 0
have rw₂ : Eq.{u_8 + 1} (α := A') ((f : (a : A) → A') 0 : A') ((f : (a : A) → A') 0 : A')
Tactic: rw [← f.map_zero, ← smul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : Zero M₀
inst_1 : Zero A
inst_2 : SMulWithZero M₀ A
a : M₀
b : A
inst_3 : Zero M₀'
inst_4 : Zero A'
inst_5 : SMul M₀ A'
f : ZeroHom A A'
hf : Surjective.{u_7 + 1, u_8 + 1} (α := A) (β := A') (⇑f : (a : A) → A')
smul : ∀ (a : M₀) (b : A), (f : (a : A) → A') (a • b) = HSMul.hSMul (β := A') a ((f : (a : A) → A') b : A')
m : A'
⊢ HSMul.hSMul.{u_2, u_8, u_8} (α := M₀) 0 m = 0
have rcases : ∀ (x : A), HSMul.hSMul.{u_2, u_8, u_8} (α := M₀) (β := A') 0 ((f : (a : A) → A') x : A') = 0
Tactic: rcases hf m with ⟨x, rfl⟩
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : Zero M₀
inst_1 : Zero A
inst_2 : SMulWithZero M₀ A
a : M₀
b : A
inst_3 : Zero M₀'
inst_4 : Zero A'
inst_5 : SMul M₀ A'
f : ZeroHom M₀' M₀
m : A
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := M₀') 0 m = 0
have change : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) ((f : (a : M₀') → M₀) 0 : M₀) m = 0
Tactic: change (f 0) • m = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : Zero M₀
inst_1 : Zero A
inst_2 : SMulWithZero M₀ A
a : M₀
b : A
inst_3 : Zero M₀'
inst_4 : Zero A'
inst_5 : SMul M₀ A'
f : ZeroHom M₀' M₀
m : A
⊢ HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) ((f : (a : M₀') → M₀) 0 : M₀) m = 0
have rw : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 m = 0
Tactic: rw [map_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : Zero M₀
inst_1 : Zero A
inst_2 : SMulWithZero M₀ A
a : M₀
b : A
inst_3 : Zero M₀'
inst_4 : Zero A'
inst_5 : SMul M₀ A'
f : ZeroHom M₀' M₀
m : A
rw : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 m = 0
⊢ HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) ((f : (a : M₀') → M₀) 0 : M₀) m = 0
have rw₁ : Eq.{u_7 + 1} (α := A) 0 0
Tactic: rw [map_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M₀ : Type u_2
A : Type u_7
inst : MonoidWithZero M₀
inst_1 : Zero A
inst_2 : MulActionWithZero M₀ A
inst_3 : Subsingleton M₀
x y : A
⊢ x = y
have rw : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 x = y
Tactic: rw [← one_smul M₀ x, ← one_smul M₀ y, Subsingleton.elim (1 : M₀) 0, zero_smul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M₀ : Type u_2
A : Type u_7
inst : MonoidWithZero M₀
inst_1 : Zero A
inst_2 : MulActionWithZero M₀ A
inst_3 : Subsingleton M₀
x y : A
rw : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 x = y
⊢ x = y
have rw₁ : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 x = HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 y
Tactic: rw [← one_smul M₀ x, ← one_smul M₀ y, Subsingleton.elim (1 : M₀) 0, zero_smul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M₀ : Type u_2
A : Type u_7
inst : MonoidWithZero M₀
inst_1 : Zero A
inst_2 : MulActionWithZero M₀ A
inst_3 : Subsingleton M₀
x y : A
rw : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 x = y
rw₁ : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 x = HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 y
⊢ x = y
have rw₂ : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 x = HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 y
Tactic: rw [← one_smul M₀ x, ← one_smul M₀ y, Subsingleton.elim (1 : M₀) 0, zero_smul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M₀ : Type u_2
A : Type u_7
inst : MonoidWithZero M₀
inst_1 : Zero A
inst_2 : MulActionWithZero M₀ A
inst_3 : Subsingleton M₀
x y : A
rw : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 x = y
rw₁ : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 x = HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 y
rw₂ : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 x = HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 y
⊢ x = y
have rw₃ : 0 = HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 y
Tactic: rw [← one_smul M₀ x, ← one_smul M₀ y, Subsingleton.elim (1 : M₀) 0, zero_smul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M₀ : Type u_2
A : Type u_7
inst : MonoidWithZero M₀
inst_1 : Zero A
inst_2 : MulActionWithZero M₀ A
inst_3 : Subsingleton M₀
x y : A
rw : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 x = y
rw₁ : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 x = HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 y
rw₂ : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 x = HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 y
rw₃ : 0 = HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 y
⊢ x = y
have rw₄ : Eq.{u_7 + 1} (α := A) 0 0
Tactic: rw [← one_smul M₀ x, ← one_smul M₀ y, Subsingleton.elim (1 : M₀) 0, zero_smul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M₀ : Type u_2
A : Type u_7
inst : MonoidWithZero M₀
inst_1 : Zero A
inst_2 : MulActionWithZero M₀ A
p : Prop
inst_3 : Decidable p
a : M₀
b : A
⊢ (if p then a else 0) • b = if p then a • b else 0
have rw : (if p then a • b else HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 b) = if p then a • b else 0
Tactic: rw [ite_smul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M₀ : Type u_2
A : Type u_7
inst : MonoidWithZero M₀
inst_1 : Zero A
inst_2 : MulActionWithZero M₀ A
p : Prop
inst_3 : Decidable p
a : M₀
b : A
rw : (if p then a • b else HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 b) = if p then a • b else 0
⊢ (if p then a else 0) • b = if p then a • b else 0
have rw₁ : (if p then a • b else 0) = if p then a • b else 0
Tactic: rw [ite_smul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M₀ : Type u_2
A : Type u_7
inst : MonoidWithZero M₀
inst_1 : Zero A
inst_2 : MulActionWithZero M₀ A
ι : Type u_12
inst_3 : DecidableEq ι
x : A
i j : ι
⊢ HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) (single (M := fun (a : ι) ↦ M₀) i 1 j : M₀) x =
    single (M := fun (a : ι) ↦ A) i x j
have rw : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) (if j = i then 1 else 0) x = single (M := fun (a : ι) ↦ A) i x j
Tactic: rw [single_apply, ite_smul, one_smul, zero_smul, single_apply]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M₀ : Type u_2
A : Type u_7
inst : MonoidWithZero M₀
inst_1 : Zero A
inst_2 : MulActionWithZero M₀ A
ι : Type u_12
inst_3 : DecidableEq ι
x : A
i j : ι
rw : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) (if j = i then 1 else 0) x = single (M := fun (a : ι) ↦ A) i x j
⊢ HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) (single (M := fun (a : ι) ↦ M₀) i 1 j : M₀) x =
    single (M := fun (a : ι) ↦ A) i x j
have rw₁ : (if j = i then HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 x else HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 x) =
  single (M := fun (a : ι) ↦ A) i x j
Tactic: rw [single_apply, ite_smul, one_smul, zero_smul, single_apply]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M₀ : Type u_2
A : Type u_7
inst : MonoidWithZero M₀
inst_1 : Zero A
inst_2 : MulActionWithZero M₀ A
ι : Type u_12
inst_3 : DecidableEq ι
x : A
i j : ι
rw : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) (if j = i then 1 else 0) x = single (M := fun (a : ι) ↦ A) i x j
rw₁ :
  (if j = i then HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 x else HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 x) =
    single (M := fun (a : ι) ↦ A) i x j
⊢ HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) (single (M := fun (a : ι) ↦ M₀) i 1 j : M₀) x =
    single (M := fun (a : ι) ↦ A) i x j
have rw₂ : (if j = i then x else HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 x) = single (M := fun (a : ι) ↦ A) i x j
Tactic: rw [single_apply, ite_smul, one_smul, zero_smul, single_apply]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M₀ : Type u_2
A : Type u_7
inst : MonoidWithZero M₀
inst_1 : Zero A
inst_2 : MulActionWithZero M₀ A
ι : Type u_12
inst_3 : DecidableEq ι
x : A
i j : ι
rw : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) (if j = i then 1 else 0) x = single (M := fun (a : ι) ↦ A) i x j
rw₁ :
  (if j = i then HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 x else HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 x) =
    single (M := fun (a : ι) ↦ A) i x j
rw₂ : (if j = i then x else HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 x) = single (M := fun (a : ι) ↦ A) i x j
⊢ HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) (single (M := fun (a : ι) ↦ M₀) i 1 j : M₀) x =
    single (M := fun (a : ι) ↦ A) i x j
have rw₃ : (if j = i then x else 0) = single (M := fun (a : ι) ↦ A) i x j
Tactic: rw [single_apply, ite_smul, one_smul, zero_smul, single_apply]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M₀ : Type u_2
A : Type u_7
inst : MonoidWithZero M₀
inst_1 : Zero A
inst_2 : MulActionWithZero M₀ A
ι : Type u_12
inst_3 : DecidableEq ι
x : A
i j : ι
rw : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) (if j = i then 1 else 0) x = single (M := fun (a : ι) ↦ A) i x j
rw₁ :
  (if j = i then HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 1 x else HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 x) =
    single (M := fun (a : ι) ↦ A) i x j
rw₂ : (if j = i then x else HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 x) = single (M := fun (a : ι) ↦ A) i x j
rw₃ : (if j = i then x else 0) = single (M := fun (a : ι) ↦ A) i x j
⊢ HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) (single (M := fun (a : ι) ↦ M₀) i 1 j : M₀) x =
    single (M := fun (a : ι) ↦ A) i x j
have rw₄ : (if j = i then x else 0) = if j = i then x else 0
Tactic: rw [single_apply, ite_smul, one_smul, zero_smul, single_apply]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero M₀'
inst_2 : Zero A
inst_3 : MulActionWithZero M₀ A
inst_4 : Zero A'
inst_5 : SMul M₀ A'
p : Prop
inst_6 : Decidable p
f : M₀' →*₀ M₀
r s : M₀'
m : A
⊢ (r * s) • m = r • s • m
have change : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) ((f : (a : M₀') → M₀) (r * s) : M₀) m =
  HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) ((f : (a : M₀') → M₀) r : M₀)
    (HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) ((f : (a : M₀') → M₀) s : M₀) m)
Tactic: change f (r * s) • m = f r • f s • m
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero M₀'
inst_2 : Zero A
inst_3 : MulActionWithZero M₀ A
inst_4 : Zero A'
inst_5 : SMul M₀ A'
p : Prop
inst_6 : Decidable p
f : M₀' →*₀ M₀
m : A
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := M₀') 1 m = m
have change : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) ((f : (a : M₀') → M₀) 1 : M₀) m = m
Tactic: change f 1 • m = m
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
G₀ : Type u_4
G₀' : Type u_5
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : MulActionWithZero G₀ G₀'
inst_3 : SMulCommClass G₀ G₀' G₀'
inst_4 : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
have inl : (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 x)⁻¹ = HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0⁻¹ x⁻¹
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
G₀ : Type u_4
G₀' : Type u_5
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : MulActionWithZero G₀ G₀'
inst_3 : SMulCommClass G₀ G₀' G₀'
inst_4 : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
inl : (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 x)⁻¹ = HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0⁻¹ x⁻¹
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
have inr : ∀ (hc : c ≠ 0), (c • x)⁻¹ = c⁻¹ • x⁻¹
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
G₀ : Type u_4
G₀' : Type u_5
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : MulActionWithZero G₀ G₀'
inst_3 : SMulCommClass G₀ G₀' G₀'
inst_4 : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
hc : c ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
have inr : (HSMul.hSMul (β := G₀') c 0)⁻¹ = HSMul.hSMul (β := G₀') c⁻¹ 0⁻¹
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
G₀ : Type u_4
G₀' : Type u_5
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : MulActionWithZero G₀ G₀'
inst_3 : SMulCommClass G₀ G₀' G₀'
inst_4 : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
hc : c ≠ 0
inr : (HSMul.hSMul (β := G₀') c 0)⁻¹ = HSMul.hSMul (β := G₀') c⁻¹ 0⁻¹
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
have inr₁ : ∀ (hx : x ≠ 0), (c • x)⁻¹ = c⁻¹ • x⁻¹
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
G₀ : Type u_4
G₀' : Type u_5
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : MulActionWithZero G₀ G₀'
inst_3 : SMulCommClass G₀ G₀' G₀'
inst_4 : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
hc : c ≠ 0
hx : x ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
have inr : c⁻¹ • x⁻¹ * c • x = 1
Tactic: refine inv_eq_of_mul_eq_one_left ?_
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
G₀ : Type u_4
G₀' : Type u_5
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : MulActionWithZero G₀ G₀'
inst_3 : SMulCommClass G₀ G₀' G₀'
inst_4 : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
hc : c ≠ 0
hx : x ≠ 0
⊢ c⁻¹ • x⁻¹ * c • x = 1
have inr : (c⁻¹ * c) • (x⁻¹ * x) = 1
Tactic: rw [smul_mul_smul_comm, inv_mul_cancel₀ hc, inv_mul_cancel₀ hx, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
G₀ : Type u_4
G₀' : Type u_5
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : MulActionWithZero G₀ G₀'
inst_3 : SMulCommClass G₀ G₀' G₀'
inst_4 : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
hc : c ≠ 0
hx : x ≠ 0
inr : (c⁻¹ * c) • (x⁻¹ * x) = 1
⊢ c⁻¹ • x⁻¹ * c • x = 1
have inr₁ : HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 1 (x⁻¹ * x) = 1
Tactic: rw [smul_mul_smul_comm, inv_mul_cancel₀ hc, inv_mul_cancel₀ hx, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
G₀ : Type u_4
G₀' : Type u_5
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : MulActionWithZero G₀ G₀'
inst_3 : SMulCommClass G₀ G₀' G₀'
inst_4 : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
hc : c ≠ 0
hx : x ≠ 0
inr : (c⁻¹ * c) • (x⁻¹ * x) = 1
inr₁ : HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 1 (x⁻¹ * x) = 1
⊢ c⁻¹ • x⁻¹ * c • x = 1
have inr₂ : HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) (β := G₀') 1 1 = 1
Tactic: rw [smul_mul_smul_comm, inv_mul_cancel₀ hc, inv_mul_cancel₀ hx, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
G₀ : Type u_4
G₀' : Type u_5
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : MulActionWithZero G₀ G₀'
inst_3 : SMulCommClass G₀ G₀' G₀'
inst_4 : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
hc : c ≠ 0
hx : x ≠ 0
inr : (c⁻¹ * c) • (x⁻¹ * x) = 1
inr₁ : HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 1 (x⁻¹ * x) = 1
inr₂ : HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) (β := G₀') 1 1 = 1
⊢ c⁻¹ • x⁻¹ * c • x = 1
have inr₃ : Eq.{u_5 + 1} (α := G₀') 1 1
Tactic: rw [smul_mul_smul_comm, inv_mul_cancel₀ hc, inv_mul_cancel₀ hx, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : AddZeroClass A
inst_1 : DistribSMul M A
inst_2 : AddZeroClass B
inst_3 : SMul M B
f : A →+ B
hf : Surjective.{u_7 + 1, u_9 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
smul : ∀ (c : M) (x : A), (f : (a : A) → B) (c • x) = HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B)
c : M
x y : B
⊢ c • (x + y) = c • x + c • y
have rcases : ∀ (x : A), c • HAdd.hAdd (α := B) ((f : (a : A) → B) x : B) y = HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B) + c • y
Tactic: rcases hf x with ⟨x, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : AddZeroClass A
inst_1 : DistribSMul M A
inst_2 : AddZeroClass B
inst_3 : SMul M B
f : A →+ B
hf : Surjective.{u_7 + 1, u_9 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
smul : ∀ (c : M) (x : A), (f : (a : A) → B) (c • x) = HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B)
c : M
y : B
x : A
⊢ c • HAdd.hAdd (α := B) ((f : (a : A) → B) x : B) y = HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B) + c • y
have rcases : ∀ (y : A),
  c • HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) =
    HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B) + HSMul.hSMul (β := B) c ((f : (a : A) → B) y : B)
Tactic: rcases hf y with ⟨y, rfl⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
A : Type u_7
inst : AddGroup A
inst_1 : DistribSMul M A
r : M
x : A
⊢ r • -x + r • x = 0
have rw : r • (-x + x) = 0
Tactic: rw [← smul_add, neg_add_cancel, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
A : Type u_7
inst : AddGroup A
inst_1 : DistribSMul M A
r : M
x : A
rw : r • (-x + x) = 0
⊢ r • -x + r • x = 0
have rw₁ : HSMul.hSMul (β := A) r 0 = 0
Tactic: rw [← smul_add, neg_add_cancel, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
A : Type u_7
inst : AddGroup A
inst_1 : DistribSMul M A
r : M
x : A
rw : r • (-x + x) = 0
rw₁ : HSMul.hSMul (β := A) r 0 = 0
⊢ r • -x + r • x = 0
have rw₂ : Eq.{u_7 + 1} (α := A) 0 0
Tactic: rw [← smul_add, neg_add_cancel, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
A : Type u_7
inst : AddGroup A
inst_1 : DistribSMul M A
r : M
x y : A
⊢ r • (x - y) = r • x - r • y
have rw : r • (x + -y) = r • x - r • y
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, smul_add, smul_neg]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Action.Defs (goal)
Goal:
M : Type u_1
A : Type u_7
inst : AddGroup A
inst_1 : DistribSMul M A
r : M
x y : A
rw : r • (x + -y) = r • x - r • y
⊢ r • (x - y) = r • x - r • y
have rw₁ : r • (x + -y) = r • x + -(r • y)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, smul_add, smul_neg]