mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝ : Ring α
a b : α
h : Commute a b
m : ℤ
⊢ Commute (↑m * a) b

Tactic:
by

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

Goal state before:
pp: A : Type u_5
inst✝ : AddGroupWithOne A
f : ℤ →+ A
h1 : f 1 = 1
⊢ f 1 = (castAddHom A) 1

Tactic:
by

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

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : AddGroupWithOne α
inst✝² : AddGroupWithOne β
inst✝¹ : FunLike F α β
inst✝ : AddMonoidHomClass F α β
f : F
h₁ : f 1 = 1
⊢ ((↑f).comp (castAddHom α)) 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : S → R
hf : Injective f
inst✝⁴ : Add S
inst✝³ : Mul S
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : LeftDistribClass R
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
x y z : S
⊢ f (x * (y + z)) = f (x * y + x * z)

Tactic:
by

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

Goal state before:
pp: M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
⊢ f = g

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : Group α
f : Multiplicative ℤ →* α
n : Multiplicative ℤ
⊢ f n = f (ofAdd 1) ^ toAdd n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : S → R
hf : Injective f
inst✝⁴ : Add S
inst✝³ : Mul S
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : RightDistribClass R
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
x y z : S
⊢ f ((x + y) * z) = f (x * z + y * z)

Tactic:
by

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

Goal state before:
pp: β : Type u_4
inst✝ : AddGroup β
f : ℤ →+ β
n : ℤ
⊢ f n = n • f 1

Tactic:
by

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : CommGroup α
inst✝ : AddCommGroup β
a b : β
n : ℤ
⊢ ((zmultiplesHom β).toFun (a + b)) n = ((zmultiplesHom β).toFun a + (zmultiplesHom β).toFun b) n

Tactic:
by

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : CommGroup α
inst✝ : AddCommGroup β
a b : α
n : Multiplicative ℤ
⊢ ((zpowersHom α).toFun (a * b)) n = ((zpowersHom α).toFun a * (zpowersHom α).toFun b) n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective f✝
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
f : S → R
hf : Injective f
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
⊢ f (-x * y) = f (-(x * y))

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
⊢ q • 1 = ↑q

Tactic:
by

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

