awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
⊢ p * q + q * p - p = p

Tactic:
simp_rw [IsIdempotentElem, mul_sub, sub_mul,
    hp.eq, hq.eq, ← sub_add_eq_sub_sub, sub_right_inj, add_sub] at hqp

Premises used: mul_sub, sub_right_inj, add_sub, sub_mul, IsIdempotentElem, sub_add_eq_sub_sub, IsIdempotentElem.eq
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ q * x) (p * q + q * p - p)) ((fun (x : R) ↦ q * x) p)

Tactic:
have h1 := congr_arg (q * ·) hqp
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h1 : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ q * x) (p * q + q * p - p)) ((fun (x : R) ↦ q * x) p)
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ x * q) (p * q + q * p - p)) ((fun (x : R) ↦ x * q) p)

Tactic:
have h2 := congr_arg (· * q) hqp
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h1 : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ q * x) (p * q + q * p - p)) ((fun (x : R) ↦ q * x) p)
h2 : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ x * q) (p * q + q * p - p)) ((fun (x : R) ↦ x * q) p)
⊢ q * p * q = q * p

Tactic:
simp_rw [mul_sub, mul_add, ← mul_assoc, hq.eq, add_sub_cancel_right] at h1

Premises used: mul_sub, mul_assoc, mul_add, IsIdempotentElem.eq, add_sub_cancel_right
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h2 : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ x * q) (p * q + q * p - p)) ((fun (x : R) ↦ x * q) p)
h1 : q * p * q = q * p
⊢ q * p * q = p * q

Tactic:
simp_rw [sub_mul, add_mul, mul_assoc, hq.eq, add_sub_cancel_left, ← mul_assoc] at h2

Premises used: add_mul, add_sub_cancel_left, mul_assoc, sub_mul, IsIdempotentElem.eq
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h1 : q * p * q = q * p
h2 : q * p * q = p * q
⊢ Commute p q

Tactic:
h2.symm.trans h1

Premises used: SemiconjBy, Commute, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h1 : q * p * q = q * p
h2 : q * p * q = p * q
⊢ Commute p q

Tactic:
exact h2.symm.trans h1

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
⊢ Commute p q

Tactic:
have hpq : Commute p q := by
    simp_rw [IsIdempotentElem, mul_sub, sub_mul,
    hp.eq, hq.eq, ← sub_add_eq_sub_sub, sub_right_inj, add_sub] at hqp
    have h1 := congr_arg (q * ·) hqp
    have h2 := congr_arg (· * q) hqp
    simp_rw [mul_sub, mul_add, ← mul_assoc, hq.eq, add_sub_cancel_right] at h1
    simp_rw [sub_mul, add_mul, mul_assoc, hq.eq, add_sub_cancel_left, ← mul_assoc] at h2
    exact h2.symm.trans h1
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
hpq : Commute p q
⊢ Ne (α := ℕ) 2 0

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
hpq : Commute p q
rw : HSMul.hSMul (α := ℕ) 2 (q * p) = 0 + HSMul.hSMul (α := ℕ) 2 p
⊢ p * q = p ∧ q * p = p

Tactic:
rw [hpq.eq, and_self, ← nsmul_right_inj (by simp : 2 ≠ 0), ← zero_add (2 • p)]

Premises used: and_self, zero_add, nsmul_right_inj, HSMul.hSMul, OfNat.ofNat, Commute.eq
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
hpq : Commute p q
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ x + HSMul.hSMul (α := ℕ) 2 p) (p * (q - p) + (q - p) * p))
    ((fun (x : R) ↦ x + HSMul.hSMul (α := ℕ) 2 p) 0)

Tactic:
congrArg (· + 2 • p) h

Premises used: congrArg, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
hpq : Commute p q
h₁ : HSMul.hSMul (α := ℕ) 2 (q * p) = p * (q - p) + (q - p) * p + HSMul.hSMul (α := ℕ) 2 p
⊢ HSMul.hSMul (α := ℕ) 2 (q * p) = 0 + HSMul.hSMul (α := ℕ) 2 p

Tactic:
convert! congrArg (· + 2 • p) h using 1

Premises used: congrArg, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Idempotent
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
hpq : Commute p q
⊢ HSMul.hSMul (α := ℕ) 2 (q * p) = p * (q - p) + (q - p) * p + HSMul.hSMul (α := ℕ) 2 p

Tactic:
simp [sub_mul, mul_sub, hp.eq, hpq.eq, two_nsmul, sub_add, sub_sub]

Premises used: sub_add, mul_sub, sub_mul, sub_sub, IsIdempotentElem.eq, Commute.eq, two_nsmul
-- Module: Mathlib.Algebra.Ring.Identities
Goal:
R : Type u_1
inst : CommRing R
x₁ x₂ y₁ y₂ : R
⊢ (HPow.hPow (β := ℕ) x₁ 2 + HPow.hPow (β := ℕ) x₂ 2) * (HPow.hPow (β := ℕ) y₁ 2 + HPow.hPow (β := ℕ) y₂ 2) =
    HPow.hPow (β := ℕ) (x₁ * y₁ - x₂ * y₂) 2 + HPow.hPow (β := ℕ) (x₁ * y₂ + x₂ * y₁) 2

Tactic:
ring
-- Module: Mathlib.Algebra.Ring.Identities
Goal:
R : Type u_1
inst : CommRing R
x₁ x₂ y₁ y₂ n : R
⊢ (HPow.hPow (β := ℕ) x₁ 2 + n * HPow.hPow (β := ℕ) x₂ 2) * (HPow.hPow (β := ℕ) y₁ 2 + n * HPow.hPow (β := ℕ) y₂ 2) =
    HPow.hPow (β := ℕ) (x₁ * y₁ - n * x₂ * y₂) 2 + n * HPow.hPow (β := ℕ) (x₁ * y₂ + x₂ * y₁) 2

Tactic:
ring
-- Module: Mathlib.Algebra.Ring.Identities
Goal:
R : Type u_1
inst : CommRing R
a b : R
⊢ HPow.hPow (β := ℕ) a 4 + 4 * HPow.hPow (β := ℕ) b 4 =
    (HPow.hPow (β := ℕ) (a - b) 2 + HPow.hPow (β := ℕ) b 2) * (HPow.hPow (β := ℕ) (a + b) 2 + HPow.hPow (β := ℕ) b 2)

Tactic:
ring
-- Module: Mathlib.Algebra.Ring.Identities
Goal:
R : Type u_1
inst : CommRing R
a b : R
⊢ HPow.hPow (β := ℕ) a 4 + 4 * HPow.hPow (β := ℕ) b 4 =
    (HPow.hPow (β := ℕ) a 2 - 2 * a * b + 2 * HPow.hPow (β := ℕ) b 2) *
      (HPow.hPow (β := ℕ) a 2 + 2 * a * b + 2 * HPow.hPow (β := ℕ) b 2)

Tactic:
ring
-- Module: Mathlib.Algebra.Ring.Identities
Goal:
R : Type u_1
inst : CommRing R
x₁ x₂ x₃ x₄ y₁ y₂ y₃ y₄ : R
⊢ (HPow.hPow (β := ℕ) x₁ 2 + HPow.hPow (β := ℕ) x₂ 2 + HPow.hPow (β := ℕ) x₃ 2 + HPow.hPow (β := ℕ) x₄ 2) *
      (HPow.hPow (β := ℕ) y₁ 2 + HPow.hPow (β := ℕ) y₂ 2 + HPow.hPow (β := ℕ) y₃ 2 + HPow.hPow (β := ℕ) y₄ 2) =
    HPow.hPow (β := ℕ) (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄) 2 +
          HPow.hPow (β := ℕ) (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃) 2 +
        HPow.hPow (β := ℕ) (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂) 2 +
      HPow.hPow (β := ℕ) (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁) 2

