awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f : J → (X_1 ⟶ Y)
X : WalkingParallelPair
⊢ Functor.obj
      (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
        (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
      X =
    Functor.obj (𝟭 WalkingParallelPair) X
have zero : Functor.obj
    (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
      (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
      (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
        bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
    WalkingParallelPair.zero =
  Functor.obj (𝟭 WalkingParallelPair) WalkingParallelPair.zero
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f : J → (X_1 ⟶ Y)
X : WalkingParallelPair
zero :
  Functor.obj
      (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
        (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
      WalkingParallelPair.zero =
    Functor.obj (𝟭 WalkingParallelPair) WalkingParallelPair.zero
⊢ Functor.obj
      (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
        (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
      X =
    Functor.obj (𝟭 WalkingParallelPair) X
have one : Functor.obj
    (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
      (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
      (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
        bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
    WalkingParallelPair.one =
  Functor.obj (𝟭 WalkingParallelPair) WalkingParallelPair.one
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Trident f
j : J
⊢ Eq (α :=
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt)
        zero ⟶
      Y)
    (s.π.app zero ≫ f j :
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
          (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt) zero ⟶
        Y)
    (s.π.app one :
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
          (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt) one ⟶
        (parallelFamily f).obj one)
have rw : s.π.app zero ≫ f j = s.π.app zero ≫ (parallelFamily f).map (line j)
Tactic: rw [← s.w (line j), parallelFamily_map_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Trident f
j : J
rw : s.π.app zero ≫ f j = s.π.app zero ≫ (parallelFamily f).map (line j)
⊢ Eq (α :=
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt)
        zero ⟶
      Y)
    (s.π.app zero ≫ f j :
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
          (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt) zero ⟶
        Y)
    (s.π.app one :
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
          (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt) one ⟶
        (parallelFamily f).obj one)
have rw₁ : Eq (α :=
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt)
      zero ⟶
    Y)
  (s.π.app zero ≫ f j) (s.π.app zero ≫ f j)
Tactic: rw [← s.w (line j), parallelFamily_map_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Cotrident f
j : J
⊢ Eq.{v + 1} (α :=
    X ⟶
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
        (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt) one)
    (f j ≫ s.ι.app one) (s.ι.app zero)
have rw : f j ≫ s.ι.app one = (parallelFamily f).map (line j) ≫ s.ι.app one
Tactic: rw [← s.w (line j), parallelFamily_map_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Cotrident f
j : J
rw : f j ≫ s.ι.app one = (parallelFamily f).map (line j) ≫ s.ι.app one
⊢ Eq.{v + 1} (α :=
    X ⟶
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
        (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt) one)
    (f j ≫ s.ι.app one) (s.ι.app zero)
have rw₁ : Eq.{v + 1} (α :=
  X ⟶
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) s.pt)
      one)
  (f j ≫ s.ι.app one) (f j ≫ s.ι.app one)
Tactic: rw [← s.w (line j), parallelFamily_map_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : J → (X ⟶ Y)
inst_1 : Nonempty J
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f_1 j₁ = ι ≫ f_1 j₂
i j : WalkingParallelFamily J
f : i ⟶ j
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i ⟶ (parallelFamily f_1).obj j)
    (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) f ≫
      WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶
          (parallelFamily f_1).obj x)
        j ι (ι ≫ f_1 (Classical.arbitrary J)))
    (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶
          (parallelFamily f_1).obj x)
        i ι (ι ≫ f_1 (Classical.arbitrary J)) ≫
      (parallelFamily f_1).map f)
have id : Eq.{v + 1} (α :=
  Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i ⟶ (parallelFamily f_1).obj i)
  (CategoryStruct.comp (Y := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i)
    (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) (Hom.id i))
    (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶ (parallelFamily f_1).obj x)
      i ι (ι ≫ f_1 (Classical.arbitrary J))))
  (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶ (parallelFamily f_1).obj x)
      i ι (ι ≫ f_1 (Classical.arbitrary J)) ≫
    (parallelFamily f_1).map (Hom.id i))
Tactic: obtain - | k := f
Cleared hypotheses: j, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : J → (X ⟶ Y)
inst_1 : Nonempty J
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f_1 j₁ = ι ≫ f_1 j₂
i j : WalkingParallelFamily J
f : i ⟶ j
id :
  Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i ⟶ (parallelFamily f_1).obj i)
    (CategoryStruct.comp (Y := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i)
      (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) (Hom.id i))
      (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶
          (parallelFamily f_1).obj x)
        i ι (ι ≫ f_1 (Classical.arbitrary J))))
    (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶
          (parallelFamily f_1).obj x)
        i ι (ι ≫ f_1 (Classical.arbitrary J)) ≫
      (parallelFamily f_1).map (Hom.id i))
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i ⟶ (parallelFamily f_1).obj j)
    (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) f ≫
      WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶
          (parallelFamily f_1).obj x)
        j ι (ι ≫ f_1 (Classical.arbitrary J)))
    (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶
          (parallelFamily f_1).obj x)
        i ι (ι ≫ f_1 (Classical.arbitrary J)) ≫
      (parallelFamily f_1).map f)
have line : ∀ (k : J),
  Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) P)
        zero ⟶
      (parallelFamily f_1).obj one)
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) P)
        one)
      (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) (line k))
      (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶
          (parallelFamily f_1).obj x)
        one ι (ι ≫ f_1 (Classical.arbitrary J))))
    (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x ⟶
          (parallelFamily f_1).obj x)
        zero ι (ι ≫ f_1 (Classical.arbitrary J)) ≫
      (parallelFamily f_1).map (line k))
Tactic: obtain - | k := f
Cleared hypotheses: i, j, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : J → (X ⟶ Y)
inst_1 : Nonempty J
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f_1 j₁ ≫ π = f_1 j₂ ≫ π
i j : WalkingParallelFamily J
f : i ⟶ j
⊢ Eq (α :=
    (parallelFamily f_1).obj i ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) j)
    ((parallelFamily f_1).map f ≫
      WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f_1).obj x ⟶
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        j (f_1 (Classical.arbitrary J) ≫ π) π)
    (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f_1).obj x ⟶
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        i (f_1 (Classical.arbitrary J) ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) f)
have id : Eq (α :=
  (parallelFamily f_1).obj i ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i)
  ((parallelFamily f_1).map (Hom.id i) ≫
    WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
      (parallelFamily f_1).obj x ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
      i (f_1 (Classical.arbitrary J) ≫ π) π)
  (CategoryStruct.comp (Y := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i)
    (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
      (parallelFamily f_1).obj x ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
      i (f_1 (Classical.arbitrary J) ≫ π) π)
    (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) (Hom.id i)))
Tactic: obtain - | k := f
Cleared hypotheses: j, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : J → (X ⟶ Y)
inst_1 : Nonempty J
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f_1 j₁ ≫ π = f_1 j₂ ≫ π
i j : WalkingParallelFamily J
f : i ⟶ j
id :
  Eq (α :=
    (parallelFamily f_1).obj i ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i)
    ((parallelFamily f_1).map (Hom.id i) ≫
      WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f_1).obj x ⟶
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        i (f_1 (Classical.arbitrary J) ≫ π) π)
    (CategoryStruct.comp (Y := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) i)
      (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f_1).obj x ⟶
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        i (f_1 (Classical.arbitrary J) ≫ π) π)
      (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) (Hom.id i)))
⊢ Eq (α :=
    (parallelFamily f_1).obj i ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) j)
    ((parallelFamily f_1).map f ≫
      WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f_1).obj x ⟶
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        j (f_1 (Classical.arbitrary J) ≫ π) π)
    (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f_1).obj x ⟶
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        i (f_1 (Classical.arbitrary J) ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) f)
have line : ∀ (k : J),
  Eq (α :=
    (parallelFamily f_1).obj zero ⟶
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) P)
        one)
    ((parallelFamily f_1).map (line k) ≫
      WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f_1).obj x ⟶
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        one (f_1 (Classical.arbitrary J) ≫ π) π)
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) P)
        zero)
      (WalkingParallelFamily.casesOn (motive := fun (x : WalkingParallelFamily J) ↦
        (parallelFamily f_1).obj x ⟶
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WalkingParallelFamily J)) P) x)
        zero (f_1 (Classical.arbitrary J) ≫ π) π)
      (Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) P) (line k)))
Tactic: obtain - | k := f
Cleared hypotheses: i, j, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j₁ j₂ : J
t : Trident f
⊢ t.ι ≫ f j₁ = t.ι ≫ f j₂
have rw : t.π.app one = t.ι ≫ f j₂
Tactic: rw [t.app_zero, t.app_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j₁ j₂ : J
t : Trident f
rw : t.π.app one = t.ι ≫ f j₂
⊢ t.ι ≫ f j₁ = t.ι ≫ f j₂
have rw₁ : Eq (α :=
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt)
      zero ⟶
    Y)
  (t.π.app one :
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt)
        one ⟶
      (parallelFamily f).obj one)
  (t.π.app one)
Tactic: rw [t.app_zero, t.app_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j₁ j₂ : J
t : Cotrident f
⊢ f j₁ ≫ t.π = f j₂ ≫ t.π
have rw : t.ι.app zero = f j₂ ≫ t.π
Tactic: rw [t.app_one, t.app_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j₁ j₂ : J
t : Cotrident f
rw : t.ι.app zero = f j₂ ≫ t.π
⊢ f j₁ ≫ t.π = f j₂ ≫ t.π
have rw₁ : Eq (α :=
  X ⟶
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J) (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt)
      one)
  (t.ι.app zero :
    (parallelFamily f).obj zero ⟶
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
        (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) zero)
  (t.ι.app zero)
Tactic: rw [t.app_one, t.app_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
s : Trident f
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ Eq (α := W ⟶ (parallelFamily f).obj one) (k ≫ s.π.app one) (l ≫ s.π.app one)
have rw : Eq (α := W ⟶ (parallelFamily f).obj one) (k ≫ s.π.app zero ≫ f (Classical.arbitrary J))
  (l ≫ s.π.app zero ≫ f (Classical.arbitrary J))
Tactic: rw [← s.app_zero (Classical.arbitrary J), reassoc_of% h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
s : Trident f
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
rw :
  Eq (α := W ⟶ (parallelFamily f).obj one) (k ≫ s.π.app zero ≫ f (Classical.arbitrary J))
    (l ≫ s.π.app zero ≫ f (Classical.arbitrary J))
⊢ Eq (α := W ⟶ (parallelFamily f).obj one) (k ≫ s.π.app one) (l ≫ s.π.app one)
have rw₁ : l ≫ s.ι ≫ f (Classical.arbitrary J) = l ≫ s.π.app zero ≫ f (Classical.arbitrary J)
Tactic: rw [← s.app_zero (Classical.arbitrary J), reassoc_of% h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
s : Cotrident f
W : C
k l : s.pt ⟶ W
h : s.π ≫ k = s.π ≫ l
⊢ Eq (α := (parallelFamily f).obj zero ⟶ W) (s.ι.app zero ≫ k) (s.ι.app zero ≫ l)
have rw : (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ k = (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ l
Tactic: rw [← s.app_one (Classical.arbitrary J), Category.assoc, Category.assoc, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
s : Cotrident f
W : C
k l : s.pt ⟶ W
h : s.π ≫ k = s.π ≫ l
rw : (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ k = (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ l
⊢ Eq (α := (parallelFamily f).obj zero ⟶ W) (s.ι.app zero ≫ k) (s.ι.app zero ≫ l)
have rw₁ : f (Classical.arbitrary J) ≫ s.ι.app one ≫ k = (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ l
Tactic: rw [← s.app_one (Classical.arbitrary J), Category.assoc, Category.assoc, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
s : Cotrident f
W : C
k l : s.pt ⟶ W
h : s.π ≫ k = s.π ≫ l
rw : (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ k = (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ l
rw₁ : f (Classical.arbitrary J) ≫ s.ι.app one ≫ k = (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ l
⊢ Eq (α := (parallelFamily f).obj zero ⟶ W) (s.ι.app zero ≫ k) (s.ι.app zero ≫ l)
have rw₂ : Eq.{v + 1} (α := (parallelFamily f).obj zero ⟶ W) (f (Classical.arbitrary J) ≫ s.ι.app one ≫ k)
  (f (Classical.arbitrary J) ≫ s.ι.app one ≫ l)
Tactic: rw [← s.app_one (Classical.arbitrary J), Category.assoc, Category.assoc, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
s : Cotrident f
W : C
k l : s.pt ⟶ W
h : s.π ≫ k = s.π ≫ l
rw : (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ k = (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ l
rw₁ : f (Classical.arbitrary J) ≫ s.ι.app one ≫ k = (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ l
rw₂ :
  Eq.{v + 1} (α := (parallelFamily f).obj zero ⟶ W) (f (Classical.arbitrary J) ≫ s.ι.app one ≫ k)
    (f (Classical.arbitrary J) ≫ s.ι.app one ≫ l)
⊢ Eq (α := (parallelFamily f).obj zero ⟶ W) (s.ι.app zero ≫ k) (s.ι.app zero ≫ l)
have rw₃ : f (Classical.arbitrary J) ≫ s.π ≫ l = f (Classical.arbitrary J) ≫ s.ι.app one ≫ l
Tactic: rw [← s.app_one (Classical.arbitrary J), Category.assoc, Category.assoc, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
t : Trident f
lift : (s : Trident f) → s.pt ⟶ t.pt
fac : ∀ (s : Trident f), lift s ≫ t.ι = s.ι
uniq : ∀ (s : Trident f) (m : s.pt ⟶ t.pt), (∀ (j : WalkingParallelFamily J), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (parallelFamily f)
j : WalkingParallelFamily J
⊢ Eq (α := s.pt ⟶ (parallelFamily f).obj one) (lift s ≫ t.π.app one) (s.π.app one)
have rw : lift s ≫ t.π.app zero ≫ (parallelFamily f).map (line (Classical.arbitrary J)) = s.π.app one
Tactic: rw [← t.w (line (Classical.arbitrary J)), reassoc_of% fac, s.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
t : Trident f
lift : (s : Trident f) → s.pt ⟶ t.pt
fac : ∀ (s : Trident f), lift s ≫ t.ι = s.ι
uniq : ∀ (s : Trident f) (m : s.pt ⟶ t.pt), (∀ (j : WalkingParallelFamily J), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (parallelFamily f)
j : WalkingParallelFamily J
rw : lift s ≫ t.π.app zero ≫ (parallelFamily f).map (line (Classical.arbitrary J)) = s.π.app one
⊢ Eq (α := s.pt ⟶ (parallelFamily f).obj one) (lift s ≫ t.π.app one) (s.π.app one)
have rw₁ : ι s ≫ (parallelFamily f).map (line (Classical.arbitrary J)) = s.π.app one
Tactic: rw [← t.w (line (Classical.arbitrary J)), reassoc_of% fac, s.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
t : Trident f
lift : (s : Trident f) → s.pt ⟶ t.pt
fac : ∀ (s : Trident f), lift s ≫ t.ι = s.ι
uniq : ∀ (s : Trident f) (m : s.pt ⟶ t.pt), (∀ (j : WalkingParallelFamily J), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (parallelFamily f)
j : WalkingParallelFamily J
rw : lift s ≫ t.π.app zero ≫ (parallelFamily f).map (line (Classical.arbitrary J)) = s.π.app one
rw₁ : ι s ≫ (parallelFamily f).map (line (Classical.arbitrary J)) = s.π.app one
⊢ Eq (α := s.pt ⟶ (parallelFamily f).obj one) (lift s ≫ t.π.app one) (s.π.app one)
have rw₂ : Eq (α := s.pt ⟶ (parallelFamily f).obj one) (s.π.app one) (s.π.app one)
Tactic: rw [← t.w (line (Classical.arbitrary J)), reassoc_of% fac, s.w]