awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : AddZeroClass A
inst_1 : DistribSMul M A
inst_2 : AddZeroClass B
inst_3 : SMul M B
f : 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
x y : B
⊢ Eq.{u_7 + 1} (α := A) ((f : (a : B) → A) (c • (x + y)) : A) ((f : (a : B) → A) (c • x + c • y) : A)

Tactic:
simp only [smul, map_add, smul_add]

Premises used: map_add, smul_add
-- 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 : 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
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
⊢ c • (x + y) = c • x + c • y

Tactic:
rcases hf x 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 : 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
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)
⊢ 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 y with ⟨y, 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 : 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 : 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:
simp only [smul_add, ← smul, ← map_add]

Premises used: map_add, smul_add
-- 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 : AddZeroClass A
inst_1 : DistribSMul M_1 A
R : Type u_12
S : Type u_13
M : Type u_14
inst_2 : AddZeroClass M
inst_3 : DistribSMul 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
x y : M
⊢ f c • (x + y) = f c • x + f c • y

Tactic:
simp only [hsmul, smul_add]

Premises used: smul_add
-- 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_1 : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst : AddZeroClass A_1
inst_1 : DistribSMul M_1 A_1
M : Type u_12
A : Type u_13
inst_2 : AddMonoid A
inst_3 : DistribSMul M A
⊢ SMulCommClass M ℕ A

Tactic:
.symm _ _ _

Premises used: SMulCommClass.symm
-- 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 : Monoid M
inst_1 : AddMonoid A
inst_2 : DistribMulAction M A
⊢ Eq (α := SMul M A) (@SemigroupAction.toSMul _ _ Monoid.toSemigroup _) (@SMulZeroClass.toSMul _ _ AddZero.toZero _)

Tactic:
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 : AddGroup A
inst_1 : DistribSMul M A
⊢ SMulCommClass M ℤ A

Tactic:
SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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
rw₂ rw₃ : Eq.{u_7 + 1} (α := A) 0 0
⊢ r • -x + r • x = 0

Tactic:
rw [← smul_add, neg_add_cancel, smul_zero]

Premises used: smul_zero, neg_add_cancel, smul_add
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
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
rw₁ : r • (x + -y) = r • x + -(r • y)
rw₂ : r • x + r • -y = r • x + -(r • y)
rw₃ rw₄ : r • x + -(r • y) = r • x + -(r • y)
⊢ r • (x - y) = r • x - r • y

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, smul_add, smul_neg]

Premises used: sub_eq_add_neg, smul_neg, smul_add
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : AddMonoid β
inst_2 : DistribMulAction α β
a : α
x : β
h : a • x = 0
rw : a⁻¹ • a • x = 0
rw₁ : HSMul.hSMul (β := β) a⁻¹ 0 = 0
rw₂ rw₃ : Eq.{u_11 + 1} (α := β) 0 0
⊢ x = 0

Tactic:
rw [← inv_smul_smul a x, h, smul_zero]

Premises used: smul_zero, inv_smul_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : AddMonoid β
inst_2 : DistribMulAction α β
a : α
x : β
⊢ a • x ≠ 0 ↔ x ≠ 0

Tactic:
not_congr <| smul_eq_zero_iff_eq a

Premises used: smul_eq_zero_iff_eq, not_congr
-- 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 : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
rw : ¬Eq.{u_11 + 1} (α := β) 0 1
⊢ ¬HSMul.hSMul (β := β) g 0 * (HSMul.hSMul (β := β) g 0)⁻¹ = 1

Tactic:
rw [← smul_one g, ← inv_smul_eq_iff, smul_mul', inv_smul_smul, zero_mul]

Premises used: inv_smul_eq_iff, MulZeroClass.zero_mul, inv_smul_smul, MulDistribMulAction.smul_one, smul_mul'
-- 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 : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
⊢ ¬Eq.{u_11 + 1} (α := β) 0 1

Tactic:
zero_ne_one

Premises used: zero_ne_one
-- 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 : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
⊢ ¬Eq.{u_11 + 1} (α := β) 0 1

Tactic:
exact zero_ne_one

Premises used: zero_ne_one
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x : β
pos : ∀ (hx : x = 0), g • x⁻¹ = (g • x)⁻¹
neg : ∀ (hx : ¬x = 0), g • x⁻¹ = (g • x)⁻¹
⊢ g • x⁻¹ = (g • x)⁻¹

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x : β
hx : x = 0
pos : HSMul.hSMul (β := β) g 0⁻¹ = (HSMul.hSMul (β := β) g 0)⁻¹
pos₁ : HSMul.hSMul (β := β) g 0 = (HSMul.hSMul (β := β) g 0)⁻¹
pos₂ : Eq.{u_11 + 1} (α := β) 0 0⁻¹
pos₃ pos₄ : Eq.{u_11 + 1} (α := β) 0 0
⊢ g • x⁻¹ = (g • x)⁻¹

Tactic:
rw [hx, inv_zero, smul_zero, inv_zero]

Premises used: inv_zero, smul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
neg : g • x * g • x⁻¹ = 1
⊢ g • x⁻¹ = (g • x)⁻¹

Tactic:
apply eq_inv_of_mul_eq_one_right

Premises used: eq_inv_of_mul_eq_one_right
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
neg : g • (x * x⁻¹) = 1
neg₁ : HSMul.hSMul (β := β) g 1 = 1
neg₂ neg₃ : Eq.{u_11 + 1} (α := β) 1 1
⊢ g • x * g • x⁻¹ = 1

Tactic:
rw [← smul_mul', mul_inv_cancel₀ hx, smul_one]

Premises used: mul_inv_cancel₀, MulDistribMulAction.smul_one, smul_mul'
-- Module: Mathlib.Algebra.GroupWithZero.Action.Defs
Goal:
α : Type u_10
β : Type u_11
inst : Group α
inst_1 : GroupWithZero β
inst_2 : MulDistribMulAction α β
g : α
x y : β
rw : g • (x * y⁻¹) = g • x / g • y
rw₁ : g • (x * y⁻¹) = g • x * (g • y)⁻¹
rw₂ : g • x * g • y⁻¹ = g • x * (g • y)⁻¹
rw₃ rw₄ : g • x * (g • y)⁻¹ = g • x * (g • y)⁻¹
⊢ g • (x / y) = g • x / g • y

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, smul_mul', smul_inv₀']

Premises used: div_eq_mul_inv, smul_inv₀', smul_mul'
-- Module: Mathlib.Algebra.GroupWithZero.Action.End
Goal:
α : Type u_4
inst : AddMonoid α
f : AddMonoid.End α
a : α
⊢ f • a = (f : (a : α) → α) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.End
Goal:
M : Type u_1
N : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst : AddMonoid α
⊢ FaithfulSMul (AddMonoid.End α) α

Tactic:
⟨fun {_ _ h} => AddMonoidHom.ext h⟩

Premises used: AddMonoidHom.ext, FaithfulSMul.mk
-- Module: Mathlib.Algebra.GroupWithZero.Action.Faithful
Goal:
α : Type u_1
inst : MonoidWithZero α
inst_1 : IsRightCancelMulZero α
⊢ FaithfulSMul α α

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.GroupWithZero.Action.Hom
Goal:
M : Type u_1
N : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : Zero A
inst_1 : Zero B
inst_2 : Zero C
inst_3 : SMulZeroClass M B
r : M
f : ZeroHom A B
⊢ HSMul.hSMul (β := B) r ((f : (a : A) → B) 0 : B) = 0

Tactic:
simp only [map_zero, smul_zero]

Premises used: smul_zero, map_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Hom
Goal:
M : Type u_1
A : Type u_3
B : Type u_4
inst : Zero A
inst_1 : Zero B
inst_2 : SMulZeroClass M B
m : M
f : ZeroHom A B
⊢ (⇑(m • f) : (a : A) → B) = HSMul.hSMul (β := (a : A) → B) m (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Hom
Goal:
M : Type u_1
A : Type u_3
B : Type u_4
inst : Zero A
inst_1 : Zero B
inst_2 : SMulZeroClass M B
m : M
f : ZeroHom A B
a : A
⊢ (m • f : (a : A) → B) a = HSMul.hSMul (β := B) m ((f : (a : A) → B) a : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Hom
Goal:
M : Type u_1
A : Type u_3
B : Type u_4
C : Type u_5
inst : Zero A
inst_1 : Zero B
inst_2 : Zero C
inst_3 : SMulZeroClass M C
m : M
g : ZeroHom B C
f : ZeroHom A B
⊢ (m • g).comp f = m • g.comp f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Hom
Goal:
M : Type u_1
N : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : AddZeroClass A
inst_1 : AddZeroClass B
inst_2 : AddZeroClass C
inst_3 : DistribSMul M B
r : M
f : A →+ B
⊢ HSMul.hSMul (β := B) r ((f : (a : A) → B) 0 : B) = 0

Tactic:
simp only [map_zero, smul_zero]

Premises used: smul_zero, map_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Hom
Goal:
M : Type u_1
N : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : AddZeroClass A
inst_1 : AddZeroClass B
inst_2 : AddZeroClass C
inst_3 : DistribSMul M B
r : M
f : A →+ B
x x_1 : A
⊢ HSMul.hSMul (β := B) r ((f : (a : A) → B) (x + x_1) : B) =
    HSMul.hSMul (β := B) r ((f : (a : A) → B) x : B) + HSMul.hSMul (β := B) r ((f : (a : A) → B) x_1 : B)

Tactic:
simp only [map_add, smul_add]

Premises used: map_add, smul_add
-- Module: Mathlib.Algebra.GroupWithZero.Action.Hom
Goal:
M : Type u_1
A : Type u_3
B : Type u_4
inst : AddZeroClass A
inst_1 : AddZeroClass B
inst_2 : DistribSMul M B
m : M
f : A →+ B
⊢ (⇑(m • f) : (a : A) → B) = HSMul.hSMul (β := (a : A) → B) m (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Hom
Goal:
M : Type u_1
A : Type u_3
B : Type u_4
inst : AddZeroClass A
inst_1 : AddZeroClass B
inst_2 : DistribSMul M B
m : M
f : A →+ B
a : A
⊢ (m • f : (a : A) → B) a = HSMul.hSMul (β := B) m ((f : (a : A) → B) a : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Hom
Goal:
M : Type u_1
A : Type u_3
B : Type u_4
C : Type u_5
inst : AddZeroClass A
inst_1 : AddZeroClass B
inst_2 : AddZeroClass C
inst_3 : DistribSMul M C
m : M
g : B →+ C
f : A →+ B
⊢ (m • g).comp f = m • g.comp f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Opposite
Goal:
M : Type u_1
α : Type u_2
inst : MonoidWithZero α
inst_1 : IsLeftCancelMulZero α
m₁ m₂ : αᵐᵒᵖ
h : ∀ (a : α), m₁ • a = m₂ • a
inl : Subsingleton α → m₁ = m₂
inr : Nontrivial α → m₁ = m₂
⊢ m₁ = m₂

Tactic:
cases subsingleton_or_nontrivial α

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.GroupWithZero.Action.Opposite
Goal:
M : Type u_1
α : Type u_2
inst : MonoidWithZero α
inst_1 : IsLeftCancelMulZero α
m₁ m₂ : αᵐᵒᵖ
h : ∀ (a : α), m₁ • a = m₂ • a
h_1 : Subsingleton α
⊢ m₁ = m₂

Tactic:
Subsingleton.elim ..

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.GroupWithZero.Action.Opposite
Goal:
M : Type u_1
α : Type u_2
inst : MonoidWithZero α
inst_1 : IsLeftCancelMulZero α
m₁ m₂ : αᵐᵒᵖ
h : ∀ (a : α), m₁ • a = m₂ • a
h_1 : Subsingleton α
⊢ m₁ = m₂

Tactic:
exact Subsingleton.elim ..

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.GroupWithZero.Action.Opposite
Goal:
M : Type u_1
α : Type u_2
inst : MonoidWithZero α
inst_1 : IsLeftCancelMulZero α
m₁ m₂ : αᵐᵒᵖ
h : ∀ (a : α), m₁ • a = m₂ • a
h_1 : Nontrivial α
⊢ m₁ = m₂

Tactic:
unop_injective <| mul_left_cancel₀ one_ne_zero (h 1)

Premises used: mul_left_cancel₀, MulOpposite.unop_injective, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Action.Opposite
Goal:
M : Type u_1
α : Type u_2
inst : MonoidWithZero α
inst_1 : IsLeftCancelMulZero α
m₁ m₂ : αᵐᵒᵖ
h : ∀ (a : α), m₁ • a = m₂ • a
h_1 : Nontrivial α
⊢ m₁ = m₂

Tactic:
exact unop_injective <| mul_left_cancel₀ one_ne_zero (h 1)

Premises used: mul_left_cancel₀, MulOpposite.unop_injective, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → Zero (g i)
inst : (i : I) → SMulZeroClass.{v, u_1} (f i) (g i)
a : (i : I) → f i
h : ∀ (x : I), HSMul.hSMul (β := (i : I) → g i) a 0 x = 0 x
⊢ HSMul.hSMul (β := (i : I) → g i) a 0 = 0

Tactic:
ext x
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → Zero (g i)
inst : (i : I) → SMulZeroClass.{v, u_1} (f i) (g i)
a : (i : I) → f i
x : I
⊢ HSMul.hSMul (β := (i : I) → g i) a 0 x = 0 x

Tactic:
smul_zero _

Premises used: smul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → Zero (g i)
inst : (i : I) → SMulZeroClass.{v, u_1} (f i) (g i)
a : (i : I) → f i
x : I
⊢ HSMul.hSMul (β := (i : I) → g i) a 0 x = 0 x

Tactic:
exact smul_zero _

Premises used: smul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst : (i : I) → DistribSMul.{v, u_1} (f i) (g i)
a : (i : I) → f i
h : ∀ (x : I), HSMul.hSMul (β := (i : I) → g i) a 0 x = 0 x
⊢ HSMul.hSMul (β := (i : I) → g i) a 0 = 0

Tactic:
ext x
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst : (i : I) → DistribSMul.{v, u_1} (f i) (g i)
a : (i : I) → f i
x : I
⊢ HSMul.hSMul (β := (i : I) → g i) a 0 x = 0 x

Tactic:
smul_zero _

Premises used: smul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst : (i : I) → DistribSMul.{v, u_1} (f i) (g i)
a : (i : I) → f i
x : I
⊢ HSMul.hSMul (β := (i : I) → g i) a 0 x = 0 x

Tactic:
exact smul_zero _

Premises used: smul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst : (i : I) → DistribSMul.{v, u_1} (f i) (g i)
a : (i : I) → f i
x y : (i : I) → g i
h : ∀ (x_1 : I), (a • (x + y)) x_1 = (a • x + a • y) x_1
⊢ a • (x + y) = a • x + a • y

Tactic:
ext x
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst : (i : I) → DistribSMul.{v, u_1} (f i) (g i)
a : (i : I) → f i
x_1 y : (i : I) → g i
x : I
⊢ (a • (x_1 + y)) x = (a • x_1 + a • y) x

Tactic:
smul_add _ _ _

Premises used: smul_add
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst : (i : I) → DistribSMul.{v, u_1} (f i) (g i)
a : (i : I) → f i
x_1 y : (i : I) → g i
x : I
⊢ (a • (x_1 + y)) x = (a • x_1 + a • y) x

Tactic:
exact smul_add _ _ _

Premises used: smul_add
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
f : I → Type v
α : Type u_1
inst : Monoid α
inst_1 : (i : I) → AddMonoid (f i)
inst_2 : (i : I) → DistribMulAction.{u_1, v} α (f i)
inst_3 : DecidableEq I
i : I
r : α
x : f i
⊢ single (M := f) i (r • x) = r • single (M := f) i x

Tactic:
single_op (fun i : I => (r • · : f i → f i)) (fun _ => smul_zero _) _ _

Premises used: smul_zero, Pi.single_op, HSMul.hSMul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : AddMonoid β
inst_2 : DistribMulAction α β
inst_3 : DecidableEq I
i : I
r : α
x : β
⊢ single (M := fun (x : I) ↦ β) i (r • x) = HSMul.hSMul (β := (j : I) → β) r (single (M := fun (x : I) ↦ β) i x)

Tactic:
single_smul (f := fun _ => β) i r x

Premises used: Pi.single_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
inst : (i : I) → MonoidWithZero (f i)
inst_1 : (i : I) → AddMonoid (g i)
inst_2 : (i : I) → DistribMulAction.{v, u_1} (f i) (g i)
inst_3 : DecidableEq I
i : I
r : f i
x : g i
⊢ single (M := g) i (r • x) = single (M := f) i r • single (M := g) i x

Tactic:
single_op₂ (fun i : I => ((· • ·) : f i → g i → g i)) (fun _ => smul_zero _) _ _ _

Premises used: Pi.single_op₂, smul_zero, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst : (i : I) → MulDistribMulAction.{v, u_1} (f i) (g i)
r : (i : I) → f i
h : ∀ (x : I), HSMul.hSMul (β := (i : I) → g i) r 1 x = 1 x
⊢ HSMul.hSMul (β := (i : I) → g i) r 1 = 1

Tactic:
ext x
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst : (i : I) → MulDistribMulAction.{v, u_1} (f i) (g i)
r : (i : I) → f i
x : I
⊢ HSMul.hSMul (β := (i : I) → g i) r 1 x = 1 x

Tactic:
apply smul_one

Premises used: MulDistribMulAction.smul_one
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst : (i : I) → MulDistribMulAction.{v, u_1} (f i) (g i)
r : (i : I) → f i
x y : (i : I) → g i
h : ∀ (x_1 : I), (r • (x * y)) x_1 = (r • x * r • y) x_1
⊢ r • (x * y) = r • x * r • y

Tactic:
ext x
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pi
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst : (i : I) → MulDistribMulAction.{v, u_1} (f i) (g i)
r : (i : I) → f i
x_1 y : (i : I) → g i
x : I
⊢ (r • (x_1 * y)) x = (r • x_1 * r • y) x

Tactic:
apply smul_mul'

Premises used: smul_mul'
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
inst_2 : Zero α
inst_3 : Mul α
inst_4 : NoZeroDivisors α
⊢ NoZeroDivisors.{u_1} (Finset α)

Tactic:
Function.Injective.noZeroDivisors _ coe_injective coe_zero coe_mul

Premises used: Finset.coe_mul, Finset.coe_injective, Finset.coe_zero, Function.Injective.noZeroDivisors
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : Zero β
inst_2 : SMulZeroClass α β
s : Finset α
⊢ HSMul.hSMul (β := Finset β) s 0 ⊆ 0

Tactic:
simp [subset_iff, mem_smul]

Premises used: Finset.subset_iff, Finset.mem_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : Zero β
inst_2 : SMulZeroClass α β
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ HSMul.hSMul (β := Finset β) s 0

Tactic:
simpa [mem_smul] using hs

Premises used: Finset.mem_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : Zero β
inst_2 : SMulZeroClass α β
t : Finset β
a : α
h : 0 ∈ t
⊢ 0 ∈ a • t

Tactic:
mem_smul_finset.2 ⟨0, h, smul_zero _⟩

Premises used: Iff.mpr, smul_zero, And.intro, Finset.mem_smul_finset, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : Zero α
inst_2 : Zero β
inst_3 : SMulWithZero α β
t : Finset β
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := Finset α) 0 t ⊆ 0

Tactic:
simp [subset_iff, mem_smul]

Premises used: Finset.subset_iff, Finset.mem_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : Zero α
inst_2 : Zero β
inst_3 : SMulWithZero α β
t : Finset β
ht : t.Nonempty
⊢ 0 ⊆ HSMul.hSMul.{u_1, u_2, u_2} (α := Finset α) 0 t

Tactic:
simpa [mem_smul] using ht

Premises used: Finset.mem_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : Zero α
inst_2 : Zero β
inst_3 : SMulWithZero α β
s : Finset β
h : s.Nonempty
⊢ (↑(HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 s) : Set β) = (↑0 : Set β)

Tactic:
simpa using @Set.zero_smul_set α _ _ _ _ _ h

Premises used: Set.zero_smul_set
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : Zero α
inst_2 : Zero β
inst_3 : SMulWithZero α β
s : Finset β
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 s ⊆ 0

Tactic:
image_subset_iff.2 fun x _ ↦ mem_zero.2 <| zero_smul α x

Premises used: Iff.mpr, Set.Mem, Finset.mem_zero, setOf, Finset.image_subset_iff, zero_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
s : Finset β
a : α
b : β
ha : a ≠ 0
⊢ a • b ∈ a • s ↔ b ∈ s

Tactic:
smul_mem_smul_finset_iff (Units.mk0 a ha)

Premises used: Set.Mem, Finset.smul_mem_smul_finset_iff, setOf, Units.mk0
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
s : Finset β
a : α
b : β
ha : a ≠ 0
⊢ a⁻¹ • b ∈ s ↔ b ∈ a • s

Tactic:
show _ ↔ _ ∈ Units.mk0 a ha • _ from inv_smul_mem_iff

Premises used: Finset.inv_smul_mem_iff, Set.Mem, setOf
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
s : Finset β
a : α
b : β
ha : a ≠ 0
⊢ b ∈ a⁻¹ • s ↔ a • b ∈ s

Tactic:
show _ ∈ (Units.mk0 a ha)⁻¹ • _ ↔ _ from mem_inv_smul_finset_iff

Premises used: Set.Mem, Finset.mem_inv_smul_finset_iff, setOf