awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y z : R
h : Relation.EqvGen (Rel r) x y
h_1 : Relation.EqvGen (Rel r) y z
a_ih : RingConGen.Rel r x y
a_ih_1 : RingConGen.Rel r y z
⊢ RingConGen.Rel r x z

Tactic:
RingConGen.Rel.trans ‹_› ‹_›

Premises used: RingConGen.Rel.trans
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y z : R
h : Relation.EqvGen (Rel r) x y
h_1 : Relation.EqvGen (Rel r) y z
a_ih : RingConGen.Rel r x y
a_ih_1 : RingConGen.Rel r y z
⊢ RingConGen.Rel r x z

Tactic:
exact RingConGen.Rel.trans ‹_› ‹_›

Premises used: RingConGen.Rel.trans
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ : R
h : Relation.EqvGen (Rel r) x₁ x₂
h₁ : ∀ (x y : R) (h : Rel r x y), RingConGen.Rel r x y
h₂ : ∀ (x : R), RingConGen.Rel r x x
h₃ : ∀ (x y : R), Relation.EqvGen (Rel r) x y → RingConGen.Rel r x y → RingConGen.Rel r y x
h₄ :
  ∀ (x y z : R),
    Relation.EqvGen (Rel r) x y →
      Relation.EqvGen (Rel r) y z → RingConGen.Rel r x y → RingConGen.Rel r y z → RingConGen.Rel r x z
⊢ RingConGen.Rel r x₁ x₂

Tactic:
induction h with
    | rel _ _ h => induction h with
      | of => exact RingConGen.Rel.of _ _ ‹_›
      | add_left _ h => exact h.add (RingConGen.Rel.refl _)
      | mul_left _ h => exact h.mul (RingConGen.Rel.refl _)
      | mul_right _ h => exact (RingConGen.Rel.refl _).mul h
    | refl => exact RingConGen.Rel.refl _
    | symm => exact RingConGen.Rel.symm ‹_›
    | trans => exact RingConGen.Rel.trans ‹_› ‹_›

Premises used: RingConGen.Rel.trans, RingConGen.Rel.symm, RingConGen.Rel.refl, RingConGen.Rel.of, symm, refl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y : R
h : r x y
⊢ Relation.EqvGen (Rel r) x y

Tactic:
Relation.EqvGen.rel _ _ (Rel.of ‹_›)

Premises used: Relation.EqvGen.rel, RingQuot.Rel.of
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y : R
h : r x y
⊢ Relation.EqvGen (Rel r) x y

Tactic:
exact Relation.EqvGen.rel _ _ (Rel.of ‹_›)

Premises used: Relation.EqvGen.rel, RingQuot.Rel.of
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x : R
⊢ Relation.EqvGen (Rel r) x x

Tactic:
(RingQuot.ringCon r).refl _

Premises used: RingQuot.ringCon, RingCon.refl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x : R
⊢ Relation.EqvGen (Rel r) x x

Tactic:
exact (RingQuot.ringCon r).refl _

Premises used: RingQuot.ringCon, RingCon.refl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y : R
h : RingConGen.Rel r x y
a_ih : Relation.EqvGen (Rel r) x y
⊢ Relation.EqvGen (Rel r) y x

Tactic:
(RingQuot.ringCon r).symm ‹_›

Premises used: RingQuot.ringCon, RingCon.symm
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y : R
h : RingConGen.Rel r x y
a_ih : Relation.EqvGen (Rel r) x y
⊢ Relation.EqvGen (Rel r) y x

Tactic:
exact (RingQuot.ringCon r).symm ‹_›

Premises used: RingQuot.ringCon, RingCon.symm
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y z : R
h : RingConGen.Rel r x y
h_1 : RingConGen.Rel r y z
a_ih : Relation.EqvGen (Rel r) x y
a_ih_1 : Relation.EqvGen (Rel r) y z
⊢ Relation.EqvGen (Rel r) x z

Tactic:
(RingQuot.ringCon r).trans ‹_› ‹_›

Premises used: RingQuot.ringCon, RingCon.trans
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y z : R
h : RingConGen.Rel r x y
h_1 : RingConGen.Rel r y z
a_ih : Relation.EqvGen (Rel r) x y
a_ih_1 : Relation.EqvGen (Rel r) y z
⊢ Relation.EqvGen (Rel r) x z

Tactic:
exact (RingQuot.ringCon r).trans ‹_› ‹_›

Premises used: RingQuot.ringCon, RingCon.trans
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ w x y z : R
h : RingConGen.Rel r w x
h_1 : RingConGen.Rel r y z
a_ih : Relation.EqvGen (Rel r) w x
a_ih_1 : Relation.EqvGen (Rel r) y z
⊢ Relation.EqvGen (Rel r) (w + y) (x + z)

Tactic:
(RingQuot.ringCon r).add ‹_› ‹_›

Premises used: RingQuot.ringCon, RingCon.add
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ w x y z : R
h : RingConGen.Rel r w x
h_1 : RingConGen.Rel r y z
a_ih : Relation.EqvGen (Rel r) w x
a_ih_1 : Relation.EqvGen (Rel r) y z
⊢ Relation.EqvGen (Rel r) (w + y) (x + z)

Tactic:
exact (RingQuot.ringCon r).add ‹_› ‹_›

Premises used: RingQuot.ringCon, RingCon.add
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ w x y z : R
h : RingConGen.Rel r w x
h_1 : RingConGen.Rel r y z
a_ih : Relation.EqvGen (Rel r) w x
a_ih_1 : Relation.EqvGen (Rel r) y z
⊢ Relation.EqvGen (Rel r) (w * y) (x * z)

Tactic:
(RingQuot.ringCon r).mul ‹_› ‹_›

Premises used: RingQuot.ringCon, RingCon.mul
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ w x y z : R
h : RingConGen.Rel r w x
h_1 : RingConGen.Rel r y z
a_ih : Relation.EqvGen (Rel r) w x
a_ih_1 : Relation.EqvGen (Rel r) y z
⊢ Relation.EqvGen (Rel r) (w * y) (x * z)

Tactic:
exact (RingQuot.ringCon r).mul ‹_› ‹_›

Premises used: RingQuot.ringCon, RingCon.mul
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ : R
h : RingConGen.Rel r x₁ x₂
h₁ : ∀ (x y : R), r x y → Relation.EqvGen (Rel r) x y
h₂ : ∀ (x : R), Relation.EqvGen (Rel r) x x
h₃ : ∀ {x y : R}, RingConGen.Rel r x y → Relation.EqvGen (Rel r) x y → Relation.EqvGen (Rel r) y x
h₄ :
  ∀ {x y z : R},
    RingConGen.Rel r x y →
      RingConGen.Rel r y z → Relation.EqvGen (Rel r) x y → Relation.EqvGen (Rel r) y z → Relation.EqvGen (Rel r) x z
h₅ :
  ∀ {w x y z : R},
    RingConGen.Rel r w x →
      RingConGen.Rel r y z →
        Relation.EqvGen (Rel r) w x → Relation.EqvGen (Rel r) y z → Relation.EqvGen (Rel r) (w + y) (x + z)
h₆ :
  ∀ {w x y z : R},
    RingConGen.Rel r w x →
      RingConGen.Rel r y z →
        Relation.EqvGen (Rel r) w x → Relation.EqvGen (Rel r) y z → Relation.EqvGen (Rel r) (w * y) (x * z)
⊢ Relation.EqvGen (Rel r) x₁ x₂

Tactic:
induction h with
    | of => exact Relation.EqvGen.rel _ _ (Rel.of ‹_›)
    | refl => exact (RingQuot.ringCon r).refl _
    | symm => exact (RingQuot.ringCon r).symm ‹_›
    | trans => exact (RingQuot.ringCon r).trans ‹_› ‹_›
    | add => exact (RingQuot.ringCon r).add ‹_› ‹_›
    | mul => exact (RingQuot.ringCon r).mul ‹_› ‹_›

Premises used: RingQuot.ringCon, RingCon.mul, RingCon.refl, RingCon.trans, RingCon.symm, Relation.EqvGen.rel, symm, RingQuot.Rel.of, refl, RingCon.add
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
x : RingQuot r
a_1 : Quot (Rel r)
a b : R
h : Rel r a b
zero : Quot.mk (Rel r) 1 = Quot.mk (Rel r) (HPow.hPow (β := ℕ) b 0)
zero₁ zero₂ : Quot.mk (Rel r) 1 = Quot.mk (Rel r) 1
⊢ Quot.mk (Rel r) (HPow.hPow (β := ℕ) a 0) = Quot.mk (Rel r) (HPow.hPow (β := ℕ) b 0)

Tactic:
rw [pow_zero, pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
x : RingQuot r
a_1 : Quot (Rel r)
a b : R
h : Rel r a b
n : ℕ
ih : Quot.mk (Rel r) (a ^ n) = Quot.mk (Rel r) (b ^ n)
⊢ Quot.mk (Rel r) (a ^ (n + 1)) = Quot.mk (Rel r) (b ^ (n + 1))

Tactic:
simpa +instances [pow_succ, (· * ·), instMul, Quot.map₂_mk, mk.injEq] using
          congr_arg₂ (fun x y ↦ (⟨x⟩ : RingQuot r) * ⟨y⟩) ih (Quot.sound h)

Premises used: HMul.hMul, Quot.sound, RingQuot.instMul, pow_succ, RingQuot.mk.injEq, Quot.map₂_mk, RingQuot.mk, congr_arg₂
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
x : RingQuot r
n : ℕ
a_1 : Quot (Rel r)
a b : R
h : Rel r a b
zero : Quot.mk (Rel r) (HPow.hPow (β := ℕ) a 0) = Quot.mk (Rel r) (HPow.hPow (β := ℕ) b 0)
succ :
  ∀ (n : ℕ) (ih : Quot.mk (Rel r) (a ^ n) = Quot.mk (Rel r) (b ^ n)),
    Quot.mk (Rel r) (a ^ (n + 1)) = Quot.mk (Rel r) (b ^ (n + 1))
⊢ Quot.mk (Rel r) (a ^ n) = Quot.mk (Rel r) (b ^ n)

Tactic:
induction n with
      | zero => rw [pow_zero, pow_zero]
      | succ n ih =>
        simpa +instances [pow_succ, (· * ·), instMul, Quot.map₂_mk, mk.injEq] using
          congr_arg₂ (fun x y ↦ (⟨x⟩ : RingQuot r) * ⟨y⟩) ih (Quot.sound h)

Premises used: HMul.hMul, RingQuot.instMul, pow_succ, RingQuot.mk.injEq, Quot.map₂_mk, pow_zero
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
⊢ mk (r := r) (Quot.mk (Rel r) 0) = 0

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
⊢ mk (r := r) (Quot.mk (Rel r) 1) = 1

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
a b : R
⊢ mk (r := r) (Quot.mk (Rel r) a) + mk (r := r) (Quot.mk (Rel r) b) = mk (r := r) (Quot.mk (Rel r) (a + b))

Tactic:
(rfl)

Premises used: Quot.map₂, Quot.lift₂, rfl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
a b : R
⊢ mk (r := r) (Quot.mk (Rel r) a) * mk (r := r) (Quot.mk (Rel r) b) = mk (r := r) (Quot.mk (Rel r) (a * b))

Tactic:
(rfl)

Premises used: Quot.map₂, Quot.lift₂, rfl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
a : R
n : ℕ
⊢ mk (r := r) (Quot.mk (Rel r) a) ^ n = mk (r := r) (Quot.mk (Rel r) (a ^ n))

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Ring R
r : R → R → Prop
a : R
⊢ -mk (r := r) (Quot.mk (Rel r) a) = mk (r := r) (Quot.mk (Rel r) (-a))

Tactic:
(rfl)

Premises used: Quot.map, rfl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Ring R
r : R → R → Prop
a b : R
⊢ mk (r := r) (Quot.mk (Rel r) a) - mk (r := r) (Quot.mk (Rel r) b) = mk (r := r) (Quot.mk (Rel r) (a - b))

Tactic:
(rfl)

Premises used: Quot.map₂, Quot.lift₂, rfl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
r : R → R → Prop
inst_2 : Algebra S R
n : S
a : R
⊢ n • mk (r := r) (Quot.mk (Rel r) a) = mk (r := r) (Quot.mk (Rel r) (n • a))

Tactic:
(rfl)

Premises used: RingQuot.smul, Quot.map, rfl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : CommSemiring T
inst_5 : SMul S T
inst_6 : Algebra S R
inst_7 : Algebra T R
inst_8 : IsScalarTower S T R
s : S
t : T
x : RingQuot r
a : Quot (Rel r)
a' : R
⊢ (s • t) • mk (r := r) (Quot.mk (Rel r) a') = s • t • mk (r := r) (Quot.mk (Rel r) a')

Tactic:
simp only [RingQuot.smul_quot, smul_assoc]

Premises used: smul_assoc, RingQuot.smul_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : CommSemiring T
inst_5 : Algebra S R
inst_6 : Algebra T R
inst_7 : SMulCommClass S T R
s : S
t : T
x : RingQuot r
a : Quot (Rel r)
a' : R
⊢ s • t • mk (r := r) (Quot.mk (Rel r) a') = t • s • mk (r := r) (Quot.mk (Rel r) a')

Tactic:
simp only [RingQuot.smul_quot, smul_comm s t]

Premises used: RingQuot.smul_quot, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
toQuot : Quot (Rel r)
a : R
toQuot_1 : Quot (Rel r)
a_1 : R
toQuot_2 : Quot (Rel r)
a_2 : R
⊢ mk (r := r) (Quot.mk (Rel r) a) + mk (r := r) (Quot.mk (Rel r) a_1) + mk (r := r) (Quot.mk (Rel r) a_2) =
    mk (r := r) (Quot.mk (Rel r) a) + (mk (r := r) (Quot.mk (Rel r) a_1) + mk (r := r) (Quot.mk (Rel r) a_2))

Tactic:
simp only [add_quot, add_assoc]

Premises used: RingQuot.add_quot, add_assoc
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
toQuot : Quot (Rel r)
a : R
⊢ 0 + mk (r := r) (Quot.mk (Rel r) a) = mk (r := r) (Quot.mk (Rel r) a)

Tactic:
simp [add_quot, ← zero_quot, zero_add]

Premises used: RingQuot.add_quot, zero_add, RingQuot.zero_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
toQuot : Quot (Rel r)
a : R
⊢ mk (r := r) (Quot.mk (Rel r) a) + 0 = mk (r := r) (Quot.mk (Rel r) a)

Tactic:
simp only [add_quot, ← zero_quot, add_zero]

Premises used: RingQuot.add_quot, RingQuot.zero_quot, add_zero
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
toQuot : Quot (Rel r)
a : R
⊢ HSMul.hSMul (α := ℕ) 0 (mk (r := r) (Quot.mk (Rel r) a)) = 0

Tactic:
simp only [smul_quot, zero_smul, zero_quot]

Premises used: zero_smul, RingQuot.zero_quot, RingQuot.smul_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
n : ℕ
toQuot : Quot (Rel r)
a : R
⊢ (n + 1) • mk (r := r) (Quot.mk (Rel r) a) = n • mk (r := r) (Quot.mk (Rel r) a) + mk (r := r) (Quot.mk (Rel r) a)

Tactic:
simp only [smul_quot, nsmul_eq_mul, Nat.cast_add, Nat.cast_one, add_mul, one_mul,
               add_comm, add_quot]

Premises used: add_mul, RingQuot.add_quot, add_comm, Nat.cast_add, nsmul_eq_mul, RingQuot.smul_quot, Nat.cast_one, one_mul
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
toQuot : Quot (Rel r)
a : R
toQuot_1 : Quot (Rel r)
a_1 : R
⊢ mk (r := r) (Quot.mk (Rel r) a) + mk (r := r) (Quot.mk (Rel r) a_1) =
    mk (r := r) (Quot.mk (Rel r) a_1) + mk (r := r) (Quot.mk (Rel r) a)

Tactic:
simp only [add_quot, add_comm]

Premises used: RingQuot.add_quot, add_comm
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
toQuot : Quot (Rel r)
a : R
toQuot_1 : Quot (Rel r)
a_1 : R
toQuot_2 : Quot (Rel r)
a_2 : R
⊢ mk (r := r) (Quot.mk (Rel r) a) * mk (r := r) (Quot.mk (Rel r) a_1) * mk (r := r) (Quot.mk (Rel r) a_2) =
    mk (r := r) (Quot.mk (Rel r) a) * (mk (r := r) (Quot.mk (Rel r) a_1) * mk (r := r) (Quot.mk (Rel r) a_2))

Tactic:
simp only [mul_quot, mul_assoc]

Premises used: mul_assoc, RingQuot.mul_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
toQuot : Quot (Rel r)
a : R
⊢ 1 * mk (r := r) (Quot.mk (Rel r) a) = mk (r := r) (Quot.mk (Rel r) a)

Tactic:
simp only [mul_quot, ← one_quot, one_mul]

Premises used: RingQuot.mul_quot, RingQuot.one_quot, one_mul
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
toQuot : Quot (Rel r)
a : R
⊢ mk (r := r) (Quot.mk (Rel r) a) * 1 = mk (r := r) (Quot.mk (Rel r) a)

Tactic:
simp only [mul_quot, ← one_quot, mul_one]

Premises used: RingQuot.mul_quot, mul_one, RingQuot.one_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
toQuot : Quot (Rel r)
a : R
⊢ HPow.hPow (β := ℕ) (mk (r := r) (Quot.mk (Rel r) a)) 0 = 1

Tactic:
simp only [pow_quot, ← one_quot, pow_zero]

Premises used: pow_zero, RingQuot.pow_quot, RingQuot.one_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
n : ℕ
toQuot : Quot (Rel r)
a : R
⊢ mk (r := r) (Quot.mk (Rel r) a) ^ (n + 1) = mk (r := r) (Quot.mk (Rel r) a) ^ n * mk (r := r) (Quot.mk (Rel r) a)

Tactic:
simp only [pow_quot, mul_quot, pow_succ]

Premises used: pow_succ, RingQuot.mul_quot, RingQuot.pow_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
toQuot : Quot (Rel r)
a : R
⊢ 0 * mk (r := r) (Quot.mk (Rel r) a) = 0

Tactic:
simp only [mul_quot, ← zero_quot, zero_mul]

Premises used: MulZeroClass.zero_mul, RingQuot.mul_quot, RingQuot.zero_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
toQuot : Quot (Rel r)
a : R
⊢ mk (r := r) (Quot.mk (Rel r) a) * 0 = 0

Tactic:
simp only [mul_quot, ← zero_quot, mul_zero]

Premises used: RingQuot.mul_quot, MulZeroClass.mul_zero, RingQuot.zero_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
toQuot : Quot (Rel r)
a : R
toQuot_1 : Quot (Rel r)
a_1 : R
toQuot_2 : Quot (Rel r)
a_2 : R
⊢ mk (r := r) (Quot.mk (Rel r) a) * (mk (r := r) (Quot.mk (Rel r) a_1) + mk (r := r) (Quot.mk (Rel r) a_2)) =
    mk (r := r) (Quot.mk (Rel r) a) * mk (r := r) (Quot.mk (Rel r) a_1) +
      mk (r := r) (Quot.mk (Rel r) a) * mk (r := r) (Quot.mk (Rel r) a_2)

Tactic:
simp only [mul_quot, add_quot, left_distrib]

Premises used: RingQuot.add_quot, RingQuot.mul_quot, left_distrib
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
toQuot : Quot (Rel r)
a : R
toQuot_1 : Quot (Rel r)
a_1 : R
toQuot_2 : Quot (Rel r)
a_2 : R
⊢ (mk (r := r) (Quot.mk (Rel r) a) + mk (r := r) (Quot.mk (Rel r) a_1)) * mk (r := r) (Quot.mk (Rel r) a_2) =
    mk (r := r) (Quot.mk (Rel r) a) * mk (r := r) (Quot.mk (Rel r) a_2) +
      mk (r := r) (Quot.mk (Rel r) a_1) * mk (r := r) (Quot.mk (Rel r) a_2)

Tactic:
simp only [mul_quot, add_quot, right_distrib]

Premises used: RingQuot.add_quot, RingQuot.mul_quot, right_distrib
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
⊢ Eq.{uR + 1} (α := RingQuot r) (↑0) 0

Tactic:
simp +instances [instNatCast, natCast, ← zero_quot]

Premises used: RingQuot.instNatCast, RingQuot.zero_quot, RingQuot.natCast
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 r : R → R → Prop
⊢ ∀ (n : ℕ), ↑(n + 1) = HAdd.hAdd (α := RingQuot r) (↑n) 1

Tactic:
simp +instances [instNatCast, natCast, ← one_quot, add_quot]

Premises used: RingQuot.instNatCast, RingQuot.add_quot, RingQuot.natCast, RingQuot.one_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R_1 : Type uR
inst : Semiring R_1
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R_1 → R_1 → Prop
R : Type uR
inst_4 : Ring R
r : R → R → Prop
toQuot : Quot (Rel r)
a : R
toQuot_1 : Quot (Rel r)
a_1 : R
⊢ mk (r := r) (Quot.mk (Rel r) a) - mk (r := r) (Quot.mk (Rel r) a_1) =
    mk (r := r) (Quot.mk (Rel r) a) + -mk (r := r) (Quot.mk (Rel r) a_1)

Tactic:
simp [neg_quot, sub_quot, add_quot, sub_eq_add_neg]

Premises used: RingQuot.add_quot, sub_eq_add_neg, RingQuot.sub_quot, RingQuot.neg_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R_1 : Type uR
inst : Semiring R_1
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R_1 → R_1 → Prop
R : Type uR
inst_4 : Ring R
r : R → R → Prop
toQuot : Quot (Rel r)
a : R
⊢ HSMul.hSMul (α := ℤ) 0 (mk (r := r) (Quot.mk (Rel r) a)) = 0

Tactic:
simp [smul_quot, ← zero_quot]

Premises used: RingQuot.zero_quot, RingQuot.smul_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R_1 : Type uR
inst : Semiring R_1
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R_1 → R_1 → Prop
R : Type uR
inst_4 : Ring R
r : R → R → Prop
n : ℕ
toQuot : Quot (Rel r)
a : R
⊢ HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) (mk (r := r) (Quot.mk (Rel r) a)) =
    HSMul.hSMul (α := ℤ) (↑n : ℤ) (mk (r := r) (Quot.mk (Rel r) a)) + mk (r := r) (Quot.mk (Rel r) a)

