awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
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
⊢ Eq (α := Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) s.pt) none ⟶ F.obj none) (s.π.app none)
    (i.hom ≫ t.π.app none)
have none : s.π.app none = i.hom ≫ t.π.app left ≫ F.map inl
Tactic: simp_rw [h₂, ← Category.assoc, ← w₁, ← h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
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
⊢ 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)
have none₁ : s.π.app Option.none = (i.hom ≫ t.π.app left) ≫ F.map inl
Tactic: simp_rw [h₂, ← Category.assoc, ← w₁, ← h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
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
⊢ 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)
have none₂ : s.π.app Option.none = s.π.app left ≫ F.map inl
Tactic: simp_rw [h₂, ← Category.assoc, ← w₁, ← h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
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
⊢ s ≅ t
have apply : ∀ (j : WalkingSpan), s.ι.app j ≫ i.hom = t.ι.app j
Tactic: apply Cocone.ext i _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (hypothesis)
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 none ⟶ t.pt) (s.ι.app none ≫ i.hom) (t.ι.app none)
have h₁ : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (hypothesis)
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
⊢ Eq (α := F.obj none ⟶ t.pt) (s.ι.app none ≫ i.hom) (t.ι.app none)
have h₂ : F.map fst ≫ s.ι.app left = s.ι.app zero
Tactic: simp only [Category.comp_id] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (hypothesis)
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
⊢ Eq (α := F.obj none ⟶ t.pt) (s.ι.app none ≫ i.hom) (t.ι.app none)
have h₂ : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (hypothesis)
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
⊢ Eq (α := F.obj none ⟶ t.pt) (s.ι.app none ≫ i.hom) (t.ι.app none)
have h₃ : F.map fst ≫ t.ι.app left = t.ι.app zero
Tactic: simp only [Category.comp_id] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
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
⊢ Eq (α := F.obj none ⟶ t.pt) (s.ι.app none ≫ i.hom) (t.ι.app none)
have none : (F.map fst ≫ s.ι.app left) ≫ i.hom = t.ι.app none
Tactic: simp_rw [← h₁, Category.assoc, w₁, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
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
⊢ Eq (α := F.obj Option.none ⟶ t.pt) (s.ι.app Option.none ≫ i.hom) (t.ι.app Option.none)
have none₁ : F.map fst ≫ s.ι.app left ≫ i.hom = t.ι.app Option.none
Tactic: simp_rw [← h₁, Category.assoc, w₁, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
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
⊢ Eq (α := F.obj Option.none ⟶ t.pt) (s.ι.app Option.none ≫ i.hom) (t.ι.app Option.none)
have none₂ : F.map fst ≫ t.ι.app WalkingCospan.left = t.ι.app Option.none
Tactic: simp_rw [← h₁, Category.assoc, w₁, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
j : WalkingCospan
⊢ F.obj j = (cospan (F.map inl) (F.map inr)).obj j
have none : F.obj none = (cospan (F.map inl) (F.map inr)).obj none
Tactic: rcases j with (⟨⟩ | ⟨⟨⟩⟩)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
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
⊢ F.obj j = (cospan (F.map inl) (F.map inr)).obj j
have some : F.obj (some WalkingPair.left) = (cospan (F.map inl) (F.map inr)).obj (some WalkingPair.left)
Tactic: rcases j with (⟨⟩ | ⟨⟨⟩⟩)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
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)
⊢ F.obj j = (cospan (F.map inl) (F.map inr)).obj j
have some₁ : F.obj (Option.some WalkingPair.right) = (cospan (F.map inl) (F.map inr)).obj (Option.some WalkingPair.right)
Tactic: rcases j with (⟨⟩ | ⟨⟨⟩⟩)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
f : Quiver.Hom (V := WalkingCospan) none none
⊢ F.map f ≫ Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) =
    Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) ≫
      (cospan (F.map inl) (F.map inr)).map f
have none : Eq (α := F.obj none ⟶ (cospan (F.map inl) (F.map inr)).obj none)
  (F.map (WidePullbackShape.Hom.id none) ≫
    Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso sorry : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none))
  (Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso sorry : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) ≫
    (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id none))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
f : some WalkingPair.left ⟶ none
⊢ F.map f ≫ Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.left)) ≫
      (cospan (F.map inl) (F.map inr)).map f
have some : F.map (term WalkingPair.left) ≫
    Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso sorry : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) =
  Iso.hom
      ((fun (j : WalkingCospan) ↦ (eqToIso sorry : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
        (some WalkingPair.left)) ≫
    (cospan (F.map inl) (F.map inr)).map (term WalkingPair.left)
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.left)) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.left)) ≫
      (cospan (F.map inl) (F.map inr)).map f
have some : F.map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
    Iso.hom
      ((fun (j : WalkingCospan) ↦ (eqToIso sorry : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
        (some WalkingPair.left)) =
  Iso.hom
      ((fun (j : WalkingCospan) ↦ (eqToIso sorry : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
        (some WalkingPair.left)) ≫
    (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id (some WalkingPair.left))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
f : some WalkingPair.right ⟶ none
⊢ F.map f ≫ Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.right)) ≫
      (cospan (F.map inl) (F.map inr)).map f
have some : F.map (term WalkingPair.right) ≫
    Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso sorry : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) =
  Iso.hom
      ((fun (j : WalkingCospan) ↦ (eqToIso sorry : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
        (some WalkingPair.right)) ≫
    (cospan (F.map inl) (F.map inr)).map (term WalkingPair.right)
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.right)) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.right)) ≫
      (cospan (F.map inl) (F.map inr)).map f
