awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f_1 : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f_1.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j_1 : I
f : (i : I) → cG.pt ⟶ s.pt := fun (i : I) ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
i j : I
refine : ∀ (j₁ j₂ : I) (g : j₁ ⟶ j₂), f j₁ = f j₂
⊢ f i = f j

Tactic:
refine constant_of_preserves_morphisms f (fun j₁ j₂ g ↦ ?_) i j

Premises used: CategoryTheory.constant_of_preserves_morphisms
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f_1 : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f_1.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j_1 : I
f : (i : I) → cG.pt ⟶ s.pt := fun (i : I) ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
i j j₁ j₂ : I
g : j₁ ⟶ j₂
⊢ f_1.hom ≫ f j₁ = f_1.hom ≫ f j₂

Tactic:
simp [f]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f_1 : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f_1.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j_1 : I
f : (i : I) → cG.pt ⟶ s.pt := fun (i : I) ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
i j j₁ j₂ : I
g : j₁ ⟶ j₂
refine : cG.ι.app j₁ ≫ f j₁ = cG.ι.app j₁ ≫ f j₂
⊢ f j₁ = f j₂

Tactic:
refine (hf j₁).hom_ext (by simp [f]) ?_

Premises used: CategoryTheory.IsPushout.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f_1 : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f_1.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j_1 : I
f : (i : I) → cG.pt ⟶ s.pt := fun (i : I) ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
i j j₁ j₂ : I
g : j₁ ⟶ j₂
rw : s.ι.app j₁ = cG.ι.app j₁ ≫ f j₂
rw₁ : s.ι.app j₁ = (G.map g ≫ cG.ι.app j₂) ≫ f j₂
rw₂ : s.ι.app j₁ = G.map g ≫ cG.ι.app j₂ ≫ f j₂
rw₃ : s.ι.app j₁ = G.map g ≫ s.ι.app j₂
rw₄ rw₅ : s.ι.app j₁ = s.ι.app j₁
⊢ cG.ι.app j₁ ≫ f j₁ = cG.ι.app j₁ ≫ f j₂

Tactic:
rw [IsPushout.inr_desc, ← cG.w g, Category.assoc, IsPushout.inr_desc, Cocone.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cocone.w, CategoryTheory.IsPushout.inr_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f_1 : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f_1.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j : I
f : (i : I) → cG.pt ⟶ s.pt := fun (i : I) ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
this : ∀ (i j : I), f i = f j
change : cG.ι.app j ≫ f (Classical.arbitrary I) = s.ι.app j
⊢ cG.ι.app j ≫
      IsPushout.desc (Z := F.obj (Classical.arbitrary I)) (X :=
        Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const I) cF.pt) (Classical.arbitrary I)) (Y :=
        G.obj (Classical.arbitrary I)) (f :=
        (cF.ι.app (Classical.arbitrary I) :
          F.obj (Classical.arbitrary I) ⟶
            Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const I) cF.pt) (Classical.arbitrary I)))
        (g := (α.app (Classical.arbitrary I) : F.obj (Classical.arbitrary I) ⟶ G.obj (Classical.arbitrary I))) (inr :=
        (cG.ι.app (Classical.arbitrary I) :
          G.obj (Classical.arbitrary I) ⟶
            Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const I) cG.pt) (Classical.arbitrary I)))
        ⋯ (hcF.desc ((Cocone.precompose α).obj s) : cF.pt ⟶ ((Cocone.precompose α).obj s).pt)
        (s.ι.app (Classical.arbitrary I) :
          G.obj (Classical.arbitrary I) ⟶
            Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const I) s.pt) (Classical.arbitrary I))
        ⋯ =
    s.ι.app j

Tactic:
change _ ≫ f _ = _
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f_1 : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f_1.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j : I
f : (i : I) → cG.pt ⟶ s.pt := fun (i : I) ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
this : ∀ (i j : I), f i = f j
rw : cG.ι.app j ≫ f j = s.ι.app j
⊢ cG.ι.app j ≫ f (Classical.arbitrary I) = s.ι.app j

Tactic:
rw [this _ j]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f_1 : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f_1.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j : I
f : (i : I) → cG.pt ⟶ s.pt := fun (i : I) ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
this : ∀ (i j : I), f i = f j
⊢ cG.ι.app j ≫ f j = s.ι.app j

Tactic:
simp [f]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
g : cG.pt ⟶ s.pt
hg : ∀ (j : I), cG.ι.app j ≫ g = s.ι.app j
⊢ ∀ (j : I),
    cF.ι.app j ≫ f.hom ≫ g =
      cF.ι.app j ≫
        f.hom ≫
          IsPushout.desc (Z := F.obj (Classical.arbitrary I)) (X :=
            Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const I) cF.pt) (Classical.arbitrary I)) (Y :=
            G.obj (Classical.arbitrary I)) (f :=
            (cF.ι.app (Classical.arbitrary I) :
              F.obj (Classical.arbitrary I) ⟶
                Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const I) cF.pt) (Classical.arbitrary I)))
            (g := (α.app (Classical.arbitrary I) : F.obj (Classical.arbitrary I) ⟶ G.obj (Classical.arbitrary I)))
            (inr :=
            (cG.ι.app (Classical.arbitrary I) :
              G.obj (Classical.arbitrary I) ⟶
                Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const I) cG.pt) (Classical.arbitrary I)))
            ⋯ (hcF.desc ((Cocone.precompose α).obj s) : cF.pt ⟶ ((Cocone.precompose α).obj s).pt)
            (s.ι.app (Classical.arbitrary I) :
              G.obj (Classical.arbitrary I) ⟶
                Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const I) s.pt) (Classical.arbitrary I))
            ⋯

Tactic:
simp [hg]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
Goal:
I : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : IsConnected.{v_1, u_1} I
inst_2 : Category.{v_2, u_2} C
F G : Functor.{v_1, v_2, u_1, u_2} I C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
g : cG.pt ⟶ s.pt
hg : ∀ (j : I), cG.ι.app j ≫ g = s.ι.app j
⊢ Eq (α := G.obj (Classical.arbitrary I) ⟶ s.pt) (cG.ι.app (Classical.arbitrary I) ≫ g)
    (cG.ι.app (Classical.arbitrary I) ≫
      IsPushout.desc (Z := F.obj (Classical.arbitrary I)) (X :=
        Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const I) cF.pt) (Classical.arbitrary I)) (Y :=
        G.obj (Classical.arbitrary I)) (f :=
        (cF.ι.app (Classical.arbitrary I) :
          F.obj (Classical.arbitrary I) ⟶
            Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const I) cF.pt) (Classical.arbitrary I)))
        (g := (α.app (Classical.arbitrary I) : F.obj (Classical.arbitrary I) ⟶ G.obj (Classical.arbitrary I))) (inr :=
        (cG.ι.app (Classical.arbitrary I) :
          G.obj (Classical.arbitrary I) ⟶
            Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const I) cG.pt) (Classical.arbitrary I)))
        ⋯ (hcF.desc ((Cocone.precompose α).obj s) : cF.pt ⟶ ((Cocone.precompose α).obj s).pt)
        (s.ι.app (Classical.arbitrary I) :
          G.obj (Classical.arbitrary I) ⟶
            Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const I) s.pt) (Classical.arbitrary I))
        ⋯)

Tactic:
simp [hg]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
X Y : WalkingCospan
allEq : ∀ (a b : X ⟶ Y), a = b
⊢ Subsingleton (X ⟶ Y)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
X Y : WalkingCospan
a b : X ⟶ Y
⊢ a = b

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
X Y : WalkingSpan
allEq : ∀ (a b : X ⟶ Y), a = b
⊢ Subsingleton (X ⟶ Y)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
X Y : WalkingSpan
a b : X ⟶ Y
⊢ a = b

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
apply : ∀ (j : WalkingCospan), s.π.app j = i.hom ≫ t.π.app j
⊢ s ≅ t