Tactic:
simp [smul_quot, add_quot, add_mul, add_comm]

Premises used: add_mul, RingQuot.add_quot, add_comm, RingQuot.smul_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R_1 : Type uR
inst : Semiring R_1
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R_1 → R_1 → Prop
R : Type uR
inst_4 : Ring R
r : R → R → Prop
n : ℕ
toQuot : Quot (Rel r)
a : R
⊢ Int.negSucc n • mk (r := r) (Quot.mk (Rel r) a) =
    -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) (mk (r := r) (Quot.mk (Rel r) a))

Tactic:
simp [smul_quot, neg_quot, add_mul]

Premises used: add_mul, RingQuot.smul_quot, RingQuot.neg_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R_1 : Type uR
inst : Semiring R_1
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R_1 → R_1 → Prop
R : Type uR
inst_4 : Ring R
r : R → R → Prop
toQuot : Quot (Rel r)
a : R
⊢ -mk (r := r) (Quot.mk (Rel r) a) + mk (r := r) (Quot.mk (Rel r) a) = 0

Tactic:
simp [neg_quot, add_quot, ← zero_quot]

Premises used: RingQuot.add_quot, RingQuot.zero_quot, RingQuot.neg_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R_1 : Type uR
inst : Semiring R_1
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R_1 → R_1 → Prop
R : Type uR
inst_4 : Ring R
r : R → R → Prop
n : ℕ
⊢ Quot.mk (Rel r) (↑(↑n : ℤ) : R) = Quot.mk (Rel r) (↑n : R)