have some : F.map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
    Iso.hom
      ((fun (j : WalkingCospan) ↦ (eqToIso sorry : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
        (some WalkingPair.right)) =
  Iso.hom
      ((fun (j : WalkingCospan) ↦ (eqToIso sorry : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
        (some WalkingPair.right)) ≫
    (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id (some WalkingPair.right))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
j : WalkingSpan
⊢ F.obj j = (span (F.map fst) (F.map snd)).obj j
have none : F.obj none = (span (F.map fst) (F.map snd)).obj none
Tactic: rcases j with (⟨⟩ | ⟨⟨⟩⟩)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
j : WalkingSpan
none : F.obj Option.none = (span (F.map fst) (F.map snd)).obj Option.none
⊢ F.obj j = (span (F.map fst) (F.map snd)).obj j
have some : F.obj (some WalkingPair.left) = (span (F.map fst) (F.map snd)).obj (some WalkingPair.left)
Tactic: rcases j with (⟨⟩ | ⟨⟨⟩⟩)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
j : WalkingSpan
none : F.obj Option.none = (span (F.map fst) (F.map snd)).obj Option.none
some : F.obj (Option.some WalkingPair.left) = (span (F.map fst) (F.map snd)).obj (Option.some WalkingPair.left)
⊢ F.obj j = (span (F.map fst) (F.map snd)).obj j
have some₁ : F.obj (Option.some WalkingPair.right) = (span (F.map fst) (F.map snd)).obj (Option.some WalkingPair.right)
Tactic: rcases j with (⟨⟩ | ⟨⟨⟩⟩)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
f : Quiver.Hom (V := WalkingSpan) none none
⊢ F.map f ≫ Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) none) =
    Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) none) ≫
      (span (F.map fst) (F.map snd)).map f
have none : Eq (α := F.obj none ⟶ (span (F.map fst) (F.map snd)).obj none)
  (F.map (WidePushoutShape.Hom.id none) ≫
    Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso sorry : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) none))
  (Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso sorry : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) none) ≫
    (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id none))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
f : none ⟶ some WalkingPair.left
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.left)) =
    Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) none) ≫
      (span (F.map fst) (F.map snd)).map f
have none : F.map (init WalkingPair.left) ≫
    Iso.hom
      ((fun (j : WalkingSpan) ↦ (eqToIso sorry : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) (some WalkingPair.left)) =
  Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso sorry : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) none) ≫
    (span (F.map fst) (F.map snd)).map (init WalkingPair.left)
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
f : none ⟶ some WalkingPair.right
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.right)) =
    Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) none) ≫
      (span (F.map fst) (F.map snd)).map f
have none : F.map (init WalkingPair.right) ≫
    Iso.hom
      ((fun (j : WalkingSpan) ↦ (eqToIso sorry : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
        (some WalkingPair.right)) =
  Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso sorry : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) none) ≫
    (span (F.map fst) (F.map snd)).map (init WalkingPair.right)
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.left)) =
    Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.left)) ≫
      (span (F.map fst) (F.map snd)).map f
have some : F.map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
    Iso.hom
      ((fun (j : WalkingSpan) ↦ (eqToIso sorry : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) (some WalkingPair.left)) =
  Iso.hom
      ((fun (j : WalkingSpan) ↦ (eqToIso sorry : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) (some WalkingPair.left)) ≫
    (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id (some WalkingPair.left))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.right)) =
    Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.right)) ≫
      (span (F.map fst) (F.map snd)).map f
have some : F.map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
    Iso.hom
      ((fun (j : WalkingSpan) ↦ (eqToIso sorry : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
        (some WalkingPair.right)) =
  Iso.hom
      ((fun (j : WalkingSpan) ↦ (eqToIso sorry : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
        (some WalkingPair.right)) ≫
    (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id (some WalkingPair.right))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (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
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : Quiver.Hom (V := WalkingCospan) none none
⊢ Eq (α := (cospan f_1 g ⋙ F).obj none ⟶ (cospan (F.map f_1) (F.map g)).obj none)
    ((cospan f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) none (Iso.refl ((cospan f_1 g ⋙ F).obj none))
          fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) none (Iso.refl ((cospan f_1 g ⋙ F).obj none))
          fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map f)
have none : Eq (α := (cospan f_1 g ⋙ F).obj none ⟶ (cospan (F.map f_1) (F.map g)).obj none)
  ((cospan f_1 g ⋙ F).map (WidePullbackShape.Hom.id none) ≫
    Iso.hom
      (Option.casesOn (motive := fun (x : WalkingCospan) ↦
        (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) none (Iso.refl ((cospan f_1 g ⋙ F).obj none))
        fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
  (Iso.hom
      (Option.casesOn (motive := fun (x : WalkingCospan) ↦
        (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) none (Iso.refl ((cospan f_1 g ⋙ F).obj none))
        fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
    (cospan (F.map f_1) (F.map g)).map (WidePullbackShape.Hom.id none))
Tactic: cases f
Cleared hypotheses: f