[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j : J
⊢ ∀ (x y : ↑(F.obj j)), coconeFun F j (x + y) = coconeFun F j x + coconeFun F j y
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j : J
x✝ y✝ : ↑(F.obj j)
⊢ coconeFun F j (x✝ + y✝) = coconeFun F j x✝ + coconeFun F j y✝
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j : J
x✝ y✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j (x✝ + y✝)) (add (Prequotient.of j x✝) (Prequotient.of j y✝))
[PROOFSTEP]
apply Relation.add
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j : J
⊢ ∀ (r : R) (x : ↑(F.obj j)),
    AddHom.toFun
        { toFun := coconeFun F j,
          map_add' :=
            (_ :
              ∀ (x y : ↑(F.obj j)),
                Quot.mk Setoid.r (Prequotient.of j (x + y)) =
                  Quot.mk Setoid.r (add (Prequotient.of j x) (Prequotient.of j y))) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := coconeFun F j,
            map_add' :=
              (_ :
                ∀ (x y : ↑(F.obj j)),
                  Quot.mk Setoid.r (Prequotient.of j (x + y)) =
                    Quot.mk Setoid.r (add (Prequotient.of j x) (Prequotient.of j y))) }
          x
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j : J
r✝ : R
x✝ : ↑(F.obj j)
⊢ AddHom.toFun
      { toFun := coconeFun F j,
        map_add' :=
          (_ :
            ∀ (x y : ↑(F.obj j)),
              Quot.mk Setoid.r (Prequotient.of j (x + y)) =
                Quot.mk Setoid.r (add (Prequotient.of j x) (Prequotient.of j y))) }
      (r✝ • x✝) =
    ↑(RingHom.id R) r✝ •
      AddHom.toFun
        { toFun := coconeFun F j,
          map_add' :=
            (_ :
              ∀ (x y : ↑(F.obj j)),
                Quot.mk Setoid.r (Prequotient.of j (x + y)) =
                  Quot.mk Setoid.r (add (Prequotient.of j x) (Prequotient.of j y))) }
        x✝
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j : J
r✝ : R
x✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j (r✝ • x✝)) (smul (↑(RingHom.id R) r✝) (Prequotient.of j x✝))
[PROOFSTEP]
apply Relation.smul
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ ↑(F.map f ≫ coconeMorphism F j') x✝ = ↑(coconeMorphism F j) x✝
[PROOFSTEP]
apply Quot.sound
[GOAL]
case h.a
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j' (↑(F.map f) x✝)) (Prequotient.of j x✝)
[PROOFSTEP]
apply ModuleCat.Colimits.Relation.map
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ↑(coconeMorphism F j') (↑(F.map f) x) = ↑(coconeMorphism F j) x
[PROOFSTEP]
rw [← cocone_naturality F f]
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ↑(coconeMorphism F j') (↑(F.map f) x) = ↑(F.map f ≫ coconeMorphism F j') x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
⊢ ColimitType F → ↑s.pt
[PROOFSTEP]
fapply Quot.lift
[GOAL]
case f
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
⊢ Prequotient F → ↑s.pt
[PROOFSTEP]
exact descFunLift F s
[GOAL]
case a
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
⊢ ∀ (a b : Prequotient F), Setoid.r a b → descFunLift F s a = descFunLift F s b
[PROOFSTEP]
intro x y r
[GOAL]
case a
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
r : Setoid.r x y
⊢ descFunLift F s x = descFunLift F s y
[PROOFSTEP]
induction' r with h₁ r_x r_y r_h r_ih r_x r_y r_z r_h r_k r_ih_h r_ih_k r_j r_j' r_f r_x j j x j x y j s x u v r r_ih u
  v w r r_ih u v w r r_ih s u v r r_ih
[GOAL]
case a.refl
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y h₁ : Prequotient F
⊢ descFunLift F s h₁ = descFunLift F s h₁
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.refl
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y h₁ : Prequotient F
⊢ descFunLift F s h₁ = descFunLift F s h₁
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.symm
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y r_x r_y : Prequotient F
r_h : Relation F r_x r_y
r_ih : descFunLift F s r_x = descFunLift F s r_y
⊢ descFunLift F s r_y = descFunLift F s r_x
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.symm
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y r_x r_y : Prequotient F
r_h : Relation F r_x r_y
r_ih : descFunLift F s r_x = descFunLift F s r_y
⊢ descFunLift F s r_y = descFunLift F s r_x
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.trans
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y r_x r_y r_z : Prequotient F
r_h : Relation F r_x r_y
r_k : Relation F r_y r_z
r_ih_h : descFunLift F s r_x = descFunLift F s r_y
r_ih_k : descFunLift F s r_y = descFunLift F s r_z
⊢ descFunLift F s r_x = descFunLift F s r_z
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.trans
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y r_x r_y r_z : Prequotient F
r_h : Relation F r_x r_y
r_k : Relation F r_y r_z
r_ih_h : descFunLift F s r_x = descFunLift F s r_y
r_ih_k : descFunLift F s r_y = descFunLift F s r_z
⊢ descFunLift F s r_x = descFunLift F s r_z
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.map
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
r_j r_j' : J
r_f : r_j ⟶ r_j'
r_x : ↑(F.obj r_j)
⊢ descFunLift F s (Prequotient.of r_j' (↑(F.map r_f) r_x)) = descFunLift F s (Prequotient.of r_j r_x)
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.map
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
r_j r_j' : J
r_f : r_j ⟶ r_j'
r_x : ↑(F.obj r_j)
⊢ descFunLift F s (Prequotient.of r_j' (↑(F.map r_f) r_x)) = descFunLift F s (Prequotient.of r_j r_x)
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
j : J
⊢ descFunLift F s (Prequotient.of j 0) = descFunLift F s zero
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
j : J
⊢ descFunLift F s (Prequotient.of j 0) = descFunLift F s zero
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.neg
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x✝ y : Prequotient F
j : J
x : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j (-x)) = descFunLift F s (neg (Prequotient.of j x))
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.neg
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x✝ y : Prequotient F
j : J
x : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j (-x)) = descFunLift F s (neg (Prequotient.of j x))
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x✝ y✝ : Prequotient F
j : J
x y : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j (x + y)) = descFunLift F s (add (Prequotient.of j x) (Prequotient.of j y))
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x✝ y✝ : Prequotient F
j : J
x y : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j (x + y)) = descFunLift F s (add (Prequotient.of j x) (Prequotient.of j y))
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
x✝ y : Prequotient F
j : J
s : R
x : ↑(F.obj j)
⊢ descFunLift F s✝ (Prequotient.of j (s • x)) = descFunLift F s✝ (smul s (Prequotient.of j x))
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
x✝ y : Prequotient F
j : J
s : R
x : ↑(F.obj j)
⊢ descFunLift F s✝ (Prequotient.of j (s • x)) = descFunLift F s✝ (smul s (Prequotient.of j x))
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.neg_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v : Prequotient F
r : Relation F u v
r_ih : descFunLift F s u = descFunLift F s v
⊢ descFunLift F s (neg u) = descFunLift F s (neg v)
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.neg_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v : Prequotient F
r : Relation F u v
r_ih : descFunLift F s u = descFunLift F s v
⊢ descFunLift F s (neg u) = descFunLift F s (neg v)
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v w : Prequotient F
r : Relation F u v
r_ih : descFunLift F s u = descFunLift F s v
⊢ descFunLift F s (add u w) = descFunLift F s (add v w)
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v w : Prequotient F
r : Relation F u v
r_ih : descFunLift F s u = descFunLift F s v
⊢ descFunLift F s (add u w) = descFunLift F s (add v w)
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add_2
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v w : Prequotient F
r : Relation F v w
r_ih : descFunLift F s v = descFunLift F s w
⊢ descFunLift F s (add u v) = descFunLift F s (add u w)
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add_2
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v w : Prequotient F
r : Relation F v w
r_ih : descFunLift F s v = descFunLift F s w
⊢ descFunLift F s (add u v) = descFunLift F s (add u w)
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.smul_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
x y : Prequotient F
s : R
u v : Prequotient F
r : Relation F u v
r_ih : descFunLift F s✝ u = descFunLift F s✝ v
⊢ descFunLift F s✝ (smul s u) = descFunLift F s✝ (smul s v)
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.smul_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
x y : Prequotient F
s : R
u v : Prequotient F
r : Relation F u v
r_ih : descFunLift F s✝ u = descFunLift F s✝ v
⊢ descFunLift F s✝ (smul s u) = descFunLift F s✝ (smul s v)
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.zero_add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add zero x✝) = descFunLift F s x✝
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.zero_add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add zero x✝) = descFunLift F s x✝
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add_zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add x✝ zero) = descFunLift F s x✝
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add_zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add x✝ zero) = descFunLift F s x✝
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add_left_neg
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add (neg x✝) x✝) = descFunLift F s zero
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add_left_neg
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (add (neg x✝) x✝) = descFunLift F s zero
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add_comm
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ y✝ : Prequotient F
⊢ descFunLift F s (add x✝ y✝) = descFunLift F s (add y✝ x✝)
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add_comm
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ y✝ : Prequotient F
⊢ descFunLift F s (add x✝ y✝) = descFunLift F s (add y✝ x✝)
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add_assoc
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ y✝ z✝ : Prequotient F
⊢ descFunLift F s (add (add x✝ y✝) z✝) = descFunLift F s (add x✝ (add y✝ z✝))
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add_assoc
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ y✝ z✝ : Prequotient F
⊢ descFunLift F s (add (add x✝ y✝) z✝) = descFunLift F s (add x✝ (add y✝ z✝))
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.one_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (smul 1 x✝) = descFunLift F s x✝
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.one_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (smul 1 x✝) = descFunLift F s x✝
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.mul_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ t✝ : R
x✝ : Prequotient F
⊢ descFunLift F s (smul (s✝ * t✝) x✝) = descFunLift F s (smul s✝ (smul t✝ x✝))
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.mul_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ t✝ : R
x✝ : Prequotient F
⊢ descFunLift F s (smul (s✝ * t✝) x✝) = descFunLift F s (smul s✝ (smul t✝ x✝))
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.smul_add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ : R
x✝ y✝ : Prequotient F
⊢ descFunLift F s (smul s✝ (add x✝ y✝)) = descFunLift F s (add (smul s✝ x✝) (smul s✝ y✝))
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.smul_add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ : R
x✝ y✝ : Prequotient F
⊢ descFunLift F s (smul s✝ (add x✝ y✝)) = descFunLift F s (add (smul s✝ x✝) (smul s✝ y✝))
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.smul_zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ : R
⊢ descFunLift F s (smul s✝ zero) = descFunLift F s zero
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.smul_zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ : R
⊢ descFunLift F s (smul s✝ zero) = descFunLift F s zero
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.add_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ t✝ : R
x✝ : Prequotient F
⊢ descFunLift F s (smul (s✝ + t✝) x✝) = descFunLift F s (add (smul s✝ x✝) (smul t✝ x✝))
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.add_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ t✝ : R
x✝ : Prequotient F
⊢ descFunLift F s (smul (s✝ + t✝) x✝) = descFunLift F s (add (smul s✝ x✝) (smul t✝ x✝))
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.zero_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (smul 0 x✝) = descFunLift F s zero
[PROOFSTEP]
try
  dsimp
    -- refl
        -- · rfl -- porting note: `dsimp` (above) now closes this
        -- symm
[GOAL]
case a.zero_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s (smul 0 x✝) = descFunLift F s zero
[PROOFSTEP]
dsimp
  -- refl
      -- · rfl -- porting note: `dsimp` (above) now closes this
      -- symm
[GOAL]
case a.symm
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y r_x r_y : Prequotient F
r_h : Relation F r_x r_y
r_ih : descFunLift F s r_x = descFunLift F s r_y
⊢ descFunLift F s r_y = descFunLift F s r_x
[PROOFSTEP]
exact r_ih.symm
[GOAL]
case a.trans
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y r_x r_y r_z : Prequotient F
r_h : Relation F r_x r_y
r_k : Relation F r_y r_z
r_ih_h : descFunLift F s r_x = descFunLift F s r_y
r_ih_k : descFunLift F s r_y = descFunLift F s r_z
⊢ descFunLift F s r_x = descFunLift F s r_z
[PROOFSTEP]
exact Eq.trans r_ih_h r_ih_k
[GOAL]
case a.map
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
r_j r_j' : J
r_f : r_j ⟶ r_j'
r_x : ↑(F.obj r_j)
⊢ ↑(NatTrans.app s.ι r_j') (↑(F.map r_f) r_x) = ↑(NatTrans.app s.ι r_j) r_x
[PROOFSTEP]
exact s.w_apply r_f r_x
[GOAL]
case a.zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
j : J
⊢ ↑(NatTrans.app s.ι j) 0 = 0
[PROOFSTEP]
simp
  -- neg
[GOAL]
case a.neg
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x✝ y : Prequotient F
j : J
x : ↑(F.obj j)
⊢ ↑(NatTrans.app s.ι j) (-x) = -↑(NatTrans.app s.ι j) x
[PROOFSTEP]
simp
  -- add
[GOAL]
case a.add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x✝ y✝ : Prequotient F
j : J
x y : ↑(F.obj j)
⊢ ↑(NatTrans.app s.ι j) (x + y) = ↑(NatTrans.app s.ι j) x + ↑(NatTrans.app s.ι j) y
[PROOFSTEP]
simp
  -- smul,
[GOAL]
case a.smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
x✝ y : Prequotient F
j : J
s : R
x : ↑(F.obj j)
⊢ ↑(NatTrans.app s✝.ι j) (s • x) = s • ↑(NatTrans.app s✝.ι j) x
[PROOFSTEP]
simp
  -- neg_1
[GOAL]
case a.neg_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v : Prequotient F
r : Relation F u v
r_ih : descFunLift F s u = descFunLift F s v
⊢ -descFunLift F s u = -descFunLift F s v
[PROOFSTEP]
rw [r_ih]
  -- add_1
[GOAL]
case a.add_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v w : Prequotient F
r : Relation F u v
r_ih : descFunLift F s u = descFunLift F s v
⊢ descFunLift F s u + descFunLift F s w = descFunLift F s v + descFunLift F s w
[PROOFSTEP]
rw [r_ih]
  -- add_2
[GOAL]
case a.add_2
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y u v w : Prequotient F
r : Relation F v w
r_ih : descFunLift F s v = descFunLift F s w
⊢ descFunLift F s u + descFunLift F s v = descFunLift F s u + descFunLift F s w
[PROOFSTEP]
rw [r_ih]
  -- smul_1
[GOAL]
case a.smul_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
x y : Prequotient F
s : R
u v : Prequotient F
r : Relation F u v
r_ih : descFunLift F s✝ u = descFunLift F s✝ v
⊢ s • descFunLift F s✝ u = s • descFunLift F s✝ v
[PROOFSTEP]
rw [r_ih]
  -- zero_add
[GOAL]
case a.zero_add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ 0 + descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]
rw [zero_add]
  -- add_zero
[GOAL]
case a.add_zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ + 0 = descFunLift F s x✝
[PROOFSTEP]
rw [add_zero]
  -- add_left_neg
[GOAL]
case a.add_left_neg
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ -descFunLift F s x✝ + descFunLift F s x✝ = 0
[PROOFSTEP]
rw [add_left_neg]
  -- add_comm
[GOAL]
case a.add_comm
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ y✝ : Prequotient F
⊢ descFunLift F s x✝ + descFunLift F s y✝ = descFunLift F s y✝ + descFunLift F s x✝
[PROOFSTEP]
rw [add_comm]
  -- add_assoc
[GOAL]
case a.add_assoc
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ y✝ z✝ : Prequotient F
⊢ descFunLift F s x✝ + descFunLift F s y✝ + descFunLift F s z✝ =
    descFunLift F s x✝ + (descFunLift F s y✝ + descFunLift F s z✝)
[PROOFSTEP]
rw [add_assoc]
  -- one_smul
[GOAL]
case a.one_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ 1 • descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]
rw [one_smul]
  -- mul_smul
[GOAL]
case a.mul_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ t✝ : R
x✝ : Prequotient F
⊢ (s✝ * t✝) • descFunLift F s x✝ = s✝ • t✝ • descFunLift F s x✝
[PROOFSTEP]
rw [mul_smul]
  -- smul_add
[GOAL]
case a.smul_add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ : R
x✝ y✝ : Prequotient F
⊢ s✝ • (descFunLift F s x✝ + descFunLift F s y✝) = s✝ • descFunLift F s x✝ + s✝ • descFunLift F s y✝
[PROOFSTEP]
rw [smul_add]
  -- smul_zero
[GOAL]
case a.smul_zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ : R
⊢ s✝ • 0 = 0
[PROOFSTEP]
rw [smul_zero]
  -- add_smul
[GOAL]
case a.add_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : Prequotient F
s✝ t✝ : R
x✝ : Prequotient F
⊢ (s✝ + t✝) • descFunLift F s x✝ = s✝ • descFunLift F s x✝ + t✝ • descFunLift F s x✝
[PROOFSTEP]
rw [add_smul]
  -- zero_smul
