mathlib-initiative/mathlib-tactics huggingface dataset:
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 ∘ MulOpposite.op) ((unop ∘ ⇑f.symm ∘ MulOpposite.op) x) = x

Tactic:
by

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

Goal state before:
pp: R : Type v
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : RightDistribClass R
a b c d : R
⊢ (a + b + c) * d = a * d + b * d + c * d

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ (a + 1) * b = a * b + b

Tactic:
by

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

Goal state before:
pp: m n : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
⊢ ∀ (hn : m ≤ n), Int.strongRec lt ge n = ge n hn fun k x ↦ Int.strongRec lt ge k

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : LeftDistribClass α
a b : α
⊢ a * (b + 1) = a * b + a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ (1 + a) * b = b + a * b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : LeftDistribClass α
a b : α
⊢ a * (1 + b) = a + a * b

Tactic:
by

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

Goal state before:
pp: a : ℤ
h : 1 < a.natAbs
⊢ Function.Injective fun x ↦ a ^ x

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocSemiring α
n : α
⊢ 1 * n + 1 * n = n + n

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocSemiring α
n : α
⊢ n * 1 + n * 1 = n + n

Tactic:
by

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

Goal state before:
pp: n : ℤ
m : ℕ
⊢ ↑m ∣ n ↔ m ∣ n.natAbs

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocSemiring α
n : ℕ
a : α
⊢ n • a = ↑n * a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
⊢ (if P then a else 0) * b = if P then a * b else 0

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
⊢ (a * if P then b else 0) = if P then a * b else 0

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : MulZeroClass α
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b : α
⊢ ((if P then a else 0) * if Q then b else 0) = if P ∧ Q then a * b else 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MulZeroOneClass α
P : Prop
inst✝ : Decidable P
a : α
⊢ (a * if P then 1 else 0) = if P then a else 0

Tactic:
by

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

Goal state before:
pp: m : ℤ
n : ℕ
⊢ m ∣ ↑n ↔ m.natAbs ∣ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MulZeroOneClass α
P : Prop
inst✝ : Decidable P
a : α
⊢ (if P then 1 else 0) * a = if P then a else 0

Tactic:
by

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

Goal state before:
pp: m n : ℤ
⊢ (m % n).gcd n = m.gcd n

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
⊢ (a + b) * (a + b) = a * a + 2 * a * b + b * b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
⊢ (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
⊢ (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
a b : α
⊢ -a * -b = a * b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
a b : α
⊢ -a * b = a * -b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ -a = -1 * a

Tactic:
by

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

Goal state before:
pp: ⊢ AddCommMonoid ℕ

Tactic:
by

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

Goal state before:
pp: ⊢ AddMonoid ℕ

Tactic:
by

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

Goal state before:
pp: ⊢ Monoid ℕ

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ a * -1 = -a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ -1 * a = -a

Tactic:
by

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

Goal state before:
pp: ⊢ CommSemigroup ℕ

Tactic:
by

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

Goal state before:
pp: ⊢ Semigroup ℕ

Tactic:
by

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

Goal state before:
pp: ⊢ AddCommSemigroup ℕ

Tactic:
by

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

Goal state before:
pp: ⊢ AddSemigroup ℕ

Tactic:
by

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

Goal state before:
pp: α : Type u
R : Type v
inst✝¹ : MulZeroClass α
inst✝ : HasDistribNeg α
⊢ -0 = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ -a * b + a * b = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ a * -b + a * b = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : NonUnitalNonAssocRing α
a b c : α
⊢ a * (b - c) = a * b - a * c

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : NonUnitalNonAssocRing α
a b c : α
⊢ (a - b) * c = a * c - b * c

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ (a - 1) * b = a * b - b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ a * (b - 1) = a * b - a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ (1 - a) * b = b - a * b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ a * (1 - b) = a - a * b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b c : α
⊢ a * (1 - b) * c = a * c - a * b * c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Sqrt

Goal state before:
pp: n : ℤ
⊢ sqrt (n * n) = ↑n.natAbs

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Sqrt

Goal state before:
pp: x : ℤ
x✝ : ∃ n, n * n = x
n : ℤ
hn : n * n = x
⊢ sqrt x * sqrt x = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Sqrt

Goal state before:
pp: n : ℕ
⊢ sqrt ↑n = ↑n.sqrt

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
⊢ n.sqrt ^ 2 ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
⊢ n < n.sqrt.succ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
⊢ n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: m n : ℕ
⊢ m ≤ n.sqrt ↔ m ^ 2 ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: m n : ℕ
⊢ m.sqrt < n ↔ m < n * n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: m n : ℕ
⊢ m.sqrt < n ↔ m < n ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n a : ℕ
⊢ a = n.sqrt ↔ a ^ 2 ≤ n ∧ n < (a + 1) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
h : n.sqrt = 1
⊢ n.sqrt < 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
h : 1 < n
⊢ n < n * n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: a n : ℕ
h : a ≤ n + n
⊢ n * n + a < n.succ * n.succ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: a n : ℕ
h : a ≤ n + n
⊢ n * n ≤ n * n + a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: a n : ℕ
h : a ≤ n + n
⊢ (n ^ 2 + a).sqrt = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
this : n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt
⊢ n.succ < n.sqrt.succ.succ * n.sqrt.succ.succ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: ⊢ log2 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: ⊢ 0 = sqrt 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: ⊢ 1 = sqrt 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
h : n.sqrt = 0
this : n.sqrt < 1 ↔ n < 1 * 1
⊢ n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
⊢ n = 0 → n.sqrt = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: ⊢ 1 = sqrt 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (succ 0 + 1).sqrt ≤ succ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: x : ℕ
x✝ : ∃ n, n * n = x
n : ℕ
hn : n * n = x
⊢ x.sqrt * x.sqrt = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: x : ℕ
⊢ (∃ n, n ^ 2 = x) ↔ x.sqrt ^ 2 = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: m n : ℕ
hl : m * m < n
hr : n < (m + 1) * (m + 1)
⊢ ¬∃ t, t * t = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: m n : ℕ
⊢ m ^ 2 < n → n < (m + 1) ^ 2 → ¬∃ t, t ^ 2 = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: a b c : ℕ
h : a = b * c
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
a : α
f : F
x✝ : IsSquare a
r : α
h✝ : a = r * r
⊢ f a = f r * f r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
hf : Function.Surjective ⇑f
b : β
x✝ : b ∈ {b | IsSquare b}
r : α
h✝ : b = f r * f r
⊢ r * r ∈ {a | IsSquare a} ∧ f (r * r) = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
hf : Function.Surjective ⇑f
b : β
x✝ : b ∈ {b | IsSquare b}
s : β
h✝ : b = s * s
⊢ b ∈ ⇑f '' {a | IsSquare a}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
a : α
⊢ IsSquare a ↔ ∃ r, a = r ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Even

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
hn : Even n
⊢ ∀ (a : α), IsSquare (a ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: α : Type u_2
inst✝ : CommSemigroup α
a b : α
x✝¹ : IsSquare a
x✝ : IsSquare b
r : α
h✝¹ : a = r * r
s : α
h✝ : b = s * s
⊢ a * b = r * s * (r * s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
a : α
⊢ IsSquare a⁻¹ ↔ IsSquare a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ IsSquare a → IsSquare (a ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: α : Type u_2
inst✝ : DivisionCommMonoid α
a b : α
ha : IsSquare a
hb : IsSquare b
⊢ IsSquare (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: α : Type u_2
inst✝ : Group α
n : ℤ
⊢ Even n → ∀ (a : α), IsSquare (a ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
G : Type u_4
inst✝ : CommGroup G
a b c d e : G
ha : IsSquare a
n : ℕ
k : ℤ
hk : Even k
⊢ IsSquare (a * (b * b) / c ^ 2 * d ^ k * e ^ (n + n))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
G : Type u_4
inst✝ : AddCommGroup G
a b c d e : G
ha : Even a
n : ℕ
k : ℤ
hk : Even k
⊢ Even (a + (b + b) - 2 • c + k • d + (n + n) • e)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: n : ℕ
x✝ : Even n
m : ℕ
hm : n = m + m
⊢ n % 2 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: n : ℕ
h : n % 2 = 0
⊢ n = n / 2 + n / 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m✝ n m : ℕ
⊢ IsSquare m ↔ m.sqrt * m.sqrt = m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: n : ℕ
⊢ ¬Even n ↔ n % 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: n : ℕ
⊢ ¬2 ∣ n ↔ n % 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: ⊢ ¬Even 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m n : ℕ
⊢ Even (m + n) ↔ (Even m ↔ Even n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: n : ℕ
⊢ Even (n + 1) ↔ ¬Even n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m : ℕ
⊢ (m + 1) % 2 = 0 ↔ m % 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m : ℕ
⊢ (m + 1) % 2 = 1 ↔ m % 2 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: n : ℕ
⊢ ¬2 ∣ 2 * n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: n : ℕ
⊢ 0 < n → ¬2 ∣ 2 * n - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ (Even m ↔ Even n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m n : ℕ
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m n : ℕ
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m n : ℕ
h : n ≠ 0
⊢ Even (m ^ n) ↔ Even m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: n : ℕ
⊢ Even (n * (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: n : ℕ
⊢ Even (n * (n - 1))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
hn : Even n
⊢ 1 < n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m n : ℕ
hn : Even n
hm : Even m
hnm : n < m
⊢ n + 1 < m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m✝ n✝ m n : ℕ
h : Even m
⊢ ¬Even (n + 3) ↔ Even (m ^ 2 + m + n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m✝ n✝ m n : ℕ
h : Even m
⊢ ¬Even (n + 3) ↔ Even (m ^ 2 + m + n)

Tactic:
by simp [*, parity_simps]

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m n : ℕ
⊢ ¬Even 25394535

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ ¬n % 2 = 1 ↔ n % 2 = 0

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ ¬n % 2 = 0 ↔ n % 2 = 1

Tactic:
by

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

Goal state before:
pp: n : ℤ
x✝ : Even n
m : ℤ
hm : n = m + m
⊢ n % 2 = 0

Tactic:
by

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

Goal state before:
pp: n : ℤ
h : n % 2 = 0
⊢ n = n / 2 + n / 2

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ ¬Even n ↔ n % 2 = 1

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ ¬2 ∣ n ↔ n % 2 = 1

Tactic:
by

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

Goal state before:
pp: m✝ n m : ℤ
⊢ IsSquare m ↔ sqrt m * sqrt m = m

Tactic:
by

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

Goal state before:
pp: ⊢ ¬Even 1

Tactic:
by

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

Goal state before:
pp: m n : ℤ
⊢ Even (m + n) ↔ (Even m ↔ Even n)

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ ¬2 ∣ 2 * n + 1

Tactic:
by

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

Goal state before:
pp: m n : ℤ
⊢ Even (m - n) ↔ (Even m ↔ Even n)

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ Even (n + 1) ↔ ¬Even n

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ Even (n - 1) ↔ ¬Even n

Tactic:
by

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

Goal state before:
pp: m n : ℤ
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
by

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

Goal state before:
pp: m : ℤ
n : ℕ
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0

Tactic:
by

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

Goal state before:
pp: m : ℤ
n : ℕ
h : n ≠ 0
⊢ Even (m ^ n) ↔ Even m

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Even ↑n ↔ Even n

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ Even n → 2 * (n / 2) = n

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ Even n → n / 2 * 2 = n

Tactic:
by

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

Goal state before:
pp: m✝ n✝ m n : ℤ
h : Even m
⊢ ¬Even (n + 3) ↔ Even (m ^ 2 + m + n)

Tactic:
by

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

Goal state before:
pp: m n : ℤ
⊢ ¬Even 25394535

Tactic:
by

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

Goal state before:
pp: ⊢ 0 = 0 * 0

Tactic:
by

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

Goal state before:
pp: i✝ : ℕ
a✝ : IsSquare (-↑i✝).sign ↔ 0 ≤ -↑i✝
⊢ -↑i✝ - 1 < 0

Tactic:
by

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

Goal state before:
pp: case pred
i✝ : ℕ
a✝ : IsSquare (-↑i✝).sign ↔ 0 ≤ -↑i✝
⊢ IsSquare (-1) ↔ 0 ≤ -(↑i✝ + 1)

Tactic:
Int.neg_nonneg

Goal state after:
case pred
i✝ : ℕ
a✝ : IsSquare (-↑i✝).sign ↔ 0 ≤ -↑i✝
⊢ IsSquare (-1) ↔ ↑i✝ + 1 ≤ 0
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: z : ℤ
⊢ IsSquare z.sign ↔ 0 ≤ z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: A : Type u_2
F : Type u_4
inst✝² : FunLike F ℕ A
inst✝¹ : AddZeroClass A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : f 1 = g 1
⊢ ∀ (x : ℕ), f x = g x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: M : Type u_1
inst✝ : AddMonoid M
f : ℕ →+ M
n : ℕ
⊢ f n = n • f 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
f : Multiplicative ℕ →* M
n : Multiplicative ℕ
⊢ f n = f (ofAdd 1) ^ toAdd n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
b c a : α
h : b ∣ c
⊢ a * b ∣ a * c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
b c a : α
h : b ∣ᵣ c
⊢ b * a ∣ᵣ c * a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
a b : α
x✝ : a ∣ᵣ b
c : α
hc : b = c * a
⊢ MulOpposite.op b = MulOpposite.op a * MulOpposite.op c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
f g : Multiplicative ℕ →* M
h : f (ofAdd 1) = g (ofAdd 1)
n : Multiplicative ℕ
⊢ f n = g n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
a b : α
x✝ : MulOpposite.op a ∣ MulOpposite.op b
c : αᵐᵒᵖ
hc : MulOpposite.op b = MulOpposite.op a * c
⊢ b = MulOpposite.unop c * a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : a = b
⊢ a ∣ b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b : M
n : ℕ
⊢ ((multiplesHom M).toFun (a + b)) n = ((multiplesHom M).toFun a + (multiplesHom M).toFun b) n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
m n : ℕ
a : α
h : m ≤ n
⊢ a ^ n = a ^ m * a ^ (n - m)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hab : a ∣ b
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ∣ b ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : a = b
⊢ a ∣ᵣ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : c * a = b
⊢ a * c = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b : α
⊢ (∃ c, b = c * a) → a ∣ b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : M
n : Multiplicative ℕ
⊢ ((powersHom M).toFun (a * b)) n = ((powersHom M).toFun a * (powersHom M).toFun b) n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b : α
h : a ∣ b
c : α
⊢ a ∣ c * b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a c e f : α
⊢ a * e * (c * f) = a * c * (e * f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : a * b ∣ c
d : α
ceq : c = a * b * d
⊢ b * (a * d) = c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommSemigroup α
inst✝ : DecompositionMonoid α
k m n : α
⊢ k ∣ m * n ↔ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b c : α
⊢ b = c * a ↔ b = a * c

Tactic:
by

Goal state after: