awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteBiproducts.{v_1, u_1} C
inst_4 : ∀ (n : ℕ), Epi (f n)
n val : ℕ
property : ¬val < n + 1
⊢ IsIso.{v_1, u_1} (C := C) (X :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n + 1 then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ))
    (Y :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ))
    (if h : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n then eqToHom ⋯
    else
      if h' : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n + 1 then
        eqToHom ⋯ ≫ f (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) ≫ eqToHom ⋯
      else eqToHom ⋯)
have inst : ∀ (h : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n),
  IsIso.{v_1, u_1} (C := C) (X :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n + 1 then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ))
    (eqToHom sorry)
Tactic: split
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst_1 : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_2 : HasCountableProducts.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
inst_5 : ∀ (n : ℕ), Epi (f n)
n val : ℕ
property : ¬val < n + 1
inst :
  ∀ (h : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n),
    IsIso.{v_1, u_1} (C := C) (X :=
      if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n + 1 then
        M (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ)
      else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ))
      (eqToHom ⋯)
⊢ IsIso.{v_1, u_1} (C := C) (X :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n + 1 then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ))
    (Y :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ))
    (if h : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n then eqToHom ⋯
    else
      if h' : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n + 1 then
        eqToHom ⋯ ≫ f (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) ≫ eqToHom ⋯
      else eqToHom ⋯)
have inst₁ : ∀ (h : ¬(↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n),
  IsIso.{v_1, u_1} (C := C) (X :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n + 1 then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ))
    (eqToHom sorry)
Tactic: split
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SingleObj (goal)
Goal:
M G : Type v
inst : Monoid M
inst_1 : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj M) (Type u)
g h : M
x : J.obj (SingleObj.star M)
⊢ (g * h) • x = g • h • x
have change : Eq (α := (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map (g * h)) :
        (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
      x :
    (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryStruct.comp (Y := J.obj (SingleObj.star M)) (J.map h) (J.map g)) :
        (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
      x :
    (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
Tactic: change J.map (g * h) x = (J.map h ≫ J.map g) x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SingleObj (goal)
Goal:
M G : Type v
inst : Monoid M
inst_1 : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj M) (Type u)
g h : M
x : J.obj (SingleObj.star M)
⊢ Eq (α := (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map (g * h)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := J.obj (SingleObj.star M)) (J.map h) (J.map g)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
have rw : Eq (α := (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map (CategoryStruct.comp (Y := SingleObj.star M) h g)) :
        (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
      x :
    (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryStruct.comp (Y := J.obj (SingleObj.star M)) (J.map h) (J.map g)) :
        (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
      x :
    (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
Tactic: rw [← SingleObj.comp_as_mul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SingleObj (goal)
Goal:
M G : Type v
inst : Monoid M
inst_1 : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj M) (Type u)
g h : M
x : J.obj (SingleObj.star M)
rw :
  Eq (α := (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map (CategoryStruct.comp (Y := SingleObj.star M) h g)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := J.obj (SingleObj.star M)) (J.map h) (J.map g)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
⊢ Eq (α := (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map (g * h)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := J.obj (SingleObj.star M)) (J.map h) (J.map g)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
have y : SingleObj M
Tactic: rw [← SingleObj.comp_as_mul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SingleObj (goal)
Goal:
M G : Type v
inst : Monoid M
inst_1 : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj M) (Type u)
g h : M
x : J.obj (SingleObj.star M)
⊢ Eq (α := (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map (CategoryStruct.comp (Y := SingleObj.star M) h g)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := J.obj (SingleObj.star M)) (J.map h) (J.map g)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
have simp : Eq (α := J.obj (SingleObj.star M))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map g) : (a : J.obj (SingleObj.star M)) → J.obj (SingleObj.star M))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map h) : (a : J.obj (SingleObj.star M)) → J.obj (SingleObj.star M))
          x :
        J.obj (SingleObj.star M)) :
    J.obj (SingleObj.star M))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map g) : (a : J.obj (SingleObj.star M)) → J.obj (SingleObj.star M))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map h) : (a : J.obj (SingleObj.star M)) → J.obj (SingleObj.star M))
          x :
        J.obj (SingleObj.star M)) :
    J.obj (SingleObj.star M))
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SingleObj (goal)
Goal:
M G : Type v
inst : Monoid M
inst_1 : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj M) (Type u)
x : J.obj (SingleObj.star M)
⊢ HSMul.hSMul.{v, u, u} (α := M) 1 x = x
have change : (ConcreteCategory.hom (FC := TypeCat.Fun) (J.map (𝟙 (SingleObj.star M))) :
      (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    x =
  x
Tactic: change J.map (𝟙 _) x = x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SingleObj (goal)
Goal:
G : Type v
inst : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj G) (Type u)
x y : J.obj (SingleObj.star G)
| J.ColimitTypeRel (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) x)
      (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) y) ↔
    (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) x y