Goal state before:
pp: A : Type u_2
inst✝ : DivisionRing A
m : ℚ
⊢ m • 1 = ↑m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective f✝
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
f : S → R
hf : Injective f
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
⊢ f (x * -y) = f (-(x * y))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective f✝
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
⊢ f ↑0 = f 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective f✝
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ f ↑(n + 1) = f (↑n + 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : M
⊢ 0 • a = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
z : ℕ
a : M
⊢ ↑z.succ • a = ↑z • a + a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
z : ℕ
a : M
⊢ Int.negSucc z • a = -1 • ↑z.succ • a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
f✝ : S✝ → R
hf✝ : Injective f✝
inst✝²⁰ : Add S✝
inst✝¹⁹ : Mul S✝
inst✝¹⁸ : Zero S✝
inst✝¹⁷ : One S✝
inst✝¹⁶ : Neg S✝
inst✝¹⁵ : Sub S✝
inst✝¹⁴ : SMul ℕ S✝
inst✝¹³ : SMul ℤ S✝
inst✝¹² : Pow S✝ ℕ
inst✝¹¹ : NatCast S✝
inst✝¹⁰ : IntCast S✝
S : Type ?u.36
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Add S
inst✝⁶ : SMul ℕ S
inst✝⁵ : Neg S
inst✝⁴ : Sub S
inst✝³ : SMul ℤ S
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ f ↑↑n = f ↑n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : M
⊢ ↑n • b = n • b

Tactic:
by

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

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
P : Module ℕ M
n : ℕ
⊢ ∀ (m : M), n • m = n • m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
f✝ : S✝ → R
hf✝ : Injective f✝
inst✝²⁰ : Add S✝
inst✝¹⁹ : Mul S✝
inst✝¹⁸ : Zero S✝
inst✝¹⁷ : One S✝
inst✝¹⁶ : Neg S✝
inst✝¹⁵ : Sub S✝
inst✝¹⁴ : SMul ℕ S✝
inst✝¹³ : SMul ℤ S✝
inst✝¹² : Pow S✝ ℕ
inst✝¹¹ : NatCast S✝
inst✝¹⁰ : IntCast S✝
S : Type ?u.36
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Add S
inst✝⁶ : SMul ℕ S
inst✝⁵ : Neg S
inst✝⁴ : Sub S
inst✝³ : SMul ℤ S
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ f ↑(Int.negSucc n) = f (-↑(n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝⁴ : Add S
inst✝³ : Mul S
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : LeftDistribClass R
add : ∀ (x y : R), f (x + y) = f x + f y
mul : ∀ (x y : R), f (x * y) = f x * f y
x y z : R
⊢ f x * (f y + f z) = f x * f y + f x * f z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝⁴ : Add S
inst✝³ : Mul S
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : RightDistribClass R
add : ∀ (x y : R), f (x + y) = f x + f y
mul : ∀ (x y : R), f (x * y) = f x * f y
x y z : R
⊢ (f x + f y) * f z = f x * f z + f y * f z

Tactic:
by

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

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
n : ℕ
x : R
y : M
⊢ (n • x) • y = n • x • y

Tactic:
by

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

Goal state before:
pp: M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : ℕ
a : M
⊢ f (↑x • a) = ↑x • f a

Tactic:
by

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

Goal state before:
pp: R : Type u_5
inst✝ : NonAssocSemiring R
m : ℕ
⊢ m • 1 = ↑m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ -f x * f y = -(f x * f y)

Tactic:
by

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

Goal state before:
pp: R : Type u_5
inst✝ : NonAssocRing R
m : ℤ
⊢ m • 1 = ↑m

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℤ
b : M
⊢ ↑n • b = n • b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
P : Module ℤ M
n : ℤ
⊢ ∀ (m : M), n • m = n • m

Tactic:
by

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

Goal state before:
pp: M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : ℤ
a : M
⊢ f (↑x • a) = ↑x • f a

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
M✝ : Type u_3
M₂ : Type u_4
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℤ
x : R
y : M
⊢ (n • x) • y = n • x • y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
⊢ CharZero R

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ f x * -f y = -(f x * f y)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
⊢ ↑0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
⊢ Even n → ∀ (a : α), (-a) ^ n = a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
h : Even n
⊢ (-1) ^ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : AddMonoidWithOne α
⊢ 2 = 1 + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
a : α
inst✝ : LeftDistribClass α
ha : Even a
b : α
⊢ Even (b * a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
a : α
inst✝ : RightDistribClass α
ha : Even a
b : α
⊢ Even (a * b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
⊢ Even a ↔ ∃ b, a = 2 * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
⊢ Even a ↔ 2 ∣ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_4
inst✝ : NonAssocSemiring α
⊢ (Set.range fun x ↦ 2 * x) = {a | Even a}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ ↑(n + 1) = ↑n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
ha : Even a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ Even (a ^ (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ a = 2 * b + 1 ↔ a = 2 * b + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_4
inst✝ : Semiring α
⊢ (Set.range fun x ↦ 2 * x + 1) = {a | Odd a}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: N : Type u_2
r : N → N → Prop
inst✝ : Group N
⊢ Covariant N N (fun x1 x2 ↦ x1 * x2) r ↔ Contravariant N N (fun x1 x2 ↦ x1 * x2) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ a + a + (2 * b + 1) = 2 * (a + b) + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Even a → Odd b → Odd (a + b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Odd a → Odd b → Even (a + b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
⊢ Odd (a + (a + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
⊢ Odd (a + 1 + a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
⊢ Odd (a + (1 + a))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: N : Type u_2
r : N → N → Prop
inst✝ : Group N
⊢ Covariant N N (swap fun x1 x2 ↦ x1 * x2) r ↔ Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
a : α
⊢ f (2 * a + 1) = 2 * f a + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring α
inst✝² : Semiring β
a : α
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
⊢ Odd a → Odd (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
⊢ (Covariant M N μ fun x1 x2 ↦ x1 < x2) → Covariant M N μ fun x1 x2 ↦ x1 ≤ x2

Tactic:
intro h a b c bc
  rcases bc.eq_or_lt with (rfl | bc)
  · exact le_rfl
  · exact (h _ bc).le

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
⊢ (Covariant M N μ fun x1 x2 ↦ x1 < x2) → Covariant M N μ fun x1 x2 ↦ x1 ≤ x2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 ↦ x1 ≤ x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 < x2) (μ a b) (μ a c)
⊢ b ≠ c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Odd a → Odd b → Odd (a * b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
⊢ (Contravariant M N μ fun x1 x2 ↦ x1 ≤ x2) ↔
    (Contravariant M N μ fun x1 x2 ↦ x1 < x2) ∧ Contravariant M N μ fun x1 x2 ↦ x1 = x2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.ZeroLEOne

Goal state before:
pp: α : Type u_1
⊢ 0 ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Covariant N N (flip mu) r ↔ Covariant N N mu r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
n : ℕ
ha : Odd a
⊢ Odd (a ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Contravariant N N (flip mu) r ↔ Contravariant N N mu r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ a ^ 2 + a * b = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ 0 = b ^ 2 + a * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ ↑(Int.negSucc n) = -↑(n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 =
    (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * a ^ 2 + b ^ (2 * k + 3)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * a ^ 2 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * a ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
n : ℕ
inst✝ : IsCancelAdd α
hn : Odd n
hab : a + b = 0
⊢ a ^ n + b ^ n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
h : IsUnit 2
a : α
u : αˣ
hu : ↑u = 2
⊢ a = ↑u⁻¹ * a + ↑u⁻¹ * a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
h : ∀ (a : α), Even a
a : α
ha : 1 = a + a
⊢ IsUnit 2

Tactic:
rw [← two_mul, eq_comm] at ha

Goal state after:
α : Type u_2
inst✝ : Semiring α
h : ∀ (a : α), Even a
a : α
ha : 2 * a = 1
⊢ IsUnit 2
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
⊢ IsUnit 2 ↔ ∀ (a : α), Even a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
h : IsUnit 2
a : α
⊢ Odd a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
⊢ Odd n → ∀ (a : α), (-a) ^ n = -a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
h : Odd n
⊢ (-1) ^ n = -1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
⊢ Even (-2)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.OpClass

Goal state before:
pp: α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f a (f b c) = f b (f a c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a : α
hp : Odd a
⊢ Odd (-a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
⊢ Odd (-1)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.OpClass

Goal state before:
pp: α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f (f a b) c = f (f a c) b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Even b
⊢ Odd (a - b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a b : α
ha : Even a
hb : Odd b
⊢ Odd (a - b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Odd b
⊢ Even (a - b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a : α
x✝ : Even (a + 1)
⊢ Odd a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a : α
x✝ : Even (a - 1)
⊢ Odd a

Tactic:
by

Goal state after: