awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
T : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
B : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T L R B
L' : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R' : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
inst_6 : w.GuitartExact
α : L ⟶ L'
β : R' ⟶ R
inst_7 : IsIso α
inst_8 : IsIso β
⊢ (w.whiskerVertical α β).GuitartExact

Tactic:
whiskerVertical w (asIso α) (asIso β).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.asIso, CategoryTheory.TwoSquare.GuitartExact.whiskerVertical
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
R₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
hw : w.GuitartExact
hw' : w'.GuitartExact
simp : ∀ (X₂ : D₁), ((w ≫ᵥ w').structuredArrowDownwards X₂).Initial
⊢ (w ≫ᵥ w').GuitartExact

Tactic:
simp only [TwoSquare.guitartExact_iff_initial]

Premises used: CategoryTheory.TwoSquare.guitartExact_iff_initial
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
R₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
hw : w.GuitartExact
hw' : w'.GuitartExact
Y₁ : D₁
rw : (w.structuredArrowDownwards Y₁ ⋙ w'.structuredArrowDownwards (R₁.obj Y₁)).Initial
⊢ ((w ≫ᵥ w').structuredArrowDownwards Y₁).Initial

Tactic:
rw [← Functor.initial_natIso_iff (structuredArrowDownwardsComp w w' Y₁)]

Premises used: CategoryTheory.Functor.initial_natIso_iff, CategoryTheory.TwoSquare.structuredArrowDownwardsComp
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
R₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
hw : w.GuitartExact
hw' : w'.GuitartExact
Y₁ : D₁
⊢ (w.structuredArrowDownwards Y₁ ⋙ w'.structuredArrowDownwards (R₁.obj Y₁)).Initial

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
R₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
inst_6 : w.GuitartExact
inst_7 : w'.GuitartExact
L₁₂ : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R₁₂ : Functor.{v_4, v_6, u_4, u_6} D₁ D₃
eL : L₁ ⋙ L₂ ≅ L₁₂
eR : R₁ ⋙ R₂ ≅ R₁₂
⊢ ((w ≫ᵥ w').whiskerVertical eL.hom eR.inv).GuitartExact

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
R₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
inst_6 : R₁.EssSurj
inst_7 : w.GuitartExact
inst_8 : (w ≫ᵥ w').GuitartExact
rw : ∀ (X₂ : D₂), (w'.structuredArrowDownwards X₂).Initial
⊢ w'.GuitartExact

Tactic:
rw [guitartExact_iff_initial]

Premises used: CategoryTheory.TwoSquare.guitartExact_iff_initial
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
R₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
inst_6 : R₁.EssSurj
inst_7 : w.GuitartExact
inst_8 : (w ≫ᵥ w').GuitartExact
Y₂ : D₂
rw :
  Functor.Initial (C := StructuredArrow (R₁.obj (R₁.objPreimage Y₂)) H₂)
    (w'.structuredArrowDownwards (R₁.obj (R₁.objPreimage Y₂)))
⊢ (w'.structuredArrowDownwards Y₂).Initial

Tactic:
rw [structuredArrowDownwards_initial_iff_of_iso _ (R₁.objObjPreimageIso Y₂).symm]

Premises used: CategoryTheory.TwoSquare.structuredArrowDownwards_initial_iff_of_iso, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
R₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
inst_6 : R₁.EssSurj
inst_7 : w.GuitartExact
inst_8 : (w ≫ᵥ w').GuitartExact
Y₂ : D₂
⊢ Functor.Initial (C := StructuredArrow (R₁.objPreimage Y₂) H₁)
    (w.structuredArrowDownwards (R₁.objPreimage Y₂) ⋙ w'.structuredArrowDownwards (R₁.obj (R₁.objPreimage Y₂)))

Tactic:
have := Functor.initial_of_natIso (structuredArrowDownwardsComp w w' (R₁.objPreimage Y₂)).symm
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
R₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
inst_6 : R₁.EssSurj
inst_7 : w.GuitartExact
inst_8 : (w ≫ᵥ w').GuitartExact
Y₂ : D₂
this :
  Functor.Initial (C := StructuredArrow (R₁.objPreimage Y₂) H₁)
    (w.structuredArrowDownwards (R₁.objPreimage Y₂) ⋙ w'.structuredArrowDownwards (R₁.obj (R₁.objPreimage Y₂)))
⊢ Functor.Initial (C := StructuredArrow (R₁.obj (R₁.objPreimage Y₂)) H₂)
    (w'.structuredArrowDownwards (R₁.obj (R₁.objPreimage Y₂)))

Tactic:
Functor.initial_of_initial_comp (w.structuredArrowDownwards (R₁.objPreimage Y₂)) _

Premises used: CategoryTheory.Functor.objPreimage, CategoryTheory.TwoSquare.structuredArrowDownwards, CategoryTheory.Functor.initial_of_initial_comp
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
R₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
inst_6 : R₁.EssSurj
inst_7 : w.GuitartExact
inst_8 : (w ≫ᵥ w').GuitartExact
Y₂ : D₂
this :
  Functor.Initial (C := StructuredArrow (R₁.objPreimage Y₂) H₁)
    (w.structuredArrowDownwards (R₁.objPreimage Y₂) ⋙ w'.structuredArrowDownwards (R₁.obj (R₁.objPreimage Y₂)))
⊢ Functor.Initial (C := StructuredArrow (R₁.obj (R₁.objPreimage Y₂)) H₂)
    (w'.structuredArrowDownwards (R₁.obj (R₁.objPreimage Y₂)))

Tactic:
exact Functor.initial_of_initial_comp (w.structuredArrowDownwards (R₁.objPreimage Y₂)) _

Premises used: CategoryTheory.Functor.objPreimage, CategoryTheory.TwoSquare.structuredArrowDownwards, CategoryTheory.Functor.initial_of_initial_comp
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
R₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
L₁₂ : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R₁₂ : Functor.{v_4, v_6, u_4, u_6} D₁ D₃
eL : L₁ ⋙ L₂ ≅ L₁₂
eR : R₁ ⋙ R₂ ≅ R₁₂
inst_6 : R₁.EssSurj
inst_7 : w.GuitartExact
h : ((w ≫ᵥ w').whiskerVertical eL.hom eR.inv).GuitartExact
⊢ (w ≫ᵥ w').GuitartExact

Tactic:
rw [whiskerVertical_iff] at h

Premises used: CategoryTheory.TwoSquare.GuitartExact.whiskerVertical_iff
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
R₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
L₁₂ : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R₁₂ : Functor.{v_4, v_6, u_4, u_6} D₁ D₃
eL : L₁ ⋙ L₂ ≅ L₁₂
eR : R₁ ⋙ R₂ ≅ R₁₂
inst_6 : R₁.EssSurj
inst_7 : w.GuitartExact
h : (w ≫ᵥ w').GuitartExact
⊢ w'.GuitartExact

Tactic:
of_vComp w w'

Premises used: CategoryTheory.TwoSquare.GuitartExact.of_vComp
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
R₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
L₁₂ : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R₁₂ : Functor.{v_4, v_6, u_4, u_6} D₁ D₃
eL : L₁ ⋙ L₂ ≅ L₁₂
eR : R₁ ⋙ R₂ ≅ R₁₂
inst_6 : R₁.EssSurj
inst_7 : w.GuitartExact
h : (w ≫ᵥ w').GuitartExact
⊢ w'.GuitartExact

Tactic:
exact of_vComp w w'

Premises used: CategoryTheory.TwoSquare.GuitartExact.of_vComp
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
R₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
inst_6 : R₁.EssSurj
inst_7 : w.GuitartExact
⊢ (w ≫ᵥ w').GuitartExact ↔ w'.GuitartExact

Tactic:
⟨fun _ ↦ of_vComp w w', fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.TwoSquare.GuitartExact.of_vComp, Iff.intro
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
R₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare H₂ L₂ R₂ H₃
L₁₂ : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R₁₂ : Functor.{v_4, v_6, u_4, u_6} D₁ D₃
eL : L₁ ⋙ L₂ ≅ L₁₂
eR : R₁ ⋙ R₂ ≅ R₁₂
inst_6 : R₁.EssSurj
inst_7 : w.GuitartExact
⊢ (w.vComp' w' eL eR).GuitartExact ↔ w'.GuitartExact

Tactic:
⟨fun _ ↦ of_vComp' w w' eL eR, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.TwoSquare.GuitartExact.of_vComp'
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eL : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eR : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
mp : (w ≫ᵥ w'.hom).GuitartExact → w.GuitartExact
mpr : w.GuitartExact → (w ≫ᵥ w'.hom).GuitartExact
⊢ (w ≫ᵥ w'.hom).GuitartExact ↔ w.GuitartExact

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eL : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eR : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
⊢ CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'

Tactic:
have hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w' := rfl
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eL : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eR : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this_1 : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ :=
  (CatCommSq.vInvEquiv H₂ eL eR H₃ :
      (a : CatCommSq H₂ eL.functor eR.functor H₃) → CatCommSq H₃ eL.inverse eR.inverse H₂)
    inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ L₁.isoWhiskerLeft eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ R₁.isoWhiskerLeft eR.unitIso.symm ≪≫ R₁.rightUnitor
h : ∀ (X₁ : C₁), w.natTrans.app X₁ = ((w ≫ᵥ w'.hom).vComp' w''.hom α β).natTrans.app X₁
⊢ w = (w ≫ᵥ w'.hom).vComp' w''.hom α β

Tactic:
ext X₁
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eL : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eR : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this_1 : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ :=
  (CatCommSq.vInvEquiv H₂ eL eR H₃ :
      (a : CatCommSq H₂ eL.functor eR.functor H₃) → CatCommSq H₃ eL.inverse eR.inverse H₂)
    inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ L₁.isoWhiskerLeft eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ R₁.isoWhiskerLeft eR.unitIso.symm ≪≫ R₁.rightUnitor
X₁ : C₁
h :
  w.natTrans.app X₁ =
    w.natTrans.app X₁ ≫
      eR.unit.app (H₂.obj (L₁.obj X₁)) ≫
        eR.inverse.map
            ((natTrans w'.hom).app (L₁.obj X₁) ≫
              H₃.map (eL.counitIso.inv.app (eL.functor.obj (L₁.obj X₁))) ≫
                w'.inv.app (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
          eR.unitIso.inv.app (H₂.obj (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
            H₂.map (eL.unitIso.inv.app (L₁.obj X₁))
⊢ w.natTrans.app X₁ =
    w.natTrans.app X₁ ≫
      eR.unit.app (H₂.obj (L₁.obj X₁)) ≫
        eR.inverse.map ((natTrans w'.hom).app (L₁.obj X₁)) ≫
          eR.inverse.map (H₃.map (eL.counitIso.inv.app (eL.functor.obj (L₁.obj X₁)))) ≫
            eR.inverse.map
                ((CatCommSq.iso H₂ eL.functor eR.functor H₃).inv.app (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
              eR.unitIso.inv.app (H₂.obj (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
                H₂.map (eL.unitIso.inv.app (L₁.obj X₁))

Tactic:
simp only [hw', ← eR.inverse.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eL : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eR : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this_1 : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ :=
  (CatCommSq.vInvEquiv H₂ eL eR H₃ :
      (a : CatCommSq H₂ eL.functor eR.functor H₃) → CatCommSq H₃ eL.inverse eR.inverse H₂)
    inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ L₁.isoWhiskerLeft eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ R₁.isoWhiskerLeft eR.unitIso.symm ≪≫ R₁.rightUnitor
X₁ : C₁
h :
  w.natTrans.app X₁ =
    w.natTrans.app X₁ ≫
      eR.unit.app (H₂.obj (L₁.obj X₁)) ≫
        eR.inverse.map
            ((H₂ ⋙ eR.functor).map (eL.unit.app (L₁.obj X₁)) ≫
              (natTrans w'.hom).app ((eL.functor ⋙ eL.inverse).obj (L₁.obj X₁)) ≫
                w'.inv.app (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
          eR.unitIso.inv.app (H₂.obj (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
            H₂.map (eL.unitIso.inv.app (L₁.obj X₁))
⊢ w.natTrans.app X₁ =
    w.natTrans.app X₁ ≫
      eR.unit.app (H₂.obj (L₁.obj X₁)) ≫
        eR.inverse.map
            ((natTrans w'.hom).app (L₁.obj X₁) ≫
              H₃.map (eL.counitIso.inv.app (eL.functor.obj (L₁.obj X₁))) ≫
                w'.inv.app (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
          eR.unitIso.inv.app (H₂.obj (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
            H₂.map (eL.unitIso.inv.app (L₁.obj X₁))

Tactic:
rw [Equivalence.counitInv_app_functor, ← Functor.comp_map, ← NatTrans.naturality_assoc]

Premises used: CategoryTheory.Equivalence.counitInv_app_functor, CategoryTheory.Functor.comp_map, CategoryTheory.NatTrans.naturality_assoc