awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : 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₄
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_4 : L.IsEquivalence
inst_5 : R.IsEquivalence
inst_6 : IsIso w.natTrans
X₂ : C₂
this_1 : (StructuredArrow.post X₂ T R).IsEquivalence
this :
  Functor.IsEquivalence (C := Comma (Functor.fromPUnit (R.obj X₂)) (T ⋙ R))
    (Comma.mapRight (Functor.fromPUnit (R.obj X₂)) w)
⊢ (w.structuredArrowDownwards X₂).Initial
have this₁ : (StructuredArrow.pre (R.obj X₂) L B).IsEquivalence
Tactic: have := StructuredArrow.isEquivalence_pre (R.obj X₂) L B
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : 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₄
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₁ C₂
⊢ GuitartExact (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F))
have rw : ∀ {X₂ : C₁} {X₃ : C₂} (g : F.obj X₂ ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 C₂) X₃),
  IsConnected (StructuredArrowRightwards (T := 𝟭 C₁) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) g)
Tactic: rw [guitartExact_iff_isConnected_rightwards]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : 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₄
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₁ C₂
X₂ : C₁
X₃ : C₂
⊢ ∀ (g : F.obj X₂ ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 C₂) X₃),
    IsConnected (StructuredArrowRightwards (T := 𝟭 C₁) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) g)
have X₄ : ∀ (g : F.obj X₂ ⟶ X₃),
  IsConnected (StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g)
Tactic: (g : F.obj X₂ ⟶ X₃)
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : 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₄
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₁ C₂
X₂ : C₁
X₃ : C₂
g : F.obj X₂ ⟶ X₃
Z : Type (max (max u₁ v₂) v₁) :=
  StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g
X₀ : Z := StructuredArrow.mk (CostructuredArrow.homMk (𝟙 (CostructuredArrow.mk g).left) ⋯)
⊢ IsConnected (StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g)
have have : ∀ (φ : (X : Z) → X₀ ⟶ X),
  IsConnected (StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g)
Tactic: have φ : ∀ (X : Z), X₀ ⟶ X := fun X =>
    StructuredArrow.homMk (CostructuredArrow.homMk X.hom.left
      (by simpa using CostructuredArrow.w X.hom))
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (hypothesis)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : 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₄
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₁ C₂
X₂ : C₁
X₃ : C₂
g : F.obj X₂ ⟶ X₃
Z : Type (max (max u₁ v₂) v₁) :=
  StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g
X₀ : Z := StructuredArrow.mk (CostructuredArrow.homMk (𝟙 (CostructuredArrow.mk g).left) ⋯)
φ : (X : Z) → X₀ ⟶ X
⊢ IsConnected (StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g)
have this : Nonempty Z
Tactic: have : Nonempty Z := ⟨X₀⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : 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₄
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₁ C₂
X₂ : C₁
X₃ : C₂
g : F.obj X₂ ⟶ X₃
Z : Type (max (max u₁ v₂) v₁) :=
  StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g
X₀ : Z := StructuredArrow.mk (CostructuredArrow.homMk (𝟙 (CostructuredArrow.mk g).left) ⋯)
φ : (X : Z) → X₀ ⟶ X
this : Nonempty Z
⊢ IsConnected (StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g)
have h : ∀ (j₁ j₂ : StructuredArrowRightwards (T := 𝟭 C₁) (B := 𝟭 C₂) (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)) (X₂ := X₂) (X₃ := X₃) g),
  Zigzag j₁ j₂
Tactic: apply zigzag_isConnected
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₁
inst_3 : Category.{v_5, u_5} 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
T' : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
B' : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
inst_4 : w.GuitartExact
α : T ≅ T'
β : B ≅ B'
⊢ (w.whiskerHorizontal α.inv β.hom).GuitartExact
have rw : ∀ (X₃ : C₂), ((w.whiskerHorizontal α.inv β.hom).costructuredArrowRightwards X₃).Final
Tactic: rw [guitartExact_iff_final]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₁
inst_3 : Category.{v_5, u_5} 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
T' : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
B' : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
inst_4 : w.GuitartExact
α : T ≅ T'
β : B ≅ B'
X₂ : C₂
e : (w.whiskerHorizontal α.inv β.hom).costructuredArrowRightwards X₂ ≅
  w.costructuredArrowRightwards X₂ ⋙ Equivalence.functor (CostructuredArrow.mapIso (β.app X₂)) :=
  NatIso.ofComponents (fun (f : CostructuredArrow L X₂) ↦ CostructuredArrow.isoMk (α.symm.app f.left) ⋯) ⋯
⊢ ((w.whiskerHorizontal α.inv β.hom).costructuredArrowRightwards X₂).Final
have rw : (w.costructuredArrowRightwards X₂ ⋙ Equivalence.functor (CostructuredArrow.mapIso (β.app X₂))).Final
Tactic: rw [Functor.final_natIso_iff e]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₁
inst_3 : Category.{v_5, u_5} 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
T' : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
B' : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
α : T ≅ T'
β : B ≅ B'
⊢ (w.whiskerHorizontal α.inv β.hom).GuitartExact ↔ w.GuitartExact
have rw : (w.whiskerHorizontal α.inv β.hom).op.GuitartExact ↔
  (w.op.whiskerVertical (NatIso.op α.symm).hom (NatIso.op β.symm).inv).GuitartExact
Tactic: rw [← guitartExact_op_iff, ← w.guitartExact_op_iff,
    ← whiskerVertical_iff w.op (NatIso.op α.symm) (NatIso.op β.symm)]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (goal)
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 : w.GuitartExact
inst_7 : w'.GuitartExact
⊢ (w ≫ₕ w').GuitartExact
have rw : (w ≫ₕ w').op.GuitartExact
Tactic: rw [← guitartExact_op_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (goal)
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 : w.GuitartExact
inst_7 : w'.GuitartExact
⊢ (w ≫ₕ w').op = w.op ≫ᵥ w'.op
have h : ∀ (X : C₁ᵒᵖ), (w ≫ₕ w').op.natTrans.app X = (w.op ≫ᵥ w'.op).natTrans.app X
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (hypothesis)
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 : w.GuitartExact
inst_7 : w'.GuitartExact
⊢ (w ≫ₕ w').op.GuitartExact
have this : (w ≫ₕ w').op = w.op ≫ᵥ w'.op
Tactic: have : (w ≫ₕ w').op = w.op ≫ᵥ w'.op := by ext; simp
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (goal)
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 : w.GuitartExact
inst_7 : w'.GuitartExact
this : (w ≫ₕ w').op = w.op ≫ᵥ w'.op
⊢ (w ≫ₕ w').op.GuitartExact
have rw : (w.op ≫ᵥ w'.op).GuitartExact
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (goal)
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
inst_8 : (w ≫ₕ w').GuitartExact
⊢ w'.GuitartExact
have rw : ∀ (X₃ : D₂), (w'.costructuredArrowRightwards X₃).Final
Tactic: rw [guitartExact_iff_final]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (goal)
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
inst_8 : (w ≫ₕ w').GuitartExact
Y₂ : D₂
⊢ (w'.costructuredArrowRightwards Y₂).Final
have rw : Functor.Final (C := CostructuredArrow V₂ (B₁.obj (B₁.objPreimage Y₂)))
  (w'.costructuredArrowRightwards (B₁.obj (B₁.objPreimage Y₂)))
Tactic: rw [costructuredArrowRightwards_final_iff_of_iso _ (B₁.objObjPreimageIso Y₂).symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (hypothesis)
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
inst_8 : (w ≫ₕ w').GuitartExact
Y₂ : D₂
⊢ Functor.Final (C := CostructuredArrow V₂ (B₁.obj (B₁.objPreimage Y₂)))
    (w'.costructuredArrowRightwards (B₁.obj (B₁.objPreimage Y₂)))
have this : Functor.Final (C := CostructuredArrow V₁ (B₁.objPreimage Y₂))
  (w.costructuredArrowRightwards (B₁.objPreimage Y₂) ⋙ w'.costructuredArrowRightwards (B₁.obj (B₁.objPreimage Y₂)))
Tactic: have : (w.costructuredArrowRightwards (B₁.objPreimage Y₂) ⋙
      w'.costructuredArrowRightwards (B₁.obj (B₁.objPreimage Y₂))).Final :=
    (Functor.final_of_natIso (costructuredArrowRightwardsComp w w' _).symm :)
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (hypothesis)
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'.GuitartExact
have h₁ : (w ≫ₕ w').GuitartExact
Tactic: rw [whiskerHorizontal_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (goal)
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
have h : ∀ (X : C₁ᵒᵖ), (w ≫ₕ w'.hom).op.natTrans.app X = (w.op ≫ᵥ w''.hom).natTrans.app X
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (hypothesis)
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).GuitartExact ↔ w.GuitartExact
have this : (w ≫ₕ w'.hom).op = w.op ≫ᵥ w''.hom
Tactic: have : (w ≫ₕ w'.hom).op = (w.op ≫ᵥ w''.hom) := by ext; simp [w'']
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (goal)
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 ≫ₕ w'.hom).GuitartExact ↔ w.GuitartExact
have rw : (w.op ≫ᵥ w''.hom).GuitartExact ↔ (w.op ≫ᵥ w''.hom).GuitartExact
Tactic: rw [← guitartExact_op_iff, ← guitartExact_op_iff w,
    ← vComp_iff_of_equivalences _ _ _ w'', this]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (goal)
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₁₂
⊢ (w.hComp' w'.hom eT eB).GuitartExact ↔ w.GuitartExact
have rw : (w.hComp' w'.hom eT eB).GuitartExact ↔ (w ≫ₕ w'.hom).GuitartExact
Tactic: rw [← hComp_iff_of_equivalences w E E' w', TwoSquare.hComp', whiskerHorizontal_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (goal)
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
⊢ (w.hComp' w'.hom eT eB).GuitartExact ↔ w.GuitartExact
have rw₁ : ((w ≫ₕ w'.hom).whiskerHorizontal eT.inv eB.hom).GuitartExact ↔ (w ≫ₕ w'.hom).GuitartExact
Tactic: rw [← hComp_iff_of_equivalences w E E' w', TwoSquare.hComp', whiskerHorizontal_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (goal)
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
⊢ (w.hComp' w'.hom eT eB).GuitartExact ↔ w.GuitartExact
have rw₂ : (w ≫ₕ w'.hom).GuitartExact ↔ (w ≫ₕ w'.hom).GuitartExact
Tactic: rw [← hComp_iff_of_equivalences w E E' w', TwoSquare.hComp', whiskerHorizontal_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.KanExtension (goal)
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₃ ≃ E.IsPointwiseLeftKanExtensionAt (B.obj X₃)
have refine : (E.compTwoSquare w).IsPointwiseLeftKanExtensionAt X₃ ≃
  IsColimit (Cocone.whisker (w.costructuredArrowRightwards X₃) (E.coconeAt (B.obj X₃)))
Tactic: refine Equiv.trans ?_ (Final.isColimitWhiskerEquiv (w.costructuredArrowRightwards X₃) _)
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.KanExtension (goal)
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 (J := CostructuredArrow R (B.obj X₃)) (CostructuredArrow.proj R (B.obj X₃) ⋙ F)
have rw : HasColimit (CostructuredArrow.proj L X₃ ⋙ T ⋙ F) ↔
  HasColimit (w.costructuredArrowRightwards X₃ ⋙ CostructuredArrow.proj R (B.obj X₃) ⋙ F)
Tactic: rw [← Functor.Final.hasColimit_comp_iff (w.costructuredArrowRightwards X₃)]