awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (α.Y' (W := W))
T₃ : Triangle.{v_1, u_1} C := Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h
hT₃ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₃
hβγσ : W (β.s (W := W) ≫ γ.s (W := W) ≫ σ)
ψ₃ : T₂.obj₃ ⟶ T₃.obj₃
hψ₃ : W ψ₃
hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ≫ T₃.mor₂
hψ₂ : T₂.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (α.s (W := W)) = ψ₃ ≫ T₃.mor₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ (α.s (W := W)) (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (C := Triangle.{v_2, u_2} D) (X := Functor.obj L.mapTriangle T₂) (Functor.map L.mapTriangle ψ)
⊢ Eq (α := Triangle.obj₂ (Functor.obj L.mapTriangle T₁) ⟶ Triangle.obj₂ (Functor.obj L.mapTriangle T₃))
    (TriangleMorphism.hom₂
      (Functor.map L.mapTriangle
        (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ (α.f (W := W)) (γ.f (W := W) ≫ σ) ⋯)))
    (b ≫ TriangleMorphism.hom₂ (Functor.map L.mapTriangle ψ))
have refine_2 : L.map (γ.f (W := W) ≫ σ) = b ≫ L.map (β.s (W := W) ≫ γ.s (W := W) ≫ σ)
Tactic: dsimp [ψ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : HasZeroObject.{v_2, u_2} D
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : Pretriangulated.{v_2, u_2} D
inst_15 : L.IsTriangulated
inst_16 : IsTriangulated.{v_1, u_1} C
⊢ IsTriangulated.{v_2, u_2} D
have this : Functor.EssSurj (C := ComposableArrows.{v_1, u_1} C 2) (L.mapComposableArrows 2)
Tactic: have := essSurj_mapComposableArrows L W 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : HasZeroObject.{v_2, u_2} D
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : W.IsCompatibleWithTriangulation
n : ℤ
⊢ Functor.Additive (C := W.Localization) (shiftFunctor W.Localization n)
have rw : (W.Q ⋙ shiftFunctor W.Localization n).Additive
Tactic: rw [Localization.functor_additive_iff W.Q W]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : HasZeroObject.{v_2, u_2} D
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : W.IsCompatibleWithTriangulation
inst_15 : MorphismProperty.HasLocalization.{u_3, v_1, u_1} W
n : ℤ
⊢ Functor.Additive.{u_3, u_1, u_3, u_1} (C := MorphismProperty.Localization'.{u_3, v_1, u_1} W)
    (shiftFunctor (MorphismProperty.Localization'.{u_3, v_1, u_1} W) n)
have rw : Functor.Additive.{v_1, u_1, u_3, u_1} (D := MorphismProperty.Localization'.{u_3, v_1, u_1} W)
  (W.Q' ⋙ shiftFunctor (MorphismProperty.Localization'.{u_3, v_1, u_1} W) n)
Tactic: rw [Localization.functor_additive_iff W.Q' W]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : L.mapArrow.EssSurj
inst_14 : L.IsTriangulated
T : Triangle.{v_2, u_2} D
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T ↔
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T
have mp : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T →
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : L.mapArrow.EssSurj
inst_14 : L.IsTriangulated
T : Triangle.{v_2, u_2} D
mp :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T →
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T ↔
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T
have mpr : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T →
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : L.mapArrow.EssSurj
inst_14 : L.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T
f : Arrow.{v_1, u_1} C := L.mapArrow.objPreimage (Arrow.mk T.mor₁)
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T
have mp : ∀ (Z : C) (g : f.right ⟶ Z) (h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) f.left)
  (mem :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
      (Triangle.mk f.hom g h)),
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T
Tactic: obtain ⟨Z, g : f.right ⟶ Z, h : Z ⟶ f.left⟦(1 : ℤ)⟧, mem⟩ :=
      Pretriangulated.distinguished_cocone_triangle f.hom
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
inst_1 : ChosenPullbacksAlong.{v₁, u₁} (𝟙 X)
Y : Over.{v₁, u₁} X
⊢ CategoryStruct.comp (Y := Functor.obj (map (𝟙 X) ⋙ pullback (𝟙 X)) Y)
      (NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y)
      (NatTrans.app (Iso.hom (pullbackId X)) (Functor.obj (map (𝟙 X)) Y)) =
    NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y
have rw : Eq (α := Functor.obj (𝟭 (Over.{v₁, u₁} X)) Y ⟶ Functor.obj (𝟭 (Over.{v₁, u₁} X)) (Functor.obj (map (𝟙 X)) Y))
  (CategoryStruct.comp (Y := Functor.obj (map (𝟙 X) ⋙ pullback (𝟙 X)) Y)
      (NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y)
      (NatTrans.app (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (𝟙 X)) (mapPullbackAdj (𝟙 X))))
        (Functor.obj (map (𝟙 X)) Y)) :
    Functor.obj (𝟭 (Over.{v₁, u₁} X)) Y ⟶ Functor.obj (𝟭 (Over.{v₁, u₁} X)) (Functor.obj (map (𝟙 X)) Y))
  (NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y :
    Functor.obj (𝟭 (Over.{v₁, u₁} X)) Y ⟶ Functor.obj (map (𝟙 X) ⋙ pullback (𝟙 X)) Y)
Tactic: rw [pullbackId, Adjunction.unit_rightAdjointUniq_hom_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
inst_1 : ChosenPullbacksAlong.{v₁, u₁} (𝟙 X)
Y : Over.{v₁, u₁} X
rw :
  Eq (α := Functor.obj (𝟭 (Over.{v₁, u₁} X)) Y ⟶ Functor.obj (𝟭 (Over.{v₁, u₁} X)) (Functor.obj (map (𝟙 X)) Y))
    (CategoryStruct.comp (Y := Functor.obj (map (𝟙 X) ⋙ pullback (𝟙 X)) Y)
        (NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y)
        (NatTrans.app (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (𝟙 X)) (mapPullbackAdj (𝟙 X))))
          (Functor.obj (map (𝟙 X)) Y)) :
      Functor.obj (𝟭 (Over.{v₁, u₁} X)) Y ⟶ Functor.obj (𝟭 (Over.{v₁, u₁} X)) (Functor.obj (map (𝟙 X)) Y))
    (NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y :
      Functor.obj (𝟭 (Over.{v₁, u₁} X)) Y ⟶ Functor.obj (map (𝟙 X) ⋙ pullback (𝟙 X)) Y)
⊢ CategoryStruct.comp (Y := Functor.obj (map (𝟙 X) ⋙ pullback (𝟙 X)) Y)
      (NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y)
      (NatTrans.app (Iso.hom (pullbackId X)) (Functor.obj (map (𝟙 X)) Y)) =
    NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y
have rw₁ : Eq (α := Functor.obj (𝟭 (Over.{v₁, u₁} X)) Y ⟶ Functor.obj (𝟭 (Over.{v₁, u₁} X)) (Functor.obj (map (𝟙 X)) Y))
  (NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y :
    Functor.obj (𝟭 (Over.{v₁, u₁} X)) Y ⟶ Functor.obj (map (𝟙 X) ⋙ 𝟭 (Over.{v₁, u₁} X)) Y)
  (NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y :
    Functor.obj (𝟭 (Over.{v₁, u₁} X)) Y ⟶ Functor.obj (map (𝟙 X) ⋙ pullback (𝟙 X)) Y)
Tactic: rw [pullbackId, Adjunction.unit_rightAdjointUniq_hom_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
inst_1 : ChosenPullbacksAlong.{v₁, u₁} (𝟙 X)
⊢ Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ 𝟭 (Over.{v₁, u₁} X)))
    (CategoryStruct.comp (Y := map (𝟙 X) ⋙ pullback (𝟙 X)) (Adjunction.unit (mapPullbackAdj (𝟙 X)))
      (Functor.whiskerLeft (map (𝟙 X)) (Iso.hom (pullbackId X))))
    (Adjunction.unit (mapPullbackAdj (𝟙 X)))
have rw : Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ 𝟭 (Over.{v₁, u₁} X)))
  (CategoryStruct.comp (Y := map (𝟙 X) ⋙ pullback (𝟙 X)) (Adjunction.unit (mapPullbackAdj (𝟙 X)))
      (Functor.whiskerLeft (map (𝟙 X))
        (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (𝟙 X)) (mapPullbackAdj (𝟙 X))))) :
    Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ 𝟭 (Over.{v₁, u₁} X)))
  (Adjunction.unit (mapPullbackAdj (𝟙 X)) :
    Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ pullback (𝟙 X)))
Tactic: rw [pullbackId, Adjunction.unit_rightAdjointUniq_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
inst_1 : ChosenPullbacksAlong.{v₁, u₁} (𝟙 X)
rw :
  Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ 𝟭 (Over.{v₁, u₁} X)))
    (CategoryStruct.comp (Y := map (𝟙 X) ⋙ pullback (𝟙 X)) (Adjunction.unit (mapPullbackAdj (𝟙 X)))
        (Functor.whiskerLeft (map (𝟙 X))
          (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (𝟙 X)) (mapPullbackAdj (𝟙 X))))) :
      Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ 𝟭 (Over.{v₁, u₁} X)))
    (Adjunction.unit (mapPullbackAdj (𝟙 X)) :
      Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ pullback (𝟙 X)))
⊢ Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ 𝟭 (Over.{v₁, u₁} X)))
    (CategoryStruct.comp (Y := map (𝟙 X) ⋙ pullback (𝟙 X)) (Adjunction.unit (mapPullbackAdj (𝟙 X)))
      (Functor.whiskerLeft (map (𝟙 X)) (Iso.hom (pullbackId X))))
    (Adjunction.unit (mapPullbackAdj (𝟙 X)))
have rw₁ : Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ 𝟭 (Over.{v₁, u₁} X)))
  (Adjunction.unit (mapPullbackAdj (𝟙 X)) :
    Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ 𝟭 (Over.{v₁, u₁} X)))
  (Adjunction.unit (mapPullbackAdj (𝟙 X)) :
    Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ pullback (𝟙 X)))
Tactic: rw [pullbackId, Adjunction.unit_rightAdjointUniq_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
inst_1 : ChosenPullbacksAlong.{v₁, u₁} (𝟙 X)
⊢ Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (pullback (𝟙 X) ⋙ map (𝟙 X)) (𝟭 (Over.{v₁, u₁} X)))
    (Functor.whiskerRight (Iso.hom (pullbackId X)) (map (𝟙 X)) ≫ Adjunction.counit (mapPullbackAdj (𝟙 X)))
    (Adjunction.counit (mapPullbackAdj (𝟙 X)))
have this : Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (pullback (𝟙 X) ⋙ map (𝟙 X)) (𝟭 (Over.{v₁, u₁} X)))
  (CategoryStruct.comp (Y := pullback (𝟙 X) ⋙ map (𝟙 X))
    (Functor.whiskerRight (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (𝟙 X)) (mapPullbackAdj (𝟙 X))))
      (map (𝟙 X)))
    (Adjunction.counit (mapPullbackAdj (𝟙 X))))
  (Adjunction.counit (mapPullbackAdj (𝟙 X)))
Tactic: have := Adjunction.rightAdjointUniq_hom_counit (mapPullbackAdj (𝟙 X)) (id X).mapPullbackAdj
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
inst_1 : ChosenPullbacksAlong.{v₁, u₁} (𝟙 X)
this :
  Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (pullback (𝟙 X) ⋙ map (𝟙 X)) (𝟭 (Over.{v₁, u₁} X)))
    (CategoryStruct.comp (Y := pullback (𝟙 X) ⋙ map (𝟙 X))
      (Functor.whiskerRight (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (𝟙 X)) (mapPullbackAdj (𝟙 X))))
        (map (𝟙 X)))
      (Adjunction.counit (mapPullbackAdj (𝟙 X))))
    (Adjunction.counit (mapPullbackAdj (𝟙 X)))
