awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
⊢ IsConnected.{0, u_2} (StructuredArrow d (sequentialFunctor J))
have h : ∀ (j₁ j₂ : StructuredArrow d (sequentialFunctor J)),
  ∃ (l : List (StructuredArrow d (sequentialFunctor J))), List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast sorry = j₂
Tactic: apply isConnected_of_zigzag
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
⊢ ∀ (j₁ j₂ : StructuredArrow d (sequentialFunctor J)),
    ∃ (l : List (StructuredArrow d (sequentialFunctor J))), List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
have h : ∀ (i j : StructuredArrow d (sequentialFunctor J)), List.IsChain Zag [i, j] ∧ [i, j].getLast sorry = j
Tactic: refine fun i j ↦ ⟨[j], ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
⊢ List.IsChain Zag [i, j] ∧ [i, j].getLast ⋯ = j
have h : Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
Tactic: simp only [List.isChain_cons_cons, Zag, List.isChain_singleton, and_true, ne_eq,
      not_false_eq_true, List.getLast_cons, List.getLast_singleton', reduceCtorEq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
have h : ∀
  (this :
    ∀ (J : Type u_2) [inst : Countable J] [inst_3 : Preorder J] [inst_4 : IsFiltered J] (d : J) (n : ℕ)
      (g : d ≤ Functor.obj (sequentialFunctor J) n)
      (this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J)))
      (i j : StructuredArrow d (sequentialFunctor J)) (h : j.right ≤ i.right), Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i))
  (h : i.right < j.right), Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
Tactic: wlog! h : j.right ≤ i.right
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
h :
  ∀
    (this :
      ∀ (J : Type u_2) [inst : Countable J] [inst_3 : Preorder J] [inst_4 : IsFiltered J] (d : J) (n : ℕ)
        (g : d ≤ Functor.obj (sequentialFunctor J) n)
        (this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J)))
        (i j : StructuredArrow d (sequentialFunctor J)) (h : j.right ≤ i.right), Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i))
    (h : i.right < j.right), Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
have wlog! : ∀ (J : Type u_2) [inst : Countable J] [inst_3 : Preorder J] [inst_4 : IsFiltered J] (d : J) (n : ℕ)
  (g : d ≤ Functor.obj (sequentialFunctor J) n)
  (this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J)))
  (i j : StructuredArrow d (sequentialFunctor J)) (h : j.right ≤ i.right), Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
Tactic: wlog! h : j.right ≤ i.right
Cleared hypotheses: d, n, g, this, i, j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
J_1 : Type u_2
inst : Countable J_1
inst_1 : Preorder J_1
inst_2 : IsFiltered J_1
J : Type u_2
inst_3 : Countable J
inst_4 : Preorder J
inst_5 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
h : j.right ≤ i.right
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
have h₁ : Nonempty (j ⟶ i)
Tactic: right
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsCofiltered J
j : J
⊢ ∃ (n : ℕ), sequentialFunctor_obj J n ≤ j
have obtain : ∀ (m : ℕ) (h : sorry.choose (p := Function.Surjective) m = j), ∃ (n : ℕ), sequentialFunctor_obj J n ≤ j
Tactic: obtain ⟨m, h⟩ := (exists_surjective_nat _).choose_spec j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsCofiltered J
j : J
m : ℕ
h : ⋯.choose (p := Function.Surjective) m = j
⊢ ∃ (n : ℕ), sequentialFunctor_obj J n ≤ j
have refine : sequentialFunctor_obj J (m + 1) ≤ j
Tactic: refine ⟨m + 1, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsCofiltered J
d : J
⊢ IsConnected.{0, u_2} (CostructuredArrow (sequentialFunctor J) d)
have obtain : ∀ (n : ℕ) (g : Functor.obj (sequentialFunctor J) (op n) ≤ d),
  IsConnected.{0, u_2} (CostructuredArrow (sequentialFunctor J) d)
Tactic: obtain ⟨n, (g : (sequentialFunctor J).obj ⟨n⟩ ≤ d)⟩ := sequentialFunctor_initial_aux J d
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
⊢ IsConnected.{0, u_2} (CostructuredArrow (sequentialFunctor J) d)
have this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
Tactic: have : Nonempty (CostructuredArrow (sequentialFunctor J) d) :=
      ⟨CostructuredArrow.mk (homOfLE g)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
⊢ IsConnected.{0, u_2} (CostructuredArrow (sequentialFunctor J) d)
have h : ∀ (j₁ j₂ : CostructuredArrow (sequentialFunctor J) d),
  ∃ (l : List (CostructuredArrow (sequentialFunctor J) d)), List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast sorry = j₂
Tactic: apply isConnected_of_zigzag
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
⊢ ∀ (j₁ j₂ : CostructuredArrow (sequentialFunctor J) d),
    ∃ (l : List (CostructuredArrow (sequentialFunctor J) d)), List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
have h : ∀ (i j : CostructuredArrow (sequentialFunctor J) d), List.IsChain Zag [i, j] ∧ [i, j].getLast sorry = j
Tactic: refine fun i j ↦ ⟨[j], ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
⊢ List.IsChain Zag [i, j] ∧ [i, j].getLast ⋯ = j
have h : Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
Tactic: simp only [List.isChain_cons_cons, Zag, List.isChain_singleton, and_true, ne_eq,
      not_false_eq_true, List.getLast_cons, List.getLast_singleton', reduceCtorEq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
have h : ∀
  (this :
    ∀ (J : Type u_2) [inst : Countable J] [inst_3 : Preorder J] [inst_4 : IsCofiltered J] (d : J) (n : ℕ)
      (g : Functor.obj (sequentialFunctor J) (op n) ≤ d)
      (this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d))
      (i j : CostructuredArrow (sequentialFunctor J) d) (h : unop i.left ≤ unop j.left),
      Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i))
  (h : unop j.left < unop i.left), Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