[GOAL]
case a.zero_smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y x✝ : Prequotient F
⊢ 0 • descFunLift F s x✝ = 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : ↑(colimit F)
⊢ descFun F s (x + y) = descFun F s x + descFun F s y
[PROOFSTEP]
rcases x
[GOAL]
case mk
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : ↑(colimit F)
a✝ : Prequotient F
⊢ descFun F s (Quot.mk Setoid.r a✝ + y) = descFun F s (Quot.mk Setoid.r a✝) + descFun F s y
[PROOFSTEP]
rcases y
[GOAL]
case mk.mk
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
x y : ↑(colimit F)
a✝¹ a✝ : Prequotient F
⊢ descFun F s (Quot.mk Setoid.r a✝¹ + Quot.mk Setoid.r a✝) =
    descFun F s (Quot.mk Setoid.r a✝¹) + descFun F s (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
s : R
x : ↑(colimit F)
⊢ AddHom.toFun
      { toFun := descFun F s✝,
        map_add' := (_ : ∀ (x y : ↑(colimit F)), descFun F s✝ (x + y) = descFun F s✝ x + descFun F s✝ y) }
      (s • x) =
    ↑(RingHom.id R) s •
      AddHom.toFun
        { toFun := descFun F s✝,
          map_add' := (_ : ∀ (x y : ↑(colimit F)), descFun F s✝ (x + y) = descFun F s✝ x + descFun F s✝ y) }
        x
[PROOFSTEP]
rcases x
[GOAL]
case mk
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s✝ : Cocone F
s : R
x : ↑(colimit F)
a✝ : Prequotient F
⊢ AddHom.toFun
      { toFun := descFun F s✝,
        map_add' := (_ : ∀ (x y : ↑(colimit F)), descFun F s✝ (x + y) = descFun F s✝ x + descFun F s✝ y) }
      (s • Quot.mk Setoid.r a✝) =
    ↑(RingHom.id R) s •
      AddHom.toFun
        { toFun := descFun F s✝,
          map_add' := (_ : ∀ (x y : ↑(colimit F)), descFun F s✝ (x + y) = descFun F s✝ x + descFun F s✝ y) }
        (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => descMorphism F s) s
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
⊢ ↑m x = ↑((fun s => descMorphism F s) s) x
[PROOFSTEP]
refine Quot.rec (motive := fun x ↦ m x = _) (fun x ↦ ?_) (fun x_a x_b x_p ↦ ?_) x
[GOAL]
case h.refine_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : ↑(colimitCocone F).pt
x : Prequotient F
⊢ (fun x => ↑m x = ↑((fun s => descMorphism F s) s) x) (Quot.mk Setoid.r x)
case h.refine_2
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
x_a x_b : Prequotient F
x_p : Setoid.r x_a x_b
⊢ (_ : ↑m (Quot.mk Setoid.r x_b) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x_b)) =
    (_ : (fun x => ↑m x = ↑((fun s => descMorphism F s) s) x) (Quot.mk Setoid.r x_b))
[PROOFSTEP]
dsimp
[GOAL]
case h.refine_1
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x✝ : ↑(colimitCocone F).pt
x : Prequotient F
⊢ ↑m (Quot.mk Setoid.r x) = ↑(descMorphism F s) (Quot.mk Setoid.r x)
case h.refine_2
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
x_a x_b : Prequotient F
x_p : Setoid.r x_a x_b
⊢ (_ : ↑m (Quot.mk Setoid.r x_b) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x_b)) =
    (_ : (fun x => ↑m x = ↑((fun s => descMorphism F s) s) x) (Quot.mk Setoid.r x_b))
[PROOFSTEP]
induction' x with x_j x_x
[GOAL]
case h.refine_1.of
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
x_j : J
x_x : ↑(F.obj x_j)
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of x_j x_x)) = ↑(descMorphism F s) (Quot.mk Setoid.r (Prequotient.of x_j x_x))
[PROOFSTEP]
have w' := congr_fun (congr_arg (fun f : F.obj x_j ⟶ s.pt => (f : F.obj x_j → s.pt)) (w x_j)) x_x
[GOAL]
case h.refine_1.of
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
x_j : J
x_x : ↑(F.obj x_j)
w' : (fun f => ↑f) (NatTrans.app (colimitCocone F).ι x_j ≫ m) x_x = (fun f => ↑f) (NatTrans.app s.ι x_j) x_x
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of x_j x_x)) = ↑(descMorphism F s) (Quot.mk Setoid.r (Prequotient.of x_j x_x))
[PROOFSTEP]
simp only at w'
[GOAL]
case h.refine_1.of
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
x_j : J
x_x : ↑(F.obj x_j)
w' : ↑(NatTrans.app (colimitCocone F).ι x_j ≫ m) x_x = ↑(NatTrans.app s.ι x_j) x_x
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of x_j x_x)) = ↑(descMorphism F s) (Quot.mk Setoid.r (Prequotient.of x_j x_x))
[PROOFSTEP]
erw [w']
[GOAL]
case h.refine_1.of
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
x_j : J
x_x : ↑(F.obj x_j)
w' : ↑(NatTrans.app (colimitCocone F).ι x_j ≫ m) x_x = ↑(NatTrans.app s.ι x_j) x_x
⊢ ↑(NatTrans.app s.ι x_j) x_x = ↑(descMorphism F s) (Quot.mk Setoid.r (Prequotient.of x_j x_x))
[PROOFSTEP]
rfl
[GOAL]
case h.refine_1.zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
⊢ ↑m (Quot.mk Setoid.r zero) = ↑(descMorphism F s) (Quot.mk Setoid.r zero)
[PROOFSTEP]
rw [quot_zero, map_zero]
  -- porting note: was `simp` but `map_zero` won't fire
[GOAL]
case h.refine_1.zero
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
⊢ 0 = ↑(descMorphism F s) 0
[PROOFSTEP]
rfl
[GOAL]
case h.refine_1.neg
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
a✝ : Prequotient F
a_ih✝ : ↑m (Quot.mk Setoid.r a✝) = ↑(descMorphism F s) (Quot.mk Setoid.r a✝)
⊢ ↑m (Quot.mk Setoid.r (neg a✝)) = ↑(descMorphism F s) (Quot.mk Setoid.r (neg a✝))
[PROOFSTEP]
simpa
[GOAL]
case h.refine_1.add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
a✝¹ a✝ : Prequotient F
a_ih✝¹ : ↑m (Quot.mk Setoid.r a✝¹) = ↑(descMorphism F s) (Quot.mk Setoid.r a✝¹)
a_ih✝ : ↑m (Quot.mk Setoid.r a✝) = ↑(descMorphism F s) (Quot.mk Setoid.r a✝)
⊢ ↑m (Quot.mk Setoid.r (add a✝¹ a✝)) = ↑(descMorphism F s) (Quot.mk Setoid.r (add a✝¹ a✝))
[PROOFSTEP]
rw [quot_add, map_add, map_add]
  -- porting note: this was closed by `simp [*]`
[GOAL]
case h.refine_1.add
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
a✝¹ a✝ : Prequotient F
a_ih✝¹ : ↑m (Quot.mk Setoid.r a✝¹) = ↑(descMorphism F s) (Quot.mk Setoid.r a✝¹)
a_ih✝ : ↑m (Quot.mk Setoid.r a✝) = ↑(descMorphism F s) (Quot.mk Setoid.r a✝)
⊢ ↑m (ColimitType.mk a✝¹) + ↑m (ColimitType.mk a✝) =
    ↑(descMorphism F s) (ColimitType.mk a✝¹) + ↑(descMorphism F s) (ColimitType.mk a✝)
[PROOFSTEP]
congr 1
[GOAL]
case h.refine_1.smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
a✝¹ : R
a✝ : Prequotient F
a_ih✝ : ↑m (Quot.mk Setoid.r a✝) = ↑(descMorphism F s) (Quot.mk Setoid.r a✝)
⊢ ↑m (Quot.mk Setoid.r (smul a✝¹ a✝)) = ↑(descMorphism F s) (Quot.mk Setoid.r (smul a✝¹ a✝))
[PROOFSTEP]
rw [quot_smul, map_smul, map_smul]
  -- porting note: this was closed by `simp [*]`
[GOAL]
case h.refine_1.smul
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
a✝¹ : R
a✝ : Prequotient F
a_ih✝ : ↑m (Quot.mk Setoid.r a✝) = ↑(descMorphism F s) (Quot.mk Setoid.r a✝)
⊢ a✝¹ • ↑m (ColimitType.mk a✝) = a✝¹ • ↑(descMorphism F s) (ColimitType.mk a✝)
[PROOFSTEP]
congr 1
[GOAL]
case h.refine_2
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category.{v, w} J
F : J ⥤ ModuleCat R
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
x_a x_b : Prequotient F
x_p : Setoid.r x_a x_b
⊢ (_ : ↑m (Quot.mk Setoid.r x_b) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x_b)) =
    (_ : (fun x => ↑m x = ↑((fun s => descMorphism F s) s) x) (Quot.mk Setoid.r x_b))
[PROOFSTEP]
rfl
  -- porting note: this wasn't here


[GOAL]
k : Type u
inst✝² : Field k
A : Type w
inst✝¹ : Ring A
inst✝ : Algebra k A
⊢ ∀ (X Y Z : ModuleCat A) (r : k) (f : X ⟶ Y) (g : Y ⟶ Z), (r • f) ≫ g = r • f ≫ g
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case h
k : Type u
inst : Field k
A : Type w
inst_1 : Ring A
inst_2 : Algebra k A
X Y Z : ModuleCat A
r : k
f : X ⟶ Y
g : Y ⟶ Z
x✝ : ↑X
⊢ ↑g (↑(r • f) x✝) = ↑(r • f ≫ g) x✝
[PROOFSTEP]
rw [LinearMap.smul_apply, LinearMap.smul_apply, LinearMap.map_smul_of_tower]
[GOAL]
case h
k : Type u
inst : Field k
A : Type w
inst_1 : Ring A
inst_2 : Algebra k A
X Y Z : ModuleCat A
r : k
f : X ⟶ Y
g : Y ⟶ Z
x✝ : ↑X
⊢ r • ↑g (↑f x✝) = r • ↑(f ≫ g) x✝
[PROOFSTEP]
rfl


