awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst : Mono r'
inst_1 : Mono k
h₂ :
  Eq (α := Set ((fun (X : Type u) ↦ X) X₄))
    (Set.range (ι := (fun (X : Type u) ↦ X) X₂)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) r) : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) ⊔
      Set.range (ι := (fun (X : Type u) ↦ X) X₃)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) b) : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄))
    Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) b' : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                x₃ :
              (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) b' : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
x₄ : (fun (X : Type u) ↦ X) X₄
hx₄ :
  (∃ (y : X₂), (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) y = x₄) ∨
    ∃ (y : X₃), (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) y = x₄
inl :
  ∀ (x₂ : X₂),
    ∃ (a : (fun (X : Type u) ↦ X) (pushout t l)),
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) φ :
              (a : (fun (X : Type u) ↦ X) (pushout t l)) → (fun (X : Type u) ↦ X) X₄)
            a :
          (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) x₂ : X₄)
⊢ ∃ (a : (fun (X : Type u) ↦ X) (pushout t l)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) φ :
          (a : (fun (X : Type u) ↦ X) (pushout t l)) → (fun (X : Type u) ↦ X) X₄)
        a =
      x₄
have inr : ∀ (x₃ : X₃),
  ∃ (a : (fun (X : Type u) ↦ X) (pushout t l)),
    Eq (α := (fun (X : Type u) ↦ X) X₄)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) φ :
            (a : (fun (X : Type u) ↦ X) (pushout t l)) → (fun (X : Type u) ↦ X) X₄)
          a :
        (fun (X : Type u) ↦ X) X₄)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) x₃ : X₄)
Tactic: obtain (⟨x₂, rfl⟩ | ⟨x₃, rfl⟩) := hx₄
Cleared hypotheses: x₄, hx₄
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (hypothesis)
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst : Mono r'
inst_1 : Mono k
h₂ :
  Eq (α := Set ((fun (X : Type u) ↦ X) X₄))
    (Set.range (ι := (fun (X : Type u) ↦ X) X₂)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) r) : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) ⊔
      Set.range (ι := (fun (X : Type u) ↦ X) X₃)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) b) : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄))
    Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) b' : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                x₃ :
              (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) b' : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
