awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this_1 : ∀ (x : G), HSMul.hSMul (β := G₀) x 0 = 0
hb : ¬b = 0
this : h • b ≠ 0
neg : (g / h * h) • (a / b * b) = g • a
⊢ (g / h) • (a / b) = g • a / h • b

Tactic:
rw [eq_div_iff_mul_eq this, smul_mul_smul_comm]

Premises used: smul_mul_smul_comm, eq_div_iff_mul_eq
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulAction G G₀
inst_3 : IsScalarTower G G₀ G₀
inst_4 : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this_1 : ∀ (x : G), HSMul.hSMul (β := G₀) x 0 = 0
hb : ¬b = 0
this : h • b ≠ 0
⊢ (g / h * h) • (a / b * b) = g • a

Tactic:
simp [hb]
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulDistribMulAction G G₀
g : G
x : G₀
n : ℤ
ofNat : ∀ (a : ℕ), g • x ^ Int.ofNat a = (g • x) ^ Int.ofNat a
negSucc : ∀ (a : ℕ), g • x ^ Int.negSucc a = (g • x) ^ Int.negSucc a
⊢ g • x ^ n = (g • x) ^ n

Tactic:
cases n
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulDistribMulAction G G₀
g : G
x : G₀
a : ℕ
⊢ g • x ^ Int.ofNat a = (g • x) ^ Int.ofNat a

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Action.Basic
Goal:
G : Type u_1
G₀ : Type u_2
inst : Group G
inst_1 : GroupWithZero G₀
inst_2 : MulDistribMulAction G G₀
g : G
x : G₀
a : ℕ
⊢ g • x ^ Int.negSucc a = (g • x) ^ Int.negSucc a

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Action.Center
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
u : ↥(center G₀ˣ)
refine : ∀ (r : G₀), r * (↑(↑u : G₀ˣ) : G₀) = (↑(↑u : G₀ˣ) : G₀) * r
⊢ ↥(Submonoid.center G₀)

Tactic:
refine ⟨(u : G₀ˣ), Submonoid.mem_center_iff.mpr fun r ↦ ?_⟩
-- Module: Mathlib.Algebra.GroupWithZero.Action.Center
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
u : ↥(center G₀ˣ)
r : G₀
inl : 0 * (↑(↑u : G₀ˣ) : G₀) = (↑(↑u : G₀ˣ) : G₀) * 0
inr : ∀ (hr : r ≠ 0), r * (↑(↑u : G₀ˣ) : G₀) = (↑(↑u : G₀ˣ) : G₀) * r
⊢ r * (↑(↑u : G₀ˣ) : G₀) = (↑(↑u : G₀ˣ) : G₀) * r

Tactic:
obtain rfl | hr := eq_or_ne r 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Center
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
u : ↥(center G₀ˣ)
inl : 0 * (↑(↑u : G₀ˣ) : G₀) = 0
inl₁ inl₂ : Eq.{u_1 + 1} (α := G₀) 0 0
⊢ 0 * (↑(↑u : G₀ˣ) : G₀) = (↑(↑u : G₀ˣ) : G₀) * 0

Tactic:
rw [mul_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Center
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
u : ↥(center G₀ˣ)
r : G₀
hr : r ≠ 0
⊢ r * (↑(↑u : G₀ˣ) : G₀) = (↑(↑u : G₀ˣ) : G₀) * r

Tactic:
congrArg Units.val <| (u.2.comm <| Units.mk0 r hr).symm

Premises used: Units.val, congrArg, IsMulCentral.comm, Units.mk0, Commute.symm, Subtype.property
-- Module: Mathlib.Algebra.GroupWithZero.Action.Center
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
u : ↥(center G₀ˣ)
r : G₀
hr : r ≠ 0
⊢ r * (↑(↑u : G₀ˣ) : G₀) = (↑(↑u : G₀ˣ) : G₀) * r

Tactic:
exact congrArg Units.val <| (u.2.comm <| Units.mk0 r hr).symm

Premises used: Units.val, congrArg, IsMulCentral.comm, Units.mk0, Commute.symm, Subtype.property
-- Module: Mathlib.Algebra.GroupWithZero.Action.ConjAct
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
⊢ Eq.{u_2 + 1} (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) 0 : G₀) (0 : G₀)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.ConjAct
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
⊢ Eq.{u_2 + 1} (α := ConjAct G₀) ((toConjAct : (a : G₀) → ConjAct G₀) 0 : ConjAct G₀) (0 : ConjAct G₀)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.ConjAct
Goal:
α : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
⊢ ∀ (x y : ConjAct G₀) (b : G₀), (x * y) • b = x • y • b

