mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (((const J).obj
              { left := c₁.pt, right := c₂.pt, hom := (isLimitOfPreserves R t₂).lift (limitAuxiliaryCone F c₁) }).map
          t ≫
        { left := c₁.π.app j₂, right := c₂.π.app j₂, w := ⋯ }).right =
    ({ left := c₁.π.app j₁, right := c₂.π.app j₁, w := ⋯ } ≫ F.map t).right

Tactic:
·

Goal state after:
case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (((const J).obj
              { left := c₁.pt, right := c₂.pt, hom := (isLimitOfPreserves R t₂).lift (limitAuxiliaryCone F c₁) }).map
          t ≫
        { left := c₁.π.app j₂, right := c₂.π.app j₂, w := ⋯ }).right =
    ({ left := c₁.π.app j₁, right := c₂.π.app j₁, w := ⋯ } ≫ F.map t).right
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₁
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cone F
inst✝ : PreservesLimit (F ⋙ snd L R) R
h₁ : IsLimit ((fst L R).mapCone c)
h₂ : IsLimit ((snd L R).mapCone c)
s : Cone F
j : J
⊢ ({ left := h₁.lift ((fst L R).mapCone s), right := h₂.lift ((snd L R).mapCone s), w := ⋯ } ≫ c.π.app j).left =
    (s.π.app j).left

pp: case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cone F
inst✝ : PreservesLimit (F ⋙ snd L R) R
h₁ : IsLimit ((fst L R).mapCone c)
h₂ : IsLimit ((snd L R).mapCone c)
s : Cone F
j : J
⊢ ({ left := h₁.lift ((fst L R).mapCone s), right := h₂.lift ((snd L R).mapCone s), w := ⋯ } ≫ c.π.app j).right =
    (s.π.app j).right

Tactic:
·

Goal state after:
case h₁
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cone F
inst✝ : PreservesLimit (F ⋙ snd L R) R
h₁ : IsLimit ((fst L R).mapCone c)
h₂ : IsLimit ((snd L R).mapCone c)
s : Cone F
j : J
⊢ ({ left := h₁.lift ((fst L R).mapCone s), right := h₂.lift ((snd L R).mapCone s), w := ⋯ } ≫ c.π.app j).left =
    (s.π.app j).left
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cone F
inst✝ : PreservesLimit (F ⋙ snd L R) R
h₁ : IsLimit ((fst L R).mapCone c)
h₂ : IsLimit ((snd L R).mapCone c)
s : Cone F
j : J
⊢ ({ left := h₁.lift ((fst L R).mapCone s), right := h₂.lift ((snd L R).mapCone s), w := ⋯ } ≫ c.π.app j).right =
    (s.π.app j).right

Tactic:
·

Goal state after:
case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cone F
inst✝ : PreservesLimit (F ⋙ snd L R) R
h₁ : IsLimit ((fst L R).mapCone c)
h₂ : IsLimit ((snd L R).mapCone c)
s : Cone F
j : J
⊢ ({ left := h₁.lift ((fst L R).mapCone s), right := h₂.lift ((snd L R).mapCone s), w := ⋯ } ≫ c.π.app j).right =
    (s.π.app j).right
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₁
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cone F
inst✝ : PreservesLimit (F ⋙ snd L R) R
h₁ : IsLimit ((fst L R).mapCone c)
h₂ : IsLimit ((snd L R).mapCone c)
s : Cone F
x✝ : s.pt ⟶ c.pt
hm : ∀ (j : J), x✝ ≫ c.π.app j = s.π.app j
⊢ x✝.left = { left := h₁.lift ((fst L R).mapCone s), right := h₂.lift ((snd L R).mapCone s), w := ⋯ }.left

pp: case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cone F
inst✝ : PreservesLimit (F ⋙ snd L R) R
h₁ : IsLimit ((fst L R).mapCone c)
h₂ : IsLimit ((snd L R).mapCone c)
s : Cone F
x✝ : s.pt ⟶ c.pt
hm : ∀ (j : J), x✝ ≫ c.π.app j = s.π.app j
⊢ x✝.right = { left := h₁.lift ((fst L R).mapCone s), right := h₂.lift ((snd L R).mapCone s), w := ⋯ }.right

Tactic:
·

Goal state after:
case h₁
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cone F
inst✝ : PreservesLimit (F ⋙ snd L R) R
h₁ : IsLimit ((fst L R).mapCone c)
h₂ : IsLimit ((snd L R).mapCone c)
s : Cone F
x✝ : s.pt ⟶ c.pt
hm : ∀ (j : J), x✝ ≫ c.π.app j = s.π.app j
⊢ x✝.left = { left := h₁.lift ((fst L R).mapCone s), right := h₂.lift ((snd L R).mapCone s), w := ⋯ }.left
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cone F
inst✝ : PreservesLimit (F ⋙ snd L R) R
h₁ : IsLimit ((fst L R).mapCone c)
h₂ : IsLimit ((snd L R).mapCone c)
s : Cone F
x✝ : s.pt ⟶ c.pt
hm : ∀ (j : J), x✝ ≫ c.π.app j = s.π.app j
⊢ x✝.right = { left := h₁.lift ((fst L R).mapCone s), right := h₂.lift ((snd L R).mapCone s), w := ⋯ }.right

Tactic:
·

Goal state after:
case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cone F
inst✝ : PreservesLimit (F ⋙ snd L R) R
h₁ : IsLimit ((fst L R).mapCone c)
h₂ : IsLimit ((snd L R).mapCone c)
s : Cone F
x✝ : s.pt ⟶ c.pt
hm : ∀ (j : J), x✝ ≫ c.π.app j = s.π.app j
⊢ x✝.right = { left := h₁.lift ((fst L R).mapCone s), right := h₂.lift ((snd L R).mapCone s), w := ⋯ }.right
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case left
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ { hom' := m }.hom.toIntAlgHom.comp Algebra.TensorProduct.includeLeft =
    (Algebra.TensorProduct.liftEquiv.symm
          (Hom.hom
              (ofHom
                (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                    ⋯).toRingHom)).toIntAlgHom).1.1

pp: case right
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ (AlgHom.restrictScalars ℤ { hom' := m }.hom.toIntAlgHom).comp Algebra.TensorProduct.includeRight =
    (Algebra.TensorProduct.liftEquiv.symm
          (Hom.hom
              (ofHom
                (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                    ⋯).toRingHom)).toIntAlgHom).1.2

Tactic:
·

Goal state after:
case left
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ { hom' := m }.hom.toIntAlgHom.comp Algebra.TensorProduct.includeLeft =
    (Algebra.TensorProduct.liftEquiv.symm
          (Hom.hom
              (ofHom
                (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                    ⋯).toRingHom)).toIntAlgHom).1.1
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₁
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := ⋯ }).left =
    ({ left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := ⋯ } ≫
        ((const J).obj
              { left := c₁.pt, right := c₂.pt,
                hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) }).map
          t).left

pp: case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := ⋯ }).right =
    ({ left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := ⋯ } ≫
        ((const J).obj
              { left := c₁.pt, right := c₂.pt,
                hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) }).map
          t).right

Tactic:
·

Goal state after:
case h₁
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := ⋯ }).left =
    ({ left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := ⋯ } ≫
        ((const J).obj
              { left := c₁.pt, right := c₂.pt,
                hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) }).map
          t).left
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case right
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ (AlgHom.restrictScalars ℤ { hom' := m }.hom.toIntAlgHom).comp Algebra.TensorProduct.includeRight =
    (Algebra.TensorProduct.liftEquiv.symm
          (Hom.hom
              (ofHom
                (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                    ⋯).toRingHom)).toIntAlgHom).1.2

Tactic:
·

Goal state after:
case right
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ (AlgHom.restrictScalars ℤ { hom' := m }.hom.toIntAlgHom).comp Algebra.TensorProduct.includeRight =
    (Algebra.TensorProduct.liftEquiv.symm
          (Hom.hom
              (ofHom
                (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                    ⋯).toRingHom)).toIntAlgHom).1.2
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := ⋯ }).right =
    ({ left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := ⋯ } ≫
        ((const J).obj
              { left := c₁.pt, right := c₂.pt,
                hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) }).map
          t).right

Tactic:
·

Goal state after:
case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := ⋯ }).right =
    ({ left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := ⋯ } ≫
        ((const J).obj
              { left := c₁.pt, right := c₂.pt,
                hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) }).map
          t).right
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case refine_1
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
⊢ f ≫ ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } = 𝟙 (of PUnit.{u + 1})

pp: case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
⊢ ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f = 𝟙 X

Tactic:
·

Goal state after:
case refine_1
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
⊢ f ≫ ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } = 𝟙 (of PUnit.{u + 1})
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
⊢ ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f = 𝟙 X

Tactic:
·

Goal state after:
case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
⊢ ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f = 𝟙 X
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₁
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫ { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }).left =
    (s.ι.app j).left

pp: case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫ { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }).right =
    (s.ι.app j).right

Tactic:
·

Goal state after:
case h₁
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫ { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }).left =
    (s.ι.app j).left
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫ { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }).right =
    (s.ι.app j).right

Tactic:
·

Goal state after:
case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫ { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }).right =
    (s.ι.app j).right
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₁
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
x✝ : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ x✝ = s.ι.app j
⊢ x✝.left = { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }.left

pp: case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
x✝ : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ x✝ = s.ι.app j
⊢ x✝.right = { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }.right

Tactic:
·

Goal state after:
case h₁
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
x✝ : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ x✝ = s.ι.app j
⊢ x✝.left = { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }.left
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
x✝ : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ x✝ = s.ι.app j
⊢ x✝.right = { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }.right

Tactic:
·

Goal state after:
case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
x✝ : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ x✝ = s.ι.app j
⊢ x✝.right = { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }.right
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
x : ↑s.pt
eq1 : (ConcreteCategory.hom (m ≫ (A.prodFan B).fst)) x = (ConcreteCategory.hom (BinaryFan.fst s)) x
⊢ (ConcreteCategory.hom m) x = ((ConcreteCategory.hom (BinaryFan.fst s)) x, (ConcreteCategory.hom (BinaryFan.snd s)) x)

Tactic:
have eq2 : (m ≫ (A.prodFan B).snd) x = (BinaryFan.snd s) x :=
      ConcreteCategory.congr_hom (h ⟨WalkingPair.right⟩) x

Goal state after:
A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
x : ↑s.pt
eq1 : (ConcreteCategory.hom (m ≫ (A.prodFan B).fst)) x = (ConcreteCategory.hom (BinaryFan.fst s)) x
eq2 : (ConcreteCategory.hom (m ≫ (A.prodFan B).snd)) x = (ConcreteCategory.hom (BinaryFan.snd s)) x
⊢ (ConcreteCategory.hom m) x = ((ConcreteCategory.hom (BinaryFan.fst s)) x, (ConcreteCategory.hom (BinaryFan.snd s)) x)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case property.left
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
⊢ ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯) ≫ (equalizerFork f g).ι = s.ι

pp: case property.right
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
⊢ ∀ {m : s.pt ⟶ (equalizerFork f g).pt},
    m ≫ (equalizerFork f g).ι = s.ι → m = ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯)

Tactic:
·

Goal state after:
case property.left
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
⊢ ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯) ≫ (equalizerFork f g).ι = s.ι
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case property.right
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
⊢ ∀ {m : s.pt ⟶ (equalizerFork f g).pt},
    m ≫ (equalizerFork f g).ι = s.ι → m = ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯)

Tactic:
·

Goal state after:
case property.right
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
⊢ ∀ {m : s.pt ⟶ (equalizerFork f g).pt},
    m ≫ (equalizerFork f g).ι = s.ι → m = ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case zero
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPair ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)

pp: case one
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPair ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app one)) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)

Tactic:
·

Goal state after:
case zero
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPair ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case one
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPair ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app one)) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)

Tactic:
·

Goal state after:
case one
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPair ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app one)) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)