rw :
  Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (pullback (𝟙 X) ⋙ map (𝟙 X)) (𝟭 (Over.{v₁, u₁} X)))
    (CategoryStruct.comp (Y := 𝟭 (Over.{v₁, u₁} X) ⋙ map (𝟙 X))
      (Functor.whiskerRight (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (𝟙 X)) (mapPullbackAdj (𝟙 X))))
          (map (𝟙 X)) :
        Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (pullback (𝟙 X) ⋙ map (𝟙 X))
          (𝟭 (Over.{v₁, u₁} X) ⋙ map (𝟙 X)))
      (Adjunction.counit (mapPullbackAdj (𝟙 X)) :
        Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (pullback (𝟙 X) ⋙ map (𝟙 X)) (𝟭 (Over.{v₁, u₁} X))))
    (Adjunction.counit (mapPullbackAdj (𝟙 X)))
⊢ Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (pullback (𝟙 X) ⋙ map (𝟙 X)) (𝟭 (Over.{v₁, u₁} X)))
    (Functor.whiskerRight (Iso.hom (pullbackId X)) (map (𝟙 X)) ≫ Adjunction.counit (mapPullbackAdj (𝟙 X)))
    (Adjunction.counit (mapPullbackAdj (𝟙 X)))
have rw₁ : Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (pullback (𝟙 X) ⋙ map (𝟙 X)) (𝟭 (Over.{v₁, u₁} X)))
  (Adjunction.counit (mapPullbackAdj (𝟙 X))) (Adjunction.counit (mapPullbackAdj (𝟙 X)))
Tactic: rw [pullbackId, Adjunction.rightAdjointUniq_hom_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : ChosenPullbacksAlong f
inst_2 : ChosenPullbacksAlong g
inst_3 : ChosenPullbacksAlong (f ≫ g)
⊢ Eq (α := 𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback g ⋙ pullback f)
    (CategoryStruct.comp (Y := map (f ≫ g) ⋙ pullback (f ≫ g)) (Adjunction.unit (mapPullbackAdj (f ≫ g)))
      ((map (f ≫ g)).whiskerLeft (Iso.hom (pullbackComp f g))))
    (Adjunction.unit (mapPullbackAdj (f ≫ g)))
have rw : Eq (α := 𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback g ⋙ pullback f)
  (CategoryStruct.comp (Y := map (f ≫ g) ⋙ pullback (f ≫ g)) (Adjunction.unit (mapPullbackAdj (f ≫ g)))
      ((map (f ≫ g)).whiskerLeft
        (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (f ≫ g)) (mapPullbackAdj (f ≫ g))))) :
    𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback g ⋙ pullback f)
  (Adjunction.unit (mapPullbackAdj (f ≫ g)) : 𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback (f ≫ g))
Tactic: rw [pullbackComp, Adjunction.unit_rightAdjointUniq_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : ChosenPullbacksAlong f
inst_2 : ChosenPullbacksAlong g
inst_3 : ChosenPullbacksAlong (f ≫ g)
rw :
  Eq (α := 𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback g ⋙ pullback f)
    (CategoryStruct.comp (Y := map (f ≫ g) ⋙ pullback (f ≫ g)) (Adjunction.unit (mapPullbackAdj (f ≫ g)))
        ((map (f ≫ g)).whiskerLeft
          (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (f ≫ g)) (mapPullbackAdj (f ≫ g))))) :
      𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback g ⋙ pullback f)
    (Adjunction.unit (mapPullbackAdj (f ≫ g)) : 𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback (f ≫ g))
⊢ Eq (α := 𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback g ⋙ pullback f)
    (CategoryStruct.comp (Y := map (f ≫ g) ⋙ pullback (f ≫ g)) (Adjunction.unit (mapPullbackAdj (f ≫ g)))
      ((map (f ≫ g)).whiskerLeft (Iso.hom (pullbackComp f g))))
    (Adjunction.unit (mapPullbackAdj (f ≫ g)))
have rw₁ : Eq (α := 𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback g ⋙ pullback f)
  (Adjunction.unit (mapPullbackAdj (f ≫ g)) : 𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback g ⋙ pullback f)
  (Adjunction.unit (mapPullbackAdj (f ≫ g)) : 𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback (f ≫ g))