[GOAL]
J✝ : Type
inst✝⁴ : SmallCategory J✝
inst✝³ : FinCategory J✝
k : Type v
inst✝² : Field k
J : Type
inst✝¹ : Fintype J
Z : J → ModuleCat k
inst✝ : ∀ (j : J), FiniteDimensional k ↑(Z j)
⊢ FiniteDimensional k ↑(ModuleCat.of k ((j : J) → ↑(Z j)))
[PROOFSTEP]
unfold ModuleCat.of
[GOAL]
J✝ : Type
inst✝⁴ : SmallCategory J✝
inst✝³ : FinCategory J✝
k : Type v
inst✝² : Field k
J : Type
inst✝¹ : Fintype J
Z : J → ModuleCat k
inst✝ : ∀ (j : J), FiniteDimensional k ↑(Z j)
⊢ FiniteDimensional k ↑(ModuleCat.mk ((j : J) → ↑(Z j)))
[PROOFSTEP]
infer_instance
[GOAL]
J✝ : Type
inst✝⁴ : SmallCategory J✝
inst✝³ : FinCategory J✝
k : Type v
inst✝² : Field k
J : Type
inst✝¹ : Fintype J
Z : J → ModuleCat k
inst✝ : ∀ (j : J), FiniteDimensional k ↑(Z j)
this : FiniteDimensional k ↑(ModuleCat.of k ((j : J) → ↑(Z j)))
⊢ Mono (ModuleCat.piIsoPi fun j => Z j).hom
[PROOFSTEP]
infer_instance
[GOAL]
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
k : Type v
inst✝ : Field k
F : J ⥤ FGModuleCat k
⊢ ∀ (j : J), FiniteDimensional k ↑((F ⋙ forget₂ (FGModuleCat k) (ModuleCat k)).obj j)
[PROOFSTEP]
intro j
[GOAL]
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
k : Type v
inst✝ : Field k
F : J ⥤ FGModuleCat k
j : J
⊢ FiniteDimensional k ↑((F ⋙ forget₂ (FGModuleCat k) (ModuleCat k)).obj j)
[PROOFSTEP]
change FiniteDimensional k (F.obj j)
[GOAL]
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
k : Type v
inst✝ : Field k
F : J ⥤ FGModuleCat k
j : J
⊢ FiniteDimensional k ↑(F.obj j)
[PROOFSTEP]
infer_instance


[GOAL]
R : CommRingCat
⊢ IsIso (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away 1)))
[PROOFSTEP]
cases R
[GOAL]
case mk
α✝ : Type ?u.2107
str✝ : CommRing α✝
⊢ IsIso (CommRingCat.ofHom (algebraMap (↑(Bundled.mk α✝)) (Localization.Away 1)))
[PROOFSTEP]
exact localization_unit_isIso _
[GOAL]
R : CommRingCat
M : Submonoid ↑R
⊢ Epi (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))
[PROOFSTEP]
rcases R with ⟨α, str⟩
[GOAL]
case mk
α : Type ?u.6171
str : CommRing α
M : Submonoid ↑(Bundled.mk α)
⊢ Epi (CommRingCat.ofHom (algebraMap (↑(Bundled.mk α)) (Localization M)))
[PROOFSTEP]
exact IsLocalization.epi M _
[GOAL]
R S : CommRingCat
f : R ≅ S
a : ↑R
ha : IsUnit (↑f.hom a)
⊢ IsUnit a
[PROOFSTEP]
convert f.inv.isUnit_map ha
[GOAL]
case h.e'_3
R S : CommRingCat
f : R ≅ S
a : ↑R
ha : IsUnit (↑f.hom a)
⊢ a = ↑f.inv (↑f.hom a)
[PROOFSTEP]
exact (RingHom.congr_fun f.hom_inv_id _).symm


[GOAL]
⊢ ∀ {α β : Type ?u.90} (Iα : Mul α) (Iβ : Mul β), Function.Injective MulHom.toFun
[PROOFSTEP]
intros
[GOAL]
α✝ β✝ : Type ?u.90
Iα✝ : Mul α✝
Iβ✝ : Mul β✝
⊢ Function.Injective MulHom.toFun
[PROOFSTEP]
apply @FunLike.coe_injective
[GOAL]
⊢ ∀ {α : Type ?u.90} (I : Mul α), (MulHom.id α).toFun = id
[PROOFSTEP]
aesop_cat
[GOAL]
⊢ ∀ {α β γ : Type ?u.90} (Iα : Mul α) (Iβ : Mul β) (Iγ : Mul γ) (f : α →ₙ* β) (g : β →ₙ* γ),
    (MulHom.comp g f).toFun = g.toFun ∘ f.toFun
