awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 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 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 ⥤ 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.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 ⥤ 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 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 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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
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 => ?_

Premises used: Quot.induction_on₂
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x y : ColimitType F
refine :
  ∀ (a b : Prequotient F),
    descFun F s
        (HAdd.hAdd (α := ColimitType F) (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a)
          (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) b)) =
      descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a) +
        descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) b)
⊢ descFun F s (x + y) = descFun F s x + descFun F s y

Tactic:
refine Quot.induction_on₂ x y fun a b => ?_
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x y : ColimitType F
a b : Prequotient F
dsimp :
  Quot.lift (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (descFunLift F s) ⋯
      (HAdd.hAdd (α := ColimitType F) (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) b)) =
    descFunLift F s a + descFunLift F s b
⊢ descFun F s
      (HAdd.hAdd (α := ColimitType F) (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) b)) =
    descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a) +
      descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) b)

Tactic:
dsimp [descFun]

Premises used: RingCat.Colimits.descFun
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x y : ColimitType F
a b : Prequotient F
⊢ Quot.lift (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (descFunLift F s) ⋯
      (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (a.add b)) =
    descFunLift F s a + descFunLift F s b

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : (↑(colimitCocone F).pt : Type v)
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))

Tactic:
Quot.inductionOn x ?_

Premises used: Quot.inductionOn
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : (↑(colimitCocone F).pt : Type v)
refine :
  ∀ (a : Prequotient F),
    Eq (α := (↑s.pt : Type v))
      ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
          (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a) :
        (↑s.pt : Type v))
      ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
          (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a) :
        (↑s.pt : Type v))
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))

Tactic:
refine Quot.inductionOn x ?_
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : (↑(colimitCocone F).pt : Type v)
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) zero) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) zero) :
      (↑s.pt : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : (↑(colimitCocone F).pt : Type v)
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) one) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) one) :
      (↑s.pt : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x_1 : (↑(colimitCocone F).pt : Type v)
x : Prequotient F
ih :
  Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
      (↑s.pt : Type v))
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x.neg) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x.neg) :
      (↑s.pt : Type v))

Tactic:
simp [ih]
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x_1 : (↑(colimitCocone F).pt : Type v)
j : J
x : (↑(F.obj j) : Type v)
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (Prequotient.of j x)) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (Prequotient.of j x)) :
      (↑s.pt : Type v))

Tactic:
congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x

Premises used: CategoryTheory.ConcreteCategory.hom, RingCat.Colimits.coconeFun, congr_arg, RingCat.Colimits.descFun, RingCat.Colimits.descFunLift, congr_fun, DFunLike.coe
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x_1 : (↑(colimitCocone F).pt : Type v)
j : J
x : (↑(F.obj j) : Type v)
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (Prequotient.of j x)) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (Prequotient.of j x)) :
      (↑s.pt : Type v))

Tactic:
exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x

Premises used: CategoryTheory.ConcreteCategory.hom, congr_arg, congr_fun, DFunLike.coe
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x_1 : (↑(colimitCocone F).pt : Type v)
x y : Prequotient F
ih_x :
  Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
      (↑s.pt : Type v))
ih_y :
  Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y) :
      (↑s.pt : Type v))
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (x.add y)) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (x.add y)) :
      (↑s.pt : Type v))

Tactic:
simp [ih_x, ih_y]
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x_1 : (↑(colimitCocone F).pt : Type v)
x y : Prequotient F
ih_x :
  Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
      (↑s.pt : Type v))
ih_y :
  Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y) :
      (↑s.pt : Type v))
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (x.mul y)) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (x.mul y)) :
      (↑s.pt : Type v))

Tactic:
simp [ih_x, ih_y]
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
⊢ 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 ⥤ CommRingCat
⊢ 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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
j : J
⊢ (colimitSetoid F : Prequotient F → Prequotient F → Prop) (Prequotient.of j 1) one

Tactic:
apply Relation.one

Premises used: CommRingCat.Colimits.Relation.one