awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : none ⟶ some WalkingPair.left
⊢ Eq (α :=
    (span f_1 g).obj none ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some WalkingPair.left))
    ((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)
        (some WalkingPair.left) (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) (some WalkingPair.left))
  ((span f_1 g).map (init WalkingPair.left) ≫
    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)
      (some WalkingPair.left) (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) (init WalkingPair.left))
Tactic: cases f
Cleared hypotheses: f
-- 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 : none ⟶ some WalkingPair.right
⊢ Eq (α :=
    (span f_1 g).obj none ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some WalkingPair.right))
    ((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)
        (some WalkingPair.right) (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) (some WalkingPair.right))
  ((span f_1 g).map (init WalkingPair.right) ≫
    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)
      (some WalkingPair.right) (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) (init WalkingPair.right))
Tactic: cases f
Cleared hypotheses: f
-- 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 : some WalkingPair.left ⟶ some WalkingPair.left
⊢ Eq (α :=
    (span f_1 g).obj (some WalkingPair.left) ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some WalkingPair.left))
    ((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)
        (some WalkingPair.left) (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)
        (some WalkingPair.left) (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 some : Eq (α :=
  (span f_1 g).obj (some WalkingPair.left) ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some WalkingPair.left))
  ((span f_1 g).map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
    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)
      (some WalkingPair.left) (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)
      (some WalkingPair.left) (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 (some WalkingPair.left)))
Tactic: cases f
Cleared hypotheses: f
-- 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 : some WalkingPair.right ⟶ some WalkingPair.right
⊢ Eq (α :=
    (span f_1 g).obj (some WalkingPair.right) ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some WalkingPair.right))
    ((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)
        (some WalkingPair.right) (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)
        (some WalkingPair.right) (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 some : Eq (α :=
  (span f_1 g).obj (some WalkingPair.right) ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some WalkingPair.right))
  ((span f_1 g).map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
    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)
      (some WalkingPair.right) (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)
      (some WalkingPair.right) (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 (some WalkingPair.right)))
Tactic: cases f
Cleared hypotheses: f
-- 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 ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ Eq (α := (span f g).obj none ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) none)
    ((span f g).map (WidePushoutShape.Hom.id none) ≫
      Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x) none (f ≫ inl)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f 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 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x) none (f ≫ inl)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f 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))
have none : (span f g).map (𝟙 none) ≫ f ≫ inl = (f ≫ inl) ≫ 𝟙 W
Tactic: dsimp
-- 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 ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ Eq (α :=
    (span f g).obj none ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some WalkingPair.left))
    ((span f g).map (init WalkingPair.left) ≫
      Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x)
        (some WalkingPair.left) (f ≫ inl) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f 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 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x) none (f ≫ inl)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f 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) (init WalkingPair.left))
have none : f ≫ inl = (f ≫ inl) ≫ 𝟙 W
Tactic: dsimp
-- 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 ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ Eq (α :=
    (span f g).obj none ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some WalkingPair.right))
    ((span f g).map (init WalkingPair.right) ≫
      Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x)
        (some WalkingPair.right) (f ≫ inl) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f 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 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x) none (f ≫ inl)
        fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f 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) (init WalkingPair.right))
have none : g ≫ inr = (f ≫ inl) ≫ 𝟙 W
Tactic: dsimp
-- 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 ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ Eq (α :=
    (span f g).obj (some WalkingPair.left) ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some WalkingPair.left))
    ((span f g).map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
      Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x)
        (some WalkingPair.left) (f ≫ inl) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f 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 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x)
        (some WalkingPair.left) (f ≫ inl) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f 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 (some WalkingPair.left)))
