awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
inst_1 : LinearOrder ι
I : MultispanIndex.{w, w, v, u} (MultispanShape.prod ι) C
c : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
h : I.SymmStruct
x y : ι
hxy : y < x
this : Eq (α := I.left (y, x) ⟶ c.pt) (I.fst (y, x) ≫ c.π y) (I.snd (y, x) ≫ c.π x)
inr : Eq (α := I.left (x, y) ⟶ c.pt) (I.fst (x, y) ≫ c.π x) ((h.iso x y).hom ≫ I.fst (y, x) ≫ c.π y)
⊢ Eq (α := I.left (x, y) ⟶ c.pt) (I.fst (x, y) ≫ c.π x) (I.snd (x, y) ≫ c.π y)
have inr₁ : Eq (α := I.left (x, y) ⟶ c.pt) ((h.iso x y).hom ≫ I.snd (y, x) ≫ c.π x) ((h.iso x y).hom ≫ I.fst (y, x) ≫ c.π y)
Tactic: rw [← h.iso_hom_fst_assoc, ← h.iso_hom_snd_assoc, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
inst_1 : LinearOrder ι
I : MultispanIndex.{w, w, v, u} (MultispanShape.prod ι) C
c : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
h : I.SymmStruct
x y : ι
hxy : y < x
this : Eq (α := I.left (y, x) ⟶ c.pt) (I.fst (y, x) ≫ c.π y) (I.snd (y, x) ≫ c.π x)
inr : Eq (α := I.left (x, y) ⟶ c.pt) (I.fst (x, y) ≫ c.π x) ((h.iso x y).hom ≫ I.fst (y, x) ≫ c.π y)
inr₁ : Eq (α := I.left (x, y) ⟶ c.pt) ((h.iso x y).hom ≫ I.snd (y, x) ≫ c.π x) ((h.iso x y).hom ≫ I.fst (y, x) ≫ c.π y)
⊢ Eq (α := I.left (x, y) ⟶ c.pt) (I.fst (x, y) ≫ c.π x) (I.snd (x, y) ≫ c.π y)
have inr₂ : Eq (α := I.left (x, y) ⟶ c.pt) ((h.iso x y).hom ≫ I.snd (y, x) ≫ c.π x) ((h.iso x y).hom ≫ I.snd (y, x) ≫ c.π x)
Tactic: rw [← h.iso_hom_fst_assoc, ← h.iso_hom_snd_assoc, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
inst_1 : LinearOrder ι
I : MultispanIndex.{w, w, v, u} (MultispanShape.prod ι) C
c : Multicofork I
hc : IsColimit c
h : I.SymmStruct
s : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
m : Cocone.pt (J := WalkingMultispan (MultispanShape.ofLinearOrder ι)) c.toLinearOrder ⟶ s.pt
hm : ∀ (i : (MultispanShape.ofLinearOrder ι).R), π c.toLinearOrder i ≫ m = s.π i
i : (MultispanShape.prod ι).R
⊢ c.π i ≫ m =
    c.π i ≫
      (fun (s : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder) ↦
          (hc.desc (s.ofLinearOrder h) : c.pt ⟶ (s.ofLinearOrder h).pt))
        s
have this : Eq (α := I.multispan.obj (WalkingMultispan.right i) ⟶ (s.ofLinearOrder h).pt)
  (c.ι.app (WalkingMultispan.right i) ≫ hc.desc (s.ofLinearOrder h))
  ((s.ofLinearOrder h).ι.app (WalkingMultispan.right i))
Tactic: have := hc.fac (ofLinearOrder s h) (.right i)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
inst_1 : LinearOrder ι
I : MultispanIndex.{w, w, v, u} (MultispanShape.prod ι) C
c : Multicofork I
hc : IsColimit c
h : I.SymmStruct
s : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder
m : Cocone.pt (J := WalkingMultispan (MultispanShape.ofLinearOrder ι)) c.toLinearOrder ⟶ s.pt
hm : ∀ (i : (MultispanShape.ofLinearOrder ι).R), π c.toLinearOrder i ≫ m = s.π i
i : (MultispanShape.prod ι).R
this : c.π i ≫ hc.desc (s.ofLinearOrder h) = (s.ofLinearOrder h).π i
⊢ c.π i ≫ m =
    c.π i ≫
      (fun (s : Multicofork (J := MultispanShape.ofLinearOrder ι) I.toLinearOrder) ↦
          (hc.desc (s.ofLinearOrder h) : c.pt ⟶ (s.ofLinearOrder h).pt))
        s
have rw : c.π i ≫ m = (s.ofLinearOrder h).π i
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
⊢ t.π.app WalkingCospan.one = t.fst ≫ f
have w : Functor.map (Functor.obj (Functor.const WalkingCospan) t.pt) inl ≫ t.π.app WalkingCospan.one =
  t.π.app WalkingCospan.left ≫ (cospan f g).map inl
Tactic: have w := t.π.naturality WalkingCospan.Hom.inl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : Quiver.Hom (V := WalkingCospan) none none
⊢ Eq.{v + 1} (α := Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) none ⟶ (cospan f g).obj none)
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) j ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd) ≫
      (cospan f g).map j)