have rhs : (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) x y
Tactic: rhs
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SingleObj (goal)
Goal:
G : Type v
inst : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj G) (Type u)
x y : J.obj (SingleObj.star G)
| (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) x y
have rw : (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) y x
Tactic: rw [Setoid.comm']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SingleObj (goal)
Goal:
G : Type v
inst : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj G) (Type u)
x y : J.obj (SingleObj.star G)
| J.ColimitTypeRel (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) x)
      (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) y) ↔
    (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) x y
have rw : (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) y x
Tactic: rhs; rw [Setoid.comm']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SingleObj (goal)
Goal:
G : Type v
inst : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj G) (Type u)
x y : J.obj (SingleObj.star G)
⊢ J.ColimitTypeRel (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) x)
      (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) y) ↔
    (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) x y
have conv : J.ColimitTypeRel (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) x)
    (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) y) ↔
  (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) y x
Tactic: conv => rhs; rw [Setoid.comm']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SingleObj (goal)
Goal:
G : Type v
inst : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj G) (Type u)
x y : J.obj (SingleObj.star G)
⊢ J.ColimitTypeRel (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) x)
      (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) y) ↔
    (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) y x
have change : (∃ (g : G), y = g • x) ↔ ∃ (g : G), g • x = y
Tactic: change (∃ g : G, y = g • x) ↔ (∃ g : G, g • x = y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
⊢ F.map f ≫ F.map π = F.map g ≫ F.map π
have rw : F.map (f ≫ π) = F.map g ≫ F.map π
Tactic: rw [← F.map_comp, q.condition, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (f ≫ π) = F.map g ≫ F.map π
⊢ F.map f ≫ F.map π = F.map g ≫ F.map π
have rw₁ : F.map (g ≫ π) = F.map g ≫ F.map π
Tactic: rw [← F.map_comp, q.condition, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (f ≫ π) = F.map g ≫ F.map π
rw₁ : F.map (g ≫ π) = F.map g ≫ F.map π
⊢ F.map f ≫ F.map π = F.map g ≫ F.map π
have rw₂ : F.map g ≫ F.map π = F.map g ≫ F.map π
Tactic: rw [← F.map_comp, q.condition, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
⊢ F.map q.rightSection ≫ F.map π = 𝟙 (F.obj Z)
have rw : F.map (q.rightSection ≫ π) = 𝟙 (F.obj Z)
Tactic: rw [← F.map_comp, q.rightSection_π, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (q.rightSection ≫ π) = 𝟙 (F.obj Z)
⊢ F.map q.rightSection ≫ F.map π = 𝟙 (F.obj Z)
have rw₁ : F.map (𝟙 Z) = 𝟙 (F.obj Z)
Tactic: rw [← F.map_comp, q.rightSection_π, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (q.rightSection ≫ π) = 𝟙 (F.obj Z)
rw₁ : F.map (𝟙 Z) = 𝟙 (F.obj Z)
⊢ F.map q.rightSection ≫ F.map π = 𝟙 (F.obj Z)
have rw₂ : Eq.{v₂ + 1} (α := F.obj Z ⟶ F.obj Z) (𝟙 (F.obj Z)) (𝟙 (F.obj Z))
Tactic: rw [← F.map_comp, q.rightSection_π, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
⊢ F.map q.leftSection ≫ F.map g = 𝟙 (F.obj Y)
have rw : F.map (q.leftSection ≫ g) = 𝟙 (F.obj Y)
Tactic: rw [← F.map_comp, q.leftSection_bottom, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (q.leftSection ≫ g) = 𝟙 (F.obj Y)
⊢ F.map q.leftSection ≫ F.map g = 𝟙 (F.obj Y)
have rw₁ : F.map (𝟙 Y) = 𝟙 (F.obj Y)
Tactic: rw [← F.map_comp, q.leftSection_bottom, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (q.leftSection ≫ g) = 𝟙 (F.obj Y)
rw₁ : F.map (𝟙 Y) = 𝟙 (F.obj Y)
⊢ F.map q.leftSection ≫ F.map g = 𝟙 (F.obj Y)
have rw₂ : Eq.{v₂ + 1} (α := F.obj Y ⟶ F.obj Y) (𝟙 (F.obj Y)) (𝟙 (F.obj Y))
Tactic: rw [← F.map_comp, q.leftSection_bottom, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
⊢ F.map q.leftSection ≫ F.map f = F.map π ≫ F.map q.rightSection
have rw : F.map (q.leftSection ≫ f) = F.map π ≫ F.map q.rightSection
Tactic: rw [← F.map_comp, q.leftSection_top, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (q.leftSection ≫ f) = F.map π ≫ F.map q.rightSection
⊢ F.map q.leftSection ≫ F.map f = F.map π ≫ F.map q.rightSection
have rw₁ : F.map (π ≫ q.rightSection) = F.map π ≫ F.map q.rightSection
Tactic: rw [← F.map_comp, q.leftSection_top, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (q.leftSection ≫ f) = F.map π ≫ F.map q.rightSection
rw₁ : F.map (π ≫ q.rightSection) = F.map π ≫ F.map q.rightSection
⊢ F.map q.leftSection ≫ F.map f = F.map π ≫ F.map q.rightSection
have rw₂ : F.map π ≫ F.map q.rightSection = F.map π ≫ F.map q.rightSection
Tactic: rw [← F.map_comp, q.leftSection_top, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
⊢ t.asCofork.π ≫ t.rightSection ≫ s.π = s.π
have dsimp : h ≫ t.rightSection ≫ s.π = s.π
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
⊢ h ≫ t.rightSection ≫ s.π = s.π
have rw : t.leftSection ≫ f ≫ s.π = s.π
Tactic: rw [← t.leftSection_top_assoc, s.condition, t.leftSection_bottom_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
rw : t.leftSection ≫ f ≫ s.π = s.π
⊢ h ≫ t.rightSection ≫ s.π = s.π
have rw₁ : t.leftSection ≫ g ≫ s.π = s.π
Tactic: rw [← t.leftSection_top_assoc, s.condition, t.leftSection_bottom_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
rw : t.leftSection ≫ f ≫ s.π = s.π
rw₁ : t.leftSection ≫ g ≫ s.π = s.π
⊢ h ≫ t.rightSection ≫ s.π = s.π
have rw₂ : s.π = s.π
Tactic: rw [← t.leftSection_top_assoc, s.condition, t.leftSection_bottom_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
⊢ F.map ι ≫ F.map f = F.map ι ≫ F.map g
have rw : F.map (ι ≫ f) = F.map ι ≫ F.map g
Tactic: rw [← F.map_comp, q.condition, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (ι ≫ f) = F.map ι ≫ F.map g
⊢ F.map ι ≫ F.map f = F.map ι ≫ F.map g
have rw₁ : F.map (ι ≫ g) = F.map ι ≫ F.map g
Tactic: rw [← F.map_comp, q.condition, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (ι ≫ f) = F.map ι ≫ F.map g
rw₁ : F.map (ι ≫ g) = F.map ι ≫ F.map g
⊢ F.map ι ≫ F.map f = F.map ι ≫ F.map g
have rw₂ : F.map ι ≫ F.map g = F.map ι ≫ F.map g
Tactic: rw [← F.map_comp, q.condition, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
⊢ F.map ι ≫ F.map q.leftRetraction = 𝟙 (F.obj W)
have rw : F.map (ι ≫ q.leftRetraction) = 𝟙 (F.obj W)
Tactic: rw [← F.map_comp, q.ι_leftRetraction, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (ι ≫ q.leftRetraction) = 𝟙 (F.obj W)
⊢ F.map ι ≫ F.map q.leftRetraction = 𝟙 (F.obj W)
have rw₁ : F.map (𝟙 W) = 𝟙 (F.obj W)
Tactic: rw [← F.map_comp, q.ι_leftRetraction, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (ι ≫ q.leftRetraction) = 𝟙 (F.obj W)
rw₁ : F.map (𝟙 W) = 𝟙 (F.obj W)
⊢ F.map ι ≫ F.map q.leftRetraction = 𝟙 (F.obj W)
have rw₂ : Eq.{v₂ + 1} (α := F.obj W ⟶ F.obj W) (𝟙 (F.obj W)) (𝟙 (F.obj W))
Tactic: rw [← F.map_comp, q.ι_leftRetraction, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
⊢ F.map g ≫ F.map q.rightRetraction = 𝟙 (F.obj X)
have rw : F.map (g ≫ q.rightRetraction) = 𝟙 (F.obj X)
Tactic: rw [← F.map_comp, q.bottom_rightRetraction, F.map_id]