mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case refine_2
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁷ : Ring R
inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M'
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x✝¹ : M₂
x✝ : x✝¹ ∈ ⇑f '' {v | ∀ (i : ι), v i ∈ p i}
x : (i : ι) → M₁ i
hx : x ∈ {v | ∀ (i : ι), v i ∈ p i}
hf : f x = x✝¹
i : ι
this : DecidableEq ι := Classical.decEq ι
j : ι
hij : ¬j = i
⊢ update x i (c • x i) j ∈ p j

Tactic:
update_of_ne hij

Goal state after:
case refine_2
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁷ : Ring R
inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M'
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x✝¹ : M₂
x✝ : x✝¹ ∈ ⇑f '' {v | ∀ (i : ι), v i ∈ p i}
x : (i : ι) → M₁ i
hx : x ∈ {v | ∀ (i : ι), v i ∈ p i}
hf : f x = x✝¹
i : ι
this : DecidableEq ι := Classical.decEq ι
j : ι
hij : ¬j = i
⊢ x j ∈ p j
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : Cᵒᵖ
x✝¹ : C
x✝ : (coyoneda.obj X).obj x✝¹
⊢ ((Functor.const C).obj PUnit.{v + 1}).obj x✝¹

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
j : J
eq :
  (hom ((hc (op s.pt)).lift ((coyoneda.obj (op s.pt)).mapCone s) ≫ ((coyoneda.obj (op s.pt)).mapCone c).π.app j))
      (𝟙 s.pt) =
    (hom (((coyoneda.obj (op s.pt)).mapCone s).π.app j)) (𝟙 s.pt)
⊢ m ≫ c.π.app j = (hom ((hc (op s.pt)).lift ((coyoneda.obj (op s.pt)).mapCone s))) (𝟙 s.pt) ≫ c.π.app j

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : C
f : (shrinkYoneda.{w, v, u}.obj Y✝).obj (op X✝)
⊢ shrinkYoneda.{w, v, u}.map (shrinkYonedaObjObjEquiv (shrinkYonedaEquiv (shrinkYonedaEquiv.symm f))) =
    shrinkYonedaEquiv.symm f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : Cᵒᵖ
f : (shrinkCoyoneda.{w, v, u}.obj Y✝).obj (unop X✝)
⊢ shrinkCoyoneda.{w, v, u}.map (shrinkCoyonedaObjObjEquiv (shrinkCoyonedaEquiv (shrinkCoyonedaEquiv.symm f))).op =
    shrinkCoyonedaEquiv.symm f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
f : Y ⟶ Z
inst✝ : IsIso f
⊢ inv (X ◁ f) = X ◁ inv f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
f : X ⟶ Y
Z : C
inst✝ : IsIso f
⊢ inv (f ▷ Z) = inv f ▷ Z

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: case mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
X₁ X₂ : D
μIso✝ : (X Y : D) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
whiskerLeft_eq✝ :
  ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso✝ X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso✝ X Y₂).hom
whiskerRight_eq✝ :
  ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso✝ X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso✝ X₂ Y).hom
tensorHom_eq✝ :
  ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    F.map (f ⊗ₘ g) = (μIso✝ X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso✝ Y₁ Y₂).hom
