awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
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₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
T₁₂ : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
B₁₂ : Functor.{v_4, v_6, u_4, u_6} D₁ D₃
eT : T₁ ⋙ T₂ ≅ T₁₂
eB : B₁ ⋙ B₂ ≅ B₁₂
inst_6 : B₁.EssSurj
inst_7 : w.GuitartExact
h : ((w ≫ₕ w').whiskerHorizontal eT.inv eB.hom).GuitartExact
⊢ (w ≫ₕ w').GuitartExact

Tactic:
rw [whiskerHorizontal_iff] at h

Premises used: CategoryTheory.TwoSquare.GuitartExact.whiskerHorizontal_iff
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
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₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
T₁₂ : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
B₁₂ : Functor.{v_4, v_6, u_4, u_6} D₁ D₃
eT : T₁ ⋙ T₂ ≅ T₁₂
eB : B₁ ⋙ B₂ ≅ B₁₂
inst_6 : B₁.EssSurj
inst_7 : w.GuitartExact
h : (w ≫ₕ w').GuitartExact
⊢ w'.GuitartExact

Tactic:
of_hComp w w'

Premises used: CategoryTheory.TwoSquare.GuitartExact.of_hComp
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
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₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
T₁₂ : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
B₁₂ : Functor.{v_4, v_6, u_4, u_6} D₁ D₃
eT : T₁ ⋙ T₂ ≅ T₁₂
eB : B₁ ⋙ B₂ ≅ B₁₂
inst_6 : B₁.EssSurj
inst_7 : w.GuitartExact
h : (w ≫ₕ w').GuitartExact
⊢ w'.GuitartExact

Tactic:
exact of_hComp w w'

Premises used: CategoryTheory.TwoSquare.GuitartExact.of_hComp
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
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₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst_6 : B₁.EssSurj
inst_7 : w.GuitartExact
⊢ (w ≫ₕ w').GuitartExact ↔ w'.GuitartExact

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

Premises used: CategoryTheory.TwoSquare.GuitartExact.of_hComp, inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
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₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
B₂ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
T₁₂ : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
B₁₂ : Functor.{v_4, v_6, u_4, u_6} D₁ D₃
eT : T₁ ⋙ T₂ ≅ T₁₂
eB : B₁ ⋙ B₂ ≅ B₁₂
inst_6 : B₁.EssSurj
inst_7 : w.GuitartExact
⊢ (w.hComp' w' eT eB).GuitartExact ↔ w'.GuitartExact

Tactic:
⟨fun _ ↦ of_hComp' w w' eT eB, fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.TwoSquare.GuitartExact.of_hComp', Iff.intro
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
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₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eT : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eB : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
w'' : V₂.op ⋙ eB.op.functor ≅ eT.op.functor ⋙ V₃.op := NatIso.op w'
h : ∀ (X : C₁ᵒᵖ), (w ≫ₕ w'.hom).op.natTrans.app X = (w.op ≫ᵥ w''.hom).natTrans.app X
⊢ (w ≫ₕ w'.hom).op = w.op ≫ᵥ w''.hom

Tactic:
ext
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
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₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eT : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eB : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
w'' : V₂.op ⋙ eB.op.functor ≅ eT.op.functor ⋙ V₃.op := NatIso.op w'
X : C₁ᵒᵖ
⊢ (w ≫ₕ w'.hom).op.natTrans.app X = (w.op ≫ᵥ w''.hom).natTrans.app X

Tactic:
simp [w'']
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
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₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eT : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eB : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
w'' : V₂.op ⋙ eB.op.functor ≅ eT.op.functor ⋙ V₃.op := NatIso.op w'
⊢ (w ≫ₕ w'.hom).op = w.op ≫ᵥ w''.hom

Tactic:
have : (w ≫ₕ w'.hom).op = (w.op ≫ᵥ w''.hom) := by ext; simp [w'']
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
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₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eT : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eB : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
w'' : V₂.op ⋙ eB.op.functor ≅ eT.op.functor ⋙ V₃.op := NatIso.op w'
this : (w ≫ₕ w'.hom).op = w.op ≫ᵥ w''.hom
rw : (w.op ≫ᵥ w''.hom).GuitartExact ↔ (w.op ≫ᵥ w''.hom).GuitartExact
⊢ (w ≫ₕ w'.hom).GuitartExact ↔ w.GuitartExact

Tactic:
rw [← guitartExact_op_iff, ← guitartExact_op_iff w,
    ← vComp_iff_of_equivalences _ _ _ w'', this]

Premises used: CategoryTheory.TwoSquare.GuitartExact.vComp_iff_of_equivalences, CategoryTheory.TwoSquare.guitartExact_op_iff
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
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₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eT : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eB : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
w'' : V₂.op ⋙ eB.op.functor ≅ eT.op.functor ⋙ V₃.op := NatIso.op w'
this : (w ≫ₕ w'.hom).op = w.op ≫ᵥ w''.hom
⊢ (w.op ≫ᵥ w''.hom).GuitartExact ↔ (w.op ≫ᵥ w''.hom).GuitartExact

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
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₃
V₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
T₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
B₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
V₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
E : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
E' : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : E.functor ⋙ V₃ ≅ V₂ ⋙ E'.functor
T₁₂ : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
B₁₂ : Functor.{v_4, v_6, u_4, u_6} D₁ D₃
eT : T₁ ⋙ E.functor ≅ T₁₂
eB : B₁ ⋙ E'.functor ≅ B₁₂
rw : (w.hComp' w'.hom eT eB).GuitartExact ↔ (w ≫ₕ w'.hom).GuitartExact
rw₁ : ((w ≫ₕ w'.hom).whiskerHorizontal eT.inv eB.hom).GuitartExact ↔ (w ≫ₕ w'.hom).GuitartExact
rw₂ rw₃ : (w ≫ₕ w'.hom).GuitartExact ↔ (w ≫ₕ w'.hom).GuitartExact
⊢ (w.hComp' w'.hom eT eB).GuitartExact ↔ w.GuitartExact

Tactic:
rw [← hComp_iff_of_equivalences w E E' w', TwoSquare.hComp', whiskerHorizontal_iff]

Premises used: CategoryTheory.TwoSquare.GuitartExact.hComp_iff_of_equivalences, CategoryTheory.TwoSquare.hComp', CategoryTheory.TwoSquare.GuitartExact.whiskerHorizontal_iff
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
E : R.LeftExtension F
w : TwoSquare T L R B
X₃ : C₃
inst_5 : (w.costructuredArrowRightwards X₃).Final
refine :
  (E.compTwoSquare w).IsPointwiseLeftKanExtensionAt X₃ ≃
    IsColimit (Cocone.whisker (w.costructuredArrowRightwards X₃) (E.coconeAt (B.obj X₃)))
⊢ (E.compTwoSquare w).IsPointwiseLeftKanExtensionAt X₃ ≃ E.IsPointwiseLeftKanExtensionAt (B.obj X₃)

Tactic:
refine Equiv.trans ?_ (Final.isColimitWhiskerEquiv (w.costructuredArrowRightwards X₃) _)

Premises used: Equiv.trans, CategoryTheory.Functor.Final.isColimitWhiskerEquiv, CategoryTheory.TwoSquare.costructuredArrowRightwards
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
E : R.LeftExtension F
w : TwoSquare T L R B
X₃ : C₃
inst_5 : (w.costructuredArrowRightwards X₃).Final
⊢ (E.compTwoSquare w).IsPointwiseLeftKanExtensionAt X₃ ≃
    IsColimit (Cocone.whisker (w.costructuredArrowRightwards X₃) (E.coconeAt (B.obj X₃)))

Tactic:
exact IsColimit.equivIsoColimit (Cocone.ext (Iso.refl _))

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.IsColimit.equivIsoColimit, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
E : R.LeftExtension F
w : TwoSquare T L R B
X₃ : C₃
inst_5 : (w.costructuredArrowRightwards X₃).Final
⊢ Nonempty ((E.compTwoSquare w).IsPointwiseLeftKanExtensionAt X₃) ↔
    Nonempty (E.IsPointwiseLeftKanExtensionAt (B.obj X₃))

Tactic:
(E.isPointwiseLeftKanExtensionAtCompTwoSquareEquiv w _).nonempty_congr

Premises used: CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtCompTwoSquareEquiv, Equiv.nonempty_congr
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
E : R.LeftExtension F
w : TwoSquare T L R B
inst_5 : w.GuitartExact
inst_6 : B.EssSurj
x : (E.compTwoSquare w).IsPointwiseLeftKanExtension
⊢ (fun (h : E.IsPointwiseLeftKanExtension) ↦ h.compTwoSquare w)
      ((fun (h : (E.compTwoSquare w).IsPointwiseLeftKanExtension) ↦ E.isPointwiseLeftKanExtensionOfCompTwoSquare w h)
        x) =
    x

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
E : R.LeftExtension F
w : TwoSquare T L R B
inst_5 : w.GuitartExact
inst_6 : B.EssSurj
x : E.IsPointwiseLeftKanExtension
⊢ (fun (h : (E.compTwoSquare w).IsPointwiseLeftKanExtension) ↦ E.isPointwiseLeftKanExtensionOfCompTwoSquare w h)
      ((fun (h : E.IsPointwiseLeftKanExtension) ↦ h.compTwoSquare w) x) =
    x

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
X₃ : C₃
inst_5 : (w.costructuredArrowRightwards X₃).Final
rw :
  HasColimit (CostructuredArrow.proj L X₃ ⋙ T ⋙ F) ↔
    HasColimit (w.costructuredArrowRightwards X₃ ⋙ CostructuredArrow.proj R (B.obj X₃) ⋙ F)
⊢ HasColimit (CostructuredArrow.proj L X₃ ⋙ T ⋙ F) ↔
    HasColimit (J := CostructuredArrow R (B.obj X₃)) (CostructuredArrow.proj R (B.obj X₃) ⋙ F)

Tactic:
rw [← Functor.Final.hasColimit_comp_iff (w.costructuredArrowRightwards X₃)]

Premises used: CategoryTheory.Functor.Final.hasColimit_comp_iff, CategoryTheory.TwoSquare.costructuredArrowRightwards
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
X₃ : C₃
inst_5 : (w.costructuredArrowRightwards X₃).Final
⊢ HasColimit (CostructuredArrow.proj L X₃ ⋙ T ⋙ F) ↔
    HasColimit (w.costructuredArrowRightwards X₃ ⋙ CostructuredArrow.proj R (B.obj X₃) ⋙ F)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : w.GuitartExact
inst_6 : B.EssSurj
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
simp : (∀ (Y : C₃), R.HasPointwiseLeftKanExtensionAt F (B.obj Y)) ↔ ∀ (Y : C₄), R.HasPointwiseLeftKanExtensionAt F Y
⊢ (∀ (Y : C₃), L.HasPointwiseLeftKanExtensionAt (T ⋙ F) Y) ↔ ∀ (Y : C₄), R.HasPointwiseLeftKanExtensionAt F Y

Tactic:
simp only [hasPointwiseLeftKanExtensionAt_iff w]

Premises used: CategoryTheory.TwoSquare.hasPointwiseLeftKanExtensionAt_iff
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : w.GuitartExact
inst_6 : B.EssSurj
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
⊢ (∀ (Y : C₃), R.HasPointwiseLeftKanExtensionAt F (B.obj Y)) ↔ ∀ (Y : C₄), R.HasPointwiseLeftKanExtensionAt F Y

Tactic:
⟨fun h X₄ ↦ ?_, fun h _ ↦ h _⟩

Premises used: Iff.intro, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : w.GuitartExact
inst_6 : B.EssSurj
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
refine :
  ∀ (h : ∀ (Y : C₃), R.HasPointwiseLeftKanExtensionAt F (B.obj Y)) (X₄ : C₄), R.HasPointwiseLeftKanExtensionAt F X₄
⊢ (∀ (Y : C₃), R.HasPointwiseLeftKanExtensionAt F (B.obj Y)) ↔ ∀ (Y : C₄), R.HasPointwiseLeftKanExtensionAt F Y

Tactic:
refine ⟨fun h X₄ ↦ ?_, fun h _ ↦ h _⟩
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : w.GuitartExact
inst_6 : B.EssSurj
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
h : ∀ (Y : C₃), R.HasPointwiseLeftKanExtensionAt F (B.obj Y)
X₄ : C₄
rw : R.HasPointwiseLeftKanExtensionAt F (B.obj (B.objPreimage X₄))
⊢ R.HasPointwiseLeftKanExtensionAt F X₄

Tactic:
rw [← Functor.hasPointwiseLeftKanExtensionAt_iff_of_iso _ _ (B.objObjPreimageIso X₄)]

Premises used: CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_iso
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : w.GuitartExact
inst_6 : B.EssSurj
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
h : ∀ (Y : C₃), R.HasPointwiseLeftKanExtensionAt F (B.obj Y)
X₄ : C₄
⊢ R.HasPointwiseLeftKanExtensionAt F (B.obj (B.objPreimage X₄))

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : w.GuitartExact
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
inst_6 : R.HasPointwiseLeftKanExtension F
⊢ L.HasPointwiseLeftKanExtension (T ⋙ F)

Tactic:
((R.pointwiseLeftKanExtensionIsPointwiseLeftKanExtension
    F).compTwoSquare w).hasPointwiseLeftKanExtension

Premises used: CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hasPointwiseLeftKanExtension, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.compTwoSquare, CategoryTheory.Functor.pointwiseLeftKanExtensionIsPointwiseLeftKanExtension
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : w.GuitartExact
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
inst_6 : R.HasPointwiseLeftKanExtension F
⊢ L.HasPointwiseLeftKanExtension (T ⋙ F)

Tactic:
have := w.hasPointwiseLeftKanExtension F
-- Module: Mathlib.CategoryTheory.GuitartExact.KanExtension
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
inst_4 : Category.{v₅, u₅} D
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
inst_5 : w.GuitartExact
F : Functor.{v₂, v₅, u₂, u₅} C₂ D
inst_6 : R.HasPointwiseLeftKanExtension F
this : L.HasPointwiseLeftKanExtension (T ⋙ F)
⊢ L.HasLeftKanExtension (T ⋙ F)

Tactic:
infer_instance