Tactic:
apply Cone.ext i _

Premises used: CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ Functor.map (Functor.obj (Functor.const WalkingCospan) s.pt) inl ≫ s.π.app one = s.π.app left ≫ F.map inl

Tactic:
have h₁ := s.π.naturality WalkingCospan.Hom.inl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
h₁ : 𝟙 s.pt ≫ s.π.app one = s.π.app left ≫ F.map inl
⊢ s.π.app one = s.π.app left ≫ F.map inl

Tactic:
simp only [Category.id_comp] at h₁

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
h₁ : s.π.app one = s.π.app left ≫ F.map inl
⊢ Functor.map (Functor.obj (Functor.const WalkingCospan) t.pt) inl ≫ t.π.app one = t.π.app left ≫ F.map inl

Tactic:
have h₂ := t.π.naturality WalkingCospan.Hom.inl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
h₁ : s.π.app one = s.π.app left ≫ F.map inl
h₂ : 𝟙 t.pt ≫ t.π.app one = t.π.app left ≫ F.map inl
⊢ t.π.app one = t.π.app left ≫ F.map inl

Tactic:
simp only [Category.id_comp] at h₂

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
h₁ : s.π.app one = s.π.app left ≫ F.map inl
h₂ : t.π.app one = t.π.app left ≫ F.map inl
none : s.π.app Option.none = i.hom ≫ t.π.app left ≫ F.map inl
none₁ : s.π.app Option.none = (i.hom ≫ t.π.app left) ≫ F.map inl
none₂ : s.π.app Option.none = s.π.app left ≫ F.map inl
⊢ Eq (α := Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) s.pt) Option.none ⟶ F.obj Option.none)
    (s.π.app Option.none) (i.hom ≫ t.π.app Option.none)

Tactic:
simp_rw [h₂, ← Category.assoc, ← w₁, ← h₁]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) s.pt) (some WalkingPair.left) ⟶
      F.obj (some WalkingPair.left))
    (s.π.app (some WalkingPair.left)) (i.hom ≫ t.π.app (some WalkingPair.left))

Tactic:
w₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) s.pt) (some WalkingPair.left) ⟶
      F.obj (some WalkingPair.left))
    (s.π.app (some WalkingPair.left)) (i.hom ≫ t.π.app (some WalkingPair.left))

Tactic:
exact w₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) s.pt) (some WalkingPair.right) ⟶
      F.obj (some WalkingPair.right))
    (s.π.app (some WalkingPair.right)) (i.hom ≫ t.π.app (some WalkingPair.right))

Tactic:
w₂
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) s.pt) (some WalkingPair.right) ⟶
      F.obj (some WalkingPair.right))
    (s.π.app (some WalkingPair.right)) (i.hom ≫ t.π.app (some WalkingPair.right))

Tactic:
exact w₂
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
apply : ∀ (j : WalkingSpan), s.ι.app j ≫ i.hom = t.ι.app j
⊢ s ≅ t

Tactic:
apply Cocone.ext i _

Premises used: CategoryTheory.Limits.Cocone.ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
⊢ F.map fst ≫ s.ι.app left = s.ι.app zero ≫ Functor.map (Functor.obj (Functor.const WalkingSpan) s.pt) fst

Tactic:
have h₁ := s.ι.naturality WalkingSpan.Hom.fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
h₁ : F.map fst ≫ s.ι.app left = s.ι.app zero ≫ 𝟙 s.pt
⊢ F.map fst ≫ s.ι.app left = s.ι.app zero

