awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
T : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
L : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R : Functor.{v_2, v_4, u_2, u_4} C₂ C₄
B : Equivalence.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ NatTrans.app (Iso.hom (iso T.symm.inverse L R B.symm.inverse)) X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫
      NatTrans.app (Iso.hom (iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)
have iso : (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
      B.symm.inverse.map (NatTrans.app (Iso.inv (iso T.symm.functor R L B.symm.functor)) (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
    (L ⋙ B.functor).map (T.unitIso.hom.app X) =
  (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫
    NatTrans.app (Iso.hom (iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)
Tactic: rw [hInv_iso_hom_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
T : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
L : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R : Functor.{v_2, v_4, u_2, u_4} C₂ C₄
B : Equivalence.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map (NatTrans.app (Iso.inv (iso T.symm.functor R L B.symm.functor)) (T.symm.inverse.obj X)) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫
      NatTrans.app (Iso.hom (iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)
have iso : (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
      B.symm.inverse.map (NatTrans.app (Iso.inv (iso T.inverse R L B.inverse)) (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
    (L ⋙ B.functor).map (T.unitIso.hom.app X) =
  (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫
    NatTrans.app (Iso.hom (iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)
Tactic: simp only [Equivalence.symm_functor]
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
T : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
L : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R : Functor.{v_2, v_4, u_2, u_4} C₂ C₄
B : Equivalence.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map (NatTrans.app (Iso.inv (iso T.inverse R L B.inverse)) (T.symm.inverse.obj X)) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫
      NatTrans.app (Iso.hom (iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)
have iso : (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
      B.symm.inverse.map
          (B.inverse.map (R.map (T.counitIso.inv.app (T.symm.inverse.obj X))) ≫
            B.inverse.map
                (NatTrans.app (Iso.hom (iso T.functor L R B.functor)) (T.inverse.obj (T.symm.inverse.obj X))) ≫
              B.unitIso.inv.app (L.obj (T.inverse.obj (T.symm.inverse.obj X)))) ≫
        B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
    (L ⋙ B.functor).map (T.unitIso.hom.app X) =
  (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫
    NatTrans.app (Iso.hom (iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)
Tactic: rw [hInv_iso_inv_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
T : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
L : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R : Functor.{v_2, v_4, u_2, u_4} C₂ C₄
B : Equivalence.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map
            (B.inverse.map (R.map (T.counitIso.inv.app (T.symm.inverse.obj X))) ≫
              B.inverse.map
                  (NatTrans.app (Iso.hom (iso T.functor L R B.functor)) (T.inverse.obj (T.symm.inverse.obj X))) ≫
                B.unitIso.inv.app (L.obj (T.inverse.obj (T.symm.inverse.obj X)))) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫
      NatTrans.app (Iso.hom (iso T.functor L R B.functor)) ((T.functor ⋙ T.inverse).obj X)
have iso : (B.counitIso.inv.app (R.obj (T.functor.obj X)) ≫
      B.functor.map
          (B.inverse.map (R.map (T.counitIso.inv.app (T.functor.obj X))) ≫
            B.inverse.map (NatTrans.app (Iso.hom (iso T.functor L R B.functor)) (T.inverse.obj (T.functor.obj X))) ≫
              B.unitIso.inv.app (L.obj (T.inverse.obj (T.functor.obj X)))) ≫
        B.functor.map (L.map (T.unitIso.inv.app X))) ≫
    B.functor.map (L.map (T.unitIso.hom.app X)) =
  R.map (T.functor.map (T.unitIso.hom.app X)) ≫
    NatTrans.app (Iso.hom (iso T.functor L R B.functor)) (T.inverse.obj (T.functor.obj X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
T : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
L : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
R : Functor.{v_2, v_4, u_2, u_4} C₂ C₄
B : Equivalence.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.counitIso.inv.app (R.obj (T.functor.obj X)) ≫
        B.functor.map
            (B.inverse.map (R.map (T.counitIso.inv.app (T.functor.obj X))) ≫
              B.inverse.map (NatTrans.app (Iso.hom (iso T.functor L R B.functor)) (T.inverse.obj (T.functor.obj X))) ≫
                B.unitIso.inv.app (L.obj (T.inverse.obj (T.functor.obj X)))) ≫
          B.functor.map (L.map (T.unitIso.inv.app X))) ≫
      B.functor.map (L.map (T.unitIso.hom.app X)) =
    R.map (T.functor.map (T.unitIso.hom.app X)) ≫
      NatTrans.app (Iso.hom (iso T.functor L R B.functor)) (T.inverse.obj (T.functor.obj X))
have iso : B.counitIso.inv.app (R.obj (T.functor.obj X)) ≫
    B.functor.map
      (B.inverse.map (R.map (T.functor.map (T.unit.app X))) ≫
        B.inverse.map (NatTrans.app (Iso.hom (iso T.functor L R B.functor)) (T.inverse.obj (T.functor.obj X))) ≫
          B.unitIso.inv.app (L.obj (T.inverse.obj (T.functor.obj X))) ≫ 𝟙 (L.obj (T.inverse.obj (T.functor.obj X)))) =
  R.map (T.functor.map (T.unitIso.hom.app X)) ≫
    NatTrans.app (Iso.hom (iso T.functor L R B.functor)) (T.inverse.obj (T.functor.obj X))
Tactic: simp only [Functor.comp_obj, assoc, ← Functor.map_comp, Iso.inv_hom_id_app,
    Equivalence.counitInv_app_functor, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
⊢ vInv B L.symm R.symm T (vInv T L R B h) = h
have iso : ∀ (X : C₁), (iso T L.symm.inverse R.symm.inverse B).hom.app X = (iso T L.symm.inverse R.symm.inverse B).hom.app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ (iso T L.symm.inverse R.symm.inverse B).hom.app X = (iso T L.symm.inverse R.symm.inverse B).hom.app X
have iso : R.symm.inverse.map (T.map (L.symm.counitIso.inv.app X)) ≫
    R.symm.inverse.map ((iso B L.symm.functor R.symm.functor T).inv.app (L.symm.inverse.obj X)) ≫
      R.symm.unitIso.inv.app (B.obj (L.symm.inverse.obj X)) =
  (iso T L.symm.inverse R.symm.inverse B).hom.app X
Tactic: rw [vInv_iso_hom_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ R.symm.inverse.map (T.map (L.symm.counitIso.inv.app X)) ≫
      R.symm.inverse.map ((iso B L.symm.functor R.symm.functor T).inv.app (L.symm.inverse.obj X)) ≫
        R.symm.unitIso.inv.app (B.obj (L.symm.inverse.obj X)) =
    (iso T L.symm.inverse R.symm.inverse B).hom.app X
have iso : R.functor.map (T.map (L.unitIso.hom.app X)) ≫
    R.functor.map ((iso B L.inverse R.inverse T).inv.app (L.functor.obj X)) ≫
      R.counitIso.hom.app (B.obj (L.functor.obj X)) =
  (iso T L.functor R.functor B).hom.app X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map ((iso B L.inverse R.inverse T).inv.app (L.functor.obj X)) ≫
        R.counitIso.hom.app (B.obj (L.functor.obj X)) =
    (iso T L.functor R.functor B).hom.app X
have iso : R.functor.map (T.map (L.unitIso.hom.app X)) ≫
    R.functor.map
        (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
          R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
            R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
      R.counitIso.hom.app (B.obj (L.functor.obj X)) =
  (iso T L.functor R.functor B).hom.app X
Tactic: rw [vInv_iso_inv_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map
          (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
            R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
        R.counitIso.hom.app (B.obj (L.functor.obj X)) =
    (iso T L.functor R.functor B).hom.app X
have iso : (R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map
          (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
            R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
        R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
    B.map (L.functor.map (L.unitIso.hom.app X)) =
  (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
Tactic: rw [← cancel_mono (B.map (L.functor.map (NatTrans.app L.unitIso.hom X)))]
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ (R.functor.map (T.map (L.unitIso.hom.app X)) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
have iso : ((T ⋙ R.functor).map (L.unitIso.hom.app X) ≫
      R.functor.map
          (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
            R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
        R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
    B.map (L.functor.map (L.unitIso.hom.app X)) =
  (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
Tactic: rw [← Functor.comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ ((T ⋙ R.functor).map (L.unitIso.hom.app X) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
have iso : (R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map
          (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
            R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
        R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
    B.map (L.functor.map (L.unitIso.hom.app X)) =
  (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ (R.functor.map (T.map (L.unitIso.hom.app X)) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
have iso : R.functor.map (T.map (L.unitIso.hom.app X)) ≫
    R.functor.map (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
      R.counit.app (R.functor.obj (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
        (iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X)) ≫
          B.map (L.counitIso.hom.app (L.functor.obj X)) ≫ B.map (L.functor.map (L.unitIso.hom.app X)) =
  (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
Tactic: simp only [Functor.map_comp, Equivalence.fun_inv_map, Functor.comp_obj,
    Functor.id_obj, assoc, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.CatCommSq (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
        R.counit.app (R.functor.obj (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
          (iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X)) ≫
            B.map (L.counitIso.hom.app (L.functor.obj X)) ≫ B.map (L.functor.map (L.unitIso.hom.app X)) =
    (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
have iso : R.functor.map (T.map (L.unitIso.hom.app X)) ≫
    R.functor.map (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
      R.counit.app (R.functor.obj (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
        (iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X)) ≫
          B.map (𝟙 (L.functor.obj ((L.functor ⋙ L.inverse).obj X))) =
  (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
Tactic: rw [← B.map_comp, L.counit_app_functor, ← L.functor.map_comp, ← NatTrans.comp_app,
    Iso.inv_hom_id, NatTrans.id_app, L.functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
w : f = g
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h
have rw : g ≫ h = g ≫ h
Tactic: rw [w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ f = g
have h : f = f ≫ 𝟙 Y
Tactic: convert! w (𝟙 Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
h : f = f ≫ 𝟙 Y
⊢ f = g
have h₁ : g = g ≫ 𝟙 Y
Tactic: convert! w (𝟙 Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f = 𝟙 X
have h : f = f ≫ 𝟙 X
Tactic: convert! w (𝟙 X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
h : Y ⟶ Y
⊢ f ≫ h = f ↔ h = 𝟙 Y
have h₁ : f = f ≫ 𝟙 Y
Tactic: convert! cancel_epi f
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst_1 : Epi h
w : f ≫ g = h
⊢ Epi g
have inst : Epi (f ≫ g)
Tactic: subst h
Cleared hypotheses: h, inst_1, w
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Bipointed (goal)
Goal:
X Y Z : Bipointed
f : X.Hom Y
g : Y.Hom Z
⊢ (g.toFun ∘ f.toFun) X.toProd.1 = Z.toProd.1
have rw : g.toFun (f.toFun X.toProd.1) = Z.toProd.1
Tactic: rw [Function.comp_apply, f.map_fst, g.map_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Bipointed (goal)
Goal:
X Y Z : Bipointed
f : X.Hom Y
g : Y.Hom Z
rw : g.toFun (f.toFun X.toProd.1) = Z.toProd.1
⊢ (g.toFun ∘ f.toFun) X.toProd.1 = Z.toProd.1
have rw₁ : g.toFun Y.toProd.1 = Z.toProd.1
Tactic: rw [Function.comp_apply, f.map_fst, g.map_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Bipointed (goal)
Goal:
X Y Z : Bipointed
f : X.Hom Y
g : Y.Hom Z
rw : g.toFun (f.toFun X.toProd.1) = Z.toProd.1
rw₁ : g.toFun Y.toProd.1 = Z.toProd.1
⊢ (g.toFun ∘ f.toFun) X.toProd.1 = Z.toProd.1
have rw₂ : Z.toProd.1 = Z.toProd.1
Tactic: rw [Function.comp_apply, f.map_fst, g.map_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Bipointed (goal)
Goal:
X Y Z : Bipointed
f : X.Hom Y
g : Y.Hom Z
⊢ (g.toFun ∘ f.toFun) X.toProd.2 = Z.toProd.2
have rw : g.toFun (f.toFun X.toProd.2) = Z.toProd.2
Tactic: rw [Function.comp_apply, f.map_snd, g.map_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Bipointed (goal)
Goal:
X Y Z : Bipointed
f : X.Hom Y
g : Y.Hom Z
rw : g.toFun (f.toFun X.toProd.2) = Z.toProd.2
⊢ (g.toFun ∘ f.toFun) X.toProd.2 = Z.toProd.2
have rw₁ : g.toFun Y.toProd.2 = Z.toProd.2
Tactic: rw [Function.comp_apply, f.map_snd, g.map_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Bipointed (goal)
Goal:
X Y Z : Bipointed
f : X.Hom Y
g : Y.Hom Z
rw : g.toFun (f.toFun X.toProd.2) = Z.toProd.2
rw₁ : g.toFun Y.toProd.2 = Z.toProd.2
⊢ (g.toFun ∘ f.toFun) X.toProd.2 = Z.toProd.2
have rw₂ : Z.toProd.2 = Z.toProd.2
Tactic: rw [Function.comp_apply, f.map_snd, g.map_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Bipointed (goal)
Goal:
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
⊢ (fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
        ({ toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
            map_snd := ⋯ } :
          (pointedToBipointedFst.obj X).Hom Y))
      ((fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
          { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedFst.obj Y) })
        f) =
    f
have toFun : Bipointed.Hom.toFun
    ((fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
        ({ toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := sorry,
            map_snd := sorry } :
          (pointedToBipointedFst.obj X).Hom Y))
      ((fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
          { toFun := f.toFun ∘ some, map_point := sorry : X.Hom (bipointedToPointedFst.obj Y) })
        f)) =
  f.toFun
Tactic: apply Bipointed.Hom.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Bipointed (goal)
Goal:
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
⊢ Bipointed.Hom.toFun
      ((fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
              map_snd := ⋯ } :
            (pointedToBipointedFst.obj X).Hom Y))
        ((fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedFst.obj Y) })
          f)) =
    f.toFun
have toFun : ∀ (x : (pointedToBipointedFst.obj X).X),
  Bipointed.Hom.toFun
      ((fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := sorry,
              map_snd := sorry } :
            (pointedToBipointedFst.obj X).Hom Y))
        ((fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := sorry : X.Hom (bipointedToPointedFst.obj Y) })
          f))
      x =
    f.toFun x
Tactic: funext x