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 Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
t : Cotrident f
desc : (s : Cotrident f) → t.pt ⟶ s.pt
fac : ∀ (s : Cotrident f), t.π ≫ desc s = s.π
uniq : ∀ (s : Cotrident f) (m : t.pt ⟶ s.pt), (∀ (j : WalkingParallelFamily J), t.ι.app j ≫ m = s.ι.app j) → m = desc s
s : Cocone (parallelFamily f)
j : WalkingParallelFamily J
⊢ Eq (α := (parallelFamily f).obj zero ⟶ s.pt) (t.ι.app zero ≫ desc s) (s.ι.app zero)
have rw : (parallelFamily f).map (line (Classical.arbitrary J)) ≫ t.ι.app one ≫ desc s = s.ι.app zero
Tactic: rw [← t.w_assoc (line (Classical.arbitrary J)), 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 : Cotrident f
desc : (s : Cotrident f) → t.pt ⟶ s.pt
fac : ∀ (s : Cotrident f), t.π ≫ desc s = s.π
uniq : ∀ (s : Cotrident f) (m : t.pt ⟶ s.pt), (∀ (j : WalkingParallelFamily J), t.ι.app j ≫ m = s.ι.app j) → m = desc s
s : Cocone (parallelFamily f)
j : WalkingParallelFamily J
rw : (parallelFamily f).map (line (Classical.arbitrary J)) ≫ t.ι.app one ≫ desc s = s.ι.app zero
⊢ Eq (α := (parallelFamily f).obj zero ⟶ s.pt) (t.ι.app zero ≫ desc s) (s.ι.app zero)
have rw₁ : (parallelFamily f).map (line (Classical.arbitrary J)) ≫ π s = s.ι.app zero
Tactic: rw [← t.w_assoc (line (Classical.arbitrary J)), 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 : Cotrident f
desc : (s : Cotrident f) → t.pt ⟶ s.pt
fac : ∀ (s : Cotrident f), t.π ≫ desc s = s.π
uniq : ∀ (s : Cotrident f) (m : t.pt ⟶ s.pt), (∀ (j : WalkingParallelFamily J), t.ι.app j ≫ m = s.ι.app j) → m = desc s
s : Cocone (parallelFamily f)
j : WalkingParallelFamily J
rw : (parallelFamily f).map (line (Classical.arbitrary J)) ≫ t.ι.app one ≫ desc s = s.ι.app zero
rw₁ : (parallelFamily f).map (line (Classical.arbitrary J)) ≫ π s = s.ι.app zero
⊢ Eq (α := (parallelFamily f).obj zero ⟶ s.pt) (t.ι.app zero ≫ desc s) (s.ι.app zero)
have rw₂ : Eq (α := (parallelFamily f).obj zero ⟶ s.pt) (s.ι.app zero) (s.ι.app zero)
Tactic: rw [← t.w_assoc (line (Classical.arbitrary J)), 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_1 Y : C
f : J → (X_1 ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Trident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
X : WalkingParallelFamily J
⊢ Functor.obj.{w, v, w, u} (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) X = F.obj X
have zero : Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) zero =
  F.obj 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Trident.{w, v, u} (C := C) (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
X : WalkingParallelFamily J
zero :
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.zero =
    F.obj WalkingParallelFamily.zero
⊢ Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) X =
    F.obj X
have one : Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) one =
  F.obj 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Trident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
j j' : WalkingParallelFamily J
g : j ⟶ j'
⊢ Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) g ≫ t.π.app j' ≫ eqToHom ⋯ =
    (t.π.app j ≫ eqToHom ⋯) ≫ F.map g
have id : Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) (Hom.id j) ≫ t.π.app j ≫ eqToHom sorry =
  (t.π.app j ≫ eqToHom sorry) ≫ F.map (Hom.id j)
Tactic: cases g
Cleared hypotheses: j', g
-- 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Trident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
j j' : WalkingParallelFamily J
g : j ⟶ j'
id :
  Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) (Hom.id j) ≫ t.π.app j ≫ eqToHom ⋯ =
    (t.π.app j ≫ eqToHom ⋯) ≫ F.map (Hom.id j)
⊢ Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) g ≫ t.π.app j' ≫ eqToHom ⋯ =
    (t.π.app j ≫ eqToHom ⋯) ≫ F.map g
have line : ∀ (a : J),
  Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) (line a) ≫ t.π.app one ≫ eqToHom sorry =
    (t.π.app zero ≫ eqToHom sorry) ≫ F.map (line a)
Tactic: cases g
Cleared hypotheses: j, j', g
-- 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cotrident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
X : WalkingParallelFamily J
⊢ F.obj X = Functor.obj.{w, v, w, u} (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) X
have zero : F.obj zero =
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cotrident.{w, v, u} (C := C) (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
X : WalkingParallelFamily J
zero :
  F.obj WalkingParallelFamily.zero =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.zero
⊢ F.obj X =
    Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) X
have one : F.obj one =
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cotrident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
j j' : WalkingParallelFamily J
g : j ⟶ j'
⊢ F.map g ≫ eqToHom ⋯ ≫ t.ι.app j' =
    (eqToHom ⋯ ≫ t.ι.app j) ≫ Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) g
have id : F.map (Hom.id j) ≫ eqToHom sorry ≫ t.ι.app j =
  (eqToHom sorry ≫ t.ι.app j) ≫ Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) (Hom.id j)
Tactic: cases g
Cleared hypotheses: j', g
-- 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cotrident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
j j' : WalkingParallelFamily J
g : j ⟶ j'
id :
  F.map (Hom.id j) ≫ eqToHom ⋯ ≫ t.ι.app j =
    (eqToHom ⋯ ≫ t.ι.app j) ≫ Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) (Hom.id j)
⊢ F.map g ≫ eqToHom ⋯ ≫ t.ι.app j' =
    (eqToHom ⋯ ≫ t.ι.app j) ≫ Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) g
have line : ∀ (a : J),
  F.map (line a) ≫ eqToHom sorry ≫ t.ι.app one =
    (eqToHom sorry ≫ t.ι.app zero) ≫ Functor.map (Functor.obj (Functor.const (WalkingParallelFamily J)) t.pt) (line a)
Tactic: cases g
Cleared hypotheses: j, j', g
-- 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Trident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ Functor.obj.{w, v, w, u} (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) j = F.obj j
have zero : Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) zero =
  F.obj zero
Tactic: cases j
Cleared hypotheses: j
-- 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Trident.{w, v, u} (C := C) (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
j : WalkingParallelFamily J
zero :
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.zero =
    F.obj WalkingParallelFamily.zero
⊢ Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) j =
    F.obj j
have one : Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) one =
  F.obj one
Tactic: cases j
Cleared hypotheses: j
-- 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cotrident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ F.obj j = Functor.obj.{w, v, w, u} (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) j
have zero : F.obj zero =
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) zero
Tactic: cases j
Cleared hypotheses: j
-- 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cotrident.{w, v, u} (C := C) (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
j : WalkingParallelFamily J
zero :
  F.obj WalkingParallelFamily.zero =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.zero
⊢ F.obj j =
    Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) j
have one : F.obj one =
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) one
Tactic: cases j
Cleared hypotheses: j
-- 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cone F
X : WalkingParallelFamily J
⊢ F.obj X = Functor.obj.{w, v, w, u} (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) X
have zero : F.obj zero =
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cone F
X : WalkingParallelFamily J
zero :
  F.obj WalkingParallelFamily.zero =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.zero
⊢ F.obj X =
    Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) X
have one : F.obj one =
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) 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_1 Y : C
f : J → (X_1 ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cocone F
X : WalkingParallelFamily J
⊢ Functor.obj.{w, v, w, u} (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) X = F.obj X
have zero : Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) zero =
  F.obj 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cocone F
X : WalkingParallelFamily J
zero :
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.zero =
    F.obj WalkingParallelFamily.zero
⊢ Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) X =
    F.obj X
have one : Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) one =
  F.obj 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cone F
j : WalkingParallelFamily J
⊢ F.obj j = Functor.obj.{w, v, w, u} (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) j
have zero : F.obj zero =
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) zero
Tactic: cases j
Cleared hypotheses: j
-- 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cone F
j : WalkingParallelFamily J
zero :
  F.obj WalkingParallelFamily.zero =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.zero
⊢ F.obj j =
    Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) j
have one : F.obj one =
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) one
Tactic: cases j
Cleared hypotheses: j
-- 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cocone F
j : WalkingParallelFamily J
⊢ Functor.obj.{w, v, w, u} (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) j = F.obj j
have zero : Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) zero =
  F.obj zero
Tactic: cases j
Cleared hypotheses: j
-- 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)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cocone F
j : WalkingParallelFamily J
zero :
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.zero =
    F.obj WalkingParallelFamily.zero
⊢ Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) j =
    F.obj j
have one : Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) one =
  F.obj one
Tactic: cases j
Cleared hypotheses: j
-- 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 t : Trident f
i : s.pt ≅ t.pt
w : i.hom ≫ t.ι = s.ι
⊢ i.inv ≫ s.ι = t.ι
have rw : i.inv ≫ i.hom ≫ t.ι = t.ι
Tactic: rw [← w, Iso.inv_hom_id_assoc]
-- 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 t : Trident f
i : s.pt ≅ t.pt
w : i.hom ≫ t.ι = s.ι
rw : i.inv ≫ i.hom ≫ t.ι = t.ι
⊢ i.inv ≫ s.ι = t.ι
have rw₁ : t.ι = t.ι
Tactic: rw [← w, Iso.inv_hom_id_assoc]
-- 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 t : Cotrident f
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
⊢ t.π ≫ i.inv = s.π
have rw : t.π = s.π ≫ i.hom
Tactic: rw [Iso.comp_inv_eq, 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
s t : Cotrident f
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
rw : t.π = s.π ≫ i.hom
⊢ t.π ≫ i.inv = s.π
have rw₁ : t.π = t.π
Tactic: rw [Iso.comp_inv_eq, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
X Y Z : WidePullbackShape J
f : X.Hom Y
g : Y.Hom Z
⊢ X.Hom Z
have id : (g : X.Hom Z) → X.Hom Z
Tactic: cases f
Cleared hypotheses: Y, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
X Y Z : WidePullbackShape J
f : X.Hom Y
g : Y.Hom Z
id : (g : X.Hom Z) → X.Hom Z
⊢ X.Hom Z
have term : (j : J) → (g : Hom none Z) → Hom (some j) Z
Tactic: cases f
Cleared hypotheses: X, Y, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
Z : WidePullbackShape J
j : J
g : Hom none Z
⊢ Hom (some j) Z
have term : Hom (some j) none
Tactic: cases g
Cleared hypotheses: Z, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
x x_1 : WidePullbackShape J
⊢ Subsingleton.{w + 1} (x ⟶ x_1)
have allEq : ∀ (a b : x ⟶ x_1), a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
x x_1 : WidePullbackShape J
a b : x ⟶ x_1
⊢ a = b
have allEq : Eq.{w + 1} (α := Quiver.Hom (V := WidePullbackShape J) none none) (Hom.id none) (Hom.id none)
Tactic: casesm* WidePullbackShape _, (_ : WidePullbackShape _) ⟶ (_ : WidePullbackShape _)
Cleared hypotheses: x, x_1, a, b
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
x x_1 : WidePullbackShape J
a b : x ⟶ x_1
allEq : Eq.{w + 1} (α := Quiver.Hom (V := WidePullbackShape J) none none) (Hom.id none) (Hom.id none)
⊢ a = b
have allEq₁ : ∀ (b : J), Hom.term b = Hom.term b
Tactic: casesm* WidePullbackShape _, (_ : WidePullbackShape _) ⟶ (_ : WidePullbackShape _)
Cleared hypotheses: x, x_1, a, b
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
x x_1 : WidePullbackShape J
a b : x ⟶ x_1
allEq : Eq.{w + 1} (α := Quiver.Hom (V := WidePullbackShape J) none none) (Hom.id none) (Hom.id none)
allEq₁ : ∀ (b : J), Hom.term b = Hom.term b
⊢ a = b
have allEq₂ : ∀ (x : J), Hom.id (some x) = Hom.id (some x)
Tactic: casesm* WidePullbackShape _, (_ : WidePullbackShape _) ⟶ (_ : WidePullbackShape _)
Cleared hypotheses: x, x_1, a, b
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
X Y : WidePullbackShape J
f : X ⟶ Y
⊢ Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ C) X B objs : C)
    (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ C) Y B objs : C)
have id : Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ C) X B objs : C)
  (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ C) X B objs : C)
Tactic: obtain - | j := f
Cleared hypotheses: Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePullbackShape J) C
X : C
f_1 : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f_1
j j' : WidePullbackShape J
f : j ⟶ j'
⊢ Eq.{v + 1} (α := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) j ⟶ F.obj j')
    (Functor.map (Functor.obj (Functor.const (WidePullbackShape J)) X) f ≫
      match (motive :=
        (j : WidePullbackShape J) →
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) j ⟶ F.obj j)
        j' with
      | none => f_1
      | some j => π j)
    ((match (motive :=
        (j : WidePullbackShape J) →
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) j ⟶ F.obj j)
        j with
      | none => f_1
      | some j => π j) ≫
      F.map f)
have none : ∀ (f : none ⟶ j'),
  Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (C := WidePullbackShape J) (Functor.obj (Functor.const (WidePullbackShape J)) X) none ⟶
      F.obj j')
    (Functor.map (Functor.obj (Functor.const (WidePullbackShape J)) X) f ≫
      match (motive :=
        (j : WidePullbackShape J) →
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) j ⟶ F.obj j)
        j' with
      | none => f_1
      | some j => π j)
    ((match (motive :=
        (j : WidePullbackShape J) →
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) j ⟶ F.obj j)
        none with
      | none => f_1
      | some j => π j) ≫
      F.map f)
Tactic: cases j
Cleared hypotheses: j, f