Tactic:
simp only [Category.comp_id] at h₁

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
h₁ : F.map fst ≫ s.ι.app left = s.ι.app zero
⊢ F.map fst ≫ t.ι.app left = t.ι.app zero ≫ Functor.map (Functor.obj (Functor.const WalkingSpan) t.pt) fst

Tactic:
have h₂ := t.ι.naturality WalkingSpan.Hom.fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
h₁ : F.map fst ≫ s.ι.app left = s.ι.app zero
h₂ : F.map fst ≫ t.ι.app left = t.ι.app zero ≫ 𝟙 t.pt
⊢ F.map fst ≫ t.ι.app left = t.ι.app zero

Tactic:
simp only [Category.comp_id] at h₂

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
h₁ : F.map fst ≫ s.ι.app left = s.ι.app zero
h₂ : F.map fst ≫ t.ι.app left = t.ι.app zero
none : (F.map fst ≫ s.ι.app left) ≫ i.hom = t.ι.app Option.none
none₁ : F.map fst ≫ s.ι.app left ≫ i.hom = t.ι.app Option.none
none₂ : F.map fst ≫ t.ι.app WalkingCospan.left = t.ι.app Option.none
⊢ Eq (α := F.obj Option.none ⟶ t.pt) (s.ι.app Option.none ≫ i.hom) (t.ι.app Option.none)

Tactic:
simp_rw [← h₁, Category.assoc, w₁, h₂]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
⊢ Eq (α := F.obj (some WalkingPair.left) ⟶ t.pt) (s.ι.app (some WalkingPair.left) ≫ i.hom)
    (t.ι.app (some WalkingPair.left))

Tactic:
w₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
⊢ Eq (α := F.obj (some WalkingPair.left) ⟶ t.pt) (s.ι.app (some WalkingPair.left) ≫ i.hom)
    (t.ι.app (some WalkingPair.left))

Tactic:
exact w₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
⊢ Eq (α := F.obj (some WalkingPair.right) ⟶ t.pt) (s.ι.app (some WalkingPair.right) ≫ i.hom)
    (t.ι.app (some WalkingPair.right))

Tactic:
w₂
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
⊢ Eq (α := F.obj (some WalkingPair.right) ⟶ t.pt) (s.ι.app (some WalkingPair.right) ≫ i.hom)
    (t.ι.app (some WalkingPair.right))

Tactic:
exact w₂
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g).obj WalkingCospan.left = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (span f g).obj WalkingSpan.left = Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g).obj WalkingCospan.right = Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (span f g).obj WalkingSpan.right = Z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g).obj WalkingCospan.one = Z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (span f g).obj WalkingSpan.zero = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g).map inl = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (span f g).map fst = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g).map inr = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (span f g).map snd = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
w : WalkingCospan
⊢ (cospan f g).map (WalkingCospan.Hom.id w) = 𝟙 ((cospan f g).obj w)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
w : WalkingSpan
⊢ (span f g).map (WalkingSpan.Hom.id w) = 𝟙 ((span f g).obj w)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
j : WalkingCospan
none : F.obj Option.none = (cospan (F.map inl) (F.map inr)).obj Option.none
some : F.obj (Option.some WalkingPair.left) = (cospan (F.map inl) (F.map inr)).obj (Option.some WalkingPair.left)
some₁ : F.obj (Option.some WalkingPair.right) = (cospan (F.map inl) (F.map inr)).obj (Option.some WalkingPair.right)
⊢ F.obj j = (cospan (F.map inl) (F.map inr)).obj j

Tactic:
rcases j with (⟨⟩ | ⟨⟨⟩⟩)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
⊢ F.obj none = (cospan (F.map inl) (F.map inr)).obj none

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
⊢ F.obj (some WalkingPair.left) = (cospan (F.map inl) (F.map inr)).obj (some WalkingPair.left)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
⊢ F.obj (some WalkingPair.right) = (cospan (F.map inl) (F.map inr)).obj (some WalkingPair.right)

Tactic:
rfl