have none : Eq.{v + 1} (α := Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) none ⟶ (cospan f g).obj none)
  (Functor.map (Functor.obj (Functor.const WalkingCospan) W) (WidePullbackShape.Hom.id none) ≫
    Option.casesOn (motive := fun (x : WalkingCospan) ↦
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
      fun (j' : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x)) j'
        fst snd)
  ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
      fun (j' : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x)) j'
        fst snd) ≫
    (cospan f g).map (WidePullbackShape.Hom.id none))
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.left ⟶ none
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some WalkingPair.left) ⟶
      (cospan f g).obj none)
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) j ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd) ≫
      (cospan f g).map j)
have some : Eq.{v + 1} (α :=
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some WalkingPair.left) ⟶
    (cospan f g).obj none)
  (Functor.map (Functor.obj (Functor.const WalkingCospan) W) (term WalkingPair.left) ≫
    Option.casesOn (motive := fun (x : WalkingCospan) ↦
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
      fun (j' : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x)) j'
        fst snd)
  ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
      (some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x)) j'
        fst snd) ≫
    (cospan f g).map (term WalkingPair.left))
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.left ⟶ some WalkingPair.left
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some WalkingPair.left) ⟶
      (cospan f g).obj (some WalkingPair.left))
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) j ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd) ≫
      (cospan f g).map j)
have some : Eq.{v + 1} (α :=
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some WalkingPair.left) ⟶
    (cospan f g).obj (some WalkingPair.left))
  (Functor.map (Functor.obj (Functor.const WalkingCospan) W) (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
    Option.casesOn (motive := fun (x : WalkingCospan) ↦
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
      (some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x)) j'
        fst snd)
  ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
      (some WalkingPair.left) (fst ≫ f) fun (j' : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x)) j'
        fst snd) ≫
    (cospan f g).map (WidePullbackShape.Hom.id (some WalkingPair.left)))
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.right ⟶ none
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some WalkingPair.right) ⟶
      (cospan f g).obj none)
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) j ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd) ≫
      (cospan f g).map j)
have some : Eq.{v + 1} (α :=
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some WalkingPair.right) ⟶
    (cospan f g).obj none)
  (Functor.map (Functor.obj (Functor.const WalkingCospan) W) (term WalkingPair.right) ≫
    Option.casesOn (motive := fun (x : WalkingCospan) ↦
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x) none (fst ≫ f)
      fun (j' : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x)) j'
        fst snd)
  ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
      (some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x)) j'
        fst snd) ≫
    (cospan f g).map (term WalkingPair.right))
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.right ⟶ some WalkingPair.right
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some WalkingPair.right) ⟶
      (cospan f g).obj (some WalkingPair.right))
    (Functor.map (Functor.obj (Functor.const WalkingCospan) W) j ≫
      Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd)
    ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
        (some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x))
          j' fst snd) ≫
      (cospan f g).map j)
