mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : 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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁸ : Category.{v₂, u₂} B
inst✝⁷ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁶ : Category.{v₄, u₄} A'
inst✝⁵ : Category.{v₅, u₅} B'
inst✝⁴ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝³ : Category.{v₇, u₇} A''
inst✝² : Category.{v₈, u₈} B''
inst✝¹ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ f.left ≫ (inv f).left = 𝟙 ψ'.left ∧ (inv f).left ≫ f.left = 𝟙 ψ'.left

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁸ : Category.{v₂, u₂} B
inst✝⁷ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁶ : Category.{v₄, u₄} A'
inst✝⁵ : Category.{v₅, u₅} B'
inst✝⁴ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝³ : Category.{v₇, u₇} A''
inst✝² : Category.{v₈, u₈} B''
inst✝¹ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ f.right ≫ (inv f).right = 𝟙 ψ'.right ∧ (inv f).right ≫ f.right = 𝟙 ψ'.right

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁸ : Category.{v₂, u₂} B
inst✝⁷ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁶ : Category.{v₄, u₄} A'
inst✝⁵ : Category.{v₅, u₅} B'
inst✝⁴ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝³ : Category.{v₇, u₇} A''
inst✝² : Category.{v₈, u₈} B''
inst✝¹ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ f.base ≫ (inv f).base = 𝟙 ψ'.base ∧ (inv f).base ≫ f.base = 𝟙 ψ'.base

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝³ : Category.{v₄, u₄} A'
inst✝² : Category.{v₅, u₅} B'
inst✝¹ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
⊢ inv f.left = (inv f).left

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝³ : Category.{v₄, u₄} A'
inst✝² : Category.{v₅, u₅} B'
inst✝¹ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
⊢ inv f.right = (inv f).right

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝³ : Category.{v₄, u₄} A'
inst✝² : Category.{v₅, u₅} B'
inst✝¹ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
⊢ inv f.base = (inv f).base

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁸ : Category.{v₂, u₂} B
inst✝⁷ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁶ : Category.{v₄, u₄} A'
inst✝⁵ : Category.{v₅, u₅} B'
inst✝⁴ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝³ : Category.{v₇, u₇} A''
inst✝² : Category.{v₈, u₈} B''
inst✝¹ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ e.hom.left ≫ e.inv.left = 𝟙 ψ.left

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁸ : Category.{v₂, u₂} B
inst✝⁷ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁶ : Category.{v₄, u₄} A'
inst✝⁵ : Category.{v₅, u₅} B'
inst✝⁴ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝³ : Category.{v₇, u₇} A''
inst✝² : Category.{v₈, u₈} B''
inst✝¹ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ e.inv.left ≫ e.hom.left = 𝟙 ψ'.left

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁸ : Category.{v₂, u₂} B
inst✝⁷ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁶ : Category.{v₄, u₄} A'
inst✝⁵ : Category.{v₅, u₅} B'
inst✝⁴ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝³ : Category.{v₇, u₇} A''
inst✝² : Category.{v₈, u₈} B''
inst✝¹ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ e.hom.right ≫ e.inv.right = 𝟙 ψ.right

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁸ : Category.{v₂, u₂} B
inst✝⁷ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁶ : Category.{v₄, u₄} A'
inst✝⁵ : Category.{v₅, u₅} B'
inst✝⁴ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝³ : Category.{v₇, u₇} A''
inst✝² : Category.{v₈, u₈} B''
inst✝¹ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ e.inv.right ≫ e.hom.right = 𝟙 ψ'.right

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁸ : Category.{v₂, u₂} B
inst✝⁷ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁶ : Category.{v₄, u₄} A'
inst✝⁵ : Category.{v₅, u₅} B'
inst✝⁴ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝³ : Category.{v₇, u₇} A''
inst✝² : Category.{v₈, u₈} B''
inst✝¹ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ e.hom.base ≫ e.inv.base = 𝟙 ψ.base

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁸ : Category.{v₂, u₂} B
inst✝⁷ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁶ : Category.{v₄, u₄} A'
inst✝⁵ : Category.{v₅, u₅} B'
inst✝⁴ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝³ : Category.{v₇, u₇} A''
inst✝² : Category.{v₈, u₈} B''
inst✝¹ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ e.inv.base ≫ e.hom.base = 𝟙 ψ'.base

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝² : Category.{v₄, u₄} A'
inst✝¹ : Category.{v₅, u₅} B'
inst✝ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
h : IsIso f.left ∧ IsIso f.base ∧ IsIso f.right
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
inst✝ : HasWeakEqualizer f g
⊢ (Iso.refl (weakLimit.cone (parallelPair f g)).pt).hom ≫ (Fork.ofι (weakEqualizer.ι f g) ⋯).ι =
    Fork.ι (weakLimit.cone (parallelPair f g))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