Tactic:
congrArg (Quot.mk _) (Int.cast_natCast _)

Premises used: Int.cast_natCast, congrArg, Quot.mk
-- Module: Mathlib.Algebra.RingQuot
Goal:
R_1 : Type uR
inst : Semiring R_1
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R_1 → R_1 → Prop
R : Type uR
inst_4 : Ring R
r : R → R → Prop
n : ℕ
⊢ Quot.mk (Rel r) (↑(↑n : ℤ) : R) = Quot.mk (Rel r) (↑n : R)

Tactic:
exact congrArg (Quot.mk _) (Int.cast_natCast _)

Premises used: Int.cast_natCast, congrArg, Quot.mk
-- Module: Mathlib.Algebra.RingQuot
Goal:
R_1 : Type uR
inst : Semiring R_1
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R_1 → R_1 → Prop
R : Type uR
inst_4 : Ring R
r : R → R → Prop
n : ℕ
⊢ Quot.mk (Rel r) (↑(Int.negSucc n) : R) = toQuot (r := r) ((instNeg r : Neg (RingQuot r)).1 (↑(n + 1) : RingQuot r))

Tactic:
congrArg (Quot.mk _) (Int.cast_negSucc n)

Premises used: congrArg, Int.cast_negSucc, Quot.map, Quot.mk
-- Module: Mathlib.Algebra.RingQuot
Goal:
R_1 : Type uR
inst : Semiring R_1
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R_1 → R_1 → Prop
R : Type uR
inst_4 : Ring R
r : R → R → Prop
n : ℕ
⊢ Quot.mk (Rel r) (↑(Int.negSucc n) : R) = toQuot (r := r) ((instNeg r : Neg (RingQuot r)).1 (↑(n + 1) : RingQuot r))

Tactic:
exact congrArg (Quot.mk _) (Int.cast_negSucc n)

Premises used: congrArg, Int.cast_negSucc, Quot.mk