Tactic: wlog! h : (unop i.left) ≤ (unop j.left)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
h :
  ∀
    (this :
      ∀ (J : Type u_2) [inst : Countable J] [inst_3 : Preorder J] [inst_4 : IsCofiltered J] (d : J) (n : ℕ)
        (g : Functor.obj (sequentialFunctor J) (op n) ≤ d)
        (this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d))
        (i j : CostructuredArrow (sequentialFunctor J) d) (h : unop i.left ≤ unop j.left),
        Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i))
    (h : unop j.left < unop i.left), Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
have wlog! : ∀ (J : Type u_2) [inst : Countable J] [inst_3 : Preorder J] [inst_4 : IsCofiltered J] (d : J) (n : ℕ)
  (g : Functor.obj (sequentialFunctor J) (op n) ≤ d)
  (this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d))
  (i j : CostructuredArrow (sequentialFunctor J) d) (h : unop i.left ≤ unop j.left), Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
Tactic: wlog! h : (unop i.left) ≤ (unop j.left)
Cleared hypotheses: d, n, g, this, i, j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
J_1 : Type u_2
inst : Countable J_1
inst_1 : Preorder J_1
inst_2 : IsCofiltered J_1
J : Type u_2
inst_3 : Countable J
inst_4 : Preorder J
inst_5 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
h : unop i.left ≤ unop j.left
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
have h₁ : Nonempty (j ⟶ i)
Tactic: right
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
inst_1 : HasPullback f f
inst_2 : Mono f
⊢ IsIso (Y := diagonalObj f) (diagonal f)
have rw : IsIso (Y := diagonalObj f) (inv (fst f f))
Tactic: rw [(IsIso.inv_eq_of_inv_hom_id (diagonal_fst f)).symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullback f f
H : IsIso (Y := diagonalObj f) (diagonal f)
Z : C
x x_1 : Z ⟶ X
e : x ≫ f = x_1 ≫ f
⊢ x = x_1
have rw : CategoryStruct.comp (Y := pullback f f) (lift x x_1 e) (fst f f) = x_1
Tactic: rw [← lift_fst _ _ e, (cancel_epi (g := fst f f) (h := snd f f)
    (diagonal f)).mp (by simp), lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullback f f
H : IsIso (Y := diagonalObj f) (diagonal f)
Z : C
x x_1 : Z ⟶ X
e : x ≫ f = x_1 ≫ f
rw : CategoryStruct.comp (Y := pullback f f) (lift x x_1 e) (fst f f) = x_1
⊢ x = x_1
have rw₁ : CategoryStruct.comp (Y := pullback f f) (lift x x_1 e) (snd f f) = x_1
Tactic: rw [← lift_fst _ _ e, (cancel_epi (g := fst f f) (h := snd f f)
    (diagonal f)).mp (by simp), lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullback f f
H : IsIso (Y := diagonalObj f) (diagonal f)
Z : C
x x_1 : Z ⟶ X
e : x ≫ f = x_1 ≫ f
rw : CategoryStruct.comp (Y := pullback f f) (lift x x_1 e) (fst f f) = x_1
rw₁ : CategoryStruct.comp (Y := pullback f f) (lift x x_1 e) (snd f f) = x_1
⊢ x = x_1
have rw₂ : x_1 = x_1
Tactic: rw [← lift_fst _ _ e, (cancel_epi (g := fst f f) (h := snd f f)
    (diagonal f)).mp (by simp), lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
| fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯)
have rw : fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫ 𝟙 X
Tactic: rw [← Category.comp_id (pullback.fst _ _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      X)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
have conv_rhs : Eq (α :=
  pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
    X)
  (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
    fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i)
  (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫ 𝟙 X)
Tactic: conv_rhs => rw [← Category.comp_id (pullback.fst _ _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      X)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X)
have rw : Eq (α :=
  pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
    X)
  (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
    fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i)
  (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
    CategoryStruct.comp (Y := diagonalObj f) (diagonal f) (fst f f))
Tactic: rw [← diagonal_fst f, pullback.condition_assoc, pullback.lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
rw :
  Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      X)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      CategoryStruct.comp (Y := diagonalObj f) (diagonal f) (fst f f))
⊢ Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      X)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X)
have rw₁ : Eq (α :=
  pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
    X)
  (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
    fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i)
  (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
    CategoryStruct.comp (Y := diagonalObj f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry)
      (fst f f))
Tactic: rw [← diagonal_fst f, pullback.condition_assoc, pullback.lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
rw :
  Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      X)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      CategoryStruct.comp (Y := diagonalObj f) (diagonal f) (fst f f))
rw₁ :
  Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      X)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      CategoryStruct.comp (Y := diagonalObj f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) (fst f f))
⊢ Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      X)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X)
have rw₂ : Eq (α :=
  pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
    X)
  (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
    fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i)
  (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
    fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i)
Tactic: rw [← diagonal_fst f, pullback.condition_assoc, pullback.lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      X)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
have conv_rhs : Eq (α :=
  pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
    X)
  (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
    snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i)
  (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫ 𝟙 X)
Tactic: conv_rhs => rw [← Category.comp_id (pullback.fst _ _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      X)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X)
have rw : Eq (α :=
  pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
    X)
  (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
    snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i)
  (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
    CategoryStruct.comp (Y := diagonalObj f) (diagonal f) (snd f f))
Tactic: rw [← diagonal_snd f, pullback.condition_assoc, pullback.lift_snd]