awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
φ : (f : Arrow.{v, u} C) → (s : C) × (t : C) × (s ⟶ t) :=
  fun (f : Arrow.{v, u} C) ↦
    Sigma.mk (β := fun (s : C) ↦ (t : C) × (s ⟶ t)) f.left (Sigma.mk (β := fun (t : C) ↦ f.left ⟶ t) f.right f.hom)
s t : C
f : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t
s' t' : C
f' : Functor.obj.{v, v, u, u} (𝟭 C) s' ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t'
h :
  φ { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
    φ { left := s', right := t', hom := f' }
⊢ { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = { left := s', right := t', hom := f' }
have obtain : ∀ (f' : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t')
  (h :
    φ { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
      φ { left := s, right := t', hom := f' }),
  { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = { left := s, right := t', hom := f' }
Tactic: obtain rfl : s = s' := congr_arg Sigma.fst h
Cleared hypotheses: s', f', h
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
φ : (f : Arrow.{v, u} C) → (s : C) × (t : C) × (s ⟶ t) :=
  fun (f : Arrow.{v, u} C) ↦
    Sigma.mk (β := fun (s : C) ↦ (t : C) × (s ⟶ t)) f.left (Sigma.mk (β := fun (t : C) ↦ f.left ⟶ t) f.right f.hom)
s t : C
f : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t
t' : C
f' : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t'
h :
  φ { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = φ { left := s, right := t', hom := f' }
⊢ { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = { left := s, right := t', hom := f' }
have h₁ : Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
    Arrow.right { left := s, right := t', hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ∧
  Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ≍
    Arrow.hom { left := s, right := t', hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
Tactic: simp only [Sigma.mk.injEq, heq_eq_eq, true_and, φ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
φ : (f : Arrow.{v, u} C) → (s : C) × (t : C) × (s ⟶ t) :=
  fun (f : Arrow.{v, u} C) ↦
    Sigma.mk (β := fun (s : C) ↦ (t : C) × (s ⟶ t)) f.left (Sigma.mk (β := fun (t : C) ↦ f.left ⟶ t) f.right f.hom)
s t : C
f : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t
t' : C
f' : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t'
h :
  Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
      Arrow.right { left := s, right := t', hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ∧
    Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ≍
      Arrow.hom { left := s, right := t', hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
⊢ { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = { left := s, right := t', hom := f' }
have obtain : ∀ (f' : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t)
  (h :
    Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
        Arrow.right { left := s, right := t, hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ∧
      Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ≍
        Arrow.hom { left := s, right := t, hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }),
  { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = { left := s, right := t, hom := f' }
Tactic: obtain rfl : t = t' := h.1
Cleared hypotheses: t', f', h
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
φ : (f : Arrow.{v, u} C) → (s : C) × (t : C) × (s ⟶ t) :=
  fun (f : Arrow.{v, u} C) ↦
    Sigma.mk (β := fun (s : C) ↦ (t : C) × (s ⟶ t)) f.left (Sigma.mk (β := fun (t : C) ↦ f.left ⟶ t) f.right f.hom)
s t : C
f f' : Functor.obj.{v, v, u, u} (𝟭 C) s ⟶ Functor.obj.{v, v, u, u} (𝟭 C) t
h :
  Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
      Arrow.right { left := s, right := t, hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ∧
    Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ≍
      Arrow.hom { left := s, right := t, hom := f' : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
⊢ { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = { left := s, right := t, hom := f' }
have obtain : ∀
  (h :
    Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } =
        Arrow.right { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ∧
      Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } ≍
        Arrow.hom { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }),
  { left := s, right := t, hom := f : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } = { left := s, right := t, hom := f }
Tactic: obtain rfl : f = f' := by simpa using h
Cleared hypotheses: f', h
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : Small.{w, u'} D
inst_5 : LocallySmall.{w, v', u'} D
⊢ Small.{w, max (max (max u' u) v') v} (Functor.{v, v', u, u'} C D)
have refine_1 : ∀ (F G : Functor.{v, v', u, u'} C D)
  (h :
    Eq (α := (f : Arrow.{v, u} C) → Arrow.{v', u'} D)
      ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) F)
      ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) G))
  (X : C), F.obj X = G.obj X
Tactic: refine small_of_injective (f := fun F (f : Arrow C) ↦ Arrow.mk (F.map f.hom))
    (fun F G h ↦ Functor.ext (fun X ↦ ?_) (fun X Y f ↦ ?_))
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : Small.{w, u'} D
inst_5 : LocallySmall.{w, v', u'} D
refine_1 :
  ∀ (F G : Functor.{v, v', u, u'} C D)
    (h :
      Eq (α := (f : Arrow.{v, u} C) → Arrow.{v', u'} D)
        ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) F)
        ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) G))
    (X : C), F.obj X = G.obj X
⊢ Small.{w, max (max (max u' u) v') v} (Functor.{v, v', u, u'} C D)
have refine_2 : ∀ (F G : Functor.{v, v', u, u'} C D)
  (h :
    Eq (α := (f : Arrow.{v, u} C) → Arrow.{v', u'} D)
      ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) F)
      ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) G))
  (X Y : C) (f : X ⟶ Y), F.map f = eqToHom sorry ≫ G.map f ≫ eqToHom sorry
Tactic: refine small_of_injective (f := fun F (f : Arrow C) ↦ Arrow.mk (F.map f.hom))
    (fun F G h ↦ Functor.ext (fun X ↦ ?_) (fun X Y f ↦ ?_))
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : Small.{w, u'} D
inst_5 : LocallySmall.{w, v', u'} D
F G : Functor.{v, v', u, u'} C D
h :
  Eq (α := (f : Arrow.{v, u} C) → Arrow.{v', u'} D)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) F)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) G)
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have this : Arrow.mk (F.map f) = Arrow.mk (G.map f)
Tactic: have : Arrow.mk (F.map f) = Arrow.mk (G.map f) := congr_fun h (Arrow.mk f)
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : Small.{w, u'} D
inst_5 : LocallySmall.{w, v', u'} D
F G : Functor.{v, v', u, u'} C D
h :
  Eq (α := (f : Arrow.{v, u} C) → Arrow.{v', u'} D)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) F)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) G)
X Y : C
f : X ⟶ Y
this : Arrow.mk (F.map f) = Arrow.mk (G.map f)
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have this₁ : ∃ (hX : F.obj X = G.obj X) (hY : F.obj Y = G.obj Y), F.map f = eqToHom hX ≫ G.map f ≫ eqToHom sorry
Tactic: rw [Arrow.mk_eq_mk_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : Small.{w, u'} D
inst_5 : LocallySmall.{w, v', u'} D
F G : Functor.{v, v', u, u'} C D
h :
  Eq (α := (f : Arrow.{v, u} C) → Arrow.{v', u'} D)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) F)
    ((fun (F : Functor.{v, v', u, u'} C D) (f : Arrow.{v, u} C) ↦ Arrow.mk (F.map f.hom)) G)
X Y : C
f : X ⟶ Y
this : ∃ (hX : F.obj X = G.obj X) (hY : F.obj Y = G.obj Y), F.map f = eqToHom hX ≫ G.map f ≫ eqToHom ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have refine_2 : ∀ (w : F.obj X = G.obj X) (w_1 : F.obj Y = G.obj Y),
  F.map f = eqToHom w ≫ G.map f ≫ eqToHom sorry → F.map f = eqToHom sorry ≫ G.map f ≫ eqToHom sorry
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
F : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
⊢ F = pair X Y
have h_obj : ∀ (X_1 : Discrete WalkingPair), F.obj X_1 = Functor.obj.{0, v, 0, u} (pair X Y) X_1
Tactic: apply Functor.hext
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
F : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
h_obj : ∀ (X_1 : Discrete WalkingPair), F.obj X_1 = Functor.obj.{0, v, 0, u} (pair X Y) X_1
⊢ F = pair X Y
have h_map : ∀ (X_1 Y_1 : Discrete WalkingPair) (f : X_1 ⟶ Y_1),
  HEq (F.map f) (β := Functor.obj.{0, v, 0, u} (pair X Y) X_1 ⟶ Functor.obj.{0, v, 0, u} (pair X Y) Y_1)
    (Functor.map (pair X Y) f)
Tactic: apply Functor.hext
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
F : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
⊢ IsVanKampenColimit c
have this : F = pair X Y
Tactic: have : F = pair X Y := by
    apply Functor.hext
    · rintro ⟨⟨⟩⟩ <;> rfl
    · rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp [X, Y]
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
F : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
this : F = pair X Y
⊢ IsVanKampenColimit c
have clear_value : ∀ (X Y : C) (this : F = pair X Y), IsVanKampenColimit c
Tactic: clear_value X Y
Cleared hypotheses: X, Y, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryExtensive.{v, u} C
F : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
hc : IsColimit c
X Y : C
this : F = pair X Y
⊢ IsVanKampenColimit c
have subst : ∀ (c : Cocone.{0, v, 0, u} (pair X Y)) (hc : IsColimit c), IsVanKampenColimit c
Tactic: subst this
Cleared hypotheses: F, c, hc, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : HasBinaryCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
⊢ HasPullback f coprod.inr
have this : IsPullback (Y := coprod.{v, u} Y X) (𝟙 Z) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X) f
  (Iso.hom (coprod.braiding Y X) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y)
Tactic: have : IsPullback (𝟙 _) (f ≫ (coprod.braiding X Y).hom) f (coprod.braiding Y X).hom :=
    IsPullback.of_horiz_isIso ⟨by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : HasBinaryCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
this :
  IsPullback (Y := coprod.{v, u} Y X) (𝟙 Z) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X) f
    (Iso.hom (coprod.braiding Y X) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y)
⊢ HasPullback f coprod.inr
have this₁ : IsPullback (P :=
  pullback (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
    (coprod.inl : Y ⟶ coprod.{v, u} Y X))
  (pullback.fst (f ≫ Iso.hom (coprod.braiding X Y)) coprod.inl ≫ 𝟙 Z :
    pullback (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
        (coprod.inl : Y ⟶ coprod.{v, u} Y X) ⟶
      Z)
  (pullback.snd (f ≫ Iso.hom (coprod.braiding X Y)) coprod.inl :
    pullback (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
        (coprod.inl : Y ⟶ coprod.{v, u} Y X) ⟶
      Y)
  f
  (CategoryStruct.comp (Y := coprod.{v, u} Y X) (coprod.inl : Y ⟶ coprod.{v, u} Y X)
    (Iso.hom (coprod.braiding Y X) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y))
Tactic: have := (IsPullback.of_hasPullback (f ≫ (coprod.braiding X Y).hom) coprod.inl).paste_horiz this
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X_1 Y_1 : C
inst_3 : HasBinaryCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
this_1 :
  IsPullback (Y := coprod.{v, u} Y X) (𝟙 Z) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X) f
    (Iso.hom (coprod.braiding Y X) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y)
this :
  IsPullback (P :=
    pullback (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
      (coprod.inl : Y ⟶ coprod.{v, u} Y X))
    (pullback.fst (f ≫ Iso.hom (coprod.braiding X Y)) coprod.inl ≫ 𝟙 Z :
      pullback (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
          (coprod.inl : Y ⟶ coprod.{v, u} Y X) ⟶
        Z)
    (pullback.snd (f ≫ Iso.hom (coprod.braiding X Y)) coprod.inl :
      pullback (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
          (coprod.inl : Y ⟶ coprod.{v, u} Y X) ⟶
        Y)
    f
    (CategoryStruct.comp (Y := coprod.{v, u} Y X) (coprod.inl : Y ⟶ coprod.{v, u} Y X)
      (Iso.hom (coprod.braiding Y X) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y))
⊢ HasPullback f coprod.inr
have this₁ : IsPullback (P := pullback (Z := coprod.{v, u} Y X) (f ≫ coprod.desc coprod.inr coprod.inl) coprod.inl)
  (pullback.fst (f ≫ coprod.desc coprod.inr coprod.inl) coprod.inl)
  (pullback.snd (f ≫ coprod.desc coprod.inr coprod.inl) coprod.inl) f coprod.inr
Tactic: simp only [coprod.braiding_hom, Category.comp_id, colimit.ι_desc, BinaryCofan.mk_pt,
    BinaryCofan.ι_app_left, BinaryCofan.mk_inl] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u''
inst_2 : Category.{v'', u''} D_1
X_1 Y_1 : C
D : Type u_1
inst_3 : Category.{v_1, u_1} D
inst_4 : HasBinaryCoproducts.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
inst_5 : PreservesPullbacksOfInclusions F
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
⊢ PreservesLimit (cospan f coprod.inr) F
have h : cospan (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
    (coprod.inl : Y ⟶ coprod.{v, u} Y X) ≅
  cospan f coprod.inr
Tactic: apply preservesLimit_of_iso_diagram (K₁ := cospan (f ≫ (coprod.braiding X Y).hom) coprod.inl)
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u''
inst_2 : Category.{v'', u''} D_1
X_1 Y_1 : C
D : Type u_1
inst_3 : Category.{v_1, u_1} D
inst_4 : HasBinaryCoproducts.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
inst_5 : PreservesPullbacksOfInclusions F
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
⊢ cospan (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
      (coprod.inl : Y ⟶ coprod.{v, u} Y X) ≅
    cospan f coprod.inr
have h : Iso.hom (Iso.refl Z) ≫ f =
  CategoryStruct.comp (Y := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
    (Iso.hom (Iso.symm (coprod.braiding X Y)) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y)
Tactic: apply cospanExt (Iso.refl _) (Iso.refl _) (coprod.braiding X Y).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u''
inst_2 : Category.{v'', u''} D_1
X_1 Y_1 : C
D : Type u_1
inst_3 : Category.{v_1, u_1} D
inst_4 : HasBinaryCoproducts.{v, u} C
F : Functor.{v, v_1, u, u_1} C D
inst_5 : PreservesPullbacksOfInclusions F
X Y Z : C
f : Z ⟶ coprod.{v, u} X Y
h :
  Iso.hom (Iso.refl Z) ≫ f =
    CategoryStruct.comp (Y := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
      (Iso.hom (Iso.symm (coprod.braiding X Y)) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y)
⊢ cospan (Z := coprod.{v, u} Y X) (f ≫ Iso.hom (coprod.braiding X Y) : Z ⟶ coprod.{v, u} Y X)
      (coprod.inl : Y ⟶ coprod.{v, u} Y X) ≅
    cospan f coprod.inr
have h₁ : Eq.{v + 1} (α := Y ⟶ coprod.{v, u} X Y) (Iso.hom (Iso.refl Y) ≫ coprod.inr : Y ⟶ coprod.{v, u} X Y)
  (CategoryStruct.comp (Y := coprod.{v, u} Y X) (coprod.inl : Y ⟶ coprod.{v, u} Y X)
      (Iso.hom (Iso.symm (coprod.braiding X Y)) : coprod.{v, u} Y X ⟶ coprod.{v, u} X Y) :
    Y ⟶ coprod.{v, u} X Y)
Tactic: apply cospanExt (Iso.refl _) (Iso.refl _) (coprod.braiding X Y).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
inst_3 : FinitaryPreExtensive.{v, u} C
⊢ IsIso.{v, u} (Y :=
    Functor.obj.{0, v, 0, u}
      (Functor.obj (Functor.const (Discrete WalkingPair))
        (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))))
      { as := WalkingPair.right : Discrete WalkingPair })
    (BinaryCofan.inr (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C))))
have dsimp : IsIso.{v, u} (𝟙 (initial.{v, u} C))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
⊢ FinitaryExtensive.{v, u} C ↔ IsVanKampenColimit c₀
have refine : ∀ (H : IsVanKampenColimit c₀), FinitaryExtensive.{v, u} C
Tactic: refine ⟨fun H => H.van_kampen' c₀ hc₀, fun H => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H : IsVanKampenColimit c₀
⊢ FinitaryExtensive.{v, u} C
have van_kampen' : ∀ {X Y : C} (c : BinaryCofan.{v, u} X Y) (a : IsColimit c), IsVanKampenColimit c
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H : IsVanKampenColimit c₀
⊢ ∀ {X Y : C} (c : BinaryCofan.{v, u} X Y) (a : IsColimit c), IsVanKampenColimit c
have van_kampen' : ∀
  (H :
    ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
      αX ≫ c₀.inl = c'.inl ≫ f →
        αY ≫ c₀.inr = c'.inr ≫ f →
          (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr))
  {X Y : C} (c : BinaryCofan.{v, u} X Y) (a : IsColimit c) {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ X)
  (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
  αX ≫ c.inl = c'.inl ≫ f →
    αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
Tactic: simp_rw [BinaryCofan.isVanKampen_iff] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
⊢ Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
have van_kampen' : ∀
  (d :
    c.pt ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
        { as := WalkingPair.left : Discrete WalkingPair })
  (hd : c.inl ≫ d = HT.from X ≫ c₀.inl) (hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr),
  Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
Tactic: obtain ⟨d, hd, hd'⟩ :=
    Limits.BinaryCofan.IsColimit.desc' hc (HT.from _ ≫ c₀.inl) (HT.from _ ≫ c₀.inr)
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
⊢ (αX ≫ HT.from X) ≫ c₀.inl = c'.inl ≫ f ≫ d
have rw : (αX ≫ HT.from X) ≫ c₀.inl = αX ≫ c.inl ≫ d
Tactic: rw [← reassoc_of% hX, hd, Category.assoc]