εIso✝ : 𝟙_ C ≅ F.obj (𝟙_ D)
associator_eq✝ :
  ∀ (X Y Z : D),
    F.map (α_ X Y Z).hom =
      (((μIso✝ (X ⊗ Y) Z).symm ≪≫ ((μIso✝ X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
          α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ μIso✝ Y Z) ≪≫ μIso✝ X (Y ⊗ Z)).hom
leftUnitor_eq✝ :
  ∀ (X : D), F.map (λ_ X).hom = (((μIso✝ (𝟙_ D) X).symm ≪≫ (εIso✝.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫ λ_ (F.obj X)).hom
rightUnitor_eq✝ :
  ∀ (X : D), F.map (ρ_ X).hom = (((μIso✝ X (𝟙_ D)).symm ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso✝.symm)) ≪≫ ρ_ (F.obj X)).hom
⊢ F.map (𝟙 X₁ ⊗ₘ 𝟙 X₂) = F.map (𝟙 (X₁ ⊗ X₂))

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: case mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : D
f₁ : X₁✝ ⟶ Y₁✝
f₂ : X₂✝ ⟶ Y₂✝
g₁ : Y₁✝ ⟶ Z₁✝
g₂ : Y₂✝ ⟶ Z₂✝
μIso✝ : (X Y : D) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
whiskerLeft_eq✝ :
  ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso✝ X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso✝ X Y₂).hom
whiskerRight_eq✝ :
  ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso✝ X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso✝ X₂ Y).hom
tensorHom_eq✝ :
  ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    F.map (f ⊗ₘ g) = (μIso✝ X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso✝ Y₁ Y₂).hom
εIso✝ : 𝟙_ C ≅ F.obj (𝟙_ D)
associator_eq✝ :
  ∀ (X Y Z : D),
    F.map (α_ X Y Z).hom =
      (((μIso✝ (X ⊗ Y) Z).symm ≪≫ ((μIso✝ X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
          α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ μIso✝ Y Z) ≪≫ μIso✝ X (Y ⊗ Z)).hom
leftUnitor_eq✝ :
  ∀ (X : D), F.map (λ_ X).hom = (((μIso✝ (𝟙_ D) X).symm ≪≫ (εIso✝.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫ λ_ (F.obj X)).hom
rightUnitor_eq✝ :
  ∀ (X : D), F.map (ρ_ X).hom = (((μIso✝ X (𝟙_ D)).symm ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso✝.symm)) ≪≫ ρ_ (F.obj X)).hom
⊢ F.map ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) = F.map (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: case mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
X Y : D
μIso✝ : (X Y : D) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
whiskerLeft_eq✝ :
  ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso✝ X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso✝ X Y₂).hom
whiskerRight_eq✝ :
  ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso✝ X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso✝ X₂ Y).hom
tensorHom_eq✝ :
  ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    F.map (f ⊗ₘ g) = (μIso✝ X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso✝ Y₁ Y₂).hom
εIso✝ : 𝟙_ C ≅ F.obj (𝟙_ D)
associator_eq✝ :
  ∀ (X Y Z : D),
    F.map (α_ X Y Z).hom =
      (((μIso✝ (X ⊗ Y) Z).symm ≪≫ ((μIso✝ X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
          α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ μIso✝ Y Z) ≪≫ μIso✝ X (Y ⊗ Z)).hom
leftUnitor_eq✝ :
  ∀ (X : D), F.map (λ_ X).hom = (((μIso✝ (𝟙_ D) X).symm ≪≫ (εIso✝.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫ λ_ (F.obj X)).hom
rightUnitor_eq✝ :
  ∀ (X : D), F.map (ρ_ X).hom = (((μIso✝ X (𝟙_ D)).symm ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso✝.symm)) ≪≫ ρ_ (F.obj X)).hom
⊢ F.map ((α_ X (𝟙_ D) Y).hom ≫ X ◁ (λ_ Y).hom) = F.map ((ρ_ X).hom ▷ Y)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝¹³ : Semiring R
C : Type u_2
D : Type u_3
inst✝¹² : Category.{v_1, u_2} C
inst✝¹¹ : Category.{v_2, u_3} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryTheory.Linear R C
inst✝⁷ : CategoryTheory.Linear R D
F : C ⥤ D
inst✝⁶ : Linear R F
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
inst✝⁴ : Preadditive E
inst✝³ : CategoryTheory.Linear R E
G : D ⥤ E
inst✝² : F.Full
inst✝¹ : F.EssSurj
inst✝ : Linear R (F ⋙ G)
X Y : D
f : X ⟶ Y
r : R
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
⊢ f = (F.objObjPreimageIso X).inv ≫ F.map f' ≫ (F.objObjPreimageIso Y).hom

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfg : C
η : g ≅ h
η_f : p ⊗ f ≅ pf
η_fg : pf ⊗ g ≅ pfg
η_fh : pf ⊗ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)

Tactic:
apply Iso.ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfg : C
η : g ≅ h
η_f : p ⊗ f ≅ pf
η_fg : pf ⊗ g ≅ pfg
η_fh : pf ⊗ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ (p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh).hom = (normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)).hom
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfh : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
η_fh : pf ⊗ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh

Tactic:
apply Iso.ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfh : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
η_fh : pf ⊗ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh).hom = (normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh).hom
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g pf : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g = η_g

Tactic:
apply Iso.ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g pf : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g).hom = η_g.hom
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
h_η : 𝟙_ C ◁ η ≪≫ η_g = η_f
h_θ : 𝟙_ C ◁ θ ≪≫ η_g = η_f
⊢ η = θ

Tactic:
apply Iso.ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
h_η : 𝟙_ C ◁ η ≪≫ η_g = η_f
h_θ : 𝟙_ C ◁ θ ≪≫ η_g = η_f
⊢ η.hom = θ.hom
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.leftUnitor x✝).hom =
    (((Iso.refl
              (MonoidalCategoryStruct.tensorObj
                (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)))
                (equivalenceSemimoduleCat.functor.obj x✝))).symm ≪≫
          MonoidalCategory.tensorIso (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R))).symm
            (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
        MonoidalCategoryStruct.leftUnitor (equivalenceSemimoduleCat.functor.obj x✝)).hom

