awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
x_1 y_1 z_1 : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
      (Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y))
      (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) z) =
    Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
      (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
      (Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) z))

Tactic:
exact Quot.sound (Relation.mul_assoc _ _ _)

Premises used: Quot.sound, RingCat.Colimits.Relation.mul_assoc
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
x_1 y_1 z_1 : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
      (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
      (Quotient.map₂ add ⋯ (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) z)) =
    Quotient.map₂ add ⋯
      (Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y))
      (Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) z))

Tactic:
Quot.sound (Relation.left_distrib _ _ _)

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, Quotient.map₂, Quotient, RingCat.Colimits.ColimitType, RingCat.Colimits.Relation.left_distrib
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
x_1 y_1 z_1 : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
      (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
      (Quotient.map₂ add ⋯ (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) z)) =
    Quotient.map₂ add ⋯
      (Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y))
      (Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) z))

Tactic:
exact Quot.sound (Relation.left_distrib _ _ _)

Premises used: Quot.sound, RingCat.Colimits.Relation.left_distrib
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
x_1 y_1 z_1 : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
      (Quotient.map₂ add ⋯ (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y))
      (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) z) =
    Quotient.map₂ add ⋯
      (Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) z))
      (Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) z))

Tactic:
Quot.sound (Relation.right_distrib _ _ _)

Premises used: RingCat.Colimits.Relation.right_distrib, Quot.sound, Quot.map₂, Quot.lift₂, Quotient.map₂, Quotient, RingCat.Colimits.ColimitType
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
x_1 y_1 z_1 : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
      (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
      (Quotient.map₂ add ⋯ (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y))
      (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) z) =
    Quotient.map₂ add ⋯
      (Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) z))
      (Quot.map₂ (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (s :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (t :=
        (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) mul ⋯ ⋯
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) z))

Tactic:
exact Quot.sound (Relation.right_distrib _ _ _)

Premises used: RingCat.Colimits.Relation.right_distrib, Quot.sound
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
⊢ Eq.{v + 1} (α := Quot (α := Prequotient F) (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop))
    (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) zero) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
⊢ Eq.{v + 1} (α := Quot (α := Prequotient F) (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop))
    (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) one) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
x : Prequotient F
⊢ Eq (α := Quot (α := Prequotient F) (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop))
    (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x.neg)
    (-have this : ColimitType F := Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x;
      this)

Tactic:
rfl

Premises used: Quotient.map, Quot.map, rfl
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
x y : Prequotient F
⊢ Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (x.add y) =
    HAdd.hAdd (α := ColimitType F)
      (have this : ColimitType F := Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x;
      this)
      (have this : ColimitType F := Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y;
      this)

Tactic:
rfl

Premises used: Quotient.map₂, rfl
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
x y : Prequotient F
⊢ Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (x.mul y) =
    HMul.hMul (α := ColimitType F)
      (have this : ColimitType F := Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x;
      this)
      (have this : ColimitType F := Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y;
      this)

Tactic:
rfl

Premises used: Quot.map₂, Quot.lift₂, rfl
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
j : J
a : (colimitSetoid F : Prequotient F → Prequotient F → Prop) (Prequotient.of j 1) one
⊢ coconeFun F j 1 = 1

Tactic:
apply Quot.sound

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

Tactic:
apply Relation.one

Premises used: RingCat.Colimits.Relation.one
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
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 ⥤ RingCat
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: RingCat.Colimits.Relation.mul
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
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 ⥤ RingCat
j : J
⊢ (colimitSetoid F : Prequotient F → Prequotient F → Prop) (Prequotient.of j 0) zero

Tactic:
apply Relation.zero

Premises used: RingCat.Colimits.Relation.zero
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
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 ⥤ RingCat
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: RingCat.Colimits.Relation.add
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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: RingCat.Colimits.Relation.map
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
rw :
  Eq (α := (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{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 : RingCat.{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 : RingCat.{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 : RingCat.{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 : RingCat.{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 : RingCat.{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 : RingCat.{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 : RingCat.{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 : RingCat.{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 : RingCat.{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: RingCat.Colimits.cocone_naturality, RingCat.comp_apply
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
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 ⥤ RingCat
s : Cocone F
⊢ (a : Prequotient F) → (↑s.pt : Type v)

Tactic:
exact descFunLift F s

Premises used: RingCat.Colimits.descFunLift
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 : RingCat.{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: congrArg, RingHom.congr_fun, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality, RingCat.Colimits.descFunLift, RingCat.Hom.hom
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
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 : RingCat.{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: congrArg, RingHom.congr_fun, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality, RingCat.Hom.hom
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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