awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
W X Y Z : Functor.{v'', v, u'', u} D C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ H.IsVanKampen
have van_kampen : IsVanKampenColimit (PushoutCocone.mk h i sorry)
Tactic: rw [IsPushout.isVanKampen_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
W X Y Z : Functor.{v'', v, u'', u} D C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ IsVanKampenColimit (PushoutCocone.mk h i ⋯)
have van_kampen : ∀ (x : D),
  IsVanKampenColimit (F := span f g ⋙ Functor.obj (evaluation D C) x)
    (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i sorry))
Tactic: apply isVanKampenColimit_of_evaluation
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
W X Y Z : Functor.{v'', v, u'', u} D C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
⊢ IsVanKampenColimit (F := span f g ⋙ Functor.obj (evaluation D C) x)
    (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯))
have van_kampen : IsVanKampenColimit
  ((Cocone.precompose (diagramIsoSpan (span f g ⋙ Functor.obj (evaluation D C) x)).inv).obj
    (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i sorry)))
Tactic: refine (IsVanKampenColimit.precompose_isIso_iff (diagramIsoSpan _).inv).mp ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
W X Y Z : Functor.{v'', v, u'', u} D C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
⊢ IsVanKampenColimit
    ((Cocone.precompose (diagramIsoSpan (span f g ⋙ Functor.obj (evaluation D C) x)).inv).obj
      (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯)))
have van_kampen : IsVanKampenColimit (F :=
  span ((span f g ⋙ Functor.obj (evaluation D C) x).map WalkingSpan.Hom.fst)
    ((span f g ⋙ Functor.obj (evaluation D C) x).map WalkingSpan.Hom.snd))
  (PushoutCocone.mk (W :=
    Functor.obj.{0, v, 0, u}
      (Functor.obj (Functor.const WalkingSpan)
        (Cocone.pt (F := span f g ⋙ Functor.obj (evaluation D C) x)
          (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i sorry))))
      WalkingSpan.left)
    (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i sorry)))
      WalkingSpan.left)
    (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i sorry)))
      WalkingSpan.right)
    sorry)
Tactic: refine IsVanKampenColimit.of_iso ?_ (PushoutCocone.isoMk _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W_1 X_1 Y_1 Z_1 : C
f_1 : W_1 ⟶ X_1
g_1 : W_1 ⟶ Y_1
h_1 : X_1 ⟶ Z_1
i_1 : Y_1 ⟶ Z_1
D : Type u''
inst_2 : Category.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
W X Y Z : Functor.{v'', v, u'', u} D C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
⊢ IsVanKampenColimit (F :=
    span ((span f g ⋙ Functor.obj (evaluation D C) x).map WalkingSpan.Hom.fst)
      ((span f g ⋙ Functor.obj (evaluation D C) x).map WalkingSpan.Hom.snd))
    (PushoutCocone.mk (W :=
      Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const WalkingSpan)
          (Cocone.pt (F := span f g ⋙ Functor.obj (evaluation D C) x)
            (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯))))
        WalkingSpan.left)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯)))
        WalkingSpan.left)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation D C) x) (PushoutCocone.mk h i ⋯)))
        WalkingSpan.right)
      ⋯)
have van_kampen : IsPushout.IsVanKampen (W := Functor.obj (Functor.obj (evaluation D C) x) W) sorry
Tactic: refine (IsPushout.isVanKampen_iff (H.map ((evaluation _ _).obj x))).mp ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : Adhesive.{v'', u''} D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst_3 : PreservesLimitsOfShape WalkingCospan F
inst_4 : ReflectsLimitsOfShape WalkingCospan F
inst_5 : PreservesColimitsOfShape WalkingSpan F
inst_6 : ReflectsColimitsOfShape WalkingSpan F
⊢ Adhesive.{v, u} C
have apply : ∀ {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Mono f] (H : IsPushout f g h i), H.IsVanKampen
Tactic: apply Adhesive.mk (hasPullback_of_mono_left := H₁) (hasPushout_of_mono_left := H₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : Adhesive.{v'', u''} D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst_3 : PreservesLimitsOfShape WalkingCospan F
inst_4 : ReflectsLimitsOfShape WalkingCospan F
inst_5 : PreservesColimitsOfShape WalkingSpan F
inst_6 : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ H.IsVanKampen
have rw : IsVanKampenColimit (PushoutCocone.mk h i sorry)
Tactic: rw [IsPushout.isVanKampen_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : Adhesive.{v'', u''} D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst_3 : PreservesLimitsOfShape WalkingCospan F
inst_4 : ReflectsLimitsOfShape WalkingCospan F
inst_5 : PreservesColimitsOfShape WalkingSpan F
inst_6 : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ IsVanKampenColimit (PushoutCocone.mk h i ⋯)
have refine : IsVanKampenColimit (F.mapCocone (PushoutCocone.mk h i sorry))
Tactic: refine IsVanKampenColimit.of_mapCocone F ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : Adhesive.{v'', u''} D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst_3 : PreservesLimitsOfShape WalkingCospan F
inst_4 : ReflectsLimitsOfShape WalkingCospan F
inst_5 : PreservesColimitsOfShape WalkingSpan F
inst_6 : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ IsVanKampenColimit (F.mapCocone (PushoutCocone.mk h i ⋯))
have refine : IsVanKampenColimit ((Cocone.precompose (diagramIsoSpan (span f g ⋙ F)).inv).obj (F.mapCocone (PushoutCocone.mk h i sorry)))
Tactic: refine (IsVanKampenColimit.precompose_isIso_iff (diagramIsoSpan _).inv).mp ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : Adhesive.{v'', u''} D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst_3 : PreservesLimitsOfShape WalkingCospan F
inst_4 : ReflectsLimitsOfShape WalkingCospan F
inst_5 : PreservesColimitsOfShape WalkingSpan F
inst_6 : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ IsVanKampenColimit
    ((Cocone.precompose (diagramIsoSpan (span f g ⋙ F)).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯)))
have refine : IsVanKampenColimit
  (PushoutCocone.mk ((F.mapCocone (PushoutCocone.mk h i sorry)).ι.app WalkingSpan.left)
    ((F.mapCocone (PushoutCocone.mk h i sorry)).ι.app WalkingSpan.right) sorry)
Tactic: refine IsVanKampenColimit.of_iso ?_ (PushoutCocone.isoMk _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : Adhesive.{v'', u''} D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst_3 : PreservesLimitsOfShape WalkingCospan F
inst_4 : ReflectsLimitsOfShape WalkingCospan F
inst_5 : PreservesColimitsOfShape WalkingSpan F
inst_6 : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ IsVanKampenColimit
    (PushoutCocone.mk ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.left)
      ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.right) ⋯)
have refine : sorry.IsVanKampen
Tactic: refine (IsPushout.isVanKampen_iff (H.map F)).mp ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : Adhesive.{v'', u''} D
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasPushouts.{v, u} C
inst_5 : PreservesLimitsOfShape WalkingCospan F
inst_6 : PreservesColimitsOfShape WalkingSpan F
inst_7 : F.ReflectsIsomorphisms
⊢ Adhesive.{v, u} C
have this : ReflectsLimitsOfShape WalkingCospan F
Tactic: haveI : ReflectsLimitsOfShape WalkingCospan F :=
    reflectsLimitsOfShape_of_reflectsIsomorphisms
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : Adhesive.{v'', u''} D
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasPushouts.{v, u} C
inst_5 : PreservesLimitsOfShape WalkingCospan F
inst_6 : PreservesColimitsOfShape WalkingSpan F
inst_7 : F.ReflectsIsomorphisms
this : ReflectsLimitsOfShape WalkingCospan F
⊢ Adhesive.{v, u} C
have this₁ : ReflectsColimitsOfShape WalkingSpan F
Tactic: haveI : ReflectsColimitsOfShape WalkingSpan F :=
    reflectsColimitsOfShape_of_reflectsIsomorphisms
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
⊢ Adhesive.{v'', u''} D
have this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
Tactic: have := adj.leftAdjoint_preservesColimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
⊢ Adhesive.{v'', u''} D
have this₁ : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
Tactic: have := adj.rightAdjoint_preservesLimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
⊢ Adhesive.{v'', u''} D
have apply : ∀ {W X Y Z : D} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Mono f] (H : IsPushout f g h i), H.IsVanKampen
Tactic: apply Adhesive.mk (hasPushout_of_mono_left := H₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_9 : Mono f
H : IsPushout f g h i
⊢ H.IsVanKampen
have this₁ : IsPushout.IsVanKampen (Z := pushout (Gr.map f) (Gr.map g)) sorry
Tactic: have := Adhesive.van_kampen (IsPushout.of_hasPushout (Gr.map f) (Gr.map g))
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this_2 : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_9 : Mono f
H : IsPushout f g h i
this : IsPushout.IsVanKampen (Z := pushout (Gr.map f) (Gr.map g)) ⋯
⊢ H.IsVanKampen
have rw : ∀
  (this :
    IsVanKampenColimit
      (PushoutCocone.mk (W := pushout (Gr.map f) (Gr.map g)) (pushout.inl (Gr.map f) (Gr.map g))
        (pushout.inr (Gr.map f) (Gr.map g)) sorry)),
  IsVanKampenColimit (PushoutCocone.mk h i sorry)
Tactic: rw [IsPushout.isVanKampen_iff] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this_2 : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_9 : Mono f
H : IsPushout f g h i
this :
  IsVanKampenColimit
    (PushoutCocone.mk (W := pushout (Gr.map f) (Gr.map g)) (pushout.inl (Gr.map f) (Gr.map g))
      (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
⊢ IsVanKampenColimit (PushoutCocone.mk h i ⋯)
have refine : IsVanKampenColimit
  ((Cocone.precompose ((span f g).isoWhiskerLeft (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj
    (PushoutCocone.mk h i sorry))
Tactic: refine (IsVanKampenColimit.precompose_isIso_iff
    (Functor.isoWhiskerLeft _ (asIso adj.counit) ≪≫ Functor.rightUnitor _).hom).mp ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this_2 : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_9 : Mono f
H : IsPushout f g h i
this :
  IsVanKampenColimit
    (PushoutCocone.mk (W := pushout (Gr.map f) (Gr.map g)) (pushout.inl (Gr.map f) (Gr.map g))
      (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
⊢ IsVanKampenColimit
    ((Cocone.precompose ((span f g).isoWhiskerLeft (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj
      (PushoutCocone.mk h i ⋯))
have refine_1 : IsColimit
  (Gl.mapCocone
    ((Cocone.precompose (spanCompIso Gr f g).hom).obj
      (PushoutCocone.mk (W := pushout (Gr.map f) (Gr.map g)) (pushout.inl (Gr.map f) (Gr.map g))
        (pushout.inr (Gr.map f) (Gr.map g)) sorry)))
Tactic: refine ((this.precompose_isIso (spanCompIso _ _ _).hom).map_reflective adj).of_iso
    (IsColimit.uniqueUpToIso ?_ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasPullbacks.{v'', u''} D
inst_3 : Adhesive.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasPushouts.{v, u} C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_6 : Gr.Full
inst_7 : Gr.Faithful
inst_8 : PreservesLimitsOfShape WalkingCospan Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
this_2 : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_9 : Mono f
H : IsPushout f g h i
this :
  IsVanKampenColimit
    (PushoutCocone.mk (W := pushout (Gr.map f) (Gr.map g)) (pushout.inl (Gr.map f) (Gr.map g))
      (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
refine_1 :
  IsColimit
    (Gl.mapCocone
      ((Cocone.precompose (spanCompIso Gr f g).hom).obj
        (PushoutCocone.mk (W := pushout (Gr.map f) (Gr.map g)) (pushout.inl (Gr.map f) (Gr.map g))
          (pushout.inr (Gr.map f) (Gr.map g)) ⋯)))
⊢ IsVanKampenColimit
    ((Cocone.precompose ((span f g).isoWhiskerLeft (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj
      (PushoutCocone.mk h i ⋯))
have refine_2 : IsColimit
  ((Cocone.precompose ((span f g).isoWhiskerLeft (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj
    (PushoutCocone.mk h i sorry))
Tactic: refine ((this.precompose_isIso (spanCompIso _ _ _).hom).map_reflective adj).of_iso
    (IsColimit.uniqueUpToIso ?_ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Adhesive.{v, u} C
X : C
a b : Subobject.{v, u} X
s : BinaryCofan a b
⊢ Eq (α :=
    Limits.pullback a.arrow b.arrow ⟶
      Functor.obj underlying
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
          { as := WalkingPair.left : Discrete WalkingPair }))
    (pullback.fst a.arrow b.arrow ≫ Functor.map underlying (s.ι.app { as := WalkingPair.left }))
    (pullback.snd a.arrow b.arrow ≫ Functor.map underlying (s.ι.app { as := WalkingPair.right }))
have h : Eq (α := Limits.pullback a.arrow b.arrow ⟶ X)
  ((pullback.fst a.arrow b.arrow ≫ Functor.map underlying (s.ι.app { as := WalkingPair.left })) ≫
    (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).arrow)
  ((pullback.snd a.arrow b.arrow ≫ Functor.map underlying (s.ι.app { as := WalkingPair.right })) ≫
    (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).arrow)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Subobject (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Adhesive.{v, u} C
X : C
F : Discrete WalkingPair ⥤ Subobject.{v, u} X
⊢ HasColimit F
have this : HasColimit (pair (F.obj { as := WalkingPair.left }) (F.obj { as := WalkingPair.right }))
Tactic: have : HasColimit (pair (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)) :=
      ⟨⟨⟨_, isColimitBinaryCofan (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Additive (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
X : C
Y : D
x x_1 : F.obj X ⟶ Y
⊢ (adj.homEquiv X Y).toFun (x + x_1) = (adj.homEquiv X Y).toFun x + (adj.homEquiv X Y).toFun x_1
have this : G.Additive
Tactic: have := adj.right_adjoint_additive
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
G : Functor.{v₁, v, u₁, u} D C
inst_2 : G.IsRightAdjoint
A : C
⊢ ∃ (ι : Type w) (B : ι → D) (f : (i : ι) → A ⟶ G.obj (B i)),
    ∀ (X : D) (h : A ⟶ G.obj X), ∃ (i : ι) (g : B i ⟶ X), f i ≫ G.map g = h
have fun : ∀ (X : D) (h : A ⟶ G.obj X),
  ∃ (i : PUnit.{w + 1}) (g : (fun (x : PUnit.{w + 1}) ↦ G.leftAdjoint.obj A) i ⟶ X),
    (fun (x : PUnit.{w + 1}) ↦
            (NatTrans.app (Adjunction.unit (Adjunction.ofIsRightAdjoint G)) A :
              Functor.obj.{v, v, u, u} (𝟭 C) A ⟶ (G.leftAdjoint ⋙ G).obj A))
          i ≫
        G.map g =
      h
Tactic: refine
    ⟨PUnit, fun _ => G.leftAdjoint.obj A, fun _ => (Adjunction.ofIsRightAdjoint G).unit.app A, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
G : Functor.{v₁, v, u₁, u} D C
inst_2 : G.IsRightAdjoint
A : C
B : D
h : A ⟶ G.obj B
⊢ ∃ (i : PUnit.{w + 1}) (g : (fun (x : PUnit.{w + 1}) ↦ G.leftAdjoint.obj A) i ⟶ B),
    (fun (x : PUnit.{w + 1}) ↦
            (NatTrans.app (Adjunction.unit (Adjunction.ofIsRightAdjoint G)) A :
              Functor.obj.{v, v, u, u} (𝟭 C) A ⟶ (G.leftAdjoint ⋙ G).obj A))
          i ≫
        G.map g =
      h
have refine : CategoryStruct.comp (Y := G.obj ((fun (x : PUnit.{w + 1}) ↦ G.leftAdjoint.obj A) PUnit.unit))
    ((fun (x : PUnit.{w + 1}) ↦
        (NatTrans.app (Adjunction.unit (Adjunction.ofIsRightAdjoint G)) A :
          Functor.obj.{v, v, u, u} (𝟭 C) A ⟶ (G.leftAdjoint ⋙ G).obj A))
      PUnit.unit)
    (G.map
      (((Equiv.symm (Adjunction.homEquiv (Adjunction.ofIsRightAdjoint G) A B) :
            Equiv.{v + 1, v₁ + 1} (A ⟶ G.obj B) (G.leftAdjoint.obj A ⟶ B)) :
          (a : A ⟶ G.obj B) → G.leftAdjoint.obj A ⟶ B)
        h)) =
  h
Tactic: refine ⟨PUnit.unit, ((Adjunction.ofIsRightAdjoint G).homEquiv _ _).symm h, ?_⟩