Tactic:
ring
-- Module: Mathlib.Algebra.Ring.Identities
Goal:
R : Type u_1
inst : CommRing R
x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ : R
⊢ (HPow.hPow (β := ℕ) x₁ 2 + HPow.hPow (β := ℕ) x₂ 2 + HPow.hPow (β := ℕ) x₃ 2 + HPow.hPow (β := ℕ) x₄ 2 +
              HPow.hPow (β := ℕ) x₅ 2 +
            HPow.hPow (β := ℕ) x₆ 2 +
          HPow.hPow (β := ℕ) x₇ 2 +
        HPow.hPow (β := ℕ) x₈ 2) *
      (HPow.hPow (β := ℕ) y₁ 2 + HPow.hPow (β := ℕ) y₂ 2 + HPow.hPow (β := ℕ) y₃ 2 + HPow.hPow (β := ℕ) y₄ 2 +
              HPow.hPow (β := ℕ) y₅ 2 +
            HPow.hPow (β := ℕ) y₆ 2 +
          HPow.hPow (β := ℕ) y₇ 2 +
        HPow.hPow (β := ℕ) y₈ 2) =
    HPow.hPow (β := ℕ) (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄ - x₅ * y₅ - x₆ * y₆ - x₇ * y₇ - x₈ * y₈) 2 +
                  HPow.hPow (β := ℕ) (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃ + x₅ * y₆ - x₆ * y₅ - x₇ * y₈ + x₈ * y₇) 2 +
                HPow.hPow (β := ℕ) (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂ + x₅ * y₇ + x₆ * y₈ - x₇ * y₅ - x₈ * y₆) 2 +
              HPow.hPow (β := ℕ) (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁ + x₅ * y₈ - x₆ * y₇ + x₇ * y₆ - x₈ * y₅) 2 +
            HPow.hPow (β := ℕ) (x₁ * y₅ - x₂ * y₆ - x₃ * y₇ - x₄ * y₈ + x₅ * y₁ + x₆ * y₂ + x₇ * y₃ + x₈ * y₄) 2 +
          HPow.hPow (β := ℕ) (x₁ * y₆ + x₂ * y₅ - x₃ * y₈ + x₄ * y₇ - x₅ * y₂ + x₆ * y₁ - x₇ * y₄ + x₈ * y₃) 2 +
        HPow.hPow (β := ℕ) (x₁ * y₇ + x₂ * y₈ + x₃ * y₅ - x₄ * y₆ - x₅ * y₃ + x₆ * y₄ + x₇ * y₁ - x₈ * y₂) 2 +
      HPow.hPow (β := ℕ) (x₁ * y₈ - x₂ * y₇ + x₃ * y₆ + x₄ * y₅ - x₅ * y₄ - x₆ * y₃ + x₇ * y₂ + x₈ * y₁) 2

Tactic:
ring
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
f : S → R
hf : Injective f
inst : Add S
inst_1 : Mul S
inst_2 : Mul R
inst_3 : Add R
inst_4 : LeftDistribClass R
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
x y z : S
⊢ f (x * (y + z)) = f (x * y + x * z)

Tactic:
simp only [*, left_distrib]

Premises used: left_distrib
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
f : S → R
hf : Injective f
inst : Add S
inst_1 : Mul S
inst_2 : Mul R
inst_3 : Add R
inst_4 : RightDistribClass R
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
x y z : S
⊢ f ((x + y) * z) = f (x * z + y * z)

Tactic:
simp only [*, right_distrib]

Premises used: right_distrib
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
f : S → R
hf : Injective f
inst_11 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
rw : f (-x * y) = -f (x * y)
rw₁ : f (-x) * f y = -f (x * y)
rw₂ : -f x * f y = -f (x * y)
rw₃ : -(f x * f y) = -f (x * y)
rw₄ rw₅ : -(f x * f y) = -(f x * f y)
⊢ f (-x * y) = f (-(x * y))

Tactic:
rw [neg, mul, neg, neg_mul, mul]

Premises used: neg_mul
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
f : S → R
hf : Injective f
inst_11 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
rw : f (x * -y) = -f (x * y)
rw₁ : f x * f (-y) = -f (x * y)
rw₂ : f x * -f y = -f (x * y)
rw₃ : -(f x * f y) = -f (x * y)
rw₄ rw₅ : -(f x * f y) = -(f x * f y)
⊢ f (x * -y) = f (-(x * y))

Tactic:
rw [neg, mul, neg, mul_neg, mul]

Premises used: mul_neg
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
rw : (↑0 : R) = f 0
rw₁ : 0 = f 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ f (↑0 : S) = f 0

Tactic:
rw [natCast, Nat.cast_zero, zero]

Premises used: Nat.cast_zero
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
f_1 : S → R
hf_1 : Injective f_1
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
n : ℕ
rw : (↑(n + 1) : R) = f (HAdd.hAdd (α := S) (↑n : S) 1)
rw₁ : HAdd.hAdd (α := R) (↑n : R) 1 = f (HAdd.hAdd (α := S) (↑n : S) 1)
rw₂ : HAdd.hAdd (α := R) (↑n : R) 1 = f (↑n : S) + f 1
rw₃ : HAdd.hAdd (α := R) (↑n : R) 1 = f (↑n : S) + 1
rw₄ rw₅ : HAdd.hAdd (α := R) (↑n : R) 1 = HAdd.hAdd (α := R) (↑n : R) 1
⊢ f (↑(n + 1) : S) = f (HAdd.hAdd (α := S) (↑n : S) 1)

Tactic:
rw [natCast, Nat.cast_succ, add, one, natCast]

Premises used: Nat.cast_succ
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S_1 : Type u_2
f_1 : S_1 → R
hf_1 : Injective f_1
inst : Add S_1
inst_1 : Mul S_1
inst_2 : Zero S_1
inst_3 : One S_1
inst_4 : Neg S_1
inst_5 : Sub S_1
inst_6 : SMul ℕ S_1
inst_7 : SMul ℤ S_1
inst_8 : Pow S_1 ℕ
inst_9 : NatCast S_1
inst_10 : IntCast S_1
S : Type u_3
inst_11 : Zero S
inst_12 : One S
inst_13 : Add S
inst_14 : SMul ℕ S
inst_15 : Neg S
inst_16 : Sub S
inst_17 : SMul ℤ S
inst_18 : NatCast S
inst_19 : IntCast S
inst_20 : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
intCast : ∀ (n : ℤ), f (↑n : S) = (↑n : R)
n : ℕ
rw : f (↑(↑n : ℤ) : S) = (↑n : R)
rw₁ : Eq.{u_1 + 1} (α := R) (↑(↑n : ℤ) : R) (↑n : R)
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) (↑n : R) (↑n : R)
⊢ f (↑(↑n : ℤ) : S) = f (↑n : S)

Tactic:
rw [natCast, intCast, Int.cast_natCast]

Premises used: Int.cast_natCast
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S_1 : Type u_2
f_1 : S_1 → R
hf_1 : Injective f_1
inst : Add S_1
inst_1 : Mul S_1
inst_2 : Zero S_1
inst_3 : One S_1
inst_4 : Neg S_1
inst_5 : Sub S_1
inst_6 : SMul ℕ S_1
inst_7 : SMul ℤ S_1
inst_8 : Pow S_1 ℕ
inst_9 : NatCast S_1
inst_10 : IntCast S_1
S : Type u_3
inst_11 : Zero S
inst_12 : One S
inst_13 : Add S
inst_14 : SMul ℕ S
inst_15 : Neg S
inst_16 : Sub S
inst_17 : SMul ℤ S
inst_18 : NatCast S
inst_19 : IntCast S
inst_20 : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : S) = (↑n : R)
intCast : ∀ (n : ℤ), f (↑n : S) = (↑n : R)
n : ℕ
rw : (↑(Int.negSucc n) : R) = f (-(↑(n + 1) : S))
rw₁ : (↑(Int.negSucc n) : R) = -f (↑(n + 1) : S)
rw₂ : Eq.{u_1 + 1} (α := R) (↑(Int.negSucc n) : R) (-(↑(n + 1) : R))
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) (-(↑(n + 1) : R)) (-(↑(n + 1) : R))
⊢ f (↑(Int.negSucc n) : S) = f (-(↑(n + 1) : S))

Tactic:
rw [intCast, neg, natCast, Int.cast_negSucc]

Premises used: Int.cast_negSucc
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst : Add S
inst_1 : Mul S
inst_2 : Mul R
inst_3 : Add R
inst_4 : LeftDistribClass R
add : ∀ (x y : R), f (x + y) = f x + f y
mul : ∀ (x y : R), f (x * y) = f x * f y
x y z : R
⊢ f x * (f y + f z) = f x * f y + f x * f z

Tactic:
simp only [← add, ← mul, left_distrib]

Premises used: left_distrib
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst : Add S
inst_1 : Mul S
inst_2 : Mul R
inst_3 : Add R
inst_4 : RightDistribClass R
add : ∀ (x y : R), f (x + y) = f x + f y
mul : ∀ (x y : R), f (x * y) = f x * f y
x y z : R
⊢ (f x + f y) * f z = f x * f z + f y * f z

Tactic:
simp only [← add, ← mul, right_distrib]

Premises used: right_distrib
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
rw : f (-x) * f y = -(f x * f y)
rw₁ : f (-x * y) = -(f x * f y)
rw₂ : f (-(x * y)) = -(f x * f y)
rw₃ : -f (x * y) = -(f x * f y)
rw₄ rw₅ : -(f x * f y) = -(f x * f y)
⊢ -f x * f y = -(f x * f y)

Tactic:
rw [← neg, ← mul, neg_mul, neg, mul]

Premises used: neg_mul
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : Mul R
inst_12 : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
rw : f x * f (-y) = -(f x * f y)
rw₁ : f (x * -y) = -(f x * f y)
rw₂ : f (-(x * y)) = -(f x * f y)
rw₃ : -f (x * y) = -(f x * f y)
rw₄ rw₅ : -(f x * f y) = -(f x * f y)
⊢ f x * -f y = -(f x * f y)

Tactic:
rw [← neg, ← mul, mul_neg, neg, mul]

Premises used: mul_neg
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
rw : f (↑0 : R) = 0
rw₁ : f 0 = 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := S) 0 0
⊢ Eq.{u_2 + 1} (α := S) (↑0 : S) 0

Tactic:
rw [← natCast, Nat.cast_zero, zero]

Premises used: Nat.cast_zero
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : AddMonoidWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
n : ℕ
rw : f (↑(n + 1) : R) = HAdd.hAdd (α := S) (↑n : S) 1
rw₁ : f (HAdd.hAdd (α := R) (↑n : R) 1) = HAdd.hAdd (α := S) (↑n : S) 1
rw₂ : f (↑n : R) + f 1 = HAdd.hAdd (α := S) (↑n : S) 1
rw₃ : f (↑n : R) + 1 = HAdd.hAdd (α := S) (↑n : S) 1
rw₄ rw₅ : HAdd.hAdd (α := S) (↑n : S) 1 = HAdd.hAdd (α := S) (↑n : S) 1
⊢ (↑(n + 1) : S) = HAdd.hAdd (α := S) (↑n : S) 1

Tactic:
rw [← natCast, Nat.cast_succ, add, one, natCast]

Premises used: Nat.cast_succ
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
intCast : ∀ (n : ℤ), f (↑n : R) = (↑n : S)
n : ℕ
rw : f (↑(↑n : ℤ) : R) = (↑n : S)
rw₁ : f (↑n : R) = (↑n : S)
rw₂ rw₃ : Eq.{u_2 + 1} (α := S) (↑n : S) (↑n : S)
⊢ Eq.{u_2 + 1} (α := S) (↑(↑n : ℤ) : S) (↑n : S)

Tactic:
rw [← intCast, Int.cast_natCast, natCast]

Premises used: Int.cast_natCast
-- Module: Mathlib.Algebra.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst : Add S
inst_1 : Mul S
inst_2 : Zero S
inst_3 : One S
inst_4 : Neg S
inst_5 : Sub S
inst_6 : SMul ℕ S
inst_7 : SMul ℤ S
inst_8 : Pow S ℕ
inst_9 : NatCast S
inst_10 : IntCast S
inst_11 : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f (↑n : R) = (↑n : S)
intCast : ∀ (n : ℤ), f (↑n : R) = (↑n : S)
n : ℕ
rw : f (↑(Int.negSucc n) : R) = -(↑(n + 1) : S)
rw₁ : f (-(↑(n + 1) : R)) = -(↑(n + 1) : S)
rw₂ : -f (↑(n + 1) : R) = -(↑(n + 1) : S)
rw₃ rw₄ : Eq.{u_2 + 1} (α := S) (-(↑(n + 1) : S)) (-(↑(n + 1) : S))
⊢ Eq.{u_2 + 1} (α := S) (↑(Int.negSucc n) : S) (-(↑(n + 1) : S))

Tactic:
rw [← intCast, Int.cast_negSucc, neg, natCast]

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

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.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.Ring.Int.Defs
Goal:
α : Type u_1
inst : NonAssocRing α
m : ℤ
inl : ∀ (m : ℕ) (n : ℤ), (↑((↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑m : ℤ) : α) (↑n : α)
inr : ∀ (m : ℕ) (n : ℤ), (↑(-(↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(-(↑m : ℤ)) : α) (↑n : α)
⊢ ∀ (n : ℤ), (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)

Tactic:
obtain ⟨m, rfl | rfl⟩ := Int.eq_nat_or_neg m

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Algebra.Ring.Int.Defs
Goal:
α : Type u_1
inst : NonAssocRing α
⊢ ∀ (n : ℤ), (↑((↑0 : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑0 : ℤ) : α) (↑n : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Int.Defs
Goal:
α : Type u_1
inst : NonAssocRing α
m : ℕ
ih : ∀ (n : ℤ), (↑((↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑m : ℤ) : α) (↑n : α)
⊢ ∀ (n : ℤ), (↑((↑(m + 1) : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑(m + 1) : ℤ) : α) (↑n : α)

Tactic:
simp_all [add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Ring.Int.Defs
Goal:
α : Type u_1
inst : NonAssocRing α
m : ℕ
inl : ∀ (n : ℤ), (↑((↑0 : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑0 : ℤ) : α) (↑n : α)
inl₁ :
  ∀ (m : ℕ) (ih : ∀ (n : ℤ), (↑((↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑m : ℤ) : α) (↑n : α)) (n : ℤ),
    (↑((↑(m + 1) : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑(m + 1) : ℤ) : α) (↑n : α)
⊢ ∀ (n : ℤ), (↑((↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(↑m : ℤ) : α) (↑n : α)

Tactic:
induction m with
    | zero => simp
    | succ m ih => simp_all [add_mul]

Premises used: add_mul, Int.succ
-- Module: Mathlib.Algebra.Ring.Int.Defs
Goal:
α : Type u_1
inst : NonAssocRing α
⊢ ∀ (n : ℤ), (↑(-(↑0 : ℤ) * n) : α) = HMul.hMul (α := α) (↑(-(↑0 : ℤ)) : α) (↑n : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Int.Defs
Goal:
α : Type u_1
inst : NonAssocRing α
m : ℕ
ih : ∀ (n : ℤ), (↑(-(↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(-(↑m : ℤ)) : α) (↑n : α)
⊢ ∀ (n : ℤ), (↑(-(↑(m + 1) : ℤ) * n) : α) = HMul.hMul (α := α) (↑(-(↑(m + 1) : ℤ)) : α) (↑n : α)

Tactic:
simp_all [add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Ring.Int.Defs
Goal:
α : Type u_1
inst : NonAssocRing α
m : ℕ
inr : ∀ (n : ℤ), (↑(-(↑0 : ℤ) * n) : α) = HMul.hMul (α := α) (↑(-(↑0 : ℤ)) : α) (↑n : α)
inr₁ :
  ∀ (m : ℕ) (ih : ∀ (n : ℤ), (↑(-(↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(-(↑m : ℤ)) : α) (↑n : α)) (n : ℤ),
    (↑(-(↑(m + 1) : ℤ) * n) : α) = HMul.hMul (α := α) (↑(-(↑(m + 1) : ℤ)) : α) (↑n : α)
⊢ ∀ (n : ℤ), (↑(-(↑m : ℤ) * n) : α) = HMul.hMul (α := α) (↑(-(↑m : ℤ)) : α) (↑n : α)

Tactic:
induction m with
    | zero => simp
    | succ m ih => simp_all [add_mul]

Premises used: add_mul, Int.succ
-- Module: Mathlib.Algebra.Ring.Int.Defs
Goal:
α : Type u_1
inst : AddGroupWithOne α
m : ℤ
⊢ ∀ (n : ℤ), (↑(0 * n) : α) = HSMul.hSMul (α := ℤ) (β := α) 0 (↑n : α)

Tactic:
simp