awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_6 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_7 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₂₃ : ρ₂₃.I₂₃
h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃
rw : ρ₂₃.q (i₁, i₂₃) = r (i₁, i₂, i₃)
rw₁ : ρ₂₃.q (i₁, ρ₂₃.p (i₂, i₃)) = r (i₁, i₂, i₃)
⊢ ρ₂₃.q (i₁, i₂₃) = j
have rw₂ : ρ₂₃.q (i₁, ρ₂₃.p (i₂, i₃)) = ρ₂₃.q ((i₁, i₂, i₃).1, ρ₂₃.p (i₁, i₂, i₃).2)
Tactic: rw [← h, ← h₂₃, ← ρ₂₃.hpq]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_5 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_6 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₂₃ : ρ₂₃.I₂₃
h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃
⊢ Eq (α :=
    (F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶
      mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j)
    (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
    ((F.obj (X₁ i₁)).map (ιMapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃ i₂ i₃ i₂₃ h₂₃) ≫
      ιMapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) i₁ i₂₃ j ⋯)
have subst : Eq (α :=
  (F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶
    mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j)
  (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
  ((F.obj (X₁ i₁)).map (ιMapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃ i₂ i₃ (ρ₂₃.p (i₂, i₃)) sorry) ≫
    ιMapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) i₁ (ρ₂₃.p (i₂, i₃)) j sorry)
Tactic: subst h₂₃
Cleared hypotheses: i₂₃, h₂₃
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_6 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_7 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
c₂₃ : (i₂₃ : ρ₂₃.I₂₃) → (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).CofanMapObjFun ρ₂₃.p i₂₃ :=
  fun (i₂₃ : ρ₂₃.I₂₃) ↦ (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).cofanMapObj ρ₂₃.p i₂₃
⊢ IsColimit (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
have have : (h₂₃ : (i₂₃ : ρ₂₃.I₂₃) → IsColimit (c₂₃ i₂₃)) → IsColimit (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
Tactic: have h₂₃ : ∀ i₂₃, IsColimit (c₂₃ i₂₃) := fun i₂₃ =>
    (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).isColimitCofanMapObj ρ₂₃.p i₂₃
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_6 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_7 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
c₂₃ : (i₂₃ : ρ₂₃.I₂₃) → (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).CofanMapObjFun ρ₂₃.p i₂₃ :=
  fun (i₂₃ : ρ₂₃.I₂₃) ↦ (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).cofanMapObj ρ₂₃.p i₂₃
h₂₃ : (i₂₃ : ρ₂₃.I₂₃) → IsColimit (c₂₃ i₂₃)
c : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).CofanMapObjFun ρ₂₃.q
  j :=
  (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).cofanMapObj ρ₂₃.q j
⊢ IsColimit (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
have have : (hc : IsColimit c) → IsColimit (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
Tactic: have hc : IsColimit c := (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
    (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).isColimitCofanMapObj ρ₂₃.q j
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_6 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_7 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
c₂₃ : (i₂₃ : ρ₂₃.I₂₃) → (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).CofanMapObjFun ρ₂₃.p i₂₃ :=
  fun (i₂₃ : ρ₂₃.I₂₃) ↦ (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).cofanMapObj ρ₂₃.p i₂₃
h₂₃ : (i₂₃ : ρ₂₃.I₂₃) → IsColimit (c₂₃ i₂₃)
c : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).CofanMapObjFun ρ₂₃.q
  j :=
  (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).cofanMapObj ρ₂₃.q j
hc : IsColimit c
c₂₃' : (i : (↑(ρ₂₃.q ⁻¹' {j}) : Type (max u_7 u_11))) →
  Cocone (J := Discrete (↑(ρ₂₃.p ⁻¹' {(↑i : I₁ × ρ₂₃.I₂₃).2}) : Type (max u_8 u_9)))
    (Discrete.functor ((((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p (↑i : I₁ × ρ₂₃.I₂₃).2) ⋙
      F.obj (X₁ (↑i : I₁ × ρ₂₃.I₂₃).1)) :=
  fun (i : (↑(ρ₂₃.q ⁻¹' {j}) : Type (max u_7 u_11))) ↦
    (F.obj (X₁ (↑i : I₁ × ρ₂₃.I₂₃).1)).mapCocone (c₂₃ (↑i : I₁ × ρ₂₃.I₂₃).2)
⊢ IsColimit (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
have have : (hc₂₃' : (i : (↑(ρ₂₃.q ⁻¹' {j}) : Type (max u_7 u_11))) → IsColimit (c₂₃' i)) →
  IsColimit (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
Tactic: have hc₂₃' : ∀ i, IsColimit (c₂₃' i) := fun i => isColimitOfPreserves _ (h₂₃ i.1.2)
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_5 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_6 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
inst_7 : ((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ Eq (α :=
    (((bifunctorComp₂₃ F G₂₃).obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶
      mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ j)
      (ιMapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (Iso.hom (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃) j))
    (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
have dsimp : Eq (α :=
  (F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶
    mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j)
  (CategoryStruct.comp (Y := mapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ j)
    (ιMapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
    (Iso.inv (CofanMapObjFun.iso (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j))))
  (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
Tactic: dsimp [mapBifunctorComp₂₃MapObjIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_5 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_6 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
A : C₄
f g : mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
    ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f =
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
⊢ f = g
have h₁ : ∀ (i : (↑(r ⁻¹' {j}) : Type (max (max u_7 u_8) u_9))),
  Cofan.inj (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j) i ≫ f =
    Cofan.inj (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j) i ≫ g
Tactic: apply Cofan.IsColimit.hom_ext (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f : X ⟶ Y
hf : ∀ (i : β), IsIso (f i)
⊢ IsIso f
have change : IsIso (Iso.hom (X.isoMk Y fun (i : β) ↦ asIso (f i)))
Tactic: change IsIso (isoMk X Y (fun i => asIso (f i))).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f : X ⟶ Y
inst_1 : IsIso f
i : β
⊢ IsIso (f i)
have change : IsIso (X := Functor.obj (eval i) X) (Functor.map (eval i) f)
Tactic: change IsIso ((eval i).map f)
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
J : Type u_4
inst : Category.{v_1, u_1} C
X Y : GradedObject J C
e : X ≅ Y
j : J
⊢ e.hom j ≫ e.inv j = 𝟙 (X j)
have rw : (e.hom ≫ e.inv) j = 𝟙 (X j)
Tactic: rw [← GradedObject.categoryOfGradedObjects_comp, e.hom_inv_id,
    GradedObject.categoryOfGradedObjects_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
J : Type u_4
inst : Category.{v_1, u_1} C
X Y : GradedObject J C
e : X ≅ Y
j : J
rw : (e.hom ≫ e.inv) j = 𝟙 (X j)
⊢ e.hom j ≫ e.inv j = 𝟙 (X j)
have rw₁ : Eq.{v_1 + 1} (α := X j ⟶ X j) (𝟙 X j : X j ⟶ X j) (𝟙 (X j) : X j ⟶ X j)
Tactic: rw [← GradedObject.categoryOfGradedObjects_comp, e.hom_inv_id,
    GradedObject.categoryOfGradedObjects_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
J : Type u_4
inst : Category.{v_1, u_1} C
X Y : GradedObject J C
e : X ≅ Y
j : J
rw : (e.hom ≫ e.inv) j = 𝟙 (X j)
rw₁ : Eq.{v_1 + 1} (α := X j ⟶ X j) (𝟙 X j : X j ⟶ X j) (𝟙 (X j) : X j ⟶ X j)
⊢ e.hom j ≫ e.inv j = 𝟙 (X j)
have rw₂ : Eq.{v_1 + 1} (α := X j ⟶ X j) (𝟙 (X j)) (𝟙 (X j))
Tactic: rw [← GradedObject.categoryOfGradedObjects_comp, e.hom_inv_id,
    GradedObject.categoryOfGradedObjects_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
J : Type u_4
inst : Category.{v_1, u_1} C
X Y : GradedObject J C
e : X ≅ Y
j : J
⊢ e.inv j ≫ e.hom j = 𝟙 (Y j)
have rw : (e.inv ≫ e.hom) j = 𝟙 (Y j)
Tactic: rw [← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id,
    GradedObject.categoryOfGradedObjects_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
J : Type u_4
inst : Category.{v_1, u_1} C
X Y : GradedObject J C
e : X ≅ Y
j : J
rw : (e.inv ≫ e.hom) j = 𝟙 (Y j)
⊢ e.inv j ≫ e.hom j = 𝟙 (Y j)
have rw₁ : Eq.{v_1 + 1} (α := Y j ⟶ Y j) (𝟙 Y j : Y j ⟶ Y j) (𝟙 (Y j) : Y j ⟶ Y j)
Tactic: rw [← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id,
    GradedObject.categoryOfGradedObjects_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
J : Type u_4
inst : Category.{v_1, u_1} C
X Y : GradedObject J C
e : X ≅ Y
j : J
rw : (e.inv ≫ e.hom) j = 𝟙 (Y j)
rw₁ : Eq.{v_1 + 1} (α := Y j ⟶ Y j) (𝟙 Y j : Y j ⟶ Y j) (𝟙 (Y j) : Y j ⟶ Y j)
⊢ e.inv j ≫ e.hom j = 𝟙 (Y j)
have rw₂ : Eq.{v_1 + 1} (α := Y j ⟶ Y j) (𝟙 (Y j)) (𝟙 (Y j))
Tactic: rw [← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id,
    GradedObject.categoryOfGradedObjects_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J
⊢ F.map (e.hom j) ≫ F.map (e.inv j) = 𝟙 (F.obj (X j))
have rw : F.map (e.hom j ≫ e.inv j) = 𝟙 (F.obj (X j))
Tactic: rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.hom_inv_id,
    GradedObject.categoryOfGradedObjects_id, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J
rw : F.map (e.hom j ≫ e.inv j) = 𝟙 (F.obj (X j))
⊢ F.map (e.hom j) ≫ F.map (e.inv j) = 𝟙 (F.obj (X j))
have rw₁ : F.map ((e.hom ≫ e.inv) j) = 𝟙 (F.obj (X j))
Tactic: rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.hom_inv_id,
    GradedObject.categoryOfGradedObjects_id, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J
rw : F.map (e.hom j ≫ e.inv j) = 𝟙 (F.obj (X j))
rw₁ : F.map ((e.hom ≫ e.inv) j) = 𝟙 (F.obj (X j))
⊢ F.map (e.hom j) ≫ F.map (e.inv j) = 𝟙 (F.obj (X j))
have rw₂ : F.map (𝟙 X j) = 𝟙 (F.obj (X j))
Tactic: rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.hom_inv_id,
    GradedObject.categoryOfGradedObjects_id, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J
rw : F.map (e.hom j ≫ e.inv j) = 𝟙 (F.obj (X j))
rw₁ : F.map ((e.hom ≫ e.inv) j) = 𝟙 (F.obj (X j))
rw₂ : F.map (𝟙 X j) = 𝟙 (F.obj (X j))
⊢ F.map (e.hom j) ≫ F.map (e.inv j) = 𝟙 (F.obj (X j))
have rw₃ : F.map (𝟙 (X j)) = 𝟙 (F.obj (X j))
Tactic: rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.hom_inv_id,
    GradedObject.categoryOfGradedObjects_id, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J
rw : F.map (e.hom j ≫ e.inv j) = 𝟙 (F.obj (X j))
rw₁ : F.map ((e.hom ≫ e.inv) j) = 𝟙 (F.obj (X j))
rw₂ : F.map (𝟙 X j) = 𝟙 (F.obj (X j))
rw₃ : F.map (𝟙 (X j)) = 𝟙 (F.obj (X j))
⊢ F.map (e.hom j) ≫ F.map (e.inv j) = 𝟙 (F.obj (X j))
have rw₄ : Eq.{v_2 + 1} (α := F.obj (X j) ⟶ F.obj (X j)) (𝟙 (F.obj (X j))) (𝟙 (F.obj (X j)))
Tactic: rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.hom_inv_id,
    GradedObject.categoryOfGradedObjects_id, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J
⊢ F.map (e.inv j) ≫ F.map (e.hom j) = 𝟙 (F.obj (Y j))
have rw : F.map (e.inv j ≫ e.hom j) = 𝟙 (F.obj (Y j))
Tactic: rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id,
    GradedObject.categoryOfGradedObjects_id, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J
rw : F.map (e.inv j ≫ e.hom j) = 𝟙 (F.obj (Y j))
⊢ F.map (e.inv j) ≫ F.map (e.hom j) = 𝟙 (F.obj (Y j))
have rw₁ : F.map ((e.inv ≫ e.hom) j) = 𝟙 (F.obj (Y j))
Tactic: rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id,
    GradedObject.categoryOfGradedObjects_id, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J
rw : F.map (e.inv j ≫ e.hom j) = 𝟙 (F.obj (Y j))
rw₁ : F.map ((e.inv ≫ e.hom) j) = 𝟙 (F.obj (Y j))
⊢ F.map (e.inv j) ≫ F.map (e.hom j) = 𝟙 (F.obj (Y j))
have rw₂ : F.map (𝟙 Y j) = 𝟙 (F.obj (Y j))
Tactic: rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id,
    GradedObject.categoryOfGradedObjects_id, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J
rw : F.map (e.inv j ≫ e.hom j) = 𝟙 (F.obj (Y j))
rw₁ : F.map ((e.inv ≫ e.hom) j) = 𝟙 (F.obj (Y j))
rw₂ : F.map (𝟙 Y j) = 𝟙 (F.obj (Y j))
⊢ F.map (e.inv j) ≫ F.map (e.hom j) = 𝟙 (F.obj (Y j))
have rw₃ : F.map (𝟙 (Y j)) = 𝟙 (F.obj (Y j))
Tactic: rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id,
    GradedObject.categoryOfGradedObjects_id, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J
rw : F.map (e.inv j ≫ e.hom j) = 𝟙 (F.obj (Y j))
rw₁ : F.map ((e.inv ≫ e.hom) j) = 𝟙 (F.obj (Y j))
rw₂ : F.map (𝟙 Y j) = 𝟙 (F.obj (Y j))
rw₃ : F.map (𝟙 (Y j)) = 𝟙 (F.obj (Y j))
⊢ F.map (e.inv j) ≫ F.map (e.hom j) = 𝟙 (F.obj (Y j))
have rw₄ : Eq.{v_2 + 1} (α := F.obj (Y j) ⟶ F.obj (Y j)) (𝟙 (F.obj (Y j))) (𝟙 (F.obj (Y j)))
Tactic: rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id,
    GradedObject.categoryOfGradedObjects_id, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
X Y_1 : GradedObject J C
e : X ≅ Y_1
F : C ⥤ Functor.{v_2, v_3, u_2, u_3} D E
j : J
Y : D
⊢ (F.map (e.hom j)).app Y ≫ (F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
have rw : (F.map (e.hom j) ≫ F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
Tactic: rw [← NatTrans.comp_app, ← F.map_comp, hom_inv_id_eval,
    Functor.map_id, NatTrans.id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
X Y_1 : GradedObject J C
e : X ≅ Y_1
F : C ⥤ Functor.{v_2, v_3, u_2, u_3} D E
j : J
Y : D
rw : (F.map (e.hom j) ≫ F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
⊢ (F.map (e.hom j)).app Y ≫ (F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
have rw₁ : (F.map (e.hom j ≫ e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
Tactic: rw [← NatTrans.comp_app, ← F.map_comp, hom_inv_id_eval,
    Functor.map_id, NatTrans.id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
X Y_1 : GradedObject J C
e : X ≅ Y_1
F : C ⥤ Functor.{v_2, v_3, u_2, u_3} D E
j : J
Y : D
rw : (F.map (e.hom j) ≫ F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
rw₁ : (F.map (e.hom j ≫ e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
⊢ (F.map (e.hom j)).app Y ≫ (F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
have rw₂ : (F.map (𝟙 (X j))).app Y = 𝟙 ((F.obj (X j)).obj Y)
Tactic: rw [← NatTrans.comp_app, ← F.map_comp, hom_inv_id_eval,
    Functor.map_id, NatTrans.id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
X Y_1 : GradedObject J C
e : X ≅ Y_1
F : C ⥤ Functor.{v_2, v_3, u_2, u_3} D E
j : J
Y : D
rw : (F.map (e.hom j) ≫ F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
rw₁ : (F.map (e.hom j ≫ e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
rw₂ : (F.map (𝟙 (X j))).app Y = 𝟙 ((F.obj (X j)).obj Y)
⊢ (F.map (e.hom j)).app Y ≫ (F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
have rw₃ : NatTrans.app (𝟙 (F.obj (X j))) Y = 𝟙 ((F.obj (X j)).obj Y)
Tactic: rw [← NatTrans.comp_app, ← F.map_comp, hom_inv_id_eval,
    Functor.map_id, NatTrans.id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
X Y_1 : GradedObject J C
e : X ≅ Y_1
F : C ⥤ Functor.{v_2, v_3, u_2, u_3} D E
j : J
Y : D
rw : (F.map (e.hom j) ≫ F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
rw₁ : (F.map (e.hom j ≫ e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
rw₂ : (F.map (𝟙 (X j))).app Y = 𝟙 ((F.obj (X j)).obj Y)
rw₃ : NatTrans.app (𝟙 (F.obj (X j))) Y = 𝟙 ((F.obj (X j)).obj Y)
⊢ (F.map (e.hom j)).app Y ≫ (F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
have rw₄ : Eq.{v_3 + 1} (α := (F.obj (X j)).obj Y ⟶ (F.obj (X j)).obj Y) (𝟙 ((F.obj (X j)).obj Y)) (𝟙 ((F.obj (X j)).obj Y))
Tactic: rw [← NatTrans.comp_app, ← F.map_comp, hom_inv_id_eval,
    Functor.map_id, NatTrans.id_app]