awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
a b : R
h₁ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (a + b) + b
h₂ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (b + a) + b
⊢ a + (a + b) + b = a + (b + a) + b

Tactic:
have := h₁.symm.trans h₂
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this_1 : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
a b : R
h₁ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (a + b) + b
h₂ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (b + a) + b
this : a + (a + b) + b = a + (b + a) + b
rwa : ∀ (this : a + (a + b) = a + (b + a)), a + b = b + a
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : a + b = b + a), a + b = b + a
⊢ a + b = b + a

Tactic:
rwa [add_left_inj, add_right_inj] at this

Premises used: add_left_inj, add_right_inj
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
rw rw₁ : 0 * a = 0 * a
⊢ 0 * a = HAdd.hAdd (α := R) 0 0 * a

Tactic:
rw [zero_add]
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
rw rw₁ : 0 * a + 0 * a = 0 * a + 0 * a
⊢ HAdd.hAdd (α := R) 0 0 * a = 0 * a + 0 * a

Tactic:
rw [right_distrib]
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
⊢ 0 * a = 0 * a + 0 * a

Tactic:
have : 0 * a = 0 * a + 0 * a :=
      calc 0 * a = (0 + 0) * a := by rw [zero_add]
      _ = 0 * a + 0 * a := by rw [right_distrib]
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this_1 : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
this : 0 * a = 0 * a + 0 * a
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : 0 * a = 0), 0 * a = 0
⊢ 0 * a = 0

Tactic:
rwa [left_eq_add] at this

Premises used: left_eq_add
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
rw rw₁ : a * 0 = a * 0
⊢ a * 0 = a * HAdd.hAdd (α := R) 0 0

Tactic:
rw [zero_add]
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
rw rw₁ : a * 0 + a * 0 = a * 0 + a * 0
⊢ a * HAdd.hAdd (α := R) 0 0 = a * 0 + a * 0

Tactic:
rw [left_distrib]
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
⊢ a * 0 = a * 0 + a * 0

Tactic:
have : a * 0 = a * 0 + a * 0 :=
      calc a * 0 = a * (0 + 0) := by rw [zero_add]
      _ = a * 0 + a * 0 := by rw [left_distrib]
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this_1 : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
this : a * 0 = a * 0 + a * 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : a * 0 = 0), a * 0 = 0
⊢ a * 0 = 0

Tactic:
rwa [left_eq_add] at this

Premises used: left_eq_add
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
a : R
rw : 1 * a = a
rw₁ rw₂ : a = a
⊢ a * 1 = a

Tactic:
rw [mul_comm, one_mul]
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
mul_one : ∀ (a : R), a * 1 = a
a b c : R
rw : c * (a + b) = a * c + b * c
rw₁ : c * a + c * b = a * c + b * c
rw₂ : a * c + c * b = a * c + b * c
rw₃ rw₄ : a * c + c * b = a * c + c * b
⊢ (a + b) * c = a * c + b * c

Tactic:
rw [mul_comm, left_distrib, mul_comm, mul_comm b c]
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
⊢ n.negOnePow = HPow.hPow (α := ℤˣ) (-1) n

Tactic:
rfl

Premises used: Int.negOnePow, rfl
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n₁ n₂ : ℤ
⊢ (n₁ + n₂).negOnePow = n₁.negOnePow * n₂.negOnePow

Tactic:
zpow_add _ _ _

Premises used: zpow_add, Int.negOnePow
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
⊢ negOnePow 0 = 1

Tactic:
rfl

Premises used: Int.pow, Int.negOnePow, rfl, ite
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
⊢ negOnePow 1 = -1

Tactic:
rfl

Premises used: Int.pow, Int.neg, Int.negOnePow, rfl, Int.negOfNat, ite
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
rw : n.negOnePow * negOnePow 1 = -n.negOnePow
rw₁ : n.negOnePow * -1 = -n.negOnePow
rw₂ : -(n.negOnePow * 1) = -n.negOnePow
rw₃ rw₄ : -n.negOnePow = -n.negOnePow
⊢ (n + 1).negOnePow = -n.negOnePow

Tactic:
rw [negOnePow_add, negOnePow_one, mul_neg, mul_one]

Premises used: Int.negOnePow_add, Int.negOnePow_one, mul_one, mul_neg
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
hn : Even n
obtain : ∀ (k : ℤ), (k + k).negOnePow = 1
⊢ n.negOnePow = 1