Tactic: rw [pullbackComp, Adjunction.unit_rightAdjointUniq_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : ChosenPullbacksAlong f
inst_2 : ChosenPullbacksAlong g
inst_3 : ChosenPullbacksAlong (f ≫ g)
⊢ Eq (α := pullback (f ≫ g) ⋙ map (f ≫ g) ⟶ 𝟭 (Over.{v₁, u₁} Z))
    (CategoryStruct.comp (Y := (pullback g ⋙ pullback f) ⋙ map (f ≫ g))
      (Functor.whiskerRight (Iso.hom (pullbackComp f g)) (map (f ≫ g))) (Adjunction.counit (mapPullbackAdj (f ≫ g))))
    (Adjunction.counit (mapPullbackAdj (f ≫ g)))
have rw : Eq (α := pullback (f ≫ g) ⋙ map (f ≫ g) ⟶ 𝟭 (Over.{v₁, u₁} Z))
  (CategoryStruct.comp (Y := (pullback g ⋙ pullback f) ⋙ map (f ≫ g))
    (Functor.whiskerRight (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (f ≫ g)) (mapPullbackAdj (f ≫ g))))
        (map (f ≫ g)) :
      pullback (f ≫ g) ⋙ map (f ≫ g) ⟶ (pullback g ⋙ pullback f) ⋙ map (f ≫ g))
    (Adjunction.counit (mapPullbackAdj (f ≫ g)) : pullback (f ≫ g) ⋙ map (f ≫ g) ⟶ 𝟭 (Over.{v₁, u₁} Z)))
  (Adjunction.counit (mapPullbackAdj (f ≫ g)))
Tactic: rw [pullbackComp, Adjunction.rightAdjointUniq_hom_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : ChosenPullbacksAlong f
inst_2 : ChosenPullbacksAlong g
inst_3 : ChosenPullbacksAlong (f ≫ g)
rw :
  Eq (α := pullback (f ≫ g) ⋙ map (f ≫ g) ⟶ 𝟭 (Over.{v₁, u₁} Z))
    (CategoryStruct.comp (Y := (pullback g ⋙ pullback f) ⋙ map (f ≫ g))
      (Functor.whiskerRight (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (f ≫ g)) (mapPullbackAdj (f ≫ g))))
          (map (f ≫ g)) :
        pullback (f ≫ g) ⋙ map (f ≫ g) ⟶ (pullback g ⋙ pullback f) ⋙ map (f ≫ g))
      (Adjunction.counit (mapPullbackAdj (f ≫ g)) : pullback (f ≫ g) ⋙ map (f ≫ g) ⟶ 𝟭 (Over.{v₁, u₁} Z)))
    (Adjunction.counit (mapPullbackAdj (f ≫ g)))
⊢ Eq (α := pullback (f ≫ g) ⋙ map (f ≫ g) ⟶ 𝟭 (Over.{v₁, u₁} Z))
    (CategoryStruct.comp (Y := (pullback g ⋙ pullback f) ⋙ map (f ≫ g))
      (Functor.whiskerRight (Iso.hom (pullbackComp f g)) (map (f ≫ g))) (Adjunction.counit (mapPullbackAdj (f ≫ g))))
    (Adjunction.counit (mapPullbackAdj (f ≫ g)))
have rw₁ : Eq (α := pullback (f ≫ g) ⋙ map (f ≫ g) ⟶ 𝟭 (Over.{v₁, u₁} Z)) (Adjunction.counit (mapPullbackAdj (f ≫ g)))
  (Adjunction.counit (mapPullbackAdj (f ≫ g)))
Tactic: rw [pullbackComp, Adjunction.rightAdjointUniq_hom_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over.{v₁, u₁} Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
φ₂' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₂ ⋯
⊢ φ₁' = φ₂'
have a : Eq (α := (map g).obj U ⟶ Over.mk f)
  ((Equiv.symm (adj.homEquiv U (Over.mk f)) : (a : U ⟶ (pullback g).obj (Over.mk f)) → (map g).obj U ⟶ Over.mk f) φ₁' :
    (map g).obj U ⟶ Over.mk f)
  ((Equiv.symm (adj.homEquiv U (Over.mk f)) : (a : U ⟶ (pullback g).obj (Over.mk f)) → (map g).obj U ⟶ Over.mk f) φ₂' :
    (map g).obj U ⟶ Over.mk f)
Tactic: apply (adj.homEquiv U _).symm.injective