[PROOFSTEP]
aesop_cat
[GOAL]
X Y : Type u
inst✝¹ : Mul X
inst✝ : Mul Y
e : X ≃* Y
⊢ toMulHom e ≫ toMulHom (symm e) = 𝟙 (MagmaCat.of X)
[PROOFSTEP]
ext
[GOAL]
case w
X Y : Type u
inst✝¹ : Mul X
inst✝ : Mul Y
e : X ≃* Y
x✝ : (forget MagmaCat).obj (MagmaCat.of X)
⊢ ↑(toMulHom e ≫ toMulHom (symm e)) x✝ = ↑(𝟙 (MagmaCat.of X)) x✝
[PROOFSTEP]
simp_rw [comp_apply, toMulHom_eq_coe, MagmaCat.MulEquiv_coe_eq, symm_apply_apply, id_apply]
[GOAL]
X✝ Y✝ : Type u
X Y : MagmaCat
f : X ⟶ Y
x✝ : IsIso ((forget MagmaCat).map f)
⊢ IsIso f
[PROOFSTEP]
skip
[GOAL]
X✝ Y✝ : Type u
X Y : MagmaCat
f : X ⟶ Y
x✝ : IsIso ((forget MagmaCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget MagmaCat).map f)
[GOAL]
X✝ Y✝ : Type u
X Y : MagmaCat
f : X ⟶ Y
x✝ : IsIso ((forget MagmaCat).map f)
i : (forget MagmaCat).obj X ≅ (forget MagmaCat).obj Y := asIso ((forget MagmaCat).map f)
⊢ IsIso f
[PROOFSTEP]
let e : X ≃* Y := { f, i.toEquiv with }
[GOAL]
X✝ Y✝ : Type u
X Y : MagmaCat
f : X ⟶ Y
x✝ : IsIso ((forget MagmaCat).map f)
i : (forget MagmaCat).obj X ≅ (forget MagmaCat).obj Y := asIso ((forget MagmaCat).map f)
e : ↑X ≃* ↑Y :=
  let src := i.toEquiv;
  {
    toEquiv :=
      { toFun := f.toFun, invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
        right_inv := (_ : Function.RightInverse src.invFun src.toFun) },
    map_mul' := (_ : ∀ (x y : ↑X), MulHom.toFun f (x * y) = MulHom.toFun f x * MulHom.toFun f y) }
⊢ IsIso f
[PROOFSTEP]
exact ⟨(IsIso.of_iso e.toMagmaCatIso).1⟩
[GOAL]
X✝ Y✝ : Type u
X Y : SemigroupCat
f : X ⟶ Y
x✝ : IsIso ((forget SemigroupCat).map f)
⊢ IsIso f
[PROOFSTEP]
skip
[GOAL]
X✝ Y✝ : Type u
X Y : SemigroupCat
f : X ⟶ Y
x✝ : IsIso ((forget SemigroupCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget SemigroupCat).map f)
[GOAL]
X✝ Y✝ : Type u
X Y : SemigroupCat
f : X ⟶ Y
x✝ : IsIso ((forget SemigroupCat).map f)
i : (forget SemigroupCat).obj X ≅ (forget SemigroupCat).obj Y := asIso ((forget SemigroupCat).map f)
⊢ IsIso f
[PROOFSTEP]
let e : X ≃* Y := { f, i.toEquiv with }
[GOAL]
X✝ Y✝ : Type u
X Y : SemigroupCat
f : X ⟶ Y
x✝ : IsIso ((forget SemigroupCat).map f)
i : (forget SemigroupCat).obj X ≅ (forget SemigroupCat).obj Y := asIso ((forget SemigroupCat).map f)
e : ↑X ≃* ↑Y :=
  let src := i.toEquiv;
  {
    toEquiv :=
      { toFun := f.toFun, invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
        right_inv := (_ : Function.RightInverse src.invFun src.toFun) },
    map_mul' := (_ : ∀ (x y : ↑X), MulHom.toFun f (x * y) = MulHom.toFun f x * MulHom.toFun f y) }
⊢ IsIso f
[PROOFSTEP]
exact ⟨(IsIso.of_iso e.toSemigroupCatIso).1⟩


[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H✝ H : LieSubalgebra R L
inst✝ : IsCartanSubalgebra H
⊢ LieSubmodule.normalizer (toLieSubmodule H) = toLieSubmodule H
[PROOFSTEP]
rw [← LieSubmodule.coe_toSubmodule_eq_iff, coe_normalizer_eq_normalizer, IsCartanSubalgebra.self_normalizing,
  coe_toLieSubmodule]
[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H✝ H : LieSubalgebra R L
inst✝ : IsCartanSubalgebra H
k : ℕ
⊢ LieSubmodule.ucs k (toLieSubmodule H) = toLieSubmodule H
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H✝ H : LieSubalgebra R L
inst✝ : IsCartanSubalgebra H
⊢ LieSubmodule.ucs Nat.zero (toLieSubmodule H) = toLieSubmodule H
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H✝ H : LieSubalgebra R L
inst✝ : IsCartanSubalgebra H
k : ℕ
ih : LieSubmodule.ucs k (toLieSubmodule H) = toLieSubmodule H
⊢ LieSubmodule.ucs (Nat.succ k) (toLieSubmodule H) = toLieSubmodule H
[PROOFSTEP]
simp [ih]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ IsCartanSubalgebra H ↔ LieSubmodule.IsUcsLimit (toLieSubmodule H)
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ IsCartanSubalgebra H → LieSubmodule.IsUcsLimit (toLieSubmodule H)
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
⊢ LieSubmodule.IsUcsLimit (toLieSubmodule H)
[PROOFSTEP]
have h₁ : LieAlgebra.IsNilpotent R H := by infer_instance
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
⊢ LieAlgebra.IsNilpotent R { x // x ∈ H }
[PROOFSTEP]
infer_instance
[GOAL]
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
h₁ : LieAlgebra.IsNilpotent R { x // x ∈ H }
⊢ LieSubmodule.IsUcsLimit (toLieSubmodule H)
[PROOFSTEP]
obtain ⟨k, hk⟩ := H.toLieSubmodule.isNilpotent_iff_exists_self_le_ucs.mp h₁
[GOAL]
case mp.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
h₁ : LieAlgebra.IsNilpotent R { x // x ∈ H }
k : ℕ
hk : toLieSubmodule H ≤ LieSubmodule.ucs k ⊥
⊢ LieSubmodule.IsUcsLimit (toLieSubmodule H)
[PROOFSTEP]
replace hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥ :=
  le_antisymm hk (LieSubmodule.ucs_le_of_normalizer_eq_self H.normalizer_eq_self_of_isCartanSubalgebra k)
[GOAL]
case mp.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
h₁ : LieAlgebra.IsNilpotent R { x // x ∈ H }
k : ℕ
hk : toLieSubmodule H = LieSubmodule.ucs k ⊥
⊢ LieSubmodule.IsUcsLimit (toLieSubmodule H)
[PROOFSTEP]
refine' ⟨k, fun l hl => _⟩
[GOAL]
case mp.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
h₁ : LieAlgebra.IsNilpotent R { x // x ∈ H }
k : ℕ
hk : toLieSubmodule H = LieSubmodule.ucs k ⊥
l : ℕ
hl : k ≤ l
⊢ LieSubmodule.ucs l ⊥ = toLieSubmodule H
[PROOFSTEP]
rw [← Nat.sub_add_cancel hl, LieSubmodule.ucs_add, ← hk, LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra]
[GOAL]
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ LieSubmodule.IsUcsLimit (toLieSubmodule H) → IsCartanSubalgebra H
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case mpr.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ IsCartanSubalgebra H
[PROOFSTEP]
exact
  { nilpotent := by
      dsimp only [LieAlgebra.IsNilpotent]
      erw [H.toLieSubmodule.isNilpotent_iff_exists_lcs_eq_bot]
      use k
      rw [_root_.eq_bot_iff, LieSubmodule.lcs_le_iff, hk k (le_refl k)]
    self_normalizing := by
      have hk' := hk (k + 1) k.le_succ
      rw [LieSubmodule.ucs_succ, hk k (le_refl k)] at hk'
      rw [← LieSubalgebra.coe_to_submodule_eq_iff, ← LieSubalgebra.coe_normalizer_eq_normalizer, hk',
        LieSubalgebra.coe_toLieSubmodule] }
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ LieAlgebra.IsNilpotent R { x // x ∈ H }
[PROOFSTEP]
dsimp only [LieAlgebra.IsNilpotent]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ LieModule.IsNilpotent R { x // x ∈ H } { x // x ∈ H }
[PROOFSTEP]
erw [H.toLieSubmodule.isNilpotent_iff_exists_lcs_eq_bot]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ ∃ k, LieSubmodule.lcs k (toLieSubmodule H) = ⊥
[PROOFSTEP]
use k
[GOAL]
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ LieSubmodule.lcs k (toLieSubmodule H) = ⊥
[PROOFSTEP]
rw [_root_.eq_bot_iff, LieSubmodule.lcs_le_iff, hk k (le_refl k)]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ normalizer H = H
[PROOFSTEP]
have hk' := hk (k + 1) k.le_succ
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
hk' : LieSubmodule.ucs (k + 1) ⊥ = toLieSubmodule H
⊢ normalizer H = H
[PROOFSTEP]
rw [LieSubmodule.ucs_succ, hk k (le_refl k)] at hk'
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
hk' : LieSubmodule.normalizer (toLieSubmodule H) = toLieSubmodule H
⊢ normalizer H = H
[PROOFSTEP]
rw [← LieSubalgebra.coe_to_submodule_eq_iff, ← LieSubalgebra.coe_normalizer_eq_normalizer, hk',
  LieSubalgebra.coe_toLieSubmodule]
[GOAL]
R✝ : Type u
L✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : LieRing L✝
inst✝³ : LieAlgebra R✝ L✝
H : LieSubalgebra R✝ L✝
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ LieSubalgebra.normalizer (↑R L I) = ⊤
[PROOFSTEP]
ext x
[GOAL]
case h
R✝ : Type u
L✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : LieRing L✝
inst✝³ : LieAlgebra R✝ L✝
H : LieSubalgebra R✝ L✝
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
⊢ x ∈ LieSubalgebra.normalizer (↑R L I) ↔ x ∈ ⊤
[PROOFSTEP]
simpa only [LieSubalgebra.mem_normalizer_iff, LieSubalgebra.mem_top, iff_true_iff] using fun y hy => I.lie_mem hy
[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : IsNilpotent R L
⊢ LieSubalgebra.normalizer ⊤ = ⊤
[PROOFSTEP]
rw [← top_coe_lieSubalgebra, normalizer_eq_top, top_coe_lieSubalgebra]


[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
src✝ : AddGroupWithOne (ColimitType F) := ColimitType.AddGroupWithOne F
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.mk Setoid.r x * (Quot.mk Setoid.r y + Quot.mk Setoid.r z) =
    Quot.mk Setoid.r x * Quot.mk Setoid.r y + Quot.mk Setoid.r x * Quot.mk Setoid.r z
[PROOFSTEP]
simp only [(· + ·), (· * ·), Add.add]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
src✝ : AddGroupWithOne (ColimitType F) := ColimitType.AddGroupWithOne F
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
      (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r x)
      (Quotient.map₂ add (_ : ∀ (x x' : Prequotient F), x ≈ x' → ∀ (y y' : Prequotient F), y ≈ y' → add x y ≈ add x' y')
        (Quot.mk Setoid.r y) (Quot.mk Setoid.r z)) =
    Quotient.map₂ add (_ : ∀ (x x' : Prequotient F), x ≈ x' → ∀ (y y' : Prequotient F), y ≈ y' → add x y ≈ add x' y')
      (Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
        (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r x)
        (Quot.mk Setoid.r y))
      (Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
        (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r x)
        (Quot.mk Setoid.r z))
[PROOFSTEP]
exact Quot.sound (Relation.left_distrib _ _ _)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
src✝ : AddGroupWithOne (ColimitType F) := ColimitType.AddGroupWithOne F
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ (Quot.mk Setoid.r x + Quot.mk Setoid.r y) * Quot.mk Setoid.r z =
    Quot.mk Setoid.r x * Quot.mk Setoid.r z + Quot.mk Setoid.r y * Quot.mk Setoid.r z
[PROOFSTEP]
simp only [(· + ·), (· * ·), Add.add]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
src✝ : AddGroupWithOne (ColimitType F) := ColimitType.AddGroupWithOne F
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
      (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y))
      (Quotient.map₂ add (_ : ∀ (x x' : Prequotient F), x ≈ x' → ∀ (y y' : Prequotient F), y ≈ y' → add x y ≈ add x' y')
        (Quot.mk Setoid.r x) (Quot.mk Setoid.r y))
      (Quot.mk Setoid.r z) =
    Quotient.map₂ add (_ : ∀ (x x' : Prequotient F), x ≈ x' → ∀ (y y' : Prequotient F), y ≈ y' → add x y ≈ add x' y')
      (Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
        (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r x)
        (Quot.mk Setoid.r z))
      (Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
        (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r y)
        (Quot.mk Setoid.r z))
[PROOFSTEP]
exact Quot.sound (Relation.right_distrib _ _ _)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
src✝ : AddGroupWithOne (ColimitType F) := ColimitType.AddGroupWithOne F
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.mk Setoid.r x * Quot.mk Setoid.r y * Quot.mk Setoid.r z =
    Quot.mk Setoid.r x * (Quot.mk Setoid.r y * Quot.mk Setoid.r z)
[PROOFSTEP]
simp only [(· * ·)]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
src✝ : AddGroupWithOne (ColimitType F) := ColimitType.AddGroupWithOne F
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
      (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y))
      (Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
        (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r x)
        (Quot.mk Setoid.r y))
      (Quot.mk Setoid.r z) =
    Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
      (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r x)
      (Quot.map₂ mul (_ : ∀ (x y y' : Prequotient F), Relation F y y' → Relation F (mul x y) (mul x y'))
        (_ : ∀ (x x' y : Prequotient F), Relation F x x' → Relation F (mul x y) (mul x' y)) (Quot.mk Setoid.r y)
        (Quot.mk Setoid.r z))
[PROOFSTEP]
exact Quot.sound (Relation.mul_assoc _ _ _)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ coconeFun F j 1 = 1
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ Setoid.r (Prequotient.of j 1) one
[PROOFSTEP]
apply Relation.one
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ ∀ (x y : ↑(F.obj j)),
    OneHom.toFun
        { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) }
        (x * y) =
      OneHom.toFun
          { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) } x *
        OneHom.toFun
          { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) } y
[PROOFSTEP]
intros
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
x✝ y✝ : ↑(F.obj j)
⊢ OneHom.toFun
      { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) }
      (x✝ * y✝) =
    OneHom.toFun
        { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) } x✝ *
      OneHom.toFun
        { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) } y✝
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
x✝ y✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j (x✝ * y✝)) (mul (Prequotient.of j x✝) (Prequotient.of j y✝))
[PROOFSTEP]
apply Relation.mul
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) },
          map_mul' :=
            (_ :
              ∀ (x y : ↑(F.obj j)),
                Quot.mk Setoid.r (Prequotient.of j (x * y)) =
                  Quot.mk Setoid.r (mul (Prequotient.of j x) (Prequotient.of j y))) })
      0 =
    0
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ Setoid.r (Prequotient.of j 0) zero
[PROOFSTEP]
apply Relation.zero
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ ∀ (x y : ↑(F.obj j)),
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := coconeFun F j,
                map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(F.obj j)),
                  Quot.mk Setoid.r (Prequotient.of j (x * y)) =
                    Quot.mk Setoid.r (mul (Prequotient.of j x) (Prequotient.of j y))) })
        (x + y) =
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := coconeFun F j,
                  map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) },
              map_mul' :=
                (_ :
                  ∀ (x y : ↑(F.obj j)),
                    Quot.mk Setoid.r (Prequotient.of j (x * y)) =
                      Quot.mk Setoid.r (mul (Prequotient.of j x) (Prequotient.of j y))) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := coconeFun F j,
                  map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) },
              map_mul' :=
                (_ :
                  ∀ (x y : ↑(F.obj j)),
                    Quot.mk Setoid.r (Prequotient.of j (x * y)) =
                      Quot.mk Setoid.r (mul (Prequotient.of j x) (Prequotient.of j y))) })
          y
[PROOFSTEP]
intros
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
x✝ y✝ : ↑(F.obj j)
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := coconeFun F j, map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) },
          map_mul' :=
            (_ :
              ∀ (x y : ↑(F.obj j)),
                Quot.mk Setoid.r (Prequotient.of j (x * y)) =
                  Quot.mk Setoid.r (mul (Prequotient.of j x) (Prequotient.of j y))) })
      (x✝ + y✝) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := coconeFun F j,
                map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(F.obj j)),
                  Quot.mk Setoid.r (Prequotient.of j (x * y)) =
                    Quot.mk Setoid.r (mul (Prequotient.of j x) (Prequotient.of j y))) })
        x✝ +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := coconeFun F j,
                map_one' := (_ : Quot.mk Setoid.r (Prequotient.of j 1) = Quot.mk Setoid.r one) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(F.obj j)),
                  Quot.mk Setoid.r (Prequotient.of j (x * y)) =
                    Quot.mk Setoid.r (mul (Prequotient.of j x) (Prequotient.of j y))) })
        y✝
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
x✝ y✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j (x✝ + y✝)) (add (Prequotient.of j x✝) (Prequotient.of j y✝))
[PROOFSTEP]
apply Relation.add
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j
[PROOFSTEP]
ext
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x✝ : (forget CommRingCat).obj (F.obj j)
⊢ ↑(F.map f ≫ coconeMorphism F j') x✝ = ↑(coconeMorphism F j) x✝
[PROOFSTEP]
apply Quot.sound
[GOAL]
case w.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x✝ : (forget CommRingCat).obj (F.obj j)
⊢ Setoid.r (Prequotient.of j' (↑(F.map f) x✝)) (Prequotient.of j x✝)
[PROOFSTEP]
apply Relation.map
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ↑(coconeMorphism F j') (↑(F.map f) x) = ↑(coconeMorphism F j) x
[PROOFSTEP]
rw [← cocone_naturality F f]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ↑(coconeMorphism F j') (↑(F.map f) x) = ↑(F.map f ≫ coconeMorphism F j') x
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
⊢ ColimitType F → ↑s.pt
[PROOFSTEP]
fapply Quot.lift
[GOAL]
case f
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
⊢ Prequotient F → ↑s.pt
[PROOFSTEP]
exact descFunLift F s
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
⊢ ∀ (a b : Prequotient F), Setoid.r a b → descFunLift F s a = descFunLift F s b
[PROOFSTEP]
intro x y r
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : Prequotient F
r : Setoid.r x y
⊢ descFunLift F s x = descFunLift F s y
[PROOFSTEP]
induction r with
| refl => rfl
| symm x y _ ih => exact ih.symm
| trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
| map j j' f x => exact RingHom.congr_fun (s.ι.naturality f) x
| zero j => simp
| one j => simp
| neg j x => simp
| add j x y => simp
| mul j x y => simp
| neg_1 x x' r ih => dsimp; rw [ih]
| add_1 x x' y r ih => dsimp; rw [ih]
| add_2 x y y' r ih => dsimp; rw [ih]
| mul_1 x x' y r ih => dsimp; rw [ih]
| mul_2 x y y' r ih => dsimp; rw [ih]
| zero_add x => dsimp; rw [zero_add]
| add_zero x => dsimp; rw [add_zero]
| one_mul x => dsimp; rw [one_mul]
| mul_one x => dsimp; rw [mul_one]
| add_left_neg x => dsimp; rw [add_left_neg]
| add_comm x y => dsimp; rw [add_comm]
| mul_comm x y => dsimp; rw [mul_comm]
| add_assoc x y z => dsimp; rw [add_assoc]
| mul_assoc x y z => dsimp; rw [mul_assoc]
| left_distrib x y z => dsimp; rw [mul_add]
| right_distrib x y z => dsimp; rw [add_mul]
| zero_mul x => dsimp; rw [zero_mul]
| mul_zero x => dsimp; rw [mul_zero]
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : Prequotient F
r : Setoid.r x y
⊢ descFunLift F s x = descFunLift F s y
[PROOFSTEP]
induction r with
| refl => rfl
| symm x y _ ih => exact ih.symm
| trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
| map j j' f x => exact RingHom.congr_fun (s.ι.naturality f) x
| zero j => simp
| one j => simp
| neg j x => simp
| add j x y => simp
| mul j x y => simp
| neg_1 x x' r ih => dsimp; rw [ih]
| add_1 x x' y r ih => dsimp; rw [ih]
| add_2 x y y' r ih => dsimp; rw [ih]
| mul_1 x x' y r ih => dsimp; rw [ih]
| mul_2 x y y' r ih => dsimp; rw [ih]
| zero_add x => dsimp; rw [zero_add]
| add_zero x => dsimp; rw [add_zero]
| one_mul x => dsimp; rw [one_mul]
| mul_one x => dsimp; rw [mul_one]
| add_left_neg x => dsimp; rw [add_left_neg]
| add_comm x y => dsimp; rw [add_comm]
| mul_comm x y => dsimp; rw [mul_comm]
| add_assoc x y z => dsimp; rw [add_assoc]
| mul_assoc x y z => dsimp; rw [mul_assoc]
| left_distrib x y z => dsimp; rw [mul_add]
| right_distrib x y z => dsimp; rw [add_mul]
| zero_mul x => dsimp; rw [zero_mul]
| mul_zero x => dsimp; rw [mul_zero]
[GOAL]
case a.refl
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]

| refl => rfl
[GOAL]
case a.refl
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y x✝ : Prequotient F
⊢ descFunLift F s x✝ = descFunLift F s x✝
[PROOFSTEP]
rfl
[GOAL]
case a.symm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝¹ y✝ x y : Prequotient F
x✝ : Relation F x y
ih : descFunLift F s x = descFunLift F s y
⊢ descFunLift F s y = descFunLift F s x
[PROOFSTEP]

| symm x y _ ih => exact ih.symm
[GOAL]
case a.symm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝¹ y✝ x y : Prequotient F
x✝ : Relation F x y
ih : descFunLift F s x = descFunLift F s y
⊢ descFunLift F s y = descFunLift F s x
[PROOFSTEP]
exact ih.symm
[GOAL]
case a.trans
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝² y✝ x y z : Prequotient F
x✝¹ : Relation F x y
x✝ : 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
[PROOFSTEP]

| trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
[GOAL]
case a.trans
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝² y✝ x y z : Prequotient F
x✝¹ : Relation F x y
x✝ : 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
[PROOFSTEP]
exact ih1.trans ih2
[GOAL]
case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y : Prequotient F
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j' (↑(F.map f) x)) = descFunLift F s (Prequotient.of j x)
[PROOFSTEP]

| map j j' f x => exact RingHom.congr_fun (s.ι.naturality f) x
[GOAL]
case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y : Prequotient F
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j' (↑(F.map f) x)) = descFunLift F s (Prequotient.of j x)
[PROOFSTEP]
exact RingHom.congr_fun (s.ι.naturality f) x
[GOAL]
case a.zero
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
[PROOFSTEP]

| zero j => simp
[GOAL]
case a.zero
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
[PROOFSTEP]
simp
[GOAL]
case a.one
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
[PROOFSTEP]

| one j => simp
[GOAL]
case a.one
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
[PROOFSTEP]
simp
[GOAL]
case a.neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y : Prequotient F
j : J
x : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j (-x)) = descFunLift F s (neg (Prequotient.of j x))
[PROOFSTEP]

| neg j x => simp
[GOAL]
case a.neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y : Prequotient F
j : J
x : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j (-x)) = descFunLift F s (neg (Prequotient.of j x))
[PROOFSTEP]
simp
[GOAL]
case a.add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ : Prequotient F
j : J
x y : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j (x + y)) = descFunLift F s (add (Prequotient.of j x) (Prequotient.of j y))
[PROOFSTEP]