Tactic:
by ext1; exact TensorProduct.ext rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.rightUnitor x✝).hom =
    (((Iso.refl
              (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝)
                (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorUnit (ModuleCat R))))).symm ≪≫
          MonoidalCategory.tensorIso (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))
            (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R))).symm) ≪≫
        MonoidalCategoryStruct.rightUnitor (equivalenceSemimoduleCat.functor.obj x✝)).hom

Tactic:
by ext1; exact TensorProduct.ext rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case ε
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
⊢ ε F = ε F

Tactic:
exact congr(($eq).ε)

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x✝¹ x✝ : SemimoduleCat R
⊢ ∀ (x : ↑x✝¹) (y : ↑x✝),
    (Hom.hom ((x✝¹.braiding x✝).hom ≫ (x✝.braiding x✝¹).hom)) (x ⊗ₜ[R] y) = (Hom.hom (𝟙 (x✝¹ ⊗ x✝))) (x ⊗ₜ[R] y)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cocone F.unop
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeUnop c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneOfCoconeUnop c).π.app j = s.π.app j
⊢ m = (hc.desc (coconeUnopOfCone s)).op

Tactic:
refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)
    simpa only [Quiver.Hom.unop_op, IsColimit.fac] using! w (op j)

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : HasWidePullbacks C
ι : Type w
⊢ HasColimitsOfShape (WidePushoutShape ι) Cᵒᵖ

Tactic:
rw [hasColimitsOfShape_opposite_iff]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : HasWidePullbacks C
ι : Type w
⊢ HasLimitsOfShape (WidePushoutShape ι)ᵒᵖ C
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} J✝
inst✝ : HasFiniteWidePullbacks C
J : Type
x✝ : Finite J
⊢ HasColimitsOfShape (WidePushoutShape J) Cᵒᵖ

Tactic:
rw [hasColimitsOfShape_opposite_iff]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} J✝
inst✝ : HasFiniteWidePullbacks C
J : Type
x✝ : Finite J
⊢ HasLimitsOfShape (WidePushoutShape J)ᵒᵖ C
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : HasFiniteWidePullbacks C
⊢ HasFiniteWidePushouts Cᵒᵖ

Tactic:
refine ⟨fun J _ ↦ ?_⟩
  rw [hasColimitsOfShape_opposite_iff]
  exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case none.none.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).map (WidePushoutShape.Hom.id none) ≫
      (match none with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.id none)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case none.some.left.init
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).map (WidePushoutShape.Hom.init WalkingPair.left) ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.init WalkingPair.left)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case none.some.right.init
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).map (WidePushoutShape.Hom.init WalkingPair.right) ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.init WalkingPair.right)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case some.left.some.left.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.id (some WalkingPair.left))

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case some.right.some.right.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom =
    (match some WalkingPair.right with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.id (some WalkingPair.right))

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: case none
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : X✝ ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
c : PushoutCocone f g
X : C
⊢ ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
            (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).π.app
      none =
    (Iso.refl
          ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
              (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).pt).hom ≫
      ((yoneda.obj X).mapCone c.op).π.app none

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: case some.left
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : X✝ ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
c : PushoutCocone f g
X : C
⊢ ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
            (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).π.app
      (some WalkingPair.left) =
    (Iso.refl
          ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
              (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).pt).hom ≫
      ((yoneda.obj X).mapCone c.op).π.app (some WalkingPair.left)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: case some.right
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : X✝ ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
c : PushoutCocone f g
X : C
⊢ ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
            (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).π.app
      (some WalkingPair.right) =
    (Iso.refl
          ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
              (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).pt).hom ≫
      ((yoneda.obj X).mapCone c.op).π.app (some WalkingPair.right)

Tactic:
cat_disch

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

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : F₁.map f ≫ app Y✝ = app X✝ ≫ F₂.map f
hg : F₁.map g ≫ app Z✝ = app Y✝ ≫ F₂.map g
| F₁.map f ≫ app Y✝

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : F₁.map f ≫ app Y✝ = app X✝ ≫ F₂.map f
hg : F₁.map g ≫ app Z✝ = app Y✝ ≫ F₂.map g
| F₂.map g

Tactic:
rw [hf]

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : F₁.map f ≫ app Y✝ = app X✝ ≫ F₂.map f
hg : F₁.map g ≫ app Z✝ = app Y✝ ≫ F₂.map g
| app X✝ ≫ F₂.map f

case a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : F₁.map f ≫ app Y✝ = app X✝ ≫ F₂.map f
hg : F₁.map g ≫ app Z✝ = app Y✝ ≫ F₂.map g
| F₂.map g