have some : (span f g).map (𝟙 (some WalkingPair.left)) ≫ inl = inl ≫ 𝟙 W
Tactic: dsimp
-- 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 ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ Eq (α :=
    (span f g).obj (some WalkingPair.right) ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) (some WalkingPair.right))
    ((span f g).map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
      Option.casesOn (motive := fun (x : WalkingSpan) ↦
        (span f g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x)
        (some WalkingPair.right) (f ≫ inl) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f 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 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) W) x)
        (some WalkingPair.right) (f ≫ inl) fun (j' : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f 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 (some WalkingPair.right)))
have some : (span f g).map (𝟙 (some WalkingPair.right)) ≫ inr = inr ≫ 𝟙 W
Tactic: dsimp
-- 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 ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
W : C
k l : t.pt ⟶ W
h₀ : t.inl ≫ k = t.inl ≫ l
h₁ : t.inr ≫ k = t.inr ≫ l
⊢ Eq (α := (span f g).obj none ⟶ W) (t.ι.app none ≫ k) (t.ι.app none ≫ l)
have rw : ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ k = ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ l
Tactic: rw [← t.w fst, Category.assoc, Category.assoc, 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 ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
W : C
k l : t.pt ⟶ W
h₀ : t.inl ≫ k = t.inl ≫ l
h₁ : t.inr ≫ k = t.inr ≫ l
rw : ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ k = ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ l
⊢ Eq (α := (span f g).obj none ⟶ W) (t.ι.app none ≫ k) (t.ι.app none ≫ l)
have rw₁ : (span f g).map fst ≫ t.ι.app WalkingSpan.left ≫ k = ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ l
Tactic: rw [← t.w fst, Category.assoc, Category.assoc, 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 ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
W : C
k l : t.pt ⟶ W
h₀ : t.inl ≫ k = t.inl ≫ l
h₁ : t.inr ≫ k = t.inr ≫ l
rw : ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ k = ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ l
rw₁ : (span f g).map fst ≫ t.ι.app WalkingSpan.left ≫ k = ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ l
⊢ Eq (α := (span f g).obj none ⟶ W) (t.ι.app none ≫ k) (t.ι.app none ≫ l)
have rw₂ : (span f g).map fst ≫ t.ι.app WalkingSpan.left ≫ k = (span f g).map fst ≫ t.ι.app WalkingSpan.left ≫ l
Tactic: rw [← t.w fst, Category.assoc, Category.assoc, 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 ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
W : C
k l : t.pt ⟶ W
h₀ : t.inl ≫ k = t.inl ≫ l
h₁ : t.inr ≫ k = t.inr ≫ l
rw : ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ k = ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ l
rw₁ : (span f g).map fst ≫ t.ι.app WalkingSpan.left ≫ k = ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ l
rw₂ : (span f g).map fst ≫ t.ι.app WalkingSpan.left ≫ k = (span f g).map fst ≫ t.ι.app WalkingSpan.left ≫ l
⊢ Eq (α := (span f g).obj none ⟶ W) (t.ι.app none ≫ k) (t.ι.app none ≫ l)
have rw₃ : (span f g).map fst ≫ t.inl ≫ l = (span f g).map fst ≫ t.ι.app WalkingSpan.left ≫ l
Tactic: rw [← t.w fst, Category.assoc, Category.assoc, 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 ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
s : PushoutCocone g f
m : t.pt ⟶ s.pt
h₁ : t.inr ≫ m = s.inl
h₂ : t.inl ≫ m = s.inr
⊢ m = (fun (s : PushoutCocone g f) ↦ (ht.desc s.flip : t.pt ⟶ s.flip.pt)) s
have h₀ : t.inl ≫ m = t.inl ≫ (fun (s : PushoutCocone g f) ↦ (ht.desc s.flip : t.pt ⟶ s.flip.pt)) s
Tactic: apply IsColimit.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 ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
s : PushoutCocone g f
m : t.pt ⟶ s.pt
h₁ : t.inr ≫ m = s.inl
h₂ : t.inl ≫ m = s.inr
h₀ : t.inl ≫ m = t.inl ≫ (fun (s : PushoutCocone g f) ↦ (ht.desc s.flip : t.pt ⟶ s.flip.pt)) s
⊢ m = (fun (s : PushoutCocone g f) ↦ (ht.desc s.flip : t.pt ⟶ s.flip.pt)) s
have h₃ : t.inr ≫ m = t.inr ≫ (fun (s : PushoutCocone g f) ↦ (ht.desc s.flip : t.pt ⟶ s.flip.pt)) s
Tactic: apply IsColimit.hom_ext ht
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
W : MorphismProperty.{v_1, u_1} C₁
F : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
hF : W.IsInvertedBy F
G : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
⊢ IsIso ((F ⋙ G).map f)
have this : IsIso (F.map f)
Tactic: haveI := hF f hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
W : MorphismProperty.{v_1, u_1} C₁
F : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
hF : W.IsInvertedBy F
G : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (F.map f)
⊢ IsIso ((F ⋙ G).map f)
have dsimp : IsIso (G.map (F.map f))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} C D
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
⊢ IsIso (L.op.map f)
have this : IsIso (L.map f.unop)
Tactic: haveI := h f.unop hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} Cᵒᵖ D
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (L.rightOp.map f)
have this : IsIso (L.map f.op)
Tactic: haveI := h f.op hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} C Dᵒᵖ
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
⊢ IsIso (L.leftOp.map f)
have this : IsIso (L.map f.unop)
Tactic: haveI := h f.unop hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} C Dᵒᵖ
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
this : IsIso (L.map f.unop)
⊢ IsIso (L.leftOp.map f)
have dsimp : IsIso (L.map f.unop).unop
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} Cᵒᵖ Dᵒᵖ
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (L.unop.map f)
have this : IsIso (L.map f.op)
Tactic: haveI := h f.op hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
L : Functor.{v, v', u, u'} Cᵒᵖ Dᵒᵖ
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
⊢ IsIso (L.unop.map f)
have dsimp : IsIso (L.map f.op).unop
Tactic: dsimp