| add j x y => simp
[GOAL]
case a.add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ : Prequotient F
j : J
x y : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j (x + y)) = descFunLift F s (add (Prequotient.of j x) (Prequotient.of j y))
[PROOFSTEP]
simp
[GOAL]
case a.mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ : Prequotient F
j : J
x y : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j (x * y)) = descFunLift F s (mul (Prequotient.of j x) (Prequotient.of j y))
[PROOFSTEP]

| mul j x y => simp
[GOAL]
case a.mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ : Prequotient F
j : J
x y : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j (x * y)) = descFunLift F s (mul (Prequotient.of j x) (Prequotient.of j y))
[PROOFSTEP]
simp
[GOAL]
case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x x' : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (neg x) = descFunLift F s (neg x')
[PROOFSTEP]

| neg_1 x x' r ih => dsimp; rw [ih]
[GOAL]
case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x x' : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (neg x) = descFunLift F s (neg x')
[PROOFSTEP]
dsimp
[GOAL]
case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x x' : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ -descFunLift F s x = -descFunLift F s x'
[PROOFSTEP]
rw [ih]
[GOAL]
case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (add x y) = descFunLift F s (add x' y)
[PROOFSTEP]

| add_1 x x' y r ih => dsimp; rw [ih]
[GOAL]
case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (add x y) = descFunLift F s (add x' y)
[PROOFSTEP]
dsimp
[GOAL]
case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s x + descFunLift F s y = descFunLift F s x' + descFunLift F s y
[PROOFSTEP]
rw [ih]
[GOAL]
case a.add_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (add x y) = descFunLift F s (add x y')
[PROOFSTEP]

| add_2 x y y' r ih => dsimp; rw [ih]
[GOAL]
case a.add_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (add x y) = descFunLift F s (add x y')
[PROOFSTEP]
dsimp
[GOAL]
case a.add_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s x + descFunLift F s y = descFunLift F s x + descFunLift F s y'
[PROOFSTEP]
rw [ih]
[GOAL]
case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (mul x y) = descFunLift F s (mul x' y)
[PROOFSTEP]

| mul_1 x x' y r ih => dsimp; rw [ih]
[GOAL]
case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (mul x y) = descFunLift F s (mul x' y)
[PROOFSTEP]
dsimp
[GOAL]
case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s x * descFunLift F s y = descFunLift F s x' * descFunLift F s y
[PROOFSTEP]
rw [ih]
[GOAL]
case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (mul x y) = descFunLift F s (mul x y')
[PROOFSTEP]

| mul_2 x y y' r ih => dsimp; rw [ih]
[GOAL]
case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (mul x y) = descFunLift F s (mul x y')
[PROOFSTEP]
dsimp
[GOAL]
case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s x * descFunLift F s y = descFunLift F s x * descFunLift F s y'
[PROOFSTEP]
rw [ih]
[GOAL]
case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (add zero x) = descFunLift F s x
[PROOFSTEP]

| zero_add x => dsimp; rw [zero_add]
[GOAL]
case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (add zero x) = descFunLift F s x
[PROOFSTEP]
dsimp
[GOAL]
case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ 0 + descFunLift F s x = descFunLift F s x
[PROOFSTEP]
rw [zero_add]
[GOAL]
case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (add x zero) = descFunLift F s x
[PROOFSTEP]

| add_zero x => dsimp; rw [add_zero]
[GOAL]
case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (add x zero) = descFunLift F s x
[PROOFSTEP]
dsimp
[GOAL]
case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s x + 0 = descFunLift F s x
[PROOFSTEP]
rw [add_zero]
[GOAL]
case a.one_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul one x) = descFunLift F s x
[PROOFSTEP]

| one_mul x => dsimp; rw [one_mul]
[GOAL]
case a.one_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul one x) = descFunLift F s x
[PROOFSTEP]
dsimp
[GOAL]
case a.one_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ 1 * descFunLift F s x = descFunLift F s x
[PROOFSTEP]
rw [one_mul]
[GOAL]
case a.mul_one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul x one) = descFunLift F s x
[PROOFSTEP]

| mul_one x => dsimp; rw [mul_one]
[GOAL]
case a.mul_one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul x one) = descFunLift F s x
[PROOFSTEP]
dsimp
[GOAL]
case a.mul_one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s x * 1 = descFunLift F s x
[PROOFSTEP]
rw [mul_one]
[GOAL]
case a.add_left_neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (add (neg x) x) = descFunLift F s zero
[PROOFSTEP]

| add_left_neg x => dsimp; rw [add_left_neg]
[GOAL]
case a.add_left_neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (add (neg x) x) = descFunLift F s zero
[PROOFSTEP]
dsimp
[GOAL]
case a.add_left_neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ -descFunLift F s x + descFunLift F s x = 0
[PROOFSTEP]
rw [add_left_neg]
[GOAL]
case a.add_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y : Prequotient F
⊢ descFunLift F s (add x y) = descFunLift F s (add y x)
[PROOFSTEP]

| add_comm x y => dsimp; rw [add_comm]
[GOAL]
case a.add_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y : Prequotient F
⊢ descFunLift F s (add x y) = descFunLift F s (add y x)
[PROOFSTEP]
dsimp
[GOAL]
case a.add_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y : Prequotient F
⊢ descFunLift F s x + descFunLift F s y = descFunLift F s y + descFunLift F s x
[PROOFSTEP]
rw [add_comm]
[GOAL]
case a.mul_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y : Prequotient F
⊢ descFunLift F s (mul x y) = descFunLift F s (mul y x)
[PROOFSTEP]

| mul_comm x y => dsimp; rw [mul_comm]
[GOAL]
case a.mul_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y : Prequotient F
⊢ descFunLift F s (mul x y) = descFunLift F s (mul y x)
[PROOFSTEP]
dsimp
[GOAL]
case a.mul_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y : Prequotient F
⊢ descFunLift F s x * descFunLift F s y = descFunLift F s y * descFunLift F s x
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case a.add_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (add (add x y) z) = descFunLift F s (add x (add y z))
[PROOFSTEP]

| add_assoc x y z => dsimp; rw [add_assoc]
[GOAL]
case a.add_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (add (add x y) z) = descFunLift F s (add x (add y z))
[PROOFSTEP]
dsimp
[GOAL]
case a.add_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x + descFunLift F s y + descFunLift F s z =
    descFunLift F s x + (descFunLift F s y + descFunLift F s z)
[PROOFSTEP]
rw [add_assoc]
[GOAL]
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (mul (mul x y) z) = descFunLift F s (mul x (mul y z))
[PROOFSTEP]

| mul_assoc x y z => dsimp; rw [mul_assoc]
[GOAL]
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (mul (mul x y) z) = descFunLift F s (mul x (mul y z))
[PROOFSTEP]
dsimp
[GOAL]
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x * descFunLift F s y * descFunLift F s z =
    descFunLift F s x * (descFunLift F s y * descFunLift F s z)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case a.left_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (mul x (add y z)) = descFunLift F s (add (mul x y) (mul x z))
[PROOFSTEP]

| left_distrib x y z => dsimp; rw [mul_add]
[GOAL]
case a.left_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (mul x (add y z)) = descFunLift F s (add (mul x y) (mul x z))
[PROOFSTEP]
dsimp
[GOAL]
case a.left_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ 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
[PROOFSTEP]
rw [mul_add]
[GOAL]
case a.right_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (mul (add x y) z) = descFunLift F s (add (mul x z) (mul y z))
[PROOFSTEP]

| right_distrib x y z => dsimp; rw [add_mul]
[GOAL]
case a.right_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (mul (add x y) z) = descFunLift F s (add (mul x z) (mul y z))
[PROOFSTEP]
dsimp
[GOAL]
case a.right_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ (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
[PROOFSTEP]
rw [add_mul]
[GOAL]
case a.zero_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul zero x) = descFunLift F s zero
[PROOFSTEP]

| zero_mul x => dsimp; rw [zero_mul]
[GOAL]
case a.zero_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul zero x) = descFunLift F s zero
[PROOFSTEP]
dsimp
[GOAL]
case a.zero_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ 0 * descFunLift F s x = 0
[PROOFSTEP]
rw [zero_mul]
[GOAL]
case a.mul_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul x zero) = descFunLift F s zero
[PROOFSTEP]

| mul_zero x => dsimp; rw [mul_zero]
[GOAL]
case a.mul_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (mul x zero) = descFunLift F s zero
[PROOFSTEP]
dsimp
[GOAL]
case a.mul_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s x * 0 = 0
[PROOFSTEP]
rw [mul_zero]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ↑(colimit F)
⊢ OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (x * y) =
    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } x *
      OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y
[PROOFSTEP]
exact Quot.induction_on₂ x y fun a b => rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ↑(colimit F)
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) },
          map_mul' :=
            (_ :
              ∀ (x y : ↑(colimit F)),
                OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (x * y) =
                  OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } x *
                    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y) })
      (x + y) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(colimit F)),
                  OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (x * y) =
                    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } x *
                      OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y) })
        x +
      OneHom.toFun
        (↑{ toOneHom := { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(colimit F)),
                  OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (x * y) =
                    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } x *
                      OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y) })
        y
[PROOFSTEP]
refine Quot.induction_on₂ x y fun a b => ?_
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ↑(colimit F)
a b : Prequotient F
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) },
          map_mul' :=
            (_ :
              ∀ (x y : ↑(colimit F)),
                OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (x * y) =
                  OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } x *
                    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y) })
      (Quot.mk Setoid.r a + Quot.mk Setoid.r b) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(colimit F)),
                  OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (x * y) =
                    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } x *
                      OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y) })
        (Quot.mk Setoid.r a) +
      OneHom.toFun
        (↑{ toOneHom := { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(colimit F)),
                  OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } (x * y) =
                    OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } x *
                      OneHom.toFun { toFun := descFun F s, map_one' := (_ : descFun F s 1 = descFun F s 1) } y) })
        (Quot.mk Setoid.r b)
[PROOFSTEP]
dsimp [descFun, (· + ·)]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ↑(colimit F)
a b : Prequotient F
⊢ Quot.lift (descFunLift F s) (_ : ∀ (x y : Prequotient F), Setoid.r x y → descFunLift F s x = descFunLift F s y)
      (Add.add (Quot.mk Setoid.r a) (Quot.mk Setoid.r b)) =
    Add.add (descFunLift F s a) (descFunLift F s b)
[PROOFSTEP]
rw [← quot_add]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ↑(colimit F)
a b : Prequotient F
⊢ Quot.lift (descFunLift F s) (_ : ∀ (x y : Prequotient F), Setoid.r x y → descFunLift F s x = descFunLift F s y)
      (Quot.mk Setoid.r (add a b)) =
    Add.add (descFunLift F s a) (descFunLift F s b)
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : ↑(colimitCocone F).pt
⊢ ↑m x = ↑((fun s => descMorphism F s) s) x
[PROOFSTEP]
change (colimitCocone F).pt →+* s.pt at m
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ ↑m x = ↑((fun s => descMorphism F s) s) x
[PROOFSTEP]
refine Quot.inductionOn x ?_
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ ∀ (a : Prequotient F), ↑m (Quot.mk Setoid.r a) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r a)
[PROOFSTEP]
intro x
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : Prequotient F
⊢ ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
[PROOFSTEP]
induction x with
| zero => erw [quot_zero, map_zero (f := m), (descMorphism F s).map_zero]
| one => erw [quot_one, map_one (f := m), (descMorphism F s).map_one]
| neg x ih => erw [quot_neg, map_neg (f := m), (descMorphism F s).map_neg, ih]
| of j x => exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x
| add x y ih_x ih_y => erw [quot_add, map_add (f := m), (descMorphism F s).map_add, ih_x, ih_y]
| mul x y ih_x ih_y => erw [quot_mul, map_mul (f := m), (descMorphism F s).map_mul, ih_x, ih_y]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : Prequotient F
⊢ ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
[PROOFSTEP]
induction x with
| zero => erw [quot_zero, map_zero (f := m), (descMorphism F s).map_zero]
| one => erw [quot_one, map_one (f := m), (descMorphism F s).map_one]
| neg x ih => erw [quot_neg, map_neg (f := m), (descMorphism F s).map_neg, ih]
| of j x => exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x
| add x y ih_x ih_y => erw [quot_add, map_add (f := m), (descMorphism F s).map_add, ih_x, ih_y]
| mul x y ih_x ih_y => erw [quot_mul, map_mul (f := m), (descMorphism F s).map_mul, ih_x, ih_y]
[GOAL]
case zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ ↑m (Quot.mk Setoid.r zero) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r zero)
[PROOFSTEP]