have some : Eq.{v + 1} (α :=
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some WalkingPair.right) ⟶
    (cospan f g).obj (some WalkingPair.right))
  (Functor.map (Functor.obj (Functor.const WalkingCospan) W) (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
    Option.casesOn (motive := fun (x : WalkingCospan) ↦
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
      (some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x)) j'
        fst snd)
  ((Option.casesOn (motive := fun (x : WalkingCospan) ↦
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) x ⟶ (cospan f g).obj x)
      (some WalkingPair.right) (fst ≫ f) fun (j' : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) W) (some x) ⟶ (cospan f g).obj (some x)) j'
        fst snd) ≫
    (cospan f g).map (WidePullbackShape.Hom.id (some WalkingPair.right)))
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
W : C
k l : W ⟶ t.pt
h₀ : k ≫ t.fst = l ≫ t.fst
h₁ : k ≫ t.snd = l ≫ t.snd
⊢ Eq (α := W ⟶ (cospan f g).obj none) (k ≫ t.π.app none) (l ≫ t.π.app none)
have rw : k ≫ t.π.app WalkingCospan.left ≫ (cospan f g).map inl = l ≫ t.π.app WalkingCospan.left ≫ (cospan f g).map inl
Tactic: rw [← t.w inl, reassoc_of% h₀]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
W : C
k l : W ⟶ t.pt
h₀ : k ≫ t.fst = l ≫ t.fst
h₁ : k ≫ t.snd = l ≫ t.snd
rw : k ≫ t.π.app WalkingCospan.left ≫ (cospan f g).map inl = l ≫ t.π.app WalkingCospan.left ≫ (cospan f g).map inl
⊢ Eq (α := W ⟶ (cospan f g).obj none) (k ≫ t.π.app none) (l ≫ t.π.app none)
have rw₁ : l ≫ t.fst ≫ (cospan f g).map inl = l ≫ t.π.app WalkingCospan.left ≫ (cospan f g).map inl
Tactic: rw [← t.w inl, reassoc_of% h₀]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt), (∀ (j : WalkingCospan), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (cospan f g)
j : WalkingCospan
⊢ Eq (α := s.pt ⟶ (cospan f g).obj none) (lift s ≫ t.π.app none) (s.π.app none)
have rw : (lift s ≫ t.π.app WalkingCospan.left) ≫ (cospan f g).map inl = s.π.app WalkingCospan.left ≫ (cospan f g).map inl
Tactic: rw [← s.w inl, ← t.w inl, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt), (∀ (j : WalkingCospan), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (cospan f g)
j : WalkingCospan
⊢ (lift s ≫ t.π.app WalkingCospan.left) ≫ (cospan f g).map inl = s.π.app WalkingCospan.left ≫ (cospan f g).map inl
have e_a : lift s ≫ t.π.app WalkingCospan.left = s.π.app WalkingCospan.left
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
s : PullbackCone g f
m : s.pt ⟶ t.pt
h₁ : m ≫ t.snd = s.fst
h₂ : m ≫ t.fst = s.snd
⊢ m = (fun (s : PullbackCone g f) ↦ (ht.lift s.flip : s.flip.pt ⟶ t.pt)) s
have h₀ : m ≫ t.fst = (fun (s : PullbackCone g f) ↦ (ht.lift s.flip : s.flip.pt ⟶ t.pt)) s ≫ t.fst
Tactic: apply IsLimit.hom_ext ht
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
s : PullbackCone g f
m : s.pt ⟶ t.pt
h₁ : m ≫ t.snd = s.fst
h₂ : m ≫ t.fst = s.snd
h₀ : m ≫ t.fst = (fun (s : PullbackCone g f) ↦ (ht.lift s.flip : s.flip.pt ⟶ t.pt)) s ≫ t.fst
⊢ m = (fun (s : PullbackCone g f) ↦ (ht.lift s.flip : s.flip.pt ⟶ t.pt)) s
have h₃ : m ≫ t.snd = (fun (s : PullbackCone g f) ↦ (ht.lift s.flip : s.flip.pt ⟶ t.pt)) s ≫ t.snd
Tactic: apply IsLimit.hom_ext ht
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
⊢ t.ι.app WalkingSpan.zero = f ≫ t.inl
have w : (span f g).map fst ≫ t.ι.app WalkingSpan.left =
  t.ι.app WalkingSpan.zero ≫ Functor.map (Functor.obj (Functor.const WalkingSpan) t.pt) fst
Tactic: have w := t.ι.naturality WalkingSpan.Hom.fst
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f_1 : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f_1 ≫ inl = g ≫ inr
f : Quiver.Hom (V := WalkingSpan) none none
⊢ Eq (α := (span f_1 g).obj none ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) none)
    ((span f_1 g).map f ≫
      Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x) none (f_1 ≫ inl)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f_1 g).obj (some x) ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some x)) j'
          inl inr)
    ((Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x) none (f_1 ≫ inl)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f_1 g).obj (some x) ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some x)) j'
          inl inr) ≫
      Functor.map (Functor.obj (Functor.const WalkingSpan) W) f)
have none : Eq (α := (span f_1 g).obj none ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) none)
  ((span f_1 g).map (WidePushoutShape.Hom.id none) ≫
    Option.casesOn (motive := fun (x : WalkingSpan) ↦
      (span f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x) none (f_1 ≫ inl)
      fun (j' : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
        (span f_1 g).obj (some x) ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some x)) j'
        inl inr)
  ((Option.casesOn (motive := fun (x : WalkingSpan) ↦
      (span f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x) none (f_1 ≫ inl)
      fun (j' : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
        (span f_1 g).obj (some x) ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some x)) j'
        inl inr) ≫
    Functor.map (Functor.obj (Functor.const WalkingSpan) W) (WidePushoutShape.Hom.id none))
Tactic: cases f
Cleared hypotheses: f