Tactic:
simp [smul_def, mul_assoc]

Premises used: ConjAct.smul_def, mul_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Action.ConjAct
Goal:
α : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
⊢ ∀ (b : G₀), HSMul.hSMul (α := ConjAct G₀) 1 b = b

Tactic:
simp [smul_def]

Premises used: ConjAct.smul_def
-- Module: Mathlib.Algebra.GroupWithZero.Action.ConjAct
Goal:
α : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : SMul α G₀
inst_2 : SMulCommClass α G₀ G₀
inst_3 : IsScalarTower α G₀ G₀
a : α
ug : ConjAct G₀
g : G₀
rw :
  a •
      HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
        (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀) =
    ug • a • g
rw₁ :
  a •
      HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
        (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀) =
    HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) (a • g))
      (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀)
rw₂ :
  a •
      HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
        (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀) =
    HMul.hMul (β := G₀) (a • HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
      (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀)
rw₃ rw₄ :
  a •
      HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
        (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀) =
    a •
      HMul.hMul (β := G₀) (HMul.hMul (α := G₀) ((ofConjAct : (a : ConjAct G₀) → G₀) ug : G₀) g)
        (((ofConjAct : (a : ConjAct G₀) → G₀) ug)⁻¹ : G₀)
⊢ a • ug • g = ug • a • g

Tactic:
rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]

Premises used: ConjAct.smul_def, smul_mul_assoc, mul_smul_comm
-- Module: Mathlib.Algebra.GroupWithZero.Action.ConjAct
Goal:
α : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : SMul α G₀
inst_2 : SMulCommClass G₀ α G₀
inst_3 : IsScalarTower α G₀ G₀
⊢ SMulCommClass (ConjAct G₀) α G₀

Tactic:
haveI := SMulCommClass.symm G₀ α G₀
  .symm ..

Premises used: SMulCommClass.symm, ConjAct
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
M : Type u_1
A : Type u_7
inst : Zero A
inst_1 : SMulZeroClass M A
a : M
⊢ HSMul.hSMul (β := A) a 0 = 0

Tactic:
SMulZeroClass.smul_zero _

Premises used: SMulZeroClass.smul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
M : Type u_1
A : Type u_7
inst : Zero A
inst_1 : SMulZeroClass M A
p : Prop
inst_2 : Decidable p
a : M
b : A
pos : p → a • b = a • b
neg : ¬p → HSMul.hSMul (β := A) a 0 = 0
⊢ (a • if p then b else 0) = if p then a • b else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
M : Type u_1
A : Type u_7
inst : Zero A
inst_1 : SMulZeroClass M A
p : Prop
inst_2 : Decidable p
a : M
b : A
h : p
⊢ a • b = a • b

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
M : Type u_1
A : Type u_7
inst : Zero A
inst_1 : SMulZeroClass M A
p : Prop
inst_2 : Decidable p
a : M
b : A
h : ¬p
⊢ HSMul.hSMul (β := A) a 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
M : Type u_1
A : Type u_7
inst : Zero A
inst_1 : SMulZeroClass M A
a : M
b : A
h : b = 0
⊢ a • b = 0

Tactic:
h.symm ▸ smul_zero a

Premises used: smul_zero, Eq.rec, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
M : Type u_1
A : Type u_7
inst : Zero A
inst_1 : SMulZeroClass M A
a : M
b : A
⊢ a • b ≠ 0 → b ≠ 0

Tactic:
mt <| smul_eq_zero_of_right a

Premises used: mt, smul_eq_zero_of_right
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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 B A
hf : Injective.{u_9 + 1, u_7 + 1} (α := B) (β := A) (⇑f : (a : B) → A)
smul : ∀ (c : M) (x : B), (f : (a : B) → A) (c • x) = HSMul.hSMul (β := A) c ((f : (a : B) → A) x : A)
c : M
⊢ Eq.{u_7 + 1} (α := A) ((f : (a : B) → A) (HSMul.hSMul (β := B) c 0) : A) ((f : (a : B) → A) 0 : A)

Tactic:
simp only [smul, map_zero, smul_zero]

Premises used: smul_zero, map_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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)
rw₂ rw₃ : Eq.{u_9 + 1} (α := B) ((f : (a : A) → B) 0 : B) ((f : (a : A) → B) 0 : B)
⊢ HSMul.hSMul (β := B) c 0 = 0

Tactic:
rw [← map_zero f, ← smul, smul_zero]

Premises used: smul_zero, map_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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
rw₁ rw₂ : Eq.{u_14 + 1} (α := M) 0 0
⊢ HSMul.hSMul (β := M) (f c) 0 = 0

Tactic:
rw [hsmul, smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
M₀ : Type u_2
A : Type u_7
inst : Zero M₀
inst_1 : Zero A
inst_2 : SMulWithZero M₀ A
m : A
⊢ HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) 0 m = 0

Tactic:
SMulWithZero.zero_smul m

Premises used: SMulWithZero.zero_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
M₀ : Type u_2
A : Type u_7
inst : Zero M₀
inst_1 : Zero A
inst_2 : SMulWithZero M₀ A
a : M₀
h : a = 0
b : A
⊢ a • b = 0

Tactic:
h.symm ▸ zero_smul _ b

Premises used: Eq.rec, zero_smul, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
M₀ : Type u_2
A : Type u_7
inst : Zero M₀
inst_1 : Zero A
inst_2 : SMulWithZero M₀ A
a : M₀
b : A
⊢ a • b ≠ 0 → a ≠ 0

Tactic:
mt fun h ↦ smul_eq_zero_of_left h b

