mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
x : M₀
⊢ 1 x = 1 ↔ x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: 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✝³ : SMulZeroClass M✝ A
R : Type u_12
S : Type u_13
M : Type u_14
inst✝² : Zero M
inst✝¹ : SMulZeroClass R M
inst✝ : SMul S M
f : R → S
hf : Surjective f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
c : R
⊢ f c • 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: 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✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a✝ : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom A' A
hf : Injective ⇑f
smul : ∀ (a : M₀) (b : A'), f (a • b) = a • f b
a : M₀
⊢ f (a • 0) = f 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a⁻¹ * a * a = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: 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✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a✝ : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom A' A
hf : Injective ⇑f
smul : ∀ (a : M₀) (b : A'), f (a • b) = a • f b
a : A'
⊢ f (0 • a) = f 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * a / a = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a / a * a = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a / (a * a) = a⁻¹⁻¹ * a⁻¹ * a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: 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✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom A A'
hf : Surjective ⇑f
smul : ∀ (a : M₀) (b : A), f (a • b) = a • f b
c : M₀
⊢ c • 0 = 0

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

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: 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✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom A A'
hf : Surjective ⇑f
smul : ∀ (a : M₀) (b : A), f (a • b) = a • f b
c : M₀
⊢ c • 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ 1 / a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a⁻¹ = 0 ↔ a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: 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✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom A A'
hf : Surjective ⇑f
smul : ∀ (a : M₀) (b : A), f (a • b) = a • f b
m : A'
⊢ 0 • m = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a / (a / a) = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : 1 / a ≠ 0
ha : a = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
g : G₀
⊢ (fun g ↦ a * g) (a⁻¹ * g) = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
g : G₀
⊢ (fun g ↦ g * a) (g * a⁻¹) = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: 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✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom M₀' M₀
m : A
⊢ 0 • m = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ 0 ^ ↑n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
x✝ : Int.negSucc n ≠ 0
⊢ 0 ^ Int.negSucc n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
inst✝ : Subsingleton M₀
x y : A
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
p : Prop
inst✝ : Decidable p
a : M₀
b : A
⊢ (if p then a else 0) • b = if p then a • b else 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
p : Prop
inst✝ : Decidable p
a : A
⊢ (if p then 1 else 0) • a = if p then a else 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
⊢ 0 ^ n = if n = 0 then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
⊢ 0 ^ n = 1 ↔ n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (↑n + 1) = a ^ ↑n * a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
ι : Type u_12
inst✝ : DecidableEq ι
x : A
i j : ι
⊢ single i 1 j • x = single i x j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ a ^ (-1 + 1) = a ^ (-1) * a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: 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✝⁵ : MonoidWithZero M₀'
inst✝⁴ : Zero A
inst✝³ : MulActionWithZero M₀ A
inst✝² : Zero A'
inst✝¹ : SMul M₀ A'
p : Prop
inst✝ : Decidable p
f : M₀' →*₀ M₀
r s : M₀'
m : A
⊢ (r * s) • m = r • s • m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: 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✝⁵ : MonoidWithZero M₀'
inst✝⁴ : Zero A
inst✝³ : MulActionWithZero M₀ A
inst✝² : Zero A'
inst✝¹ : SMul M₀ A'
p : Prop
inst✝ : Decidable p
f : M₀' →*₀ M₀
m : A
⊢ 1 • m = m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: G₀ : Type u_4
G₀' : Type u_5
inst✝⁴ : GroupWithZero G₀
inst✝³ : GroupWithZero G₀'
inst✝² : MulActionWithZero G₀ G₀'
inst✝¹ : SMulCommClass G₀ G₀' G₀'
inst✝ : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: 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✝² : DistribSMul M A
inst✝¹ : AddZeroClass B
inst✝ : SMul M B
f : B →+ A
hf : Injective ⇑f
smul : ∀ (c : M) (x : B), f (c • x) = c • f x
c : M
x y : B
⊢ f (c • (x + y)) = f (c • x + c • y)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: 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✝² : DistribSMul M A
inst✝¹ : AddZeroClass B
inst✝ : SMul M B
f : A →+ B
hf : Surjective ⇑f
smul : ∀ (c : M) (x : A), f (c • x) = c • f x
c : M
x y : B
⊢ c • (x + y) = c • x + c • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: 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✝³ : DistribSMul M✝ A
R : Type u_12
S : Type u_13
M : Type u_14
inst✝² : AddZeroClass M
inst✝¹ : DistribSMul R M
inst✝ : 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:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x : A
⊢ r • -x + r • x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x y : A
⊢ r • (x - y) = r • x - r • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction α β
a : α
x : β
h : a • x = 0
⊢ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: 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✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
⊢ ¬g • 0 * (g • 0)⁻¹ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
i : ℤ
⊢ a ^ (1 + i) = a * a ^ i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
⊢ g • x⁻¹ = (g • x)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b c : G₀
⊢ a / c * b = a * b / c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x y : β
⊢ g • (x / y) = g • x / g • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b : G₀
⊢ a ^ 2 * b / a = a * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: x✝ : ℤ
⊢ x✝ ^ 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: x✝¹ : ℕ
x✝ : ℤ
⊢ x✝ ^ (x✝¹ + 1) = x✝ ^ x✝¹ * x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: m : ℕ
n : ℤ
⊢ ↑m.succ • n = ↑m • n + n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: m : ℕ
n : ℤ
⊢ -[m+1] • n = -(↑m.succ • n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: _n : ℕ
hn : _n ≠ 0
_x _y : ℤ
⊢ ↑_n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ AddCommMonoid ℤ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ AddMonoid ℤ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ Monoid ℤ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ CommSemigroup ℤ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ Semigroup ℤ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ AddGroup ℤ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ AddCommSemigroup ℤ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: ⊢ AddSemigroup ℤ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m n : ℕ
h : ↑m = ↑n
⊢ m = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = 0 ↔ n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = 1 ↔ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddMonoidWithOne M
inst✝ : CharZero M
⊢ 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
h : m ≤ n
⊢ ↑(n - m) + ↑m = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
h : 0 < 0
⊢ ↑(0 - 1) = ↑0 - 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑(n + 1) - 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝¹ : AddGroupWithOne R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) = OfNat.ofNat n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑(-↑0) = -↑↑0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(-↑(n + 1)) = -↑↑(n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(- -[n+1]) = -↑-[n+1]

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(subNatNat m n) = ↑m - ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(negOfNat n) = -↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(↑m + ↑n) = ↑↑m + ↑↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(↑m + -[n+1]) = ↑↑m + ↑-[n+1]

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(-[m+1] + ↑n) = ↑-[m+1] + ↑↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(-[m+1] + -[n+1]) = ↑-[m+1] + ↑-[n+1]

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℤ
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
n : ℤ
⊢ n • 1 = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : R
h : a + b = 1
x : M
⊢ a • x + b • x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ 2 • x = x + x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M₂ →+ M
hf : Injective ⇑f
smul : ∀ (c : R) (x : M₂), f (c • x) = c • f x
c₁ c₂ : R
x : M₂
⊢ f ((c₁ + c₂) • x) = f (c₁ • x + c₂ • x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M₂ →+ M
hf : Injective ⇑f
smul : ∀ (c : R) (x : M₂), f (c • x) = c • f x
x : M₂
⊢ f (0 • x) = f 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M →+ M₂
hf : Surjective ⇑f
smul : ∀ (c : R) (x : M), f (c • x) = c • f x
c₁ c₂ : R
x : M₂
⊢ (c₁ + c₂) • x = c₁ • x + c₂ • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M →+ M₂
hf : Surjective ⇑f
smul : ∀ (c : R) (x : M), f (c • x) = c • f x
x : M₂
⊢ 0 • x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
zero_eq_one : 0 = 1
⊢ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: M : Type u_3
inst✝² : AddCommMonoid M
R : Type u_5
inst✝¹ : Ring R
inst✝ : Module R M
r : R
m : M
⊢ r • m + (1 - r) • m = m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ a • x + b • y = b • y - b • x + (a • x + b • x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ b • y - b • x + (a • x + b • x) = b • (y - x) + x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_5
inst✝¹ : Semiring R
M : Type u_6
inst✝ : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
⊢ P = Q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
x : M
⊢ -r • x + r • x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
x : M
⊢ -r • -x = r • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
⊢ -1 • x = -x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Defs

Goal state before:
pp: x✝ : ℤ
⊢ x✝ ^ 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Defs

Goal state before:
pp: x✝¹ : ℕ
x✝ : ℤ
⊢ x✝ ^ (x✝¹ + 1) = x✝ ^ x✝¹ * x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r s : R
y : M
⊢ (r - s) • y = r • y - s • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Defs

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocRing α
m : ℤ
⊢ ∀ (n : ℤ), ↑(m * n) = ↑m * ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Defs

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
m : ℤ
⊢ ∀ (n : ℤ), ↑(0 * n) = 0 • ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Defs

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
m : ℤ
x✝ : ℕ
ih : ∀ (n : ℤ), ↑(↑x✝ * n) = ↑x✝ • ↑n
⊢ ∀ (n : ℤ), ↑((↑x✝ + 1) * n) = (↑x✝ + 1) • ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Defs

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
m : ℤ
x✝ : ℕ
ih : ∀ (n : ℤ), ↑(-↑x✝ * n) = -↑x✝ • ↑n
⊢ ∀ (n : ℤ), ↑((-↑x✝ - 1) * n) = (-↑x✝ - 1) • ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℤ
m : ℕ
⊢ ↑(n ^ m) = ↑n ^ m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Equiv.Opposite

Goal state before:
pp: M✝ : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
hf : ∀ (x y : M), Commute (f x) (f y)
x y : M
⊢ (op ∘ ⇑f) (x * y) = (op ∘ ⇑f) x * (op ∘ ⇑f) y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Equiv.Opposite

Goal state before:
pp: M✝ : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
hf : ∀ (x y : M), Commute (f x) (f y)
x y : M
⊢ (op ∘ ⇑f) (x * y) = (op ∘ ⇑f) x * (op ∘ ⇑f) y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Equiv.Opposite

Goal state before:
pp: M : Type u_1
α✝ : Type u_2
α : Type ?u.6
β : Type ?u.8
inst✝¹ : Mul α
inst✝ : Mul β
f : αᵐᵒᵖ ≃* βᵐᵒᵖ
x : α
⊢ (unop ∘ ⇑f.symm ∘ MulOpposite.op) ((unop ∘ ⇑f ∘ MulOpposite.op) x) = x

Tactic:
by

Goal state after: