awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Inv M₁
inst_4 : Div M₁
inst_5 : Pow M₁ ℤ
inst_6 : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f x ^ Int.negSucc n = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
rw₁ : (f x ^ (n + 1))⁻¹ = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
rw₂ : (f x ^ (n + 1))⁻¹ = (f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)))⁻¹
rw₃ : (f x ^ (n + 1))⁻¹ = (HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ))⁻¹
rw₄ rw₅ : (f x ^ (n + 1))⁻¹ = (f x ^ n.succ)⁻¹
⊢ f (x ^ Int.negSucc n) = f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹

Tactic:
rw [zpow, zpow_negSucc, inv, zpow, zpow_natCast]

Premises used: zpow_natCast, zpow_negSucc
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Inv M₁
inst_4 : Div M₁
inst_5 : Pow M₁ ℤ
inst_6 : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
rw : (f (x * y))⁻¹ = f (y⁻¹ * x⁻¹)
rw₁ : (f x * f y)⁻¹ = f (y⁻¹ * x⁻¹)
rw₂ : (f y)⁻¹ * (f x)⁻¹ = f (y⁻¹ * x⁻¹)
rw₃ : (f y)⁻¹ * (f x)⁻¹ = f y⁻¹ * f x⁻¹
rw₄ : (f y)⁻¹ * (f x)⁻¹ = (f y)⁻¹ * f x⁻¹
rw₅ rw₆ : (f y)⁻¹ * (f x)⁻¹ = (f y)⁻¹ * (f x)⁻¹
⊢ f (x * y)⁻¹ = f (y⁻¹ * x⁻¹)

Tactic:
rw [inv, mul, mul_inv_rev, mul, inv, inv]

Premises used: mul_inv_rev
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Inv M₁
inst_4 : Div M₁
inst_5 : Pow M₁ ℤ
inst_6 : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
h : x * y = 1
rw : f (x * y) = 1
y₁ : M₁
rw₁ : f 1 = 1
rw₂ rw₃ : Eq.{u_2 + 1} (α := M₂) 1 1
⊢ f x * f y = 1

Tactic:
rw [← mul, h, one]
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Inv M₁
inst_4 : Div M₁
inst_5 : Pow M₁ ℤ
inst_6 : DivisionMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
h : x * y = 1
rw : (f x)⁻¹ = f y
rw₁ rw₂ : f y = f y
⊢ f x⁻¹ = f y

Tactic:
rw [inv, inv_eq_of_mul_eq_one_right (by rw [← mul, h, one])]

Premises used: inv_eq_of_mul_eq_one_right
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Inv M₁
inst_4 : Div M₁
inst_5 : Pow M₁ ℤ
inst_6 : Group M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
rw : f x⁻¹ * f x = f 1
rw₁ : (f x)⁻¹ * f x = f 1
rw₂ : 1 = f 1
rw₃ rw₄ : Eq.{u_2 + 1} (α := M₂) 1 1
⊢ f (x⁻¹ * x) = f 1

Tactic:
rw [mul, inv, inv_mul_cancel, one]

Premises used: inv_mul_cancel
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : Semigroup M₁
f : M₁ → M₂
hf : Surjective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
⊢ f x * f y * f z = f x * (f y * f z)

Tactic:
simp only [← mul, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : CommMagma M₁
f : M₁ → M₂
hf : Surjective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y : M₁
rw : f (x * y) = f y * f x
rw₁ : f (x * y) = f (y * x)
rw₂ rw₃ : f (y * x) = f (y * x)
⊢ f x * f y = f y * f x

Tactic:
rw [← mul, ← mul, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
rw : f 1 * f x = f x
rw₁ : f (1 * x) = f x
rw₂ rw₃ : f x = f x
⊢ 1 * f x = f x

Tactic:
rw [← one, ← mul, one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
rw : f x * f 1 = f x
rw₁ : f (x * 1) = f x
rw₂ rw₃ : f x = f x
⊢ f x * 1 = f x

Tactic:
rw [← one, ← mul, mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Monoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
rw : f (HPow.hPow (β := ℕ) x 0) = 1
rw₁ : f 1 = 1
rw₂ rw₃ : f 1 = f 1
⊢ HPow.hPow (β := ℕ) (f x) 0 = 1

Tactic:
rw [← npow, pow_zero, ← one]

Premises used: pow_zero
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Monoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f (x ^ (n + 1)) = f x ^ n * f x
rw₁ : f (x ^ n * x) = f x ^ n * f x
rw₂ : f (x ^ n * x) = f (x ^ n) * f x
rw₃ rw₄ : f (x ^ n * x) = f (x ^ n * x)
⊢ f x ^ (n + 1) = f x ^ n * f x

Tactic:
rw [← npow, pow_succ, ← npow, ← mul]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂_1 : Type u_2
inst : Mul M₂_1
inst_1 : One M₂_1
inst_2 : Pow M₂_1 ℕ
M₂ : Type u_3
inst_3 : Inv M₂
inst_4 : InvolutiveInv M₁
f : M₁ → M₂
hf : Surjective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
rw : (f x⁻¹)⁻¹ = f x
rw₁ : f x⁻¹⁻¹ = f x
rw₂ rw₃ : f x = f x
⊢ (f x)⁻¹⁻¹ = f x

Tactic:
rw [← inv, ← inv, inv_inv]

Premises used: inv_inv
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
rw : f x / f y = f x * f y⁻¹
rw₁ : f x / f y = f (x * y⁻¹)
rw₂ : f (x / y) = f (x * y⁻¹)
rw₃ rw₄ : f (x * y⁻¹) = f (x * y⁻¹)
⊢ f x / f y = f x * (f y)⁻¹

Tactic:
rw [← inv, ← mul, ← div, div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
rw : f (HPow.hPow (β := ℤ) x 0) = 1
rw₁ : f 1 = 1
rw₂ rw₃ : f 1 = f 1
⊢ HPow.hPow (β := ℤ) (f x) 0 = 1

Tactic:
rw [← zpow, zpow_zero, ← one]

Premises used: zpow_zero
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
rw₁ : f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
rw₂ : f (x ^ n.succ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
rw₃ : f (x ^ n.succ) = f (x ^ n) * f x
rw₄ : f (x ^ n * x) = f (x ^ n) * f x
rw₅ rw₆ : f (x ^ n * x) = f (x ^ n * x)
⊢ HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x

Tactic:
rw [← zpow, ← zpow, zpow_natCast, zpow_natCast, pow_succ, ← mul]

Premises used: zpow_natCast, pow_succ
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f (x ^ Int.negSucc n) = (HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ))⁻¹
rw₁ : f (x ^ Int.negSucc n) = (f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)))⁻¹
rw₂ : f (x ^ (n + 1))⁻¹ = (f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)))⁻¹
rw₃ : f (x ^ (n + 1))⁻¹ = (f (x ^ n.succ))⁻¹
rw₄ rw₅ : (f (x ^ (n + 1)))⁻¹ = (f (x ^ n.succ))⁻¹
⊢ f x ^ Int.negSucc n = (HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ))⁻¹

Tactic:
rw [← zpow, ← zpow, zpow_negSucc, zpow_natCast, inv]

Premises used: zpow_natCast, zpow_negSucc
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₂
inst_1 : One M₂
inst_2 : Pow M₂ ℕ
inst_3 : Inv M₂
inst_4 : Div M₂
inst_5 : Pow M₂ ℤ
inst_6 : Group M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
rw : f x⁻¹ * f x = 1
rw₁ : f (x⁻¹ * x) = 1
rw₂ : f 1 = 1
rw₃ rw₄ : Eq.{u_2 + 1} (α := M₂) 1 1
⊢ (f x)⁻¹ * f x = 1

Tactic:
rw [← inv, ← mul, inv_mul_cancel, one]

Premises used: inv_mul_cancel
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
x : ℤ
⊢ HPow.hPow (β := ℕ) x 0 = 1

Tactic:
simp [Int.pow_zero]

Premises used: Int.pow_zero
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
x : ℕ
x_1 : ℤ
⊢ x_1 ^ (x + 1) = x_1 ^ x * x_1

Tactic:
simp [Int.pow_succ]

Premises used: Int.pow_succ
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
n : ℕ
x : ℤ
rw : (↑n : ℤ) * x + 1 * x = (↑n : ℤ) * x + x
rw₁ rw₂ : (↑n : ℤ) * x + x = (↑n : ℤ) * x + x
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * x = (↑n : ℤ) * x + x

Tactic:
rw [Int.add_mul, Int.one_mul]

Premises used: Int.one_mul, Int.add_mul
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
m : ℕ
n : ℤ
⊢ (↑m.succ : ℤ) * n = (↑m : ℤ) * n + n

Tactic:
simp only [natCast_succ, Int.add_mul, Int.add_comm, Int.one_mul]

Premises used: Int.one_mul, Int.add_comm, Int.natCast_succ, Int.add_mul
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
m : ℕ
n : ℤ
⊢ -[m+1] * n = -((↑m.succ : ℤ) * n)

Tactic:
simp only [negSucc_eq, natCast_succ, Int.neg_mul]

Premises used: Int.natCast_succ, Int.negSucc_eq, Int.neg_mul
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
_n : ℕ
hn : _n ≠ 0
_x _y : ℤ
⊢ Ne (α := ℤ) (↑_n : ℤ) 0

Tactic:
lia
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
⊢ AddCommMonoid ℤ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
⊢ AddMonoid ℤ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
⊢ Monoid ℤ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
⊢ CommSemigroup ℤ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
⊢ Semigroup ℤ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
⊢ AddGroup ℤ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
⊢ AddCommSemigroup ℤ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
⊢ AddSemigroup ℤ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
n : ℕ
a : ℤ
⊢ n • a = (↑n : ℤ) * a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
n a : ℤ
⊢ n • a = n * a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
a b : ℤ
⊢ a • b = a * b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Int.Defs
Goal:
n : ℤ
⊢ HSMul.hSMul (β := ℤ) n 1 = n

Tactic:
mul_one _

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
n : ℤ
⊢ ¬n % 2 = 1 ↔ n % 2 = 0

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
⊢ HMod.hMod (α := ℤ) 1 2 = 1

Tactic:
rfl

Premises used: Int.emod, rfl
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
n : ℤ
⊢ ¬n % 2 = 0 ↔ n % 2 = 1

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
n : ℤ
h : Even n
m : ℤ
hm : n = m + m
⊢ n % 2 = 0

Tactic:
simp [← Int.two_mul, hm]

Premises used: Int.two_mul
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
n : ℤ
h : n % 2 = 0
⊢ n = n / 2 + n / 2

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
n : ℤ
⊢ ¬Even n ↔ n % 2 = 1

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
n : ℤ
⊢ ¬2 ∣ n ↔ n % 2 = 1

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m_1 n m : ℤ
simp_rw : IsSquare m ↔ ∃ (n : ℤ), n * n = m
simp_rw₁ : (∃ (r : ℤ), m = r * r) ↔ ∃ (n : ℤ), n * n = m
⊢ IsSquare m ↔ sqrt m * sqrt m = m

Tactic:
simp_rw [← exists_mul_self m, IsSquare, eq_comm]

Premises used: eq_comm, Int.exists_mul_self, IsSquare
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
⊢ ¬Even (α := ℤ) 1

Tactic:
simp [even_iff]

Premises used: Int.even_iff
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m n : ℤ
⊢ Even (m + n) ↔ (Even m ↔ Even n)

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
n : ℤ
⊢ ¬2 ∣ 2 * n + 1

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m n : ℤ
⊢ Even (m - n) ↔ (Even m ↔ Even n)

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
n : ℤ
⊢ Even (n + 1) ↔ ¬Even n

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
n : ℤ
⊢ Even (n - 1) ↔ ¬Even n

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m n : ℤ
inl : ∀ (h₁ : m % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
inr : ∀ (h₁ : m % 2 = 1), Even (m * n) ↔ Even m ∨ Even n
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
rcases emod_two_eq_zero_or_one m with h₁ | h₁

Premises used: Int.emod_two_eq_zero_or_one
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m n : ℤ
h₁ : m % 2 = 0
inl : ∀ (h₂ : n % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
inl₁ : ∀ (h₂ : n % 2 = 1), Even (m * n) ↔ Even m ∨ Even n
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
rcases emod_two_eq_zero_or_one n with h₂ | h₂

Premises used: Int.emod_two_eq_zero_or_one
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m n : ℤ
h₁ : m % 2 = 1
inr : ∀ (h₂ : n % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
inr₁ : ∀ (h₂ : n % 2 = 1), Even (m * n) ↔ Even m ∨ Even n
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
rcases emod_two_eq_zero_or_one n with h₂ | h₂

Premises used: Int.emod_two_eq_zero_or_one
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
simp [even_iff, h₁, h₂, Int.mul_emod]

Premises used: Int.even_iff, Int.mul_emod
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
simp [even_iff, h₁, h₂, Int.mul_emod]

Premises used: Int.even_iff, Int.mul_emod
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
simp [even_iff, h₁, h₂, Int.mul_emod]

Premises used: Int.even_iff, Int.mul_emod
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
simp [even_iff, h₁, h₂, Int.mul_emod]

Premises used: Int.even_iff, Int.mul_emod
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m : ℤ
⊢ Even (HPow.hPow (β := ℕ) m 0) ↔ Even m ∧ Ne (α := ℕ) 0 0

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m : ℤ
n : ℕ
h : Even (m ^ n) ↔ Even m ∧ n ≠ 0
⊢ Even (m ^ (n + 1)) ↔ Even m ∧ n + 1 ≠ 0

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m : ℤ
n : ℕ
zero : Even (HPow.hPow (β := ℕ) m 0) ↔ Even m ∧ Ne (α := ℕ) 0 0
succ : ∀ (n : ℕ), (Even (m ^ n) ↔ Even m ∧ n ≠ 0) → (Even (m ^ (n + 1)) ↔ Even m ∧ n + 1 ≠ 0)
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0

Tactic:
induction n with grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m : ℤ
n : ℕ
h : n ≠ 0
⊢ Even (m ^ n) ↔ Even m

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
n : ℕ
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ : HMod.hMod (α := ℤ) (↑n : ℤ) 2 = 0 ↔ Even n
⊢ Even (α := ℤ) (↑n : ℤ) ↔ Even n

Tactic:
rw_mod_cast [even_iff, Nat.even_iff]

Premises used: Int.even_iff, Nat.even_iff
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
n : ℤ
⊢ Even n → 2 * (n / 2) = n

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
n : ℤ
⊢ Even n → n / 2 * 2 = n

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m_1 n_1 m n : ℤ
h : Even m
⊢ ¬Even (n + 3) ↔ Even (HPow.hPow (β := ℕ) m 2 + m + n)

Tactic:
simp +decide [*, parity_simps]

Premises used: Decidable.decide
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
m n : ℤ
⊢ ¬Even (α := ℤ) 25394535

Tactic:
decide
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
⊢ 0 = HMul.hMul (α := ℤ) 0 0

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
⊢ IsSquare (sign 0) ↔ LE.le (α := ℤ) 0 0

Tactic:
simpa using ⟨0, by simp⟩
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
i : ℕ
h : IsSquare (sign (↑i : ℤ)) ↔ LE.le (α := ℤ) 0 (↑i : ℤ)
succ : IsSquare (sign (↑(i + 1) : ℤ)) ↔ 0 ≤ i + 1
⊢ IsSquare (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1).sign ↔ 0 ≤ HAdd.hAdd (α := ℤ) (↑i : ℤ) 1

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
i : ℕ
h : IsSquare (sign (↑i : ℤ)) ↔ LE.le (α := ℤ) 0 (↑i : ℤ)
⊢ IsSquare (sign (↑(i + 1) : ℤ)) ↔ 0 ≤ i + 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
i : ℕ
h : IsSquare (sign (-(↑i : ℤ))) ↔ LE.le (α := ℤ) 0 (-(↑i : ℤ))
⊢ HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1 < 0

Tactic:
lia
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
i : ℕ
h : IsSquare (sign (-(↑i : ℤ))) ↔ LE.le (α := ℤ) 0 (-(↑i : ℤ))
pred : IsSquare (α := ℤ) (-1) ↔ HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 ≤ 0
⊢ IsSquare (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1).sign ↔ 0 ≤ HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1

Tactic:
rw [sign_eq_neg_one_of_neg (by lia), ← neg_add', Int.neg_nonneg]

Premises used: Int.sign_eq_neg_one_of_neg, neg_add', Int.neg_nonneg
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
i : ℕ
h : IsSquare (sign (-(↑i : ℤ))) ↔ LE.le (α := ℤ) 0 (-(↑i : ℤ))
pred : IsSquare (α := ℤ) (-1) ↔ i + 1 ≤ 0
⊢ IsSquare (α := ℤ) (-1) ↔ HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 ≤ 0

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
i : ℕ
h : IsSquare (sign (-(↑i : ℤ))) ↔ LE.le (α := ℤ) 0 (-(↑i : ℤ))
pred : ¬IsSquare (α := ℤ) (-1)
⊢ IsSquare (α := ℤ) (-1) ↔ i + 1 ≤ 0

Tactic:
simp only [reduceNeg, le_zero_eq, Nat.add_eq_zero_iff, succ_ne_self, and_false, iff_false]

Premises used: iff_false, Int.reduceNeg, Nat.succ_ne_self, Nat.le_zero_eq, and_false, Nat.add_eq_zero_iff
-- Module: Mathlib.Algebra.Group.Int.Even
Goal:
z : ℤ
zero : IsSquare (sign 0) ↔ LE.le (α := ℤ) 0 0
succ :
  ∀ (i : ℕ),
    (IsSquare (sign (↑i : ℤ)) ↔ LE.le (α := ℤ) 0 (↑i : ℤ)) →
      (IsSquare (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1).sign ↔ 0 ≤ HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)
pred :
  ∀ (i : ℕ),
    (IsSquare (sign (-(↑i : ℤ))) ↔ LE.le (α := ℤ) 0 (-(↑i : ℤ))) →
      (IsSquare (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1).sign ↔ 0 ≤ HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)
⊢ IsSquare z.sign ↔ 0 ≤ z

Tactic:
induction z using Int.induction_on with
  | zero => simpa using ⟨0, by simp⟩
  | succ => norm_cast; simp
  | pred =>
    rw [sign_eq_neg_one_of_neg (by lia), ← neg_add', Int.neg_nonneg]
    norm_cast
    simp only [reduceNeg, le_zero_eq, Nat.add_eq_zero_iff, succ_ne_self, and_false, iff_false]
    rintro ⟨a | a, ⟨⟩⟩

Premises used: iff_false, Int.pred, Int.sign_eq_neg_one_of_neg, Int.reduceNeg, Nat.succ_ne_self, neg_add', Nat.le_zero_eq, Int.succ, Int.neg_nonneg, Nat.zero, and_false, Nat.add_eq_zero_iff
-- Module: Mathlib.Algebra.Group.Int.TypeTags
Goal:
a : Multiplicative ℤ
b : ℕ
⊢ (toAdd : (a : Multiplicative ℤ) → ℤ) (a ^ b) =
    HMul.hMul (α := ℤ) (β := ℤ) ((toAdd : (a : Multiplicative ℤ) → ℤ) a : ℤ) ((↑b : ℤ) : ℤ)

Tactic:
mul_comm _ _

Premises used: Int.mul, mul_comm
-- Module: Mathlib.Algebra.Group.Int.TypeTags
Goal:
a : Multiplicative ℤ
b : ℤ
⊢ (toAdd : (a : Multiplicative ℤ) → ℤ) (a ^ b) = HMul.hMul (α := ℤ) ((toAdd : (a : Multiplicative ℤ) → ℤ) a : ℤ) b

Tactic:
mul_comm _ _

Premises used: Int.mul, mul_comm
-- Module: Mathlib.Algebra.Group.Int.TypeTags
Goal:
a b : ℤ
⊢ (ofAdd : (a : ℤ) → Multiplicative ℤ) (a * b) =
    HPow.hPow (α := Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) a : Multiplicative ℤ) b

Tactic:
(toAdd_zpow ..).symm

Premises used: Multiplicative, Int.toAdd_zpow, Int.mul, Eq.symm
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u : ℤˣ
rw : natAbs 1 = 1
⊢ (↑u : ℤ).natAbs * (↑u⁻¹ : ℤ).natAbs = 1

Tactic:
rw [← natAbs_mul, Units.mul_inv]

Premises used: Int.natAbs_mul, Units.mul_inv
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u : ℤˣ
⊢ natAbs 1 = 1

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u : ℤˣ
rw : natAbs 1 = 1
⊢ (↑u⁻¹ : ℤ).natAbs * (↑u : ℤ).natAbs = 1

Tactic:
rw [← natAbs_mul, Units.inv_mul]

Premises used: Int.natAbs_mul, Units.inv_mul
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u : ℤ
hu : IsUnit u
⊢ u.natAbs = 1

Tactic:
units_natAbs hu.unit

Premises used: Int.units_natAbs, IsUnit.unit
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u : ℤ
hu : IsUnit u
⊢ u = 1 ∨ u = -1

Tactic:
simpa only [natAbs_of_isUnit hu] using natAbs_eq u

Premises used: Int.natAbs_eq, Int.natAbs_of_isUnit
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
hu : IsUnit u
hv : IsUnit v
inl : ∀ (hu : IsUnit (M := ℤ) 1), 1 ≠ v ↔ 1 = -v
inr : ∀ (hu : IsUnit (M := ℤ) (-1)), -1 ≠ v ↔ -1 = -v
⊢ u ≠ v ↔ u = -v

Tactic:
obtain rfl | rfl := isUnit_eq_one_or hu

Premises used: Int.isUnit_eq_one_or, rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
v : ℤ
hv : IsUnit v
hu : IsUnit (M := ℤ) 1
inl : ∀ (hv : IsUnit (M := ℤ) 1), Ne (α := ℤ) 1 1 ↔ Eq (α := ℤ) 1 (-1)
inl₁ : ∀ (hv : IsUnit (M := ℤ) (-1)), Ne (α := ℤ) 1 (-1) ↔ Eq (α := ℤ) 1 (- -1)
⊢ 1 ≠ v ↔ 1 = -v

Tactic:
obtain rfl | rfl := isUnit_eq_one_or hv

Premises used: Int.isUnit_eq_one_or, rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
v : ℤ
hv : IsUnit v
hu : IsUnit (M := ℤ) (-1)
inr : ∀ (hv : IsUnit (M := ℤ) 1), Ne (α := ℤ) (-1) 1 ↔ Eq (α := ℤ) (-1) (-1)
inr₁ : ∀ (hv : IsUnit (M := ℤ) (-1)), Ne (α := ℤ) (-1) (-1) ↔ Eq (α := ℤ) (-1) (- -1)
⊢ -1 ≠ v ↔ -1 = -v

Tactic:
obtain rfl | rfl := isUnit_eq_one_or hv

Premises used: Int.isUnit_eq_one_or, rfl
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
hu hv : IsUnit (M := ℤ) 1
⊢ Ne (α := ℤ) 1 1 ↔ Eq (α := ℤ) 1 (-1)

Tactic:
decide
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
hu : IsUnit (M := ℤ) 1
hv : IsUnit (M := ℤ) (-1)
⊢ Ne (α := ℤ) 1 (-1) ↔ Eq (α := ℤ) 1 (- -1)

Tactic:
decide
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
hu : IsUnit (M := ℤ) (-1)
hv : IsUnit (M := ℤ) 1
⊢ Ne (α := ℤ) (-1) 1 ↔ Eq (α := ℤ) (-1) (-1)

Tactic:
decide
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
hu hv : IsUnit (M := ℤ) (-1)
⊢ Ne (α := ℤ) (-1) (-1) ↔ Eq (α := ℤ) (-1) (- -1)

Tactic:
decide
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u v : ℤ
hu : IsUnit u
hv : IsUnit v
⊢ u = v ∨ u = -v

Tactic:
or_iff_not_imp_left.2 (isUnit_ne_iff_eq_neg hu hv).1

Premises used: Iff.mpr, Int.isUnit_ne_iff_eq_neg, Classical.or_iff_not_imp_left, Iff.mp
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u : ℤ
⊢ IsUnit u ↔ u = 1 ∨ u = -1

Tactic:
⟨fun h ↦ isUnit_eq_one_or h, fun h ↦ ?_⟩

Premises used: Int.isUnit_eq_one_or, Iff.intro
-- Module: Mathlib.Algebra.Group.Int.Units
Goal:
u : ℤ
refine : ∀ (h : u = 1 ∨ u = -1), IsUnit u
⊢ IsUnit u ↔ u = 1 ∨ u = -1

Tactic:
refine ⟨fun h ↦ isUnit_eq_one_or h, fun h ↦ ?_⟩