⊢ IsPushout t l r b
have this₁ : IsIso φ
Tactic: have : IsIso φ := by
    rw [isIso_iff_bijective]
    refine ⟨(mono_iff_injective _).1 (mono_of_mono φ k), fun x₄ ↦ ?_⟩
    have hx₄ := Set.mem_univ x₄
    simp only [← h₂, Set.sup_eq_union, Set.mem_union, Set.mem_range] at hx₄
    obtain (⟨x₂, rfl⟩ | ⟨x₃, rfl⟩) := hx₄
    · exact ⟨_, ConcreteCategory.congr_hom hφ₁ x₂⟩
    · exact ⟨_, ConcreteCategory.congr_hom hφ₂ x₃⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Yoneda (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
X : C
s : (↑(F ⋙ obj coyoneda (op X)).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
⊢ map (obj (const J) X) f ≫ (↑s : (j : J) → (F ⋙ coyoneda.obj (op X)).obj j) j' =
    (↑s : (j : J) → (F ⋙ coyoneda.obj (op X)).obj j) j ≫ F.map f
have dsimp : 𝟙 X ≫ (↑s : (j : J) → X ⟶ F.obj j) j' = (↑s : (j : J) → X ⟶ F.obj j) j ≫ F.map f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Yoneda (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
X : C
s : (↑(F ⋙ obj coyoneda (op X)).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
⊢ 𝟙 X ≫ (↑s : (j : J) → X ⟶ F.obj j) j' = (↑s : (j : J) → X ⟶ F.obj j) j ≫ F.map f
have rw : (↑s : (j : J) → X ⟶ F.obj j) j' = (↑s : (j : J) → X ⟶ F.obj j) j ≫ F.map f
Tactic: rw [Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Yoneda (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
X : C
s : (↑(F.op ⋙ obj yoneda X).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ (↑s : (j : Jᵒᵖ) → (F.op ⋙ yoneda.obj X).obj j) (op j') =
    (↑s : (j : Jᵒᵖ) → (F.op ⋙ yoneda.obj X).obj j) (op j) ≫ map (obj (const J) X) f
have dsimp : F.map f ≫ (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j') = (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j) ≫ 𝟙 X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Yoneda (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
X : C
s : (↑(F.op ⋙ obj yoneda X).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j') = (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j) ≫ 𝟙 X
have rw : F.map f ≫ (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j') = (↑s : (j : Jᵒᵖ) → F.obj (unop j) ⟶ X) (op j)
Tactic: rw [Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Yoneda (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J Cᵒᵖ
X : C
s : (↑(F ⋙ obj yoneda X).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
⊢ Eq (α := obj.{v_1, v_2, u_1, u_2} (obj (const J) (op X)) j ⟶ F.obj j')
    (map (obj (const J) (op X)) f ≫ Quiver.Hom.op ((↑s : (j : J) → (F ⋙ yoneda.obj X).obj j) j'))
    (Quiver.Hom.op ((↑s : (j : J) → (F ⋙ yoneda.obj X).obj j) j) ≫ F.map f)
have dsimp : 𝟙 (op X) ≫ ((↑s : (j : J) → unop (F.obj j) ⟶ X) j').op = ((↑s : (j : J) → unop (F.obj j) ⟶ X) j).op ≫ F.map f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Yoneda (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J Cᵒᵖ
X : C
s : (↑(F ⋙ obj yoneda X).sections : Type (max u_1 v_2))
j j' : J
f : j ⟶ j'
⊢ 𝟙 (op X) ≫ ((↑s : (j : J) → unop (F.obj j) ⟶ X) j').op = ((↑s : (j : J) → unop (F.obj j) ⟶ X) j).op ≫ F.map f
have rw : ((↑s : (j : J) → unop (F.obj j) ⟶ X) j').op = ((↑s : (j : J) → unop (F.obj j) ⟶ X) j).op ≫ F.map f
Tactic: rw [Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_1
inst_2 : Category.{v_1, u_1} K
D : Type u_2
inst_3 : Category.{v_2, u_2} D
F : Functor.{u', v, v', u} J C
c : Cocone F
h : IsUniversalColimit c
⊢ 𝟙 F ≫ c.ι = c.ι ≫ map (const J) (𝟙 c.pt)
have rw : 𝟙 F ≫ c.ι = c.ι ≫ 𝟙 (obj (const J) c.pt)
Tactic: rw [Functor.map_id, Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_1
inst_2 : Category.{v_1, u_1} K
D : Type u_2
inst_3 : Category.{v_2, u_2} D
F : Functor.{u', v, v', u} J C
c : Cocone F
h : IsUniversalColimit c
rw : 𝟙 F ≫ c.ι = c.ι ≫ 𝟙 (obj (const J) c.pt)
⊢ 𝟙 F ≫ c.ι = c.ι ≫ map (const J) (𝟙 c.pt)
have rw₁ : 𝟙 F ≫ c.ι = c.ι
Tactic: rw [Functor.map_id, Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_1
inst_2 : Category.{v_1, u_1} K
D : Type u_2
inst_3 : Category.{v_2, u_2} D
F : Functor.{u', v, v', u} J C
c : Cocone F
h : IsUniversalColimit c
rw : 𝟙 F ≫ c.ι = c.ι ≫ 𝟙 (obj (const J) c.pt)
rw₁ : 𝟙 F ≫ c.ι = c.ι
⊢ 𝟙 F ≫ c.ι = c.ι ≫ map (const J) (𝟙 c.pt)
have rw₂ : c.ι = c.ι
Tactic: rw [Functor.map_id, Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_1
inst_2 : Category.{v_1, u_1} K
D : Type u_2
inst_3 : Category.{v_2, u_2} D
F : Functor.{u', v, v', u} J C
c : Cocone F
h : IsUniversalColimit c
⊢ IsColimit c
have refine : ∀ (j : J), IsPullback (c.ι.app j) (NatTrans.app (𝟙 F) j) (𝟙 c.pt) (c.ι.app j)
Tactic: refine ((h c (𝟙 F) (𝟙 c.pt :) (by rw [Functor.map_id, Category.comp_id, Category.id_comp])
    (.of_isIso _)) fun j => ?_).some
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_1
inst_2 : Category.{v_1, u_1} K
D : Type u_2
inst_3 : Category.{v_2, u_2} D
F : Functor.{u', v, v', u} J C
c : Cocone F
h : IsUniversalColimit c
j : J
⊢ IsPullback (c.ι.app j) (NatTrans.app (𝟙 F) j) (𝟙 c.pt) (c.ι.app j)
have this : IsIso.{v, u} (𝟙 c.pt)
Tactic: haveI : IsIso (𝟙 c.pt) := inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
X : C
h : IsInitial.{v, u} X
F' : Functor.{0, v, 0, u} (Discrete PEmpty.{1}) C
c' : Cocone F'
α : F' ⟶ empty C
f : c'.pt ⟶ Cocone.pt.{0, v, 0, u} (asEmptyCocone X)
hf : α ≫ Cocone.ι (asEmptyCocone X) = c'.ι ≫ map (const (Discrete PEmpty.{1})) f
hα : NatTrans.Equifibered α
⊢ F' = empty C
have h_obj : ∀ (X : Discrete PEmpty.{1}), F'.obj X = obj.{0, v, 0, u} (empty C) X
Tactic: apply Functor.hext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
X : C
h : IsInitial.{v, u} X
F' : Functor.{0, v, 0, u} (Discrete PEmpty.{1}) C
c' : Cocone F'
α : F' ⟶ empty C
f : c'.pt ⟶ Cocone.pt.{0, v, 0, u} (asEmptyCocone X)
hf : α ≫ Cocone.ι (asEmptyCocone X) = c'.ι ≫ map (const (Discrete PEmpty.{1})) f
hα : NatTrans.Equifibered α
h_obj : ∀ (X : Discrete PEmpty.{1}), F'.obj X = obj.{0, v, 0, u} (empty C) X
⊢ F' = empty C
have h_map : ∀ (X Y : Discrete PEmpty.{1}) (f : X ⟶ Y),
  HEq (F'.map f) (β := obj.{0, v, 0, u} (empty C) X ⟶ obj.{0, v, 0, u} (empty C) Y) (map (empty C) f)
Tactic: apply Functor.hext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
X : C
h : IsInitial.{v, u} X
F' : Functor.{0, v, 0, u} (Discrete PEmpty.{1}) C
c' : Cocone F'
α : F' ⟶ empty C
f : c'.pt ⟶ Cocone.pt.{0, v, 0, u} (asEmptyCocone X)
hf : α ≫ Cocone.ι (asEmptyCocone X) = c'.ι ≫ map (const (Discrete PEmpty.{1})) f
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔
    ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f (NatTrans.app (Cocone.ι (asEmptyCocone X)) j)
have this : F' = empty C
Tactic: have : F' = Functor.empty C := by apply Functor.hext <;> rintro ⟨⟨⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
X : C
h : IsInitial.{v, u} X
F' : Functor.{0, v, 0, u} (Discrete PEmpty.{1}) C
c' : Cocone F'
α : F' ⟶ empty C
f : c'.pt ⟶ Cocone.pt.{0, v, 0, u} (asEmptyCocone X)
hf : α ≫ Cocone.ι (asEmptyCocone X) = c'.ι ≫ map (const (Discrete PEmpty.{1})) f
hα : NatTrans.Equifibered α
this : F' = empty C
⊢ Nonempty (IsColimit c') ↔
    ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f (NatTrans.app (Cocone.ι (asEmptyCocone X)) j)
have subst : ∀ (c' : Cocone.{0, v, 0, u} (empty C))
  (α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete PEmpty.{1}) C) (empty C) (empty C))
  (f : c'.pt ⟶ Cocone.pt.{0, v, 0, u} (asEmptyCocone X))
  (hf : α ≫ Cocone.ι (asEmptyCocone X) = c'.ι ≫ map (const (Discrete PEmpty.{1})) f) (hα : NatTrans.Equifibered α),
  Nonempty (IsColimit c') ↔
    ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f (NatTrans.app (Cocone.ι (asEmptyCocone X)) j)
Tactic: subst this
Cleared hypotheses: F', c', α, f, hf, hα, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
X : C
h : IsInitial.{v, u} X
c' : Cocone.{0, v, 0, u} (empty C)
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete PEmpty.{1}) C) (empty C) (empty C)
f : c'.pt ⟶ Cocone.pt.{0, v, 0, u} (asEmptyCocone X)
hf : α ≫ Cocone.ι (asEmptyCocone X) = c'.ι ≫ map (const (Discrete PEmpty.{1})) f
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔
    ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f (NatTrans.app (Cocone.ι (asEmptyCocone X)) j)
have this : IsIso f
Tactic: haveI := h.isIso_to f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
⊢ c'.ι ≫ map (const J) e.inv.hom = c.ι
have w : ∀ (j : J), (c'.ι ≫ map (const J) e.inv.hom).app j = c.ι.app j
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
⊢ Nonempty (IsColimit c'')
have this : c'.ι ≫ map (const J) e.inv.hom = c.ι
Tactic: have : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι := by
    ext j
    exact e.inv.2 j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
⊢ α ≫ c.ι = c''.ι ≫ map (const J) (f ≫ e.inv.hom)
have rw : α ≫ c.ι = c''.ι ≫ map (const J) f ≫ map (const J) e.inv.hom
Tactic: rw [Functor.map_comp, ← reassoc_of% h, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
rw : α ≫ c.ι = c''.ι ≫ map (const J) f ≫ map (const J) e.inv.hom
⊢ α ≫ c.ι = c''.ι ≫ map (const J) (f ≫ e.inv.hom)
have rw₁ : α ≫ c.ι = α ≫ c'.ι ≫ map (const J) e.inv.hom
Tactic: rw [Functor.map_comp, ← reassoc_of% h, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
rw : α ≫ c.ι = c''.ι ≫ map (const J) f ≫ map (const J) e.inv.hom
rw₁ : α ≫ c.ι = α ≫ c'.ι ≫ map (const J) e.inv.hom
⊢ α ≫ c.ι = c''.ι ≫ map (const J) (f ≫ e.inv.hom)
have rw₂ : α ≫ c.ι = α ≫ c.ι
Tactic: rw [Functor.map_comp, ← reassoc_of% h, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
⊢ Nonempty (IsColimit c'')
have apply : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)
Tactic: apply hc c'' α (f ≫ e.inv.1) (by rw [Functor.map_comp, ← reassoc_of% h, this]) hα
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
j : J
⊢ IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)
have rw : IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.hom) (c.ι.app j)
Tactic: rw [← Category.comp_id (α.app j)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
⊢ c'.ι ≫ map (const J) e.inv.hom = c.ι
have w : ∀ (j : J), (c'.ι ≫ map (const J) e.inv.hom).app j = c.ι.app j
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c'') ↔ ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
have this : c'.ι ≫ map (const J) e.inv.hom = c.ι
Tactic: have : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι := by
    ext j
    exact e.inv.2 j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
⊢ α ≫ c.ι = c''.ι ≫ map (const J) (f ≫ e.inv.hom)
have rw : α ≫ c.ι = c''.ι ≫ map (const J) f ≫ map (const J) e.inv.hom
Tactic: rw [Functor.map_comp, ← reassoc_of% h, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
rw : α ≫ c.ι = c''.ι ≫ map (const J) f ≫ map (const J) e.inv.hom
⊢ α ≫ c.ι = c''.ι ≫ map (const J) (f ≫ e.inv.hom)
have rw₁ : α ≫ c.ι = α ≫ c'.ι ≫ map (const J) e.inv.hom
Tactic: rw [Functor.map_comp, ← reassoc_of% h, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
rw : α ≫ c.ι = c''.ι ≫ map (const J) f ≫ map (const J) e.inv.hom
rw₁ : α ≫ c.ι = α ≫ c'.ι ≫ map (const J) e.inv.hom
⊢ α ≫ c.ι = c''.ι ≫ map (const J) (f ≫ e.inv.hom)
have rw₂ : α ≫ c.ι = α ≫ c.ι
Tactic: rw [Functor.map_comp, ← reassoc_of% h, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
⊢ Nonempty (IsColimit c'') ↔ ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
have rw : (∀ (j : J), IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)) ↔
  ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
Tactic: rw [H c'' α (f ≫ e.inv.1) (by rw [Functor.map_comp, ← reassoc_of% h, this]) hα]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
⊢ (∀ (j : J), IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)) ↔
    ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
have h₁ : ∀ (a : J),
  IsPullback (c''.ι.app a) (α.app a) (f ≫ e.inv.hom) (c.ι.app a) ↔ IsPullback (c''.ι.app a) (α.app a) f (c'.ι.app a)
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{u', v, v', u} J C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
j : J
| IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)
have rw : IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.hom) (c.ι.app j)
Tactic: rw [← Category.comp_id (α.app j)]