Premises used: smul_eq_zero_of_left, mt
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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_1 : M₀
b : A
inst_3 : Zero M₀'
inst_4 : Zero A'
inst_5 : SMul M₀ A'
f : ZeroHom A' A
hf : Injective.{u_8 + 1, u_7 + 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)
a : M₀
⊢ Eq.{u_7 + 1} (α := A) ((f : (a : A') → A) (HSMul.hSMul (β := A') a 0) : A) ((f : (a : A') → A) 0 : A)

Tactic:
simp [smul]
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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_1 : M₀
b : A
inst_3 : Zero M₀'
inst_4 : Zero A'
inst_5 : SMul M₀ A'
f : ZeroHom A' A
hf : Injective.{u_8 + 1, u_7 + 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)
a : A'
⊢ Eq.{u_7 + 1} (α := A) ((f : (a : A') → A) (HSMul.hSMul.{u_2, u_8, u_8} (α := M₀) 0 a) : A) ((f : (a : A') → A) 0 : A)

Tactic:
simp [smul]
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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')
rw₂ rw₃ : Eq.{u_8 + 1} (α := A') ((f : (a : A) → A') 0 : A') ((f : (a : A) → A') 0 : A')
⊢ HSMul.hSMul (β := A') c 0 = 0

Tactic:
rw [← f.map_zero, ← smul, smul_zero]

Premises used: smul_zero, ZeroHom.map_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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'
rcases : ∀ (x : A), HSMul.hSMul.{u_2, u_8, u_8} (α := M₀) (β := A') 0 ((f : (a : A) → A') x : A') = 0
⊢ HSMul.hSMul.{u_2, u_8, u_8} (α := M₀) 0 m = 0

Tactic:
rcases hf m with ⟨x, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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')
x : A
⊢ HSMul.hSMul.{u_2, u_8, u_8} (α := M₀) (β := A') 0 ((f : (a : A) → A') x : A') = 0

Tactic:
simp [← smul]
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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
change : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) ((f : (a : M₀') → M₀) 0 : M₀) m = 0
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := M₀') 0 m = 0

Tactic:
change (f 0) • m = 0

Premises used: OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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
rw₁ rw₂ : Eq.{u_7 + 1} (α := A) 0 0
⊢ HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) ((f : (a : M₀') → M₀) 0 : M₀) m = 0

Tactic:
rw [map_zero, zero_smul]

Premises used: map_zero, SMulWithZero.zero_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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
rw₄ rw₅ : Eq.{u_7 + 1} (α := A) 0 0
⊢ x = y

Tactic:
rw [← one_smul M₀ x, ← one_smul M₀ y, Subsingleton.elim (1 : M₀) 0, zero_smul, zero_smul]

Premises used: MulActionWithZero.zero_smul, one_smul, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
M₀ : Type u_2
A : Type u_7
inst : MonoidWithZero M₀
inst_1 : Zero A
inst_2 : MulActionWithZero M₀ A
inst_3 : Nontrivial A
⊢ Nontrivial M₀

Tactic:
(subsingleton_or_nontrivial M₀).resolve_left fun _ =>
    not_subsingleton A <| MulActionWithZero.subsingleton M₀ A

Premises used: MulActionWithZero.subsingleton, subsingleton_or_nontrivial, Or.resolve_left, not_subsingleton
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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
rw₁ rw₂ : (if p then a • b else 0) = if p then a • b else 0
⊢ (if p then a else 0) • b = if p then a • b else 0

Tactic:
rw [ite_smul, zero_smul]

Premises used: zero_smul, ite_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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 : A
⊢ HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) (if p then 1 else 0) a = if p then a else 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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
rw₄ rw₅ : (if j = i then x else 0) = if j = i then x else 0
⊢ 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

Tactic:
rw [single_apply, ite_smul, one_smul, zero_smul, single_apply]

Premises used: Pi.single_apply, one_smul, zero_smul, ite_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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
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)
⊢ (r * s) • m = r • s • m

Tactic:
change f (r * s) • m = f r • f s • m

Premises used: HMul.hMul, DFunLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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
⊢ 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:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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
change : HSMul.hSMul.{u_2, u_7, u_7} (α := M₀) ((f : (a : M₀') → M₀) 1 : M₀) m = m
⊢ HSMul.hSMul.{u_3, u_7, u_7} (α := M₀') 1 m = m

Tactic:
change f 1 • m = m

Premises used: OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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_2, u_7, u_7} (α := M₀) ((f : (a : M₀') → M₀) 1 : M₀) m = m

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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⁻¹
inr : ∀ (hc : c ≠ 0), (c • x)⁻¹ = c⁻¹ • x⁻¹
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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₀'
x : G₀'
⊢ (HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0 x)⁻¹ = HSMul.hSMul.{u_4, u_5, u_5} (α := G₀) 0⁻¹ x⁻¹

Tactic:
simp only [inv_zero, zero_smul]

Premises used: inv_zero, zero_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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⁻¹
inr₁ : ∀ (hx : x ≠ 0), (c • x)⁻¹ = c⁻¹ • x⁻¹
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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₀
hc : c ≠ 0
⊢ (HSMul.hSMul (β := G₀') c 0)⁻¹ = HSMul.hSMul (β := G₀') c⁻¹ 0⁻¹

Tactic:
simp only [inv_zero, smul_zero]

Premises used: inv_zero, smul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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⁻¹

Tactic:
inv_eq_of_mul_eq_one_left ?_

Premises used: inv_eq_of_mul_eq_one_left
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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⁻¹ • x⁻¹ * c • x = 1
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹

Tactic:
refine inv_eq_of_mul_eq_one_left ?_

Premises used: inv_eq_of_mul_eq_one_left
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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
inr₃ inr₄ : Eq.{u_5 + 1} (α := G₀') 1 1
⊢ c⁻¹ • x⁻¹ * c • x = 1

Tactic:
rw [smul_mul_smul_comm, inv_mul_cancel₀ hc, inv_mul_cancel₀ hx, one_smul]

Premises used: smul_mul_smul_comm, one_smul, inv_mul_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
M : Type u_1
A : Type u_7
inst : AddZeroClass A
inst_1 : DistribSMul M A
a : M
b₁ b₂ : A
⊢ a • (b₁ + b₂) = a • b₁ + a • b₂

Tactic:
DistribSMul.smul_add _ _ _

Premises used: DistribSMul.smul_add