awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Int.Defs
Goal:
α : Type u_1
inst : AddGroupWithOne α
m : ℤ
x : ℕ
ih : ∀ (n : ℤ), (↑((↑x : ℤ) * n) : α) = HSMul.hSMul (α := ℤ) (β := α) (↑x : ℤ) (↑n : α)
⊢ ∀ (n : ℤ), (↑(HAdd.hAdd (α := ℤ) (↑x : ℤ) 1 * n) : α) = HSMul.hSMul (β := α) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) (↑n : α)

Tactic:
simp [add_mul, add_zsmul, ih]

Premises used: add_mul, add_zsmul
-- Module: Mathlib.Algebra.Ring.Int.Defs
Goal:
α : Type u_1
inst : AddGroupWithOne α
m : ℤ
x : ℕ
ih : ∀ (n : ℤ), (↑(-(↑x : ℤ) * n) : α) = HSMul.hSMul (α := ℤ) (β := α) (-(↑x : ℤ)) (↑n : α)
⊢ ∀ (n : ℤ),
    (↑(HSub.hSub (α := ℤ) (-(↑x : ℤ)) 1 * n) : α) = HSMul.hSMul (β := α) (HSub.hSub (α := ℤ) (-(↑x : ℤ)) 1) (↑n : α)

Tactic:
simp only [sub_mul, one_mul, cast_sub, ih, sub_zsmul, one_zsmul, ← sub_eq_add_neg, forall_const]

Premises used: Int.cast_sub, sub_eq_add_neg, sub_zsmul, sub_mul, one_zsmul, forall_const, one_mul
-- Module: Mathlib.Algebra.Ring.Int.Defs
Goal:
R : Type u_1
inst : Ring R
n : ℤ
m : ℕ
zero : (↑(HPow.hPow (β := ℕ) n 0) : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0
succ :
  ∀ (n_1 : ℕ),
    (↑(n ^ n_1) : R) = HPow.hPow (α := R) (↑n : R) n_1 → (↑(n ^ (n_1 + 1)) : R) = HPow.hPow (α := R) (↑n : R) (n_1 + 1)
⊢ (↑(n ^ m) : R) = HPow.hPow (α := R) (↑n : R) m

Tactic:
induction m
-- Module: Mathlib.Algebra.Ring.Int.Defs
Goal:
R : Type u_1
inst : Ring R
n : ℤ
⊢ (↑(HPow.hPow (β := ℕ) n 0) : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0

Tactic:
simp [_root_.pow_succ, *]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Ring.Int.Defs
Goal:
R : Type u_1
inst : Ring R
n : ℤ
n_1 : ℕ
h : (↑(n ^ n_1) : R) = HPow.hPow (α := R) (↑n : R) n_1
⊢ (↑(n ^ (n_1 + 1)) : R) = HPow.hPow (α := R) (↑n : R) (n_1 + 1)

Tactic:
simp [_root_.pow_succ, *]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Ring.Int.Field
Goal:
h_1 : IsField ℤ
exists_pair_ne : ∃ (x : ℤ), ∃ (y : ℤ), x ≠ y
mul_comm : ∀ (x y : ℤ), x * y = y * x
h : ∀ {a : ℤ}, a ≠ 0 → ∃ (b : ℤ), a * b = 1
this : Ne (α := ℤ) 2 0 → ∃ (b : ℤ), 2 * b = 1
⊢ False

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
h : Odd n
m : ℤ
hm : n = 2 * m + 1
⊢ n % 2 = 1

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
h : n % 2 = 1
⊢ n = 2 * (n / 2) + 1

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
⊢ ¬Odd n ↔ n % 2 = 0

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
⊢ ¬Odd (α := ℤ) 0

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
⊢ ¬Odd n ↔ Even n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
⊢ ¬Even n ↔ Odd n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
⊢ Even n ∨ Odd n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
⊢ ∃ (k : ℤ), n = 2 * k ∨ n = 2 * k + 1

Tactic:
simpa only [two_mul, exists_or, Odd, Even] using even_or_odd n

Premises used: exists_or, Odd, two_mul, Int.even_or_odd, Even
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
⊢ Xor (Even n) (Odd n)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
inl : ∀ (k : ℤ), ∃ (k_1 : ℤ), Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)
inr : ∀ (k : ℤ), ∃ (k_1 : ℤ), Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)
⊢ ∃ (k : ℤ), Xor (n = 2 * k) (n = 2 * k + 1)

Tactic:
rcases even_or_odd n with (⟨k, rfl⟩ | ⟨k, rfl⟩)

Premises used: Int.even_or_odd, rfl
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
k : ℤ
h : Xor (k + k = 2 * k) (k + k = 2 * k + 1)
⊢ ∃ (k_1 : ℤ), Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)

Tactic:
use k
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
k : ℤ
⊢ Xor (k + k = 2 * k) (k + k = 2 * k + 1)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
k : ℤ
h : Xor (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)
⊢ ∃ (k_1 : ℤ), Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)

Tactic:
use k
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
k : ℤ
⊢ Xor (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
m n : ℤ
⊢ Even (m + n) ↔ (Odd m ↔ Odd n)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
⊢ ¬Even (2 * n + 1)

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

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
m n : ℤ
⊢ Odd (m * n) ↔ Odd m ∧ Odd n

Tactic:
simp [← not_even_iff_odd, not_or, parity_simps]

Premises used: not_or, Int.not_even_iff_odd
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
m n : ℤ
h : Odd (m * n)
⊢ Odd m

Tactic:
(odd_mul.mp h).1

Premises used: Int.odd_mul, And.left, Iff.mp
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
m n : ℤ
h : Odd (m * n)
⊢ Odd n

Tactic:
(odd_mul.mp h).2

Premises used: Int.odd_mul, And.right, Iff.mp
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
m : ℤ
n : ℕ
⊢ Odd (m ^ n) ↔ Odd m ∨ n = 0

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
m : ℤ
n : ℕ
h : n ≠ 0
⊢ Odd (m ^ n) ↔ Odd m

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
m n : ℤ
⊢ Odd (m + n) ↔ (Odd m ↔ Even n)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
m n : ℤ
⊢ Odd (m + n) ↔ (Odd n ↔ Even m)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
m n : ℤ
h : Odd (m + n)
⊢ m ≠ n

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

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

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
⊢ Even (n * (n + 1))

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
⊢ Even (n * (n - 1))

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℕ
⊢ Odd (α := ℤ) (↑n : ℤ) ↔ Odd n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
⊢ Even n.natAbs ↔ Even n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
⊢ Odd n.natAbs ↔ Odd n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
a b : ℤ
ha : Odd a
hb : Odd b
⊢ 4 ∣ a + b ∨ 4 ∣ a - b

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
k : ℤ
⊢ 2 ∣ k * (k + 1)

Tactic:
even_iff_two_dvd.mp (even_mul_succ_self k)

Premises used: Int.even_mul_succ_self, Iff.mp, even_iff_two_dvd
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
⊢ Odd n → 2 * (n / 2) + 1 = n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
⊢ Odd n → n / 2 * 2 + 1 = n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
⊢ Odd n → 1 + n / 2 * 2 = n

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℤ
h : Odd n
⊢ 2 * (n / 2) = n - 1

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
z : ℤ
⊢ Even z.sign ↔ z = 0

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
z : ℤ
⊢ Odd z.sign ↔ z ≠ 0

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℕ
mp : IsSquare (α := ℤ) (↑n : ℤ) → IsSquare n
mpr : IsSquare n → IsSquare (α := ℤ) (↑n : ℤ)
⊢ IsSquare (α := ℤ) (↑n : ℤ) ↔ IsSquare n

Tactic:
constructor
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℕ
x : ℤ
h : (↑n : ℤ) = x * x
⊢ IsSquare n

Tactic:
⟨x.natAbs, (natAbs_mul_natAbs_eq h.symm).symm⟩

Premises used: Int.natAbs_mul_natAbs_eq, Int.natAbs, IsSquare, Exists.intro, Eq.symm
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℕ
x : ℤ
h : (↑n : ℤ) = x * x
⊢ IsSquare n

Tactic:
exact ⟨x.natAbs, (natAbs_mul_natAbs_eq h.symm).symm⟩
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n x : ℕ
h : n = x * x
⊢ IsSquare (α := ℤ) (↑n : ℤ)

Tactic:
⟨x, mod_cast h⟩

Premises used: Nat.cast_mul._simp_1, congrArg, cast, Nat.cast, IsSquare, Exists.intro, Nat.cast_inj._simp_1, Eq.symm, Eq, Eq.trans
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n x : ℕ
h : n = x * x
⊢ IsSquare (α := ℤ) (↑n : ℤ)

Tactic:
exact ⟨x, mod_cast h⟩
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
n : ℕ
⊢ IsSquare (α := ℤ) (OfNat.ofNat n) ↔ IsSquare (α := ℕ) (OfNat.ofNat n)

Tactic:
isSquare_natCast_iff

Premises used: Int.isSquare_natCast_iff
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
b p : ℕ
w : 0 < b
⊢ 1 ≤ b ^ p

Tactic:
have : 1 ≤ b ^ p := Nat.one_le_pow p b w
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
b p : ℕ
w : 0 < b
this : 1 ≤ b ^ p
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : b ^ p - 1 = b ^ p - 1
⊢ (↑(b ^ p - 1) : ℤ) = HPow.hPow (α := ℤ) (↑b : ℤ) p - 1

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
p : ℕ
⊢ LT.lt (α := ℕ) 0 2

Tactic:
decide
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
n : ℤ
h : Odd n
a : α
obtain : ∀ (k : ℤ), (-a) ^ (2 * k + 1) = -a ^ (2 * k + 1)
⊢ (-a) ^ n = -a ^ n

Tactic:
obtain ⟨k, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
a : α
k : ℕ
ofNat : (-a) ^ (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) = -a ^ (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1)
⊢ (-a) ^ (2 * Int.ofNat k + 1) = -a ^ (2 * Int.ofNat k + 1)

Tactic:
rw [Int.ofNat_eq_natCast]

Premises used: Int.ofNat_eq_natCast
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
a : α
k : ℕ
ofNat : (-a) ^ (2 * k + 1) = -a ^ (2 * k + 1)
⊢ (-a) ^ (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) = -a ^ (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
a : α
k : ℕ
⊢ (-a) ^ (2 * k + 1) = -a ^ (2 * k + 1)

Tactic:
simp [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
a : α
k : ℕ
⊢ 2 * -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 + 1 = -(1 + HMul.hMul (α := ℤ) (↑k : ℤ) 2)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
a : α
k : ℕ
negSucc : ((-a) ^ (1 + HMul.hMul (α := ℤ) (↑k : ℤ) 2))⁻¹ = -(a ^ (1 + HMul.hMul (α := ℤ) (↑k : ℤ) 2))⁻¹
⊢ (-a) ^ (2 * Int.negSucc k + 1) = -a ^ (2 * Int.negSucc k + 1)

Tactic:
simp_rw [Int.negSucc_eq, show 2 * -(↑k + 1) + (1 : ℤ) = - (1 + k*2) by grind, _root_.zpow_neg]

Premises used: zpow_neg, Int.negSucc_eq
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
a : α
k : ℕ
negSucc : ((-a) ^ (1 + k * 2))⁻¹ = -(a ^ (1 + k * 2))⁻¹
⊢ ((-a) ^ (1 + HMul.hMul (α := ℤ) (↑k : ℤ) 2))⁻¹ = -(a ^ (1 + HMul.hMul (α := ℤ) (↑k : ℤ) 2))⁻¹

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
a : α
k : ℕ
⊢ ((-a) ^ (1 + k * 2))⁻¹ = -(a ^ (1 + k * 2))⁻¹

Tactic:
simp [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
a : α
k : ℤ
ofNat : ∀ (k : ℕ), (-a) ^ (2 * Int.ofNat k + 1) = -a ^ (2 * Int.ofNat k + 1)
negSucc : ∀ (k : ℕ), (-a) ^ (2 * Int.negSucc k + 1) = -a ^ (2 * Int.negSucc k + 1)
⊢ (-a) ^ (2 * k + 1) = -a ^ (2 * k + 1)

Tactic:
cases k with
  | ofNat k =>
    rw [Int.ofNat_eq_natCast]
    norm_cast
    simp [pow_add]
  | negSucc k =>
    simp_rw [Int.negSucc_eq, show 2 * -(↑k + 1) + (1 : ℤ) = - (1 + k*2) by grind, _root_.zpow_neg]
    norm_cast
    simp [pow_add]

Premises used: pow_add, Int.ofNat_eq_natCast, zpow_neg, Int.negSucc_eq
-- Module: Mathlib.Algebra.Ring.Int.Parity
Goal:
α : Type u_1
inst : DivisionMonoid α
inst_1 : HasDistribNeg α
n : ℤ
h : Odd n
rw : -HPow.hPow (α := α) 1 n = -1
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (-1) (-1)
⊢ HPow.hPow (α := α) (-1) n = -1

Tactic:
rw [h.neg_zpow, one_zpow]

Premises used: one_zpow, Odd.neg_zpow
-- Module: Mathlib.Algebra.Ring.Int.Units
Goal:
u : ℤˣ
⊢ u = 1 ∨ u = -1

Tactic:
simpa only [Units.ext_iff] using isUnit_eq_one_or u.isUnit

Premises used: Units.ext_iff, Int.isUnit_eq_one_or, Units.isUnit
-- Module: Mathlib.Algebra.Ring.Int.Units
Goal:
u v : ℤˣ
⊢ u ≠ v ↔ u = -v

Tactic:
simpa only [Ne, Units.ext_iff] using isUnit_ne_iff_eq_neg u.isUnit v.isUnit

Premises used: Units.ext_iff, Ne, Int.isUnit_ne_iff_eq_neg, Units.isUnit
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ y * (↑x : R) + y * x.neg = 0

Tactic:
simp [← mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ y * x.neg + y * (↑x : R) = 0

Tactic:
simp [← mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ (↑x : R) * y + x.neg * y = 0

Tactic:
simp [← add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ x.neg * y + (↑x : R) * y = 0

Tactic:
simp [← add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ -x.mulLeft y = (-x).mulLeft y

Tactic:
rfl

Premises used: AddUnits.mulLeft, rfl
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ -x.mulRight y = (-x).mulRight y

Tactic:
rfl

Premises used: AddUnits.mulRight, rfl
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : AddUnits R
rw : (↑(-x.mulRight (↑y : R)) : R) = (↑x : R) * (↑(-y) : R)
⊢ (↑(-x) : R) * (↑y : R) = (↑x : R) * (↑(-y) : R)

Tactic:
rw [← neg_eq_val_neg, ← val_neg_mulRight]

Premises used: AddUnits.val_neg_mulRight, AddUnits.neg_eq_val_neg
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : AddUnits R
h : (↑x : R) * (↑(-y) : R) + (↑(x.mulRight (↑y : R)) : R) = 0
⊢ (↑(-x.mulRight (↑y : R)) : R) = (↑x : R) * (↑(-y) : R)

Tactic:
apply AddUnits.neg_eq_of_add_eq_zero_left

Premises used: AddUnits.neg_eq_of_add_eq_zero_left
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ (↑x : R) * (↑(-y) : R) + (↑(x.mulRight (↑y : R)) : R) = 0

Tactic:
simp [← mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : AddUnits R
rw : y.mulLeft (↑(-x) : R) = -y.mulLeft (↑x : R)
⊢ (↑(-x) : R) * (↑(-y) : R) = (↑x : R) * (↑y : R)

Tactic:
rw [← val_mulLeft, ← val_mulLeft, ← AddUnits.ext_iff, ← neg_inj, ← y.neg_mulLeft, neg_neg]

Premises used: AddUnits.val_mulLeft, neg_neg, AddUnits.neg_mulLeft, AddUnits.ext_iff, neg_inj
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : AddUnits R
huv : (↑(y.mulLeft (↑(-x) : R)) : R) = (↑(-y.mulLeft (↑x : R)) : R)
⊢ y.mulLeft (↑(-x) : R) = -y.mulLeft (↑x : R)

Tactic:
apply AddUnits.ext

Premises used: AddUnits.ext
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ (↑(y.mulLeft (↑(-x) : R)) : R) = (↑(-y.mulLeft (↑x : R)) : R)

Tactic:
simp [neg_mul_eq_mul_neg]

Premises used: AddUnits.neg_mul_eq_mul_neg
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x : R
h : IsAddUnit x
y : R
⊢ IsAddUnit (y * x)

Tactic:
(h.addUnit.mulLeft y).isAddUnit

Premises used: AddUnits.isAddUnit, AddUnits.mulLeft, IsAddUnit.addUnit
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x : R
h : IsAddUnit x
y : R
⊢ IsAddUnit (x * y)

Tactic:
(h.addUnit.mulRight y).isAddUnit

Premises used: AddUnits.isAddUnit, AddUnits.mulRight, IsAddUnit.addUnit
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Mul R
inst_1 : One R
inst_2 : HasDistribNeg R
a : R
inst_3 : Invertible a
⊢ -@Invertible.invOf _ inst inst_1 a _ * -a = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Mul R
inst_1 : One R
inst_2 : HasDistribNeg R
a : R
inst_3 : Invertible a
⊢ -a * -@Invertible.invOf _ inst inst_1 a _ = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Monoid R
inst_1 : HasDistribNeg R
a : R
inst_2 : Invertible a
inst_3 : Invertible (-a)
⊢ -a * -@Invertible.invOf _ MulOne.toMul MulOne.toOne a _ = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Ring R
inst_1 : Invertible (α := R) 2
rw :
  HMul.hMul (α := R) 2 1 - HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) =
    HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
rw₁ : HMul.hMul (α := R) 2 1 - 1 = 1
rw₂ : HSub.hSub (α := R) 2 1 = 1
rw₃ : HAdd.hAdd (α := R) 1 1 - 1 = 1
rw₄ rw₅ : Eq.{u_1 + 1} (α := R) 1 1
⊢ 2 * HSub.hSub (α := R) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) =
    HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)

Tactic:
rw [mul_sub, mul_invOf_self, mul_one, ← one_add_one_eq_two, add_sub_cancel_right]

Premises used: mul_sub, mul_invOf_self, one_add_one_eq_two, add_sub_cancel_right, mul_one
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Invertible (α := R) 2
rw : HMul.hMul (α := R) 2 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ HAdd.hAdd (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) =
    1

Tactic:
rw [← two_mul, mul_invOf_self]

Premises used: two_mul, mul_invOf_self
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : NonAssocSemiring R
inst_1 : Nontrivial R
n : ℕ
inst_2 : Invertible (α := R) (↑n : R)
⊢ 0 < n

Tactic:
Nat.zero_lt_of_ne_zero fun h => Invertible.ne_zero (n : R) (h ▸ Nat.cast_zero)

Premises used: Invertible.ne_zero, Eq.rec, Nat.zero_lt_of_ne_zero, Nat.cast, Nat.cast_zero, Eq.symm
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Semiring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
rw :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₁ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₂ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    1 * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₃ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₄ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ *
        (b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _)
rw₅ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * 1
rw₆ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _
rw₇ rw₈ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (a + b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _

Tactic:
rw [mul_add, invOf_mul_self, add_mul, one_mul, mul_assoc, mul_invOf_self, mul_one, add_comm]

Premises used: add_mul, mul_assoc, invOf_mul_self, mul_invOf_self, add_comm, mul_add, mul_one, one_mul
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Ring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
rw :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b -
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₁ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b - 1) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₂ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ -
      1 * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₃ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₄ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ *
        (b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _) -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₅ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * 1 -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₆ rw₇ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (b - a) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _

Tactic:
rw [mul_sub, invOf_mul_self, sub_mul, one_mul, mul_assoc, mul_invOf_self, mul_one]

Premises used: mul_sub, mul_assoc, invOf_mul_self, mul_invOf_self, sub_mul, mul_one, one_mul
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Ring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
⊢ -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a →
    -a = b + a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a

Tactic:
grind