awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
j : J
x y : (↑(F.1 j) : Type v)
a :
  (colimitSetoid F : Prequotient F → Prequotient F → Prop) (Prequotient.of j (x * y))
    ((Prequotient.of j x).mul (Prequotient.of j y))
⊢ coconeFun F j (x * y) = coconeFun F j x * coconeFun F j y

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
j : J
x y : (↑(F.1 j) : Type v)
⊢ (colimitSetoid F : Prequotient F → Prequotient F → Prop) (Prequotient.of j (x * y))
    ((Prequotient.of j x).mul (Prequotient.of j y))

Tactic:
apply Relation.mul

Premises used: CommRingCat.Colimits.Relation.mul
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
j : J
a : (colimitSetoid F : Prequotient F → Prequotient F → Prop) (Prequotient.of j 0) zero
⊢ coconeFun F j 0 = 0

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ (colimitSetoid F : Prequotient F → Prequotient F → Prop) (Prequotient.of j 0) zero

Tactic:
apply Relation.zero

Premises used: CommRingCat.Colimits.Relation.zero
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
j : J
x y : (↑(F.1 j) : Type v)
a :
  (colimitSetoid F : Prequotient F → Prequotient F → Prop) (Prequotient.of j (x + y))
    ((Prequotient.of j x).add (Prequotient.of j y))
⊢ coconeFun F j (x + y) = coconeFun F j x + coconeFun F j y

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
j : J
x y : (↑(F.1 j) : Type v)
⊢ (colimitSetoid F : Prequotient F → Prequotient F → Prop) (Prequotient.of j (x + y))
    ((Prequotient.of j x).add (Prequotient.of j y))

Tactic:
apply Relation.add

Premises used: CommRingCat.Colimits.Relation.add
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
hf :
  ∀ (x : (↑(F.obj j) : Type v)),
    Eq (α := (↑(colimit F) : Type v))
      ((Hom.hom (F.map f ≫ coconeMorphism F j') : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x :
        (↑(colimit F) : Type v))
      ((Hom.hom (coconeMorphism F j) : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x :
        (↑(colimit F) : Type v))
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
hf :
  (colimitSetoid F : Prequotient F → Prequotient F → Prop)
    (Prequotient.of j' (((F.map f).hom' : (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v)) x)) (Prequotient.of j x)
⊢ Eq (α := (↑(colimit F) : Type v))
    ((Hom.hom (F.map f ≫ coconeMorphism F j') : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x :
      (↑(colimit F) : Type v))
    ((Hom.hom (coconeMorphism F j) : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x : (↑(colimit F) : Type v))

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
⊢ (colimitSetoid F : Prequotient F → Prequotient F → Prop)
    (Prequotient.of j' (((F.map f).hom' : (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v)) x)) (Prequotient.of j x)

Tactic:
apply Relation.map

Premises used: CommRingCat.Colimits.Relation.map
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
rw :
  Eq (α := (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (coconeMorphism F j') :
          (a : (↑(F.obj j') : Type v)) → (↑(colimit F) : Type v))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
          x) :
      (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (F.map f ≫ coconeMorphism F j') :
          (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v))
        x :
      (↑(colimit F) : Type v))
rw₁ rw₂ :
  Eq (α := (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (coconeMorphism F j') :
          (a : (↑(F.obj j') : Type v)) → (↑(colimit F) : Type v))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
          x) :
      (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (coconeMorphism F j') :
          (a : (↑(F.obj j') : Type v)) → (↑(colimit F) : Type v))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
          x) :
      (↑(colimit F) : Type v))
⊢ Eq (α := (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (coconeMorphism F j') :
          (a : (↑(F.obj j') : Type v)) → (↑(colimit F) : Type v))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
          x) :
      (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (coconeMorphism F j) :
          (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v))
        x :
      (↑(colimit F) : Type v))

Tactic:
rw [← cocone_naturality F f, comp_apply]

Premises used: CommRingCat.Colimits.cocone_naturality, CommRingCat.comp_apply
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
f : (a : Prequotient F) → (↑s.pt : Type v)
a :
  ∀ (a b : Prequotient F) (a_1 : (colimitSetoid F : Prequotient F → Prequotient F → Prop) a b),
    descFunLift F s a = descFunLift F s b
⊢ ColimitType F → (↑s.pt : Type v)

Tactic:
fapply Quot.lift

Premises used: Quot.lift
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
⊢ (a : Prequotient F) → (↑s.pt : Type v)

Tactic:
exact descFunLift F s

Premises used: CommRingCat.Colimits.descFunLift
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y x_1 : Prequotient F
⊢ descFunLift F s x_1 = descFunLift F s x_1

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y : Prequotient F
h : Relation F x y
ih : descFunLift F s x = descFunLift F s y
⊢ descFunLift F s y = descFunLift F s x

Tactic:
ih.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y : Prequotient F
h : Relation F x y
ih : descFunLift F s x = descFunLift F s y
⊢ descFunLift F s y = descFunLift F s x

Tactic:
exact ih.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
h : Relation F x y
h_1 : Relation F y z
ih1 : descFunLift F s x = descFunLift F s y
ih2 : descFunLift F s y = descFunLift F s z
⊢ descFunLift F s x = descFunLift F s z

Tactic:
ih1.trans ih2

Premises used: Eq.trans
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
h : Relation F x y
h_1 : Relation F y z
ih1 : descFunLift F s x = descFunLift F s y
ih2 : descFunLift F s y = descFunLift F s z
⊢ descFunLift F s x = descFunLift F s z

Tactic:
exact ih1.trans ih2

Premises used: Eq.trans
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y : Prequotient F
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
⊢ descFunLift F s
      (Prequotient.of j'
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
          x)) =
    descFunLift F s (Prequotient.of j x)

Tactic:
RingHom.congr_fun (congrArg Hom.hom <| s.ι.naturality f) x

Premises used: CommRingCat.Hom.hom, congrArg, RingHom.congr_fun, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality, CommRingCat.Colimits.descFunLift
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y : Prequotient F
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
⊢ descFunLift F s
      (Prequotient.of j'
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
          x)) =
    descFunLift F s (Prequotient.of j x)

Tactic:
exact RingHom.congr_fun (congrArg Hom.hom <| s.ι.naturality f) x

Premises used: CommRingCat.Hom.hom, congrArg, RingHom.congr_fun, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : Prequotient F
j : J
⊢ descFunLift F s (Prequotient.of j 0) = descFunLift F s zero

Tactic:
simp +instances
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : Prequotient F
j : J
⊢ descFunLift F s (Prequotient.of j 1) = descFunLift F s one

Tactic:
simp +instances
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y : Prequotient F
j : J
x : (↑(F.obj j) : Type v)
⊢ descFunLift F s (Prequotient.of j (-x)) = descFunLift F s (Prequotient.of j x).neg

Tactic:
simp +instances
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 : Prequotient F
j : J
x y : (↑(F.obj j) : Type v)
⊢ descFunLift F s (Prequotient.of j (x + y)) = descFunLift F s ((Prequotient.of j x).add (Prequotient.of j y))

Tactic:
simp +instances
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 : Prequotient F
j : J
x y : (↑(F.obj j) : Type v)
⊢ descFunLift F s (Prequotient.of j (x * y)) = descFunLift F s ((Prequotient.of j x).mul (Prequotient.of j y))

Tactic:
simp +instances
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x x' : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
a : -descFunLift F s x = -descFunLift F s x'
⊢ descFunLift F s x.neg = descFunLift F s x'.neg

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x x' : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
a a₁ : -descFunLift F s x' = -descFunLift F s x'
⊢ -descFunLift F s x = -descFunLift F s x'

Tactic:
rw [ih]
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
a : descFunLift F s x + descFunLift F s y = descFunLift F s x' + descFunLift F s y
⊢ descFunLift F s (x.add y) = descFunLift F s (x'.add y)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
a a₁ : descFunLift F s x' + descFunLift F s y = descFunLift F s x' + descFunLift F s y
⊢ descFunLift F s x + descFunLift F s y = descFunLift F s x' + descFunLift F s y

Tactic:
rw [ih]
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
a : descFunLift F s x + descFunLift F s y = descFunLift F s x + descFunLift F s y'
⊢ descFunLift F s (x.add y) = descFunLift F s (x.add y')

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
a a₁ : descFunLift F s x + descFunLift F s y' = descFunLift F s x + descFunLift F s y'
⊢ descFunLift F s x + descFunLift F s y = descFunLift F s x + descFunLift F s y'

Tactic:
rw [ih]
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
a : descFunLift F s x * descFunLift F s y = descFunLift F s x' * descFunLift F s y
⊢ descFunLift F s (x.mul y) = descFunLift F s (x'.mul y)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
a a₁ : descFunLift F s x' * descFunLift F s y = descFunLift F s x' * descFunLift F s y
⊢ descFunLift F s x * descFunLift F s y = descFunLift F s x' * descFunLift F s y

Tactic:
rw [ih]
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
a : descFunLift F s x * descFunLift F s y = descFunLift F s x * descFunLift F s y'
⊢ descFunLift F s (x.mul y) = descFunLift F s (x.mul y')

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
a a₁ : descFunLift F s x * descFunLift F s y' = descFunLift F s x * descFunLift F s y'
⊢ descFunLift F s x * descFunLift F s y = descFunLift F s x * descFunLift F s y'

Tactic:
rw [ih]
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
a : 0 + descFunLift F s x = descFunLift F s x
⊢ descFunLift F s (add zero x) = descFunLift F s x

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
a a₁ : descFunLift F s x = descFunLift F s x
⊢ 0 + descFunLift F s x = descFunLift F s x

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
a : descFunLift F s x + 0 = descFunLift F s x
⊢ descFunLift F s (x.add zero) = descFunLift F s x

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
a a₁ : descFunLift F s x = descFunLift F s x
⊢ descFunLift F s x + 0 = descFunLift F s x

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
a : 1 * descFunLift F s x = descFunLift F s x
⊢ descFunLift F s (mul one x) = descFunLift F s x

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
a a₁ : descFunLift F s x = descFunLift F s x
⊢ 1 * descFunLift F s x = descFunLift F s x

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
a : descFunLift F s x * 1 = descFunLift F s x
⊢ descFunLift F s (x.mul one) = descFunLift F s x

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
a a₁ : descFunLift F s x = descFunLift F s x
⊢ descFunLift F s x * 1 = descFunLift F s x

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
a : -descFunLift F s x + descFunLift F s x = 0
⊢ descFunLift F s (x.neg.add x) = descFunLift F s zero

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
a a₁ : Eq.{v + 1} (α := (↑s.pt : Type v)) 0 0
⊢ -descFunLift F s x + descFunLift F s x = 0

Tactic:
rw [neg_add_cancel]

Premises used: neg_add_cancel
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y : Prequotient F
a : descFunLift F s x + descFunLift F s y = descFunLift F s y + descFunLift F s x
⊢ descFunLift F s (x.add y) = descFunLift F s (y.add x)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y : Prequotient F
a a₁ : descFunLift F s y + descFunLift F s x = descFunLift F s y + descFunLift F s x
⊢ descFunLift F s x + descFunLift F s y = descFunLift F s y + descFunLift F s x

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y : Prequotient F
a : descFunLift F s x * descFunLift F s y = descFunLift F s y * descFunLift F s x
⊢ descFunLift F s (x.mul y) = descFunLift F s (y.mul x)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y : Prequotient F
a a₁ : descFunLift F s y * descFunLift F s x = descFunLift F s y * descFunLift F s x
⊢ descFunLift F s x * descFunLift F s y = descFunLift F s y * descFunLift F s x

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
a :
  descFunLift F s x + descFunLift F s y + descFunLift F s z =
    descFunLift F s x + (descFunLift F s y + descFunLift F s z)
⊢ descFunLift F s ((x.add y).add z) = descFunLift F s (x.add (y.add z))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
a a₁ :
  descFunLift F s x + (descFunLift F s y + descFunLift F s z) =
    descFunLift F s x + (descFunLift F s y + descFunLift F s z)
⊢ descFunLift F s x + descFunLift F s y + descFunLift F s z =
    descFunLift F s x + (descFunLift F s y + descFunLift F s z)

Tactic:
rw [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
a :
  descFunLift F s x * descFunLift F s y * descFunLift F s z =
    descFunLift F s x * (descFunLift F s y * descFunLift F s z)
⊢ descFunLift F s ((x.mul y).mul z) = descFunLift F s (x.mul (y.mul z))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
a a₁ :
  descFunLift F s x * (descFunLift F s y * descFunLift F s z) =
    descFunLift F s x * (descFunLift F s y * descFunLift F s z)
⊢ descFunLift F s x * descFunLift F s y * descFunLift F s z =
    descFunLift F s x * (descFunLift F s y * descFunLift F s z)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
a :
  descFunLift F s x * (descFunLift F s y + descFunLift F s z) =
    descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z
⊢ descFunLift F s (x.mul (y.add z)) = descFunLift F s ((x.mul y).add (x.mul z))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
a a₁ :
  descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z =
    descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z
⊢ descFunLift F s x * (descFunLift F s y + descFunLift F s z) =
    descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z

Tactic:
rw [mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
a :
  (descFunLift F s x + descFunLift F s y) * descFunLift F s z =
    descFunLift F s x * descFunLift F s z + descFunLift F s y * descFunLift F s z
⊢ descFunLift F s ((x.add y).mul z) = descFunLift F s ((x.mul z).add (y.mul z))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
a a₁ :
  descFunLift F s x * descFunLift F s z + descFunLift F s y * descFunLift F s z =
    descFunLift F s x * descFunLift F s z + descFunLift F s y * descFunLift F s z
⊢ (descFunLift F s x + descFunLift F s y) * descFunLift F s z =
    descFunLift F s x * descFunLift F s z + descFunLift F s y * descFunLift F s z

Tactic:
rw [add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
a : 0 * descFunLift F s x = 0
⊢ descFunLift F s (mul zero x) = descFunLift F s zero

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
a a₁ : Eq.{v + 1} (α := (↑s.pt : Type v)) 0 0
⊢ 0 * descFunLift F s x = 0

Tactic:
rw [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
a : descFunLift F s x * 0 = 0
⊢ descFunLift F s (x.mul zero) = descFunLift F s zero

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
a a₁ : Eq.{v + 1} (α := (↑s.pt : Type v)) 0 0
⊢ descFunLift F s x * 0 = 0

Tactic:
rw [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ColimitType F
⊢ descFun F s (x * y) = descFun F s x * descFun F s y

Tactic:
Quot.induction_on₂ x y fun a b => rfl

Premises used: Quot.induction_on₂
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ColimitType F
⊢ descFun F s (x * y) = descFun F s x * descFun F s y

Tactic:
exact Quot.induction_on₂ x y fun a b => rfl