mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Prod

Goal state before:
pp: case hr
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M₁
inst✝³ : Module S M₁
inst✝² : IsScalarTower R S M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝¹ : M₁
x✝ : M₃
⊢ ((AlgebraTensorModule.curry
            (((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃)) ∘ₗ
              AlgebraTensorModule.lift
                (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                  (AlgebraTensorModule.mk R S M₁ M₂).prod (AlgebraTensorModule.mk R S M₁ M₃))))
          x✝¹ ∘ₗ
        LinearMap.inr R M₂ M₃)
      x✝ =
    ((AlgebraTensorModule.curry LinearMap.id) x✝¹ ∘ₗ LinearMap.inr R M₂ M₃) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Prod

Goal state before:
pp: R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : Algebra R S
inst✝⁶ : Module R M₁
inst✝⁵ : Module S M₁
inst✝⁴ : IsScalarTower R S M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module S M₂
inst✝ : IsScalarTower R S M₂
c : S
x : (M₁ × M₂) ⊗[R] M₃
⊢ (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
          (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
      (c • 0) =
    c •
      (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
            (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
        0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g✝ : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g✝ = α.app i ≫ c.ι.app i
this✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g✝ = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
r : ↥s
this :
  (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) ((ConcreteCategory.hom g') ↑r) =
      (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) 0 ↔
    ∃ k f g,
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map f)) ((ConcreteCategory.hom g') ↑r) =
        (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map g)) 0
H : (ConcreteCategory.hom (g' ≫ c.ι.app i)) ↑r = 0
k : J
f g : i ⟶ k
e :
  (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map f)) ((ConcreteCategory.hom g') ↑r) =
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map g)) 0
⊢ ∃ i' hi', (ConcreteCategory.hom (F.map hi')) ((ConcreteCategory.hom g') ↑r) = 0

Tactic:
exact ⟨k, f, by simpa using! e⟩

Goal state after:
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: 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
f : ((coyoneda.obj (Opposite.op S)).mapCocone c).pt
⊢ ∀ (i : J),
    S.hom ≫ Under.Hom.right f =
      { app := fun i ↦ (F.obj i).hom, naturality := ⋯ }.app i ≫ ((Under.forget R).mapCocone c).ι.app i

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesColimitsOfShape J L
inst✝ : HasColimitsOfShape J A
c : (D : J ⥤ T) → [HasColimit D] → Cocone D
hc : (D : J ⥤ T) → [inst : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasColimit D] {X : T} (s : D ⟶ (Functor.const J).obj X),
    (∀ (j : J), P (s.app j)) → P ((hc D).desc { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : (MorphismProperty.costructuredArrowObj L P).ColimitOfShape J Y
hd : IsColimit ((proj L X ⋙ L).mapCocone d.cocone) := isColimitOfPreserves (proj L X ⋙ L) d.isColimit
j : J
⊢ ((proj L X ⋙ L).mapCocone d.cocone).ι.app j ≫ Y.hom = (d.diag.obj j).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
X✝ Y✝ : PullbackCone f g
f✝ : X✝ ⟶ Y✝
⊢ ((𝟭 (PullbackCone f g)).map f✝ ≫ Y✝.eta.hom).hom =
    (X✝.eta.hom ≫
        ({ obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
          f✝).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z : C
f : Y ⟶ X✝
g : Z ⟶ X✝
X : BinaryFan (Over.mk f) (Over.mk g)
⊢ Over.Hom.left
      (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
          X).fst =
    Over.Hom.left
      ((Over.isoMk
            (Iso.refl
              (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                          map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                        { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                          map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ }).obj
                    X).pt.left)
            ⋯).hom ≫
        ((𝟭 (BinaryFan (Over.mk f) (Over.mk g))).obj X).fst)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z : C
f : Y ⟶ X✝
g : Z ⟶ X✝
X : BinaryFan (Over.mk f) (Over.mk g)
⊢ Over.Hom.left
      (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
          X).snd =
    Over.Hom.left
      ((Over.isoMk
            (Iso.refl
              (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                          map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                        { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                          map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ }).obj
                    X).pt.left)
            ⋯).hom ≫
        ((𝟭 (BinaryFan (Over.mk f) (Over.mk g))).obj X).snd)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: 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
inst✝⁵ : HasPullbacks A
inst✝⁴ : HasPullbacks T
inst✝³ : PreservesLimitsOfShape WalkingCospan L
X : T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
Y : CostructuredArrow L X
pres : LimitPresentation WalkingCospan Y
hpres : ∀ (j : WalkingCospan), MorphismProperty.costructuredArrowObj L P (pres.diag.obj j)
h :
  IsPullback (L.map (pres.π.app WalkingCospan.left).left) (L.map (pres.π.app WalkingCospan.right).left)
    (L.map (pres.diag.map WalkingCospan.Hom.inl).left) (L.map (pres.diag.map WalkingCospan.Hom.inr).left)
⊢ Y.hom = L.map (pres.π.app WalkingCospan.left).left ≫ (pres.diag.obj WalkingCospan.left).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesLimitsOfShape J L
inst✝ : HasLimitsOfShape J A
c : (D : J ⥤ T) → [HasLimit D] → Cone D
hc : (D : J ⥤ T) → [inst : HasLimit D] → IsLimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasLimit D] {X : T} (s : (Functor.const J).obj X ⟶ D),
    (∀ (j : J), P (s.app j)) → P ((hc D).lift { pt := X, π := s })
X : T
Y : StructuredArrow X L
d : (MorphismProperty.structuredArrowObj L P).LimitOfShape J Y
hd : IsLimit ((proj X L ⋙ L).mapCone d.cone) := isLimitOfPreserves (proj X L ⋙ L) d.isLimit
j : J
⊢ Y.hom ≫ ((proj X L ⋙ L).mapCone d.cone).π.app j = (d.diag.obj j).hom

Tactic:
simp

Goal state after:
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.Under ⊤ X
⊢ (Under.mk ⊤ (𝟙 X) ⋯).hom ≫ Y.hom = Y.hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
X✝ Y✝ : PushoutCocone f✝ g
f : X✝ ⟶ Y✝
⊢ ((𝟭 (PushoutCocone f✝ g)).map f ≫ Y✝.eta.hom).hom =
    (X✝.eta.hom ≫
        ({ obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
          f).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z : C
f : X✝ ⟶ Y
g : X✝ ⟶ Z
X : BinaryCofan (Under.mk f) (Under.mk g)
⊢ Under.Hom.right
      ((({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                  map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                  map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
            X).inl ≫
        (Under.isoMk
            (Iso.refl
              (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                          map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ } ⋙
                        { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                          map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ }).obj
                    X).pt.right)
            ⋯).hom) =
    Under.Hom.right ((𝟭 (BinaryCofan (Under.mk f) (Under.mk g))).obj X).inl

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z : C
f : X✝ ⟶ Y
g : X✝ ⟶ Z
X : BinaryCofan (Under.mk f) (Under.mk g)
⊢ Under.Hom.right
      ((({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                  map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                  map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
            X).inr ≫
        (Under.isoMk
            (Iso.refl
              (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                          map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ } ⋙
                        { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                          map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ }).obj
                    X).pt.right)
            ⋯).hom) =
    Under.Hom.right ((𝟭 (BinaryCofan (Under.mk f) (Under.mk g))).obj X).inr

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
X✝ Y✝ : BinaryCofan (Under.mk f) (Under.mk g)
f✝ : X✝ ⟶ Y✝
⊢ Under.Hom.right
      (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                  map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                  map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
            f✝ ≫
          (BinaryCofan.ext
              (Under.isoMk
                (Iso.refl
                  (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                              map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯,
                              map_comp := ⋯ } ⋙
                            { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                              map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                              map_comp := ⋯ }).obj
                        Y✝).pt.right)
                ⋯)
              ⋯ ⋯).hom).hom =
    Under.Hom.right
      ((BinaryCofan.ext
              (Under.isoMk
                (Iso.refl
                  (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                              map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯,
                              map_comp := ⋯ } ⋙
                            { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                              map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                              map_comp := ⋯ }).obj
                        X✝).pt.right)
                ⋯)
              ⋯ ⋯).hom ≫
          (𝟭 (BinaryCofan (Under.mk f) (Under.mk g))).map f✝).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: 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
⊢ Under.Hom.right
      ({ obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.map
            ((NatIso.ofComponents (fun c ↦ c.eta) ⋯).hom.app c) ≫
          (NatIso.ofComponents
                  (fun X_1 ↦
                    BinaryCofan.ext
                      (Under.isoMk
                        (Iso.refl
                          (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                                      map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯,
                                      map_comp := ⋯ } ⋙
                                    { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                                      map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                                      map_comp := ⋯ }).obj
                                X_1).pt.right)
                        ⋯)
                      ⋯ ⋯)
                  ⋯).hom.app
            ({ obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                  map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.obj
              c)).hom =
    Under.Hom.right
      (𝟙
          ({ obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.obj
            c)).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y Z : Over X
c : BinaryFan Y Z
hc : IsLimit c
⊢ CommSq (Hom.left c.fst) (Hom.left c.snd) Y.hom Z.hom

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
J : Type u
x✝¹ : _root_.Finite J
A : Under R
x✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj.limitsOfShape (Discrete J) A
pres : LimitPresentation (Discrete J) A
hpres : ∀ (j : Discrete J), (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
i : Discrete J
⊢ pres.diag.obj i = (Discrete.functor fun i ↦ pres.diag.obj { as := i }).obj i

Tactic:
simp

Goal state after:
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

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
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
U V : P.Over Q X
k : U ⟶ V
⊢ ((map Q ⋯).map k).left = (eqToHom ⋯ ≫ (map Q hf ⋙ map Q hg).map k ≫ eqToHom ⋯).left

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.IsStableUnderBaseChange
A B : P.Over Q Y
g : A ⟶ B
⊢ pullback.lift (pullback.fst A.hom f ≫ g.left) (pullback.snd A.hom f) ⋯ ≫ (Over.mk Q (pullback.snd B.hom f) ⋯).hom =
    (Over.mk Q (pullback.snd A.hom f) ⋯).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X✝ Y Z : T
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderBaseChangeAlong f
inst✝⁴ : P.IsStableUnderBaseChangeAlong g
inst✝³ : P.HasPullbacksAlong f
inst✝² : P.HasPullbacksAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderBaseChange
fg : X✝ ⟶ Z
hfg : fg = f ≫ g
this✝ : P.HasPullbacksAlong fg
X : P.Over Q Z
this : HasPullback X.hom fg
⊢ (pullback.congrHom ⋯ hfg ≪≫ (pullbackLeftPullbackSndIso X.hom g f).symm).hom ≫
      ((pullback P Q g ⋙ pullback P Q f).obj X).hom =
    ((pullback P Q fg).obj X).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderBaseChangeAlong f
inst✝⁴ : P.IsStableUnderBaseChangeAlong g
inst✝³ : P.HasPullbacksAlong f
inst✝² : P.HasPullbacksAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderBaseChange
A : P.Over Q Z
⊢ ((pullbackComp f g (f ≫ g) ⋯).hom.app A).left ≫ pullback.fst (pullback.snd A.hom g) f ≫ pullback.fst A.hom g =
    pullback.fst A.hom (f ≫ g)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: 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
X Y Z : T
f : X ⟶ Y
hPf : P f
hQf : Q f
g : Y ⟶ Z
inst✝³ : P.IsStableUnderBaseChangeAlong f
inst✝² : P.IsStableUnderBaseChangeAlong g
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : HasPullbacks T
fg : X ⟶ Z
hfg : f ≫ g = fg
A : P.Over Q Z
⊢ A.hom ≫ 𝟙 Z = 𝟙 A.left ≫ A.hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: 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
X Y Z : T
f : X ⟶ Y
hPf : P f
hQf : Q f
g : Y ⟶ Z
inst✝³ : P.IsStableUnderBaseChangeAlong f
inst✝² : P.IsStableUnderBaseChangeAlong g
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : HasPullbacks T
fg : X ⟶ Z
hfg : f ≫ g = fg
A : P.Over Q Z
⊢ pullback.map A.hom fg A.hom g (𝟙 A.left) f (𝟙 Z) ⋯ ⋯ ≫ ((pullback P Q g).obj A).hom =
    ((pullback P Q fg ⋙ map Q hPf).obj A).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: 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
X Y Z : T
f : X ⟶ Y
hPf : P f
hQf : Q f
g : Y ⟶ Z
inst✝³ : P.IsStableUnderBaseChangeAlong f
inst✝² : P.IsStableUnderBaseChangeAlong g
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : HasPullbacks T
fg : X ⟶ Z
hfg : f ≫ g = fg
A : P.Over Q Z
⊢ A.hom = 𝟙 ((𝟭 T).obj A.left) ≫ A.hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: 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
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ 𝟙 ((𝟭 (P.Over Q X)).obj A).left ≫ ((map Q hPf).obj A).hom = A.hom ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: 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
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj A).left) A.hom ⋯ ≫ ((map Q hPf ⋙ pullback P Q f).obj A).hom =
    ((𝟭 (P.Over Q X)).obj A).hom

Tactic:
simp

Goal state after: