awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
trans :
  Eq (α := X₃ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
      (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄))))
    (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
      (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯))
trans₁ :
  Eq (α := X₃ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
      (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯))
    (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄)
⊢ Eq (α := X₃ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
      (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄))))
    (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄)

Tactic:
trans f₄ ≫ l₂'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
e_a :
  Eq (α := Y₂ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄)))
    (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯)
⊢ Eq (α := X₃ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
      (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄))))
    (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
      (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ Eq (α := Y₂ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄)))
    (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯)

Tactic:
(pushoutPushoutLeftIsPushout g₁ g₂ g₃ g₄).comp_coconePointUniqueUpToIso_inv
        (pushoutPushoutRightIsPushout g₁ g₂ g₃ g₄) WalkingCospan.right

Premises used: CategoryTheory.Limits.pushoutPushoutLeftIsPushout, CategoryTheory.Limits.pushoutPushoutRightIsPushout, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Limits.WalkingCospan.right, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.span, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ Eq (α := Y₂ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄)))
    (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯)

Tactic:
exact
      (pushoutPushoutLeftIsPushout g₁ g₂ g₃ g₄).comp_coconePointUniqueUpToIso_inv
        (pushoutPushoutRightIsPushout g₁ g₂ g₃ g₄) WalkingCospan.right

Premises used: CategoryTheory.Limits.pushoutPushoutLeftIsPushout, CategoryTheory.Limits.pushoutPushoutRightIsPushout, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Limits.WalkingCospan.right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ Eq (α := X₃ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
      (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯))
    (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄)

Tactic:
pushout.inr_desc _ _ _

Premises used: CategoryTheory.Limits.pushout.inr_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ Eq (α := X₃ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
      (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯))
    (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄)

Tactic:
exact pushout.inr_desc _ _ _

Premises used: CategoryTheory.Limits.pushout.inr_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
rw :
  Eq (α := X₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄)))
rw₁ :
  Eq (α := X₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := Y₁) (pushout.inl g₁ g₂)
      (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄))))
rw₂ rw₃ :
  Eq (α := X₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
⊢ Eq (α := X₁ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄)))
    (pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)

Tactic:
rw [Iso.comp_inv_eq, Category.assoc, inl_inl_pushoutAssoc_hom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Limits.inl_inl_pushoutAssoc_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
rw :
  Eq (α := X₂ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄)))
    (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
rw₁ :
  Eq (α := X₂ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄)))
rw₂ :
  Eq (α := X₂ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := Y₁) (pushout.inr g₁ g₂)
      (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄))))
rw₃ rw₄ :
  Eq (α := X₂ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
⊢ Eq (α := X₂ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (pushout.inl g₃ g₄)
      (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄))))
    (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)

Tactic:
rw [← Category.assoc, Iso.comp_inv_eq, Category.assoc, inr_inl_pushoutAssoc_hom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Limits.inr_inl_pushoutAssoc_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
x y : F ⊡ G
f : x ⟶ y
rw : G.map f.snd = (x.iso.inv ≫ F.map f.fst) ≫ y.iso.hom
rw₁ : G.map f.snd = x.iso.inv ≫ F.map f.fst ≫ y.iso.hom
rw₂ : x.iso.inv ≫ F.map f.fst ≫ y.iso.hom = G.map f.snd
rw₃ : F.map f.fst ≫ y.iso.hom = x.iso.hom ≫ G.map f.snd
rw₄ rw₅ : x.iso.hom ≫ G.map f.snd = x.iso.hom ≫ G.map f.snd
⊢ G.map f.snd ≫ y.iso.inv = x.iso.inv ≫ F.map f.fst

Tactic:
rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, f.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Limits.CategoricalPullback.Hom.w, Eq.comm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
x y : F ⊡ G
f g : x ⟶ y
hₗ : f.fst = g.fst
hᵣ : f.snd = g.snd
fst : f.fst = g.fst
snd : f.snd = g.snd
⊢ f = g

Tactic:
apply Hom.ext

Premises used: CategoryTheory.Limits.CategoricalPullback.Hom.ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
x y : F ⊡ G
f g : x ⟶ y
hₗ : f.fst = g.fst
hᵣ : f.snd = g.snd
⊢ f.fst = g.fst

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
x y : F ⊡ G
f g : x ⟶ y
hₗ : f.fst = g.fst
hᵣ : f.snd = g.snd
⊢ f.snd = g.snd

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
x y : F ⊡ G
eₗ : x.fst ≅ y.fst
eᵣ : x.snd ≅ y.snd
w : F.map eₗ.hom ≫ y.iso.hom = x.iso.hom ≫ G.map eᵣ.hom
⊢ F.map eₗ.inv ≫ x.iso.hom = y.iso.hom ≫ G.map eᵣ.inv

Tactic:
simpa using F.map eₗ.inv ≫= w.symm =≫ G.map eᵣ.inv

Premises used: CategoryTheory.Functor.map, Eq.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
x y : F ⊡ G
f : x ⟶ y
inst_3 : IsIso f
⊢ IsIso f.fst

Tactic:
inferInstanceAs (IsIso ((π₁ _ _).mapIso (asIso f)).hom)

Premises used: _private.0.CategoryTheory.Limits.CategoricalPullback.instIsIsoFst._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
x y : F ⊡ G
f : x ⟶ y
inst_3 : IsIso f
⊢ IsIso f.snd

Tactic:
inferInstanceAs (IsIso ((π₂ _ _).mapIso (asIso f)).hom)

Premises used: _private.0.CategoryTheory.Limits.CategoricalPullback.instIsIsoSnd._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
x y : F ⊡ G
f : x ⟶ y
inst_3 : IsIso f
symm : inv f.fst = (inv f).fst
⊢ (inv f).fst = inv f.fst

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
x y : F ⊡ G
f : x ⟶ y
inst_3 : IsIso f
hom_inv_id : f.fst ≫ (inv f).fst = 𝟙 x.fst
⊢ inv f.fst = (inv f).fst

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
x y : F ⊡ G
f : x ⟶ y
inst_3 : IsIso f
⊢ f.fst ≫ (inv f).fst = 𝟙 x.fst

Tactic:
simp [← comp_fst]

Premises used: CategoryTheory.Limits.CategoricalPullback.comp_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
x y : F ⊡ G
f : x ⟶ y
inst_3 : IsIso f
symm : inv f.snd = (inv f).snd
⊢ (inv f).snd = inv f.snd

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
x y : F ⊡ G
f : x ⟶ y
inst_3 : IsIso f
hom_inv_id : f.snd ≫ (inv f).snd = 𝟙 x.snd
⊢ inv f.snd = (inv f).snd

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
x y : F ⊡ G
f : x ⟶ y
inst_3 : IsIso f
⊢ f.snd ≫ (inv f).snd = 𝟙 x.snd

Tactic:
simp [← comp_snd]

Premises used: CategoryTheory.Limits.CategoricalPullback.comp_snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
S S' : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X
f g : S ⟶ S'
h₁ : f.fst = g.fst
h₂ : f.snd = g.snd
⊢ f = g

Tactic:
Hom.ext h₁ h₂

Premises used: CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
S : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X
x x' : X
f : x ⟶ x'
⊢ F.map (S.fst.map f) ≫ S.iso.hom.app x' = S.iso.hom.app x ≫ G.map (S.snd.map f)

Tactic:
S.iso.hom.naturality f

Premises used: CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.iso, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
S S' : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X
φ : S ⟶ S'
x : X
⊢ F.map (φ.fst.app x) ≫ S'.iso.hom.app x = S.iso.hom.app x ≫ G.map (φ.snd.app x)

Tactic:
NatTrans.congr_app φ.w x

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
S S' : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X
eₗ : S.fst ≅ S'.fst
eᵣ : S.snd ≅ S'.snd
w : whiskerRight eₗ.hom F ≫ S'.iso.hom = S.iso.hom ≫ whiskerRight eᵣ.hom G
w₁ : ∀ (t : X), (whiskerRight eₗ.inv F ≫ S.iso.hom).app t = (S'.iso.hom ≫ whiskerRight eᵣ.inv G).app t
⊢ whiskerRight eₗ.inv F ≫ S.iso.hom = S'.iso.hom ≫ whiskerRight eᵣ.inv G

Tactic:
ext t
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
S S' : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X
eₗ : S.fst ≅ S'.fst
eᵣ : S.snd ≅ S'.snd
w : whiskerRight eₗ.hom F ≫ S'.iso.hom = S.iso.hom ≫ whiskerRight eᵣ.hom G
t : X
⊢ (whiskerRight eₗ.inv F ≫ S.iso.hom).app t = (S'.iso.hom ≫ whiskerRight eᵣ.inv G).app t

Tactic:
simpa [← Functor.map_comp_assoc, ← Functor.map_comp] using
      congr_app (whiskerRight eₗ.inv F ≫= w.symm =≫ whiskerRight eᵣ.inv G) t

Premises used: CategoryTheory.eq_whisker, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp, Eq.symm, CategoryTheory.whisker_eq, CategoryTheory.congr_app, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
X_1 : X ⥤ F ⊡ G
h₁ :
  ∀ (x : X),
    NatTrans.app
        (CatCommSqOver.Hom.fst { fst := whiskerRight (𝟙 X_1) (π₁ F G), snd := whiskerRight (𝟙 X_1) (π₂ F G), w := ⋯ })
        x =
      (CatCommSqOver.Hom.fst
            (𝟙
              { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
                iso :=
                  X_1.associator (π₁ F G) F ≪≫
                    X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) G).symm :
                CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })).app
        x
h₂ :
  ∀ (x : X),
    NatTrans.app
        (CatCommSqOver.Hom.snd { fst := whiskerRight (𝟙 X_1) (π₁ F G), snd := whiskerRight (𝟙 X_1) (π₂ F G), w := ⋯ })
        x =
      (CatCommSqOver.Hom.snd
            (𝟙
              { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
                iso :=
                  X_1.associator (π₁ F G) F ≪≫
                    X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) G).symm :
                CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })).app
        x
⊢ { fst := whiskerRight (𝟙 X_1) (π₁ F G), snd := whiskerRight (𝟙 X_1) (π₂ F G), w := ⋯ } =
    𝟙
      { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
        iso :=
          X_1.associator (π₁ F G) F ≪≫
            X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) G).symm :
        CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
X_1 : X ⥤ F ⊡ G
x : X
⊢ NatTrans.app
      (CatCommSqOver.Hom.fst { fst := whiskerRight (𝟙 X_1) (π₁ F G), snd := whiskerRight (𝟙 X_1) (π₂ F G), w := ⋯ }) x =
    (CatCommSqOver.Hom.fst
          (𝟙
            { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
              iso :=
                X_1.associator (π₁ F G) F ≪≫
                  X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })).app
      x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
inst_3 : Category.{v₄, u₄} X
X_1 : X ⥤ F ⊡ G
x : X
⊢ NatTrans.app
      (CatCommSqOver.Hom.snd { fst := whiskerRight (𝟙 X_1) (π₁ F G), snd := whiskerRight (𝟙 X_1) (π₂ F G), w := ⋯ }) x =
    (CatCommSqOver.Hom.snd
          (𝟙
            { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
              iso :=
                X_1.associator (π₁ F G) F ≪≫
                  X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })).app
      x

Tactic:
simp