⊢ ψ ◁ θ ≫ η ▷ φ' = η ▷ φ ≫ ψ' ◁ θ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
inst✝ : HasWeakEqualizer f g
t : Fork f g
lift : (s : Fork f g) → s.pt ⟶ t.pt
fac : ∀ (s : Fork f g), lift s ≫ t.ι = s.ι
s : Cone (parallelPair f g)
j : WalkingParallelPair
⊢ lift s ≫ t.π.app WalkingParallelPair.one = s.π.app WalkingParallelPair.one

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ : CatCospanTransform F G F' G'
φ : CatCospanTransform F' G' F'' G''
⊢ 𝟙 ψ ▷ φ = 𝟙 (ψ.comp φ)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝² : Category.{v₄, u₄} A'
inst✝¹ : Category.{v₅, u₅} B'
inst✝ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
⊢ η ▷ id F' G' = (ρ_ ψ).hom ≫ η ≫ (ρ_ ψ').inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' ψ'' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
η' : ψ' ⟶ ψ''
φ : CatCospanTransform F' G' F'' G''
⊢ (η ≫ η') ▷ φ = η ▷ φ ≫ η' ▷ φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝¹⁰ : Category.{v₂, u₂} B
inst✝⁹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁸ : Category.{v₄, u₄} A'
inst✝⁷ : Category.{v₅, u₅} B'
inst✝⁶ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝⁵ : Category.{v₇, u₇} A''
inst✝⁴ : Category.{v₈, u₈} B''
inst✝³ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
A''' : Type u₁₀
B''' : Type u₁₁
C''' : Type u₁₂
inst✝² : Category.{v₁₀, u₁₀} A'''
inst✝¹ : Category.{v₁₁, u₁₁} B'''
inst✝ : Category.{v₁₂, u₁₂} C'''
F''' : A''' ⥤ B'''
G''' : C''' ⥤ B'''
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
τ : CatCospanTransform F'' G'' F''' G'''
⊢ η ▷ φ.comp τ = (α_ ψ φ τ).inv ≫ η ▷ φ ▷ τ ≫ (α_ ψ' φ τ).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ : CatCospanTransform F G F' G'
φ : CatCospanTransform F' G' F'' G''
⊢ ψ ◁ 𝟙 φ = 𝟙 (ψ.comp φ)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.Basic

Goal state before:
pp: J : Type u_1
inst✝³ : Category.{v_1, u_1} J
K : Type u_2
inst✝² : Category.{v_2, u_2} K
C : Type u_3
inst✝¹ : Category.{v_3, u_3} C
F : J ⥤ C
D : Type u_4
inst✝ : Category.{v_4, u_4} D
G : K ⥤ D
t t' : Cone F
l : IsLimit t
l' : IsWeakLimit t'
x✝ : J
⊢ (l'.lift t ≫ l.lift t') ≫ t.π.app x✝ = 𝟙 t.pt ≫ t.π.app x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.Basic

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
K : Type u_2
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F✝ : J ⥤ C
D : Type u_4
inst✝¹ : Category.{v_4, u_4} D
G : K ⥤ D
F : J ⥤ C
inst✝ : HasWeakLimit F
j j' : J
hj : j = j'
⊢ F.obj j = F.obj j'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝² : Category.{v₄, u₄} A'
inst✝¹ : Category.{v₅, u₅} B'
inst✝ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
⊢ id F G ◁ η = (λ_ ψ).hom ≫ η ≫ (λ_ ψ').inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.Basic

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_3
inst✝¹ : Category.{v_3, u_3} C
F : J ⥤ C
inst✝ : HasWeakLimit F
j j' : J
hj : j = j'
⊢ π F j ≫ eqToHom ⋯ = π F j'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.Basic

Goal state before:
pp: J : Type u_1
inst✝³ : Category.{v_1, u_1} J
K : Type u_2
inst✝² : Category.{v_2, u_2} K
C : Type u_3
inst✝¹ : Category.{v_3, u_3} C
F : J ⥤ C
D : Type u_4
inst✝ : Category.{v_4, u_4} D
G : K ⥤ D
r t : Cone F
i : r ≅ t
x✝ : IsWeakLimit r
⊢ (fun h ↦ h.ofIsoWeakLimit i.symm) ((fun h ↦ h.ofIsoWeakLimit i) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.Basic

Goal state before:
pp: J : Type u_1
inst✝³ : Category.{v_1, u_1} J
K : Type u_2
inst✝² : Category.{v_2, u_2} K
C : Type u_3
inst✝¹ : Category.{v_3, u_3} C
F : J ⥤ C
D : Type u_4
inst✝ : Category.{v_4, u_4} D
G : K ⥤ D
r t : Cone F
i : r ≅ t
x✝ : IsWeakLimit t
⊢ (fun h ↦ h.ofIsoWeakLimit i) ((fun h ↦ h.ofIsoWeakLimit i.symm) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ : CatCospanTransform F G F' G'
φ φ' φ'' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
θ' : φ' ⟶ φ''
⊢ ψ ◁ (θ ≫ θ') = ψ ◁ θ ≫ ψ ◁ θ'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝¹⁰ : Category.{v₂, u₂} B
inst✝⁹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁸ : Category.{v₄, u₄} A'
inst✝⁷ : Category.{v₅, u₅} B'
inst✝⁶ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝⁵ : Category.{v₇, u₇} A''
inst✝⁴ : Category.{v₈, u₈} B''
inst✝³ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
A''' : Type u₁₀
B''' : Type u₁₁
C''' : Type u₁₂
inst✝² : Category.{v₁₀, u₁₀} A'''
inst✝¹ : Category.{v₁₁, u₁₁} B'''
inst✝ : Category.{v₁₂, u₁₂} C'''
F''' : A''' ⥤ B'''
G''' : C''' ⥤ B'''
ψ : CatCospanTransform F G F' G'
φ : CatCospanTransform F' G' F'' G''
τ τ' : CatCospanTransform F'' G'' F''' G'''
γ : τ ⟶ τ'
⊢ ψ.comp φ ◁ γ = (α_ ψ φ τ).hom ≫ ψ ◁ φ ◁ γ ≫ (α_ ψ φ τ').inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f g : X ⟶ Y
inst✝ : HasWeakKernel f
⊢ (Iso.refl (weakLimit.cone (parallelPair f 0)).pt).hom ≫ (Fork.ofι (weakKernel.ι f) ⋯).ι =
    Fork.ι (weakLimit.cone (parallelPair f 0))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝¹³ : Category.{v₂, u₂} B
inst✝¹² : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝¹¹ : Category.{v₄, u₄} A'
inst✝¹⁰ : Category.{v₅, u₅} B'
inst✝⁹ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝⁸ : Category.{v₇, u₇} A''
inst✝⁷ : Category.{v₈, u₈} B''
inst✝⁶ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
A''' : Type u₁₀
B''' : Type u₁₁
C''' : Type u₁₂
inst✝⁵ : Category.{v₁₀, u₁₀} A'''
inst✝⁴ : Category.{v₁₁, u₁₁} B'''
inst✝³ : Category.{v₁₂, u₁₂} C'''
F''' : A''' ⥤ B'''
G''' : C''' ⥤ B'''
ψ : CatCospanTransform F G F' G'
φ : CatCospanTransform F' G' F'' G''
τ : CatCospanTransform F'' G'' F''' G'''
A'''' : Type u₁₃
B'''' : Type u₁₄
C'''' : Type u₁₅
inst✝² : Category.{v₁₃, u₁₃} A''''
inst✝¹ : Category.{v₁₄, u₁₄} B''''
inst✝ : Category.{v₁₅, u₁₅} C''''
F'''' : A'''' ⥤ B''''
G'''' : C'''' ⥤ B''''
σ : CatCospanTransform F''' G''' F'''' G''''
⊢ (α_ ψ φ τ).hom ▷ σ ≫ (α_ ψ (φ.comp τ) σ).hom ≫ ψ ◁ (α_ φ τ σ).hom = (α_ (ψ.comp φ) τ σ).hom ≫ (α_ ψ φ (τ.comp σ)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ : CatCospanTransform F G F' G'
φ : CatCospanTransform F' G' F'' G''
⊢ (α_ ψ (id F' G') φ).hom ≫ ψ ◁ (λ_ φ).hom = (ρ_ ψ).hom ▷ φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasWeakPullback f g
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ lift h k ⋯ ≫ fst f g = h ∧ lift h k ⋯ ≫ snd f g = k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ : CatCospanTransform F G F' G'
φ : CatCospanTransform F' G' F'' G''
⊢ (α_ ψ (id F' G') φ).inv ≫ (ρ_ ψ).hom ▷ φ = ψ ◁ (λ_ φ).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝¹ : HasWeakPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝ : HasWeakPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ (fst f₁ f₂ ≫ i₁) ≫ g₁ = (snd f₁ f₂ ≫ i₂) ≫ g₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: 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✝¹² : Category.{v₂, u₂} B
inst✝¹¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝¹⁰ : Category.{v₄, u₄} A'
inst✝⁹ : Category.{v₅, u₅} B'
inst✝⁸ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝⁷ : Category.{v₇, u₇} A''
inst✝⁶ : Category.{v₈, u₈} B''
inst✝⁵ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
A''' : Type u₁₀
B''' : Type u₁₁
C''' : Type u₁₂
inst✝⁴ : Category.{v₁₀, u₁₀} A'''
inst✝³ : Category.{v₁₁, u₁₁} B'''
inst✝² : Category.{v₁₂, u₁₂} C'''
F''' : A''' ⥤ B'''
G''' : C''' ⥤ B'''
ψ✝ ψ'✝ ψ'' : CatCospanTransform F G F' G'
η✝ : ψ✝ ⟶ ψ'✝
η' : ψ'✝ ⟶ ψ''
φ✝ φ'✝ φ'' : CatCospanTransform F' G' F'' G''
θ✝ : φ✝ ⟶ φ'✝
θ' : φ'✝ ⟶ φ''
τ τ' : CatCospanTransform F'' G'' F''' G'''
γ : τ ⟶ τ'
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst✝¹ : IsIso η
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
inst✝ : IsIso θ
⊢ ψ ◁ θ ≫ ψ ◁ inv θ = 𝟙 (ψ.comp φ)

Tactic:
by

Goal state after: