mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.Under.Limits

Goal state before:
pp: case zero
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      0 =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      0

pp: case tmul
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ : ↑S
y✝ : (i : ι) → ↑(P i).right
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ ⊗ₜ[↑R] y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      (x✝ ⊗ₜ[↑R] y✝)

pp: case add
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ y✝ : ↑S ⊗[↑R] ((i : ι) → ↑(P i).right)
a✝¹ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      x✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      x✝
a✝ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      y✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      y✝
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ + y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      (x✝ + y✝)

Tactic:
·

Goal state after:
case zero
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      0 =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      0
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
⊢ ∀ (i j : J) (xi : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i))
    (xj : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj j)),
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) xi =
        (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map f)) xi =
          (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map g)) xj

Tactic:
·

Goal state after:
case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
⊢ ∀ (i j : J) (xi : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i))
    (xj : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj j)),
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) xi =
        (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map f)) xi =
          (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map g)) xj
Module: Mathlib.Algebra.Category.Ring.Under.Limits

Goal state before:
pp: case tmul
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ : ↑S
y✝ : (i : ι) → ↑(P i).right
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ ⊗ₜ[↑R] y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      (x✝ ⊗ₜ[↑R] y✝)

pp: case add
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ y✝ : ↑S ⊗[↑R] ((i : ι) → ↑(P i).right)
a✝¹ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      x✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      x✝
a✝ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      y✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      y✝
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ + y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      (x✝ + y✝)

Tactic:
·

Goal state after:
case tmul
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ : ↑S
y✝ : (i : ι) → ↑(P i).right
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ ⊗ₜ[↑R] y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      (x✝ ⊗ₜ[↑R] y✝)
Module: Mathlib.Algebra.Category.Ring.Under.Limits

Goal state before:
pp: case add
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ y✝ : ↑S ⊗[↑R] ((i : ι) → ↑(P i).right)
a✝¹ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      x✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      x✝
a✝ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      y✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      y✝
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ + y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      (x✝ + y✝)

Tactic:
·

Goal state after:
case add
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ y✝ : ↑S ⊗[↑R] ((i : ι) → ↑(P i).right)
a✝¹ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      x✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      x✝
a✝ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      y✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      y✝
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ + y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      (x✝ + y✝)
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: case inst
T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
X : T
inst✝⁵ : P.IsStableUnderComposition
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.HasOfPostcompProperty P
inst✝² : HasPullbacks A
inst✝¹ : HasPullbacks T
inst✝ : PreservesLimitsOfShape WalkingCospan L
⊢ HasLimitsOfShape WalkingCospan (Comma L (Functor.fromPUnit X))

pp: case inst
T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
X : T
inst✝⁵ : P.IsStableUnderComposition
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.HasOfPostcompProperty P
inst✝² : HasPullbacks A
inst✝¹ : HasPullbacks T
inst✝ : PreservesLimitsOfShape WalkingCospan L
⊢ (commaObj L (Functor.fromPUnit X) P).IsClosedUnderLimitsOfShape WalkingCospan

Tactic:
·

Goal state after:
case inst
T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
X : T
inst✝⁵ : P.IsStableUnderComposition
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.HasOfPostcompProperty P
inst✝² : HasPullbacks A
inst✝¹ : HasPullbacks T
inst✝ : PreservesLimitsOfShape WalkingCospan L
⊢ HasLimitsOfShape WalkingCospan (Comma L (Functor.fromPUnit X))
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: case inst
T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
X : T
inst✝⁵ : P.IsStableUnderComposition
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.HasOfPostcompProperty P
inst✝² : HasPullbacks A
inst✝¹ : HasPullbacks T
inst✝ : PreservesLimitsOfShape WalkingCospan L
⊢ (commaObj L (Functor.fromPUnit X) P).IsClosedUnderLimitsOfShape WalkingCospan

Tactic:
·

Goal state after:
case inst
T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
X : T
inst✝⁵ : P.IsStableUnderComposition
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.HasOfPostcompProperty P
inst✝² : HasPullbacks A
inst✝¹ : HasPullbacks T
inst✝ : PreservesLimitsOfShape WalkingCospan L
⊢ (commaObj L (Functor.fromPUnit X) P).IsClosedUnderLimitsOfShape WalkingCospan
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case h₀
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ Over.Hom.left m ≫ c.fst = Over.Hom.left (Over.homMk (hc.lift (pullbackConeEquivBinaryFan.inverse.obj s)) ⋯) ≫ c.fst

pp: case h₁
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ Over.Hom.left m ≫ c.snd = Over.Hom.left (Over.homMk (hc.lift (pullbackConeEquivBinaryFan.inverse.obj s)) ⋯) ≫ c.snd

Tactic:
·

Goal state after:
case h₀
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ Over.Hom.left m ≫ c.fst = Over.Hom.left (Over.homMk (hc.lift (pullbackConeEquivBinaryFan.inverse.obj s)) ⋯) ≫ c.fst
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case h₁
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ Over.Hom.left m ≫ c.snd = Over.Hom.left (Over.homMk (hc.lift (pullbackConeEquivBinaryFan.inverse.obj s)) ⋯) ≫ c.snd

Tactic:
·

Goal state after:
case h₁
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ Over.Hom.left m ≫ c.snd = Over.Hom.left (Over.homMk (hc.lift (pullbackConeEquivBinaryFan.inverse.obj s)) ⋯) ≫ c.snd
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ HasLimitsOfShape (Discrete PEmpty.{1}) (Comma (𝟭 T) (Functor.fromPUnit X))

pp: case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (commaObj (𝟭 T) (Functor.fromPUnit X) P).IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})

Tactic:
·

Goal state after:
case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ HasLimitsOfShape (Discrete PEmpty.{1}) (Comma (𝟭 T) (Functor.fromPUnit X))
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (commaObj (𝟭 T) (Functor.fromPUnit X) P).IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})

Tactic:
·

Goal state after:
case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (commaObj (𝟭 T) (Functor.fromPUnit X) P).IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝ : P.ContainsIdentities
Y : P.Over ⊤ X
a : Y ⟶ Over.mk ⊤ (𝟙 X) ⋯
⊢ a.left = (Over.homMk Y.hom ⋯ ⋯).left

Tactic:
·

Goal state after:
T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝ : P.ContainsIdentities
Y : P.Over ⊤ X
a : Y ⟶ Over.mk ⊤ (𝟙 X) ⋯
⊢ a.left = (Over.homMk Y.hom ⋯ ⋯).left
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ HasColimitsOfShape (Discrete PEmpty.{1}) (Comma (Functor.fromPUnit X) (𝟭 T))

pp: case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (commaObj (Functor.fromPUnit X) (𝟭 T) P).IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})

Tactic:
·

Goal state after:
case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ HasColimitsOfShape (Discrete PEmpty.{1}) (Comma (Functor.fromPUnit X) (𝟭 T))
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (commaObj (Functor.fromPUnit X) (𝟭 T) P).IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})

Tactic:
·

Goal state after:
case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (commaObj (Functor.fromPUnit X) (𝟭 T) P).IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: case inst
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPushouts T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.HasOfPrecompProperty P
⊢ HasColimitsOfShape WalkingSpan (Comma (Functor.fromPUnit X) (𝟭 T))

pp: case inst
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPushouts T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.HasOfPrecompProperty P
⊢ (commaObj (Functor.fromPUnit X) (𝟭 T) P).IsClosedUnderColimitsOfShape WalkingSpan

Tactic:
·

Goal state after:
case inst
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPushouts T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.HasOfPrecompProperty P
⊢ HasColimitsOfShape WalkingSpan (Comma (Functor.fromPUnit X) (𝟭 T))
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: case inst
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPushouts T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.HasOfPrecompProperty P
⊢ (commaObj (Functor.fromPUnit X) (𝟭 T) P).IsClosedUnderColimitsOfShape WalkingSpan

Tactic:
·

Goal state after:
case inst
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPushouts T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.HasOfPrecompProperty P
⊢ (commaObj (Functor.fromPUnit X) (𝟭 T) P).IsClosedUnderColimitsOfShape WalkingSpan
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case refine_1
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
⊢ c.inl ≫ Under.Hom.right m =
    c.inl ≫
      Under.Hom.right (Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)

pp: case refine_2
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
⊢ c.inr ≫ Under.Hom.right m =
    c.inr ≫
      Under.Hom.right (Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)

Tactic:
·

Goal state after:
case refine_1
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
⊢ c.inl ≫ Under.Hom.right m =
    c.inl ≫
      Under.Hom.right (Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case refine_2
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
⊢ c.inr ≫ Under.Hom.right m =
    c.inr ≫
      Under.Hom.right (Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)

Tactic:
·

Goal state after:
case refine_2
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
⊢ c.inr ≫ Under.Hom.right m =
    c.inr ≫
      Under.Hom.right (Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case none
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
⊢ Hom.left f.hom ≫ (conesEquivInverseObj B F Y✝).π.app none = (conesEquivInverseObj B F X✝).π.app none

pp: case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ Hom.left f.hom ≫ (conesEquivInverseObj B F Y✝).π.app (some j) = (conesEquivInverseObj B F X✝).π.app (some j)

Tactic:
·

Goal state after:
case none
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
⊢ Hom.left f.hom ≫ (conesEquivInverseObj B F Y✝).π.app none = (conesEquivInverseObj B F X✝).π.app none
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ Hom.left f.hom ≫ (conesEquivInverseObj B F Y✝).π.app (some j) = (conesEquivInverseObj B F X✝).π.app (some j)

Tactic:
·

Goal state after:
case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ Hom.left f.hom ≫ (conesEquivInverseObj B F Y✝).π.app (some j) = (conesEquivInverseObj B F X✝).π.app (some j)
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: case h_obj
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
X Y Z : T
inst✝ : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ ∀ (X_1 : P.Over Q X), (map Q ⋯).obj X_1 = (map Q hf ⋙ map Q hg).obj X_1

pp: case h_map
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
X Y Z : T
inst✝ : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ autoParam
    (∀ (X_1 Y_1 : P.Over Q X) (f_1 : X_1 ⟶ Y_1),
      (map Q ⋯).map f_1 = eqToHom ⋯ ≫ (map Q hf ⋙ map Q hg).map f_1 ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
·

Goal state after:
case h_obj
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
X Y Z : T
inst✝ : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ ∀ (X_1 : P.Over Q X), (map Q ⋯).obj X_1 = (map Q hf ⋙ map Q hg).obj X_1