awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
ψ ψ' : CatCospanTransform F G F' G'
left : ψ.left ≅ ψ'.left
right : ψ.right ≅ ψ'.right
base : ψ.base ≅ ψ'.base
left_coherence :
  (CatCommSq.iso F ψ.left ψ.base F').hom ≫ Functor.whiskerRight left.hom F' =
    F.whiskerLeft base.hom ≫ (CatCommSq.iso F ψ'.left ψ'.base F').hom
right_coherence :
  (CatCommSq.iso G ψ.right ψ.base G').hom ≫ Functor.whiskerRight right.hom G' =
    G.whiskerLeft base.hom ≫ (CatCommSq.iso G ψ'.right ψ'.base G').hom
⊢ (CatCommSq.iso F ψ'.left ψ'.base F').hom ≫ Functor.whiskerRight left.inv F' =
    F.whiskerLeft base.inv ≫ (CatCommSq.iso F ψ.left ψ.base F').hom

Tactic:
simpa using ψ'.squareLeft.iso.hom ≫=
          IsIso.inv_eq_inv.mpr left_coherence =≫
          ψ.squareLeft.iso.hom

Premises used: Iff.mpr, CategoryTheory.CatCommSq.iso, CategoryTheory.IsIso.inv_eq_inv, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
ψ ψ' : CatCospanTransform F G F' G'
left : ψ.left ≅ ψ'.left
right : ψ.right ≅ ψ'.right
base : ψ.base ≅ ψ'.base
left_coherence :
  (CatCommSq.iso F ψ.left ψ.base F').hom ≫ Functor.whiskerRight left.hom F' =
    F.whiskerLeft base.hom ≫ (CatCommSq.iso F ψ'.left ψ'.base F').hom
right_coherence :
  (CatCommSq.iso G ψ.right ψ.base G').hom ≫ Functor.whiskerRight right.hom G' =
    G.whiskerLeft base.hom ≫ (CatCommSq.iso G ψ'.right ψ'.base G').hom
⊢ (CatCommSq.iso G ψ'.right ψ'.base G').hom ≫ Functor.whiskerRight right.inv G' =
    G.whiskerLeft base.inv ≫ (CatCommSq.iso G ψ.right ψ.base G').hom

Tactic:
simpa using ψ'.squareRight.iso.hom ≫=
          IsIso.inv_eq_inv.mpr right_coherence =≫
          ψ.squareRight.iso.hom

Premises used: Iff.mpr, CategoryTheory.CatCommSq.iso, CategoryTheory.IsIso.inv_eq_inv, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_9 : IsIso f
e : ψ ≅ ψ'
⊢ f.left ≫ (inv f).left = 𝟙 ψ'.left ∧ (inv f).left ≫ f.left = 𝟙 ψ'.left

Tactic:
simp [← CatCospanTransform.category_comp_left]

Premises used: CategoryTheory.Limits.CatCospanTransform.category_comp_left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_9 : IsIso f
e : ψ ≅ ψ'
⊢ f.right ≫ (inv f).right = 𝟙 ψ'.right ∧ (inv f).right ≫ f.right = 𝟙 ψ'.right

Tactic:
simp [← CatCospanTransform.category_comp_right]

Premises used: CategoryTheory.Limits.CatCospanTransform.category_comp_right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_9 : IsIso f
e : ψ ≅ ψ'
⊢ f.base ≫ (inv f).base = 𝟙 ψ'.base ∧ (inv f).base ≫ f.base = 𝟙 ψ'.base

Tactic:
simp [← CatCospanTransform.category_comp_base]

Premises used: CategoryTheory.Limits.CatCospanTransform.category_comp_base
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_6 : IsIso f
symm : (inv f).left = inv f.left
⊢ inv f.left = (inv f).left

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_6 : IsIso f
hom_inv_id : (inv f).left ≫ f.left = 𝟙 ψ'.left
⊢ (inv f).left = inv f.left

Tactic:
apply IsIso.eq_inv_of_inv_hom_id

Premises used: CategoryTheory.IsIso.eq_inv_of_inv_hom_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_6 : IsIso f
⊢ (inv f).left ≫ f.left = 𝟙 ψ'.left

Tactic:
simp [← CatCospanTransform.category_comp_left]

Premises used: CategoryTheory.Limits.CatCospanTransform.category_comp_left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_6 : IsIso f
symm : (inv f).right = inv f.right
⊢ inv f.right = (inv f).right

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_6 : IsIso f
hom_inv_id : (inv f).right ≫ f.right = 𝟙 ψ'.right
⊢ (inv f).right = inv f.right

Tactic:
apply IsIso.eq_inv_of_inv_hom_id

Premises used: CategoryTheory.IsIso.eq_inv_of_inv_hom_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_6 : IsIso f
⊢ (inv f).right ≫ f.right = 𝟙 ψ'.right

Tactic:
simp [← CatCospanTransform.category_comp_right]

Premises used: CategoryTheory.Limits.CatCospanTransform.category_comp_right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_6 : IsIso f
symm : (inv f).base = inv f.base
⊢ inv f.base = (inv f).base

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_6 : IsIso f
hom_inv_id : (inv f).base ≫ f.base = 𝟙 ψ'.base
⊢ (inv f).base = inv f.base

Tactic:
apply IsIso.eq_inv_of_inv_hom_id

Premises used: CategoryTheory.IsIso.eq_inv_of_inv_hom_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_9 : IsIso f
e : ψ ≅ ψ'
⊢ e.hom.left ≫ e.inv.left = 𝟙 ψ.left

Tactic:
simp [← category_comp_left]

Premises used: CategoryTheory.Limits.CatCospanTransform.category_comp_left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_9 : IsIso f
e : ψ ≅ ψ'
⊢ e.inv.left ≫ e.hom.left = 𝟙 ψ'.left

Tactic:
simp [← category_comp_left]

Premises used: CategoryTheory.Limits.CatCospanTransform.category_comp_left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_9 : IsIso f
e : ψ ≅ ψ'
⊢ e.hom.right ≫ e.inv.right = 𝟙 ψ.right

Tactic:
simp [← category_comp_right]

Premises used: CategoryTheory.Limits.CatCospanTransform.category_comp_right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_9 : IsIso f
e : ψ ≅ ψ'
⊢ e.inv.right ≫ e.hom.right = 𝟙 ψ'.right

Tactic:
simp [← category_comp_right]

Premises used: CategoryTheory.Limits.CatCospanTransform.category_comp_right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_9 : IsIso f
e : ψ ≅ ψ'
⊢ e.hom.base ≫ e.inv.base = 𝟙 ψ.base

Tactic:
simp [← category_comp_base]

Premises used: CategoryTheory.Limits.CatCospanTransform.category_comp_base
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst_9 : IsIso f
e : ψ ≅ ψ'
⊢ e.inv.base ≫ e.hom.base = 𝟙 ψ'.base

Tactic:
simp [← category_comp_base]

Premises used: CategoryTheory.Limits.CatCospanTransform.category_comp_base
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
h : IsIso f.left ∧ IsIso f.base ∧ IsIso f.right
⊢ IsIso f.left

Tactic:
obtain ⟨_, _, _⟩ := h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
h : IsIso f.left ∧ IsIso f.base ∧ IsIso f.right
left : IsIso f.left
⊢ IsIso f.base

Tactic:
obtain ⟨_, _, _⟩ := h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
h : IsIso f.left ∧ IsIso f.base ∧ IsIso f.right
left : IsIso f.left
left₁ : IsIso f.base
⊢ IsIso f.right

Tactic:
obtain ⟨_, _, _⟩ := h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
left : IsIso f.left
left_1 : IsIso f.base
right : IsIso f.right
h :
  f ≫ (mkIso (asIso f.left) (asIso f.right) (asIso f.base) ⋯ ⋯).inv = 𝟙 ψ' ∧
    (mkIso (asIso f.left) (asIso f.right) (asIso f.base) ⋯ ⋯).inv ≫ f = 𝟙 ψ'
⊢ IsIso f

Tactic:
use mkIso (asIso f.left) (asIso f.right) (asIso f.base)
      f.left_coherence f.right_coherence |>.inv

Premises used: CategoryTheory.Limits.CatCospanTransformMorphism.right, CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence, CategoryTheory.Limits.CatCospanTransform.mkIso, CategoryTheory.Limits.CatCospanTransformMorphism.left, CategoryTheory.Limits.CatCospanTransformMorphism.base, CategoryTheory.Iso.inv, CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
ψ : CatCospanTransform F G F' G'
φ : CatCospanTransform F' G' F'' G''
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : ψ ◁ 𝟙 φ = 𝟙 (ψ.comp φ)
⊢ ψ ◁ 𝟙 φ = 𝟙 (ψ.comp φ)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
ψ : CatCospanTransform F G F' G'
φ φ' φ'' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
θ' : φ' ⟶ φ''
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : ψ ◁ (θ ≫ θ') = ψ ◁ θ ≫ ψ ◁ θ'
⊢ ψ ◁ (θ ≫ θ') = ψ ◁ θ ≫ ψ ◁ θ'

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst_3 : Category.{v₄, u₄} A'
inst_4 : Category.{v₅, u₅} B'
inst_5 : Category.{v₆, u₆} C'
F' : Functor.{v₄, v₅, u₄, u₅} A' B'
G' : Functor.{v₆, v₅, u₆, u₅} C' B'
inst_6 : Category.{v₇, u₇} A''
inst_7 : Category.{v₈, u₈} B''
inst_8 : Category.{v₉, u₉} C''
F'' : Functor.{v₇, v₈, u₇, u₈} A'' B''
G'' : Functor.{v₉, v₈, u₉, u₈} C'' B''
A''' : Type u₁₀
B''' : Type u₁₁
C''' : Type u₁₂
inst_9 : Category.{v₁₀, u₁₀} A'''
inst_10 : Category.{v₁₁, u₁₁} B'''
inst_11 : Category.{v₁₂, u₁₂} C'''
F''' : Functor.{v₁₀, v₁₁, u₁₀, u₁₁} A''' B'''
G''' : Functor.{v₁₂, v₁₁, u₁₂, u₁₁} C''' B'''
ψ_1 ψ'_1 ψ'' : CatCospanTransform F G F' G'
η_1 : ψ_1 ⟶ ψ'_1
η' : ψ'_1 ⟶ ψ''
φ_1 φ'_1 φ'' : CatCospanTransform F' G' F'' G''
θ_1 : φ_1 ⟶ φ'_1
θ' : φ'_1 ⟶ φ''
τ τ' : CatCospanTransform F'' G'' F''' G'''
γ : τ ⟶ τ'
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst_12 : IsIso η
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
inst_13 : IsIso θ
⊢ ψ ◁ θ ≫ ψ ◁ inv θ = 𝟙 (ψ.comp φ)

Tactic:
simp [← whiskerLeft_comp]

Premises used: CategoryTheory.Limits.CatCospanTransform.whiskerLeft_comp