Tactic:
obtain ⟨k, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
k : ℤ
rw : k.negOnePow * k.negOnePow = 1
rw₁ rw₂ : Eq (α := ℤˣ) 1 1
⊢ (k + k).negOnePow = 1

Tactic:
rw [negOnePow_add, units_mul_self]

Premises used: Int.negOnePow_add, Int.units_mul_self
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
⊢ (2 * n).negOnePow = 1

Tactic:
negOnePow_even _ ⟨n, two_mul n⟩

Premises used: two_mul, Exists.intro, Int.negOnePow_even
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
hn : Odd n
obtain : ∀ (k : ℤ), (2 * k + 1).negOnePow = -1
⊢ n.negOnePow = -1

Tactic:
obtain ⟨k, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
k : ℤ
⊢ (2 * k + 1).negOnePow = -1

Tactic:
simp only [negOnePow_add, negOnePow_two_mul, negOnePow_one, mul_neg, mul_one]

Premises used: Int.negOnePow_two_mul, Int.negOnePow_add, Int.negOnePow_one, mul_one, mul_neg
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
⊢ (2 * n + 1).negOnePow = -1

Tactic:
negOnePow_odd _ ⟨n, rfl⟩

Premises used: Int.negOnePow_odd, Exists.intro, rfl
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
mp : n.negOnePow = 1 → Even n
mpr : Even n → n.negOnePow = 1
⊢ n.negOnePow = 1 ↔ Even n

Tactic:
constructor
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
h : n.negOnePow = 1
mp : ¬Odd n
⊢ Even n

Tactic:
rw [← Int.not_odd_iff_even]

Premises used: Int.not_odd_iff_even
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
h : n.negOnePow = 1
h' : Odd n
⊢ Eq (α := ℤˣ) (-1) 1

Tactic:
simp only [negOnePow_odd _ h'] at h

Premises used: Int.negOnePow_odd
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
h' : Odd n
h : Eq (α := ℤˣ) (-1) 1
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
⊢ Even n → n.negOnePow = 1

Tactic:
negOnePow_even n

Premises used: Int.negOnePow_even
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
⊢ Even n → n.negOnePow = 1

Tactic:
exact negOnePow_even n

Premises used: Int.negOnePow_even
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
mp : n.negOnePow = -1 → Odd n
mpr : Odd n → n.negOnePow = -1
⊢ n.negOnePow = -1 ↔ Odd n

Tactic:
constructor
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
h : n.negOnePow = -1
mp : ¬Even n
⊢ Odd n

Tactic:
rw [← Int.not_even_iff_odd]

Premises used: Int.not_even_iff_odd
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
h : n.negOnePow = -1
h' : Even n
⊢ Eq (α := ℤˣ) 1 (-1)

Tactic:
rw [negOnePow_even _ h'] at h

Premises used: Int.negOnePow_even
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
h : n.negOnePow = -1
h' : Even n
h₁ : Eq (α := ℤˣ) 1 (-1)
⊢ Even n

Tactic:
rw [negOnePow_even _ h'] at h

Premises used: Int.negOnePow_even
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
h : Eq (α := ℤˣ) 1 (-1)
h' : Even n
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
⊢ Odd n → n.negOnePow = -1

Tactic:
negOnePow_odd n

Premises used: Int.negOnePow_odd
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
⊢ Odd n → n.negOnePow = -1

Tactic:
exact negOnePow_odd n

Premises used: Int.negOnePow_odd
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
rw : Eq (α := ℤ) (↑(↑n.negOnePow : ℤ).natAbs : ℤ) 1
rw₁ : Eq (α := ℤ) (↑1 : ℤ) 1
rw₂ rw₃ : Eq (α := ℤ) 1 1
⊢ |(↑n.negOnePow : ℤ)| = 1

Tactic:
rw [abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]

Premises used: Int.units_natAbs, Nat.cast_one, Int.abs_eq_natAbs
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
⊢ HPow.hPow (α := ℤˣ) (-1) (-n) = HPow.hPow (α := ℤˣ) (-1) n

Tactic:
simp only [zpow_neg, ← inv_zpow, inv_neg, inv_one]

Premises used: inv_one, inv_zpow, inv_neg, zpow_neg
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
inl : ∀ (h : |n| = n), |n|.negOnePow = n.negOnePow
inr : ∀ (h : |n| = -n), |n|.negOnePow = n.negOnePow
⊢ |n|.negOnePow = n.negOnePow

Tactic:
obtain h | h := abs_choice n

Premises used: abs_choice
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
h : |n| = n
⊢ |n|.negOnePow = n.negOnePow

Tactic:
simp only [h, negOnePow_neg]

Premises used: Int.negOnePow_neg
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
h : |n| = -n
⊢ |n|.negOnePow = n.negOnePow

Tactic:
simp only [h, negOnePow_neg]

Premises used: Int.negOnePow_neg
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n₁ n₂ : ℤ
⊢ (n₁ - n₂).negOnePow = n₁.negOnePow * n₂.negOnePow

Tactic:
simp only [sub_eq_add_neg, negOnePow_add, negOnePow_neg]

Premises used: sub_eq_add_neg, Int.negOnePow_add, Int.negOnePow_neg
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n₁ n₂ : ℤ
pos : ∀ (h₂ : Even n₂), n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)
neg : ∀ (h₂ : ¬Even n₂), n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Tactic:
by_cases h₂ : Even n₂

Premises used: Even
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n₁ n₂ : ℤ
h₂ : Even n₂
pos : Even n₁ ↔ (Even n₁ ↔ Even n₂)
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Tactic:
rw [negOnePow_even _ h₂, Int.even_sub, negOnePow_eq_one_iff]

Premises used: Int.negOnePow_even, Int.even_sub, Int.negOnePow_eq_one_iff
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n₁ n₂ : ℤ
h₂ : Even n₂
pos : Even n₁ → (Even n₁ ↔ Even n₂)
pos₁ : (Even n₁ ↔ Even n₂) → Even n₁
pos₂ pos₃ : Even n₁ → (Even n₁ ↔ Even n₂)
pos₄ : Even n₁ → Even n₁ → Even n₂
pos₅ pos₆ : Even n₁ → Even n₂ → Even n₁
pos₇ : ¬Even n₁ → ¬Even n₂ → Even n₁
pos₈ pos₉ : Even n₁ → Even n₂ → Even n₁
pos₁₀ pos₁₁ pos₁₂ : Even n₁ → Even n₁ → Even n₂
pos₁₃ pos₁₄ pos₁₅ : Even n₁ → Even n₂ → Even n₁
⊢ Even n₁ ↔ (Even n₁ ↔ Even n₂)

Tactic:
tauto
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n₁ n₂ : ℤ
h₂ : ¬Even n₂
⊢ Odd n₂

Tactic:
rw [Int.not_even_iff_odd] at h₂

Premises used: Int.not_even_iff_odd
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n₁ n₂ : ℤ
h₂ : Odd n₂
neg : Odd n₁ ↔ (¬Odd n₁ ↔ ¬Odd n₂)
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Tactic:
rw [negOnePow_odd _ h₂, Int.even_sub, negOnePow_eq_neg_one_iff,
      ← Int.not_odd_iff_even, ← Int.not_odd_iff_even]

Premises used: Int.negOnePow_eq_neg_one_iff, Int.negOnePow_odd, Int.not_odd_iff_even, Int.even_sub
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n₁ n₂ : ℤ
h₂ : Odd n₂
neg : Odd n₁ → (¬Odd n₁ ↔ ¬Odd n₂)
neg₁ : (¬Odd n₁ ↔ ¬Odd n₂) → Odd n₁
neg₂ neg₃ : Odd n₁ → (¬Odd n₁ ↔ ¬Odd n₂)
neg₄ : Odd n₁ → ¬Odd n₁ → ¬Odd n₂
neg₅ : Odd n₁ → ¬Odd n₂ → ¬Odd n₁
neg₆ : ¬Odd n₁ → ¬Odd n₂ → Odd n₁
neg₇ neg₈ neg₉ : ¬¬Odd n₁ → ¬¬Odd n₂ → Odd n₁
neg₁₀ : Odd n₁ → ¬Odd n₁ → ¬Odd n₂
neg₁₁ : Odd n₁ → ¬Odd n₂ → ¬Odd n₁
neg₁₂ neg₁₃ neg₁₄ : Odd n₁ → Odd n₂ → Odd n₁
⊢ Odd n₁ ↔ (¬Odd n₁ ↔ ¬Odd n₂)

Tactic:
tauto
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℤ
⊢ (n * n).negOnePow = n.negOnePow

Tactic:
simpa [mul_sub, negOnePow_eq_iff] using n.even_mul_pred_self

Premises used: mul_sub, Int.negOnePow_eq_iff, Int.even_mul_pred_self
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
R : Type u_1
inst : Ring R
n : ℕ
inl : ∀ (k : ℕ), (↑(↑(negOnePow (↑(2 * k) : ℤ)) : ℤ) : R) = HPow.hPow (α := R) (-1) (2 * k)
inr : ∀ (k : ℕ), (↑(↑(negOnePow (↑(2 * k + 1) : ℤ)) : ℤ) : R) = HPow.hPow (α := R) (-1) (2 * k + 1)
⊢ (↑(↑(negOnePow (↑n : ℤ)) : ℤ) : R) = HPow.hPow (α := R) (-1) n

Tactic:
obtain ⟨k, rfl | rfl⟩ := Nat.even_or_odd' n

Premises used: Nat.even_or_odd', rfl
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
R : Type u_1
inst : Ring R
k : ℕ
⊢ (↑(↑(negOnePow (↑(2 * k) : ℤ)) : ℤ) : R) = HPow.hPow (α := R) (-1) (2 * k)

Tactic:
simp [pow_succ, pow_mul]

Premises used: pow_succ, pow_mul
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
R : Type u_1
inst : Ring R
k : ℕ
⊢ (↑(↑(negOnePow (↑(2 * k + 1) : ℤ)) : ℤ) : R) = HPow.hPow (α := R) (-1) (2 * k + 1)

Tactic:
simp [pow_succ, pow_mul]

Premises used: pow_succ, pow_mul
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
n : ℕ
⊢ (↑(negOnePow (↑n : ℤ)) : ℤ) = HPow.hPow (α := ℤ) (-1) n

Tactic:
cast_negOnePow_natCast ..

Premises used: Int.cast_negOnePow_natCast
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
R : Type u_1
inst : Ring R
n : ℕ
⊢ (↑(↑(ofNat n).negOnePow : ℤ) : R) = HPow.hPow (α := R) (-1) (ofNat n).natAbs

Tactic:
cast_negOnePow_natCast R n

Premises used: Int.natAbs, Int.cast_negOnePow_natCast
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
R : Type u_1
inst : Ring R
n : ℕ
⊢ (↑(↑(ofNat n).negOnePow : ℤ) : R) = HPow.hPow (α := R) (-1) (ofNat n).natAbs

Tactic:
exact cast_negOnePow_natCast R n

Premises used: Int.cast_negOnePow_natCast
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
R : Type u_1
inst : Ring R
n : ℕ
⊢ (↑(↑-[n+1].negOnePow : ℤ) : R) = HPow.hPow (α := R) (-1) -[n+1].natAbs

Tactic:
simp [negOnePow_def, Units.val_pow_eq_pow_val]

Premises used: Int.negOnePow_def, Units.val_pow_eq_pow_val
-- Module: Mathlib.Algebra.Ring.NegOnePow
Goal:
R : Type u_1
inst : Ring R
n : ℤ
ofNat : ∀ (n : ℕ), (↑(↑(Int.ofNat n).negOnePow : ℤ) : R) = HPow.hPow (α := R) (-1) (Int.ofNat n).natAbs
negSucc : ∀ (n : ℕ), (↑(↑-[n+1].negOnePow : ℤ) : R) = HPow.hPow (α := R) (-1) -[n+1].natAbs
⊢ (↑(↑n.negOnePow : ℤ) : R) = HPow.hPow (α := R) (-1) n.natAbs

Tactic:
cases n with
  | ofNat n => exact cast_negOnePow_natCast R n
  | negSucc n => simp [negOnePow_def, Units.val_pow_eq_pow_val]

Premises used: Int.ofNat, Int.negOnePow_def, Int.negSucc, Units.val_pow_eq_pow_val
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n_1 m_1 : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n_1) ((fun (n : ℕ) ↦ r ^ n) m_1)
n m : ℕ
h₁ : n ≤ m
h₂ : r ^ n = r ^ m
obtain : ∀ (l : ℕ) (h₁ : n ≤ n + l) (h₂ : r ^ n = r ^ (n + l)), n = n + l
⊢ n = m

Tactic:
obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le h₁

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n_1 m : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n_1) ((fun (n : ℕ) ↦ r ^ n) m)
n l : ℕ
h₁ : n ≤ n + l
h₂ : r ^ n = r ^ (n + l)
⊢ l = 0

Tactic:
rw [pow_add, eq_comm, IsLeftRegular.mul_left_eq_self_iff (hx.pow n), pow_eq_one_iff_right hx']
      at h₂

Premises used: pow_add, pow_eq_one_iff_right, eq_comm, IsLeftRegular.pow, IsLeftRegular.mul_left_eq_self_iff
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n_1 m : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n_1) ((fun (n : ℕ) ↦ r ^ n) m)
n l : ℕ
h₁ : n ≤ n + l
h₂ : l = 0
rw : n = n + 0
rw₁ rw₂ : n = n
⊢ n = n + l

Tactic:
rw [h₂, Nat.add_zero]

Premises used: Nat.add_zero
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n m : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n) ((fun (n : ℕ) ↦ r ^ n) m)
⊢ ∀ {n m : ℕ} (h₁ : n ≤ m) (h₂ : r ^ n = r ^ m), n = m

Tactic:
have main {n m} (h₁ : n ≤ m) (h₂ : r ^ n = r ^ m) : n = m := by
    obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le h₁
    rw [pow_add, eq_comm, IsLeftRegular.mul_left_eq_self_iff (hx.pow n), pow_eq_one_iff_right hx']
      at h₂
    rw [h₂, Nat.add_zero]
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n m : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n) ((fun (n : ℕ) ↦ r ^ n) m)
main : ∀ {n m : ℕ} (h₁ : n ≤ m) (h₂ : r ^ n = r ^ m), n = m
inl : ∀ (h : n ≤ m), n = m
inr : ∀ (h : m ≤ n), n = m
⊢ n = m

Tactic:
obtain h | h := Nat.le_or_le n m

Premises used: Nat.le_or_le
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n m : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n) ((fun (n : ℕ) ↦ r ^ n) m)
main : ∀ {n m : ℕ} (h₁ : n ≤ m) (h₂ : r ^ n = r ^ m), n = m
h : n ≤ m
⊢ n = m

Tactic:
main h hnm
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n m : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n) ((fun (n : ℕ) ↦ r ^ n) m)
main : ∀ {n m : ℕ} (h₁ : n ≤ m) (h₂ : r ^ n = r ^ m), n = m
h : n ≤ m
⊢ n = m

Tactic:
exact main h hnm
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n m : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n) ((fun (n : ℕ) ↦ r ^ n) m)
main : ∀ {n m : ℕ} (h₁ : n ≤ m) (h₂ : r ^ n = r ^ m), n = m
h : m ≤ n
⊢ n = m

Tactic:
(main h hnm.symm).symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
R : Type u_1
inst : Monoid R
r : R
inst_1 : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n m : ℕ
hnm : Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ r ^ n) n) ((fun (n : ℕ) ↦ r ^ n) m)
main : ∀ {n m : ℕ} (h₁ : n ≤ m) (h₂ : r ^ n = r ^ m), n = m
h : m ≤ n
⊢ n = m

Tactic:
exact (main h hnm.symm).symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
M : Type u_2
inst : Monoid M
inst_1 : IsMulTorsionFree M
x : M
hx : IsRightRegular x
hx' : x ≠ 1
⊢ Function.Injective.{1, u_2 + 1} (β := M) fun (n : ℕ) ↦ x ^ n

Tactic:
MulOpposite.unop_injective.comp <| (isLeftRegular_op.mpr hx).pow_injective <|
    (MulOpposite.op_eq_one_iff x).not.mpr hx'

Premises used: Iff.mpr, MulOpposite.op_eq_one_iff, Iff.not, IsLeftRegular.pow_injective, isLeftRegular_op, Function.Injective.comp, MulOpposite.unop, MulOpposite.unop_injective
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
M : Type u_2
inst : CancelMonoid M
inst_1 : IsMulTorsionFree M
x : M
hx : x ≠ 1
⊢ Function.Injective.{1, u_2 + 1} (β := M) fun (n : ℕ) ↦ x ^ n

Tactic:
IsLeftRegular.pow_injective (IsLeftRegular.all x) hx

Premises used: IsLeftRegular.all, IsLeftRegular.pow_injective
-- Module: Mathlib.Algebra.Ring.NonZeroDivisors
Goal:
M : Type u_2
inst : CancelMonoid M
inst_1 : IsMulTorsionFree M
x : M
hx : x ≠ 1
n m : ℕ
⊢ x ^ n = x ^ m ↔ n = m

Tactic:
(pow_right_injective hx).eq_iff

Premises used: Function.Injective.eq_iff, IsMulTorsionFree.pow_right_injective