| zero => erw [quot_zero, map_zero (f := m), (descMorphism F s).map_zero]
[GOAL]
case zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ ↑m (Quot.mk Setoid.r zero) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r zero)
[PROOFSTEP]
erw [quot_zero, map_zero (f := m), (descMorphism F s).map_zero]
[GOAL]
case one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ ↑m (Quot.mk Setoid.r one) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r one)
[PROOFSTEP]

| one => erw [quot_one, map_one (f := m), (descMorphism F s).map_one]
[GOAL]
case one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ ↑m (Quot.mk Setoid.r one) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r one)
[PROOFSTEP]
erw [quot_one, map_one (f := m), (descMorphism F s).map_one]
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : Prequotient F
ih : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
⊢ ↑m (Quot.mk Setoid.r (neg x)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (neg x))
[PROOFSTEP]

| neg x ih => erw [quot_neg, map_neg (f := m), (descMorphism F s).map_neg, ih]
[GOAL]
case neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : Prequotient F
ih : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
⊢ ↑m (Quot.mk Setoid.r (neg x)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (neg x))
[PROOFSTEP]
erw [quot_neg, map_neg (f := m), (descMorphism F s).map_neg, ih]
[GOAL]
case of
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
j : J
x : ↑(F.obj j)
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of j x)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (Prequotient.of j x))
[PROOFSTEP]

| of j x => exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x
[GOAL]
case of
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
j : J
x : ↑(F.obj j)
⊢ ↑m (Quot.mk Setoid.r (Prequotient.of j x)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (Prequotient.of j x))
[PROOFSTEP]
exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x
[GOAL]
case add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x y : Prequotient F
ih_x : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
ih_y : ↑m (Quot.mk Setoid.r y) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r y)
⊢ ↑m (Quot.mk Setoid.r (add x y)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (add x y))
[PROOFSTEP]

| add x y ih_x ih_y => erw [quot_add, map_add (f := m), (descMorphism F s).map_add, ih_x, ih_y]
[GOAL]
case add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x y : Prequotient F
ih_x : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
ih_y : ↑m (Quot.mk Setoid.r y) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r y)
⊢ ↑m (Quot.mk Setoid.r (add x y)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (add x y))
[PROOFSTEP]
erw [quot_add, map_add (f := m), (descMorphism F s).map_add, ih_x, ih_y]
[GOAL]
case mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x y : Prequotient F
ih_x : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
ih_y : ↑m (Quot.mk Setoid.r y) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r y)
⊢ ↑m (Quot.mk Setoid.r (mul x y)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (mul x y))
[PROOFSTEP]

| mul x y ih_x ih_y => erw [quot_mul, map_mul (f := m), (descMorphism F s).map_mul, ih_x, ih_y]
[GOAL]
case mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ : ↑(colimitCocone F).pt
m : ↑(colimitCocone F).pt →+* ↑s.pt
w : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x y : Prequotient F
ih_x : ↑m (Quot.mk Setoid.r x) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r x)
ih_y : ↑m (Quot.mk Setoid.r y) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r y)
⊢ ↑m (Quot.mk Setoid.r (mul x y)) = ↑((fun s => descMorphism F s) s) (Quot.mk Setoid.r (mul x y))
[PROOFSTEP]
erw [quot_mul, map_mul (f := m), (descMorphism F s).map_mul, ih_x, ih_y]


[GOAL]
⊢ ∀ {X' X : SemigroupCat} {Y : MonCat} (f : X' ⟶ X) (g : X ⟶ (forget₂ MonCat SemigroupCat).obj Y),
    ↑((fun S M => WithOne.lift.symm) X' Y).symm (f ≫ g) = adjoinOne.map f ≫ ↑((fun S M => WithOne.lift.symm) X Y).symm g
[PROOFSTEP]
intro S T M f g
[GOAL]
S T : SemigroupCat
M : MonCat
f : S ⟶ T
g : T ⟶ (forget₂ MonCat SemigroupCat).obj M
⊢ ↑((fun S M => WithOne.lift.symm) S M).symm (f ≫ g) = adjoinOne.map f ≫ ↑((fun S M => WithOne.lift.symm) T M).symm g
[PROOFSTEP]
ext x
[GOAL]
case w
S T : SemigroupCat
M : MonCat
f : S ⟶ T
g : T ⟶ (forget₂ MonCat SemigroupCat).obj M
x : ↑(adjoinOne.obj S)
⊢ ↑(↑((fun S M => WithOne.lift.symm) S M).symm (f ≫ g)) x =
    ↑(adjoinOne.map f ≫ ↑((fun S M => WithOne.lift.symm) T M).symm g) x
[PROOFSTEP]
simp only [Equiv.symm_symm, adjoinOne_map, coe_comp]
[GOAL]
case w
S T : SemigroupCat
M : MonCat
f : S ⟶ T
g : T ⟶ (forget₂ MonCat SemigroupCat).obj M
x : ↑(adjoinOne.obj S)
⊢ ↑(↑WithOne.lift (f ≫ g)) x = ↑(WithOne.map f ≫ ↑WithOne.lift g) x
[PROOFSTEP]
simp_rw [WithOne.map]
[GOAL]
case w
S T : SemigroupCat
M : MonCat
f : S ⟶ T
g : T ⟶ (forget₂ MonCat SemigroupCat).obj M
x : ↑(adjoinOne.obj S)
⊢ ↑(↑WithOne.lift (f ≫ g)) x = ↑(↑WithOne.lift (MulHom.comp WithOne.coeMulHom f) ≫ ↑WithOne.lift g) x
[PROOFSTEP]
cases x
[GOAL]
case w.none
S T : SemigroupCat
M : MonCat
f : S ⟶ T
g : T ⟶ (forget₂ MonCat SemigroupCat).obj M
⊢ ↑(↑WithOne.lift (f ≫ g)) none = ↑(↑WithOne.lift (MulHom.comp WithOne.coeMulHom f) ≫ ↑WithOne.lift g) none
[PROOFSTEP]
rfl
[GOAL]
case w.some
S T : SemigroupCat
M : MonCat
f : S ⟶ T
g : T ⟶ (forget₂ MonCat SemigroupCat).obj M
val✝ : ↑S
⊢ ↑(↑WithOne.lift (f ≫ g)) (some val✝) =
    ↑(↑WithOne.lift (MulHom.comp WithOne.coeMulHom f) ≫ ↑WithOne.lift g) (some val✝)
[PROOFSTEP]
simp
[GOAL]
case w.some
S T : SemigroupCat
M : MonCat
f : S ⟶ T
g : T ⟶ (forget₂ MonCat SemigroupCat).obj M
val✝ : ↑S
⊢ ↑(↑WithOne.lift (f ≫ g)) (some val✝) =
    ↑(↑WithOne.lift g) (↑(↑WithOne.lift (MulHom.comp WithOne.coeMulHom f)) (some val✝))
[PROOFSTEP]
rfl