awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
Y : B'
⊢ (equivalence₁ hF).counitIso.hom.app Y = (equivalence₁CounitIso hF).hom.app Y

Tactic:
simp [equivalence₁, equivalence₀]

Premises used: AlgebraicTopology.DoldKan.Compatibility.equivalence₁, AlgebraicTopology.DoldKan.Compatibility.equivalence₀
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
w : ∀ (X : A), (equivalence₁ hF).unitIso.hom.app X = (equivalence₁UnitIso hF).hom.app X
⊢ (equivalence₁ hF).unitIso = equivalence₁UnitIso hF

Tactic:
ext X
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
X : A
⊢ (equivalence₁ hF).unitIso.hom.app X = (equivalence₁UnitIso hF).hom.app X

Tactic:
simp [equivalence₁]

Premises used: AlgebraicTopology.DoldKan.Compatibility.equivalence₁
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
⊢ (equivalence₂ eB hF).inverse = eB.functor ⋙ e'.inverse ⋙ eA.inverse

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
w : ∀ (Y' : B), (equivalence₂ eB hF).counitIso.hom.app Y' = (equivalence₂CounitIso eB hF).hom.app Y'
⊢ (equivalence₂ eB hF).counitIso = equivalence₂CounitIso eB hF

Tactic:
ext Y'
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
Y' : B
⊢ (equivalence₂ eB hF).counitIso.hom.app Y' = (equivalence₂CounitIso eB hF).hom.app Y'

Tactic:
simp [equivalence₂, equivalence₁CounitIso_eq]

Premises used: AlgebraicTopology.DoldKan.Compatibility.equivalence₂, AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_eq
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
w : ∀ (X : A), (equivalence₂ eB hF).unitIso.hom.app X = (equivalence₂UnitIso eB hF).hom.app X
⊢ (equivalence₂ eB hF).unitIso = equivalence₂UnitIso eB hF

Tactic:
ext X
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
X : A
⊢ (equivalence₂ eB hF).unitIso.hom.app X = (equivalence₂UnitIso eB hF).hom.app X

Tactic:
simp [equivalence₂, equivalence₁]

Premises used: AlgebraicTopology.DoldKan.Compatibility.equivalence₁, AlgebraicTopology.DoldKan.Compatibility.equivalence₂
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
⊢ (equivalence hF hG).functor = F ⋙ eB.inverse

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
w : (equivalence hF hG).counitIso.hom = (equivalenceCounitIso η).hom
⊢ (equivalence hF hG).counitIso = equivalenceCounitIso η

Tactic:
ext1
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
w : (equivalence hF hG).counitIso.hom.app = (equivalenceCounitIso η).hom.app
⊢ (equivalence hF hG).counitIso.hom = (equivalenceCounitIso η).hom

Tactic:
apply NatTrans.ext

Premises used: CategoryTheory.NatTrans.ext
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
w : ∀ (Y : B), (equivalence hF hG).counitIso.hom.app Y = (equivalenceCounitIso η).hom.app Y
⊢ (equivalence hF hG).counitIso.hom.app = (equivalenceCounitIso η).hom.app

Tactic:
ext Y
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
w :
  eB.inverse.map
        (F.map
          (𝟙 (G.obj Y) ≫
            eA.unitIso.hom.app (G.obj Y) ≫
              𝟙 (eA.inverse.obj (eA.functor.obj (G.obj Y))) ≫
                eA.inverse.map (hG.inv.app Y) ≫ 𝟙 (eA.inverse.obj (e'.inverse.obj (eB.functor.obj Y))))) ≫
      (equivalence₂ eB hF).counitIso.hom.app Y =
    (equivalenceCounitIso η).hom.app Y
⊢ (equivalence hF hG).counitIso.hom.app Y = (equivalenceCounitIso η).hom.app Y

Tactic:
dsimp [equivalence]

Premises used: AlgebraicTopology.DoldKan.Compatibility.equivalence
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
w :
  eB.inverse.map (F.map (eA.unitIso.hom.app (G.obj Y))) ≫
      eB.inverse.map (F.map (eA.inverse.map (hG.inv.app Y))) ≫
        eB.inverse.map (hF.inv.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj Y)))) ≫
          eB.inverse.map (e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y)))) ≫
            eB.inverse.map (e'.counitIso.hom.app (eB.functor.obj Y)) ≫ eB.unitIso.inv.app Y =
    eB.inverse.map (η.hom.app Y) ≫ eB.unitIso.inv.app Y
⊢ eB.inverse.map
        (F.map
          (𝟙 (G.obj Y) ≫
            eA.unitIso.hom.app (G.obj Y) ≫
              𝟙 (eA.inverse.obj (eA.functor.obj (G.obj Y))) ≫
                eA.inverse.map (hG.inv.app Y) ≫ 𝟙 (eA.inverse.obj (e'.inverse.obj (eB.functor.obj Y))))) ≫
      (equivalence₂ eB hF).counitIso.hom.app Y =
    (equivalenceCounitIso η).hom.app Y

Tactic:
simp only [comp_id, id_comp, Functor.map_comp, equivalence₂CounitIso_eq,
    equivalence₂CounitIso_hom_app, assoc, equivalenceCounitIso_hom_app]

Premises used: CategoryTheory.Category.assoc, AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_hom_app, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_hom_app, AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_eq, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
w :
  eB.inverse.map
        (F.map (eA.unitIso.hom.app (G.obj Y)) ≫
          F.map (eA.inverse.map (hG.inv.app Y)) ≫
            hF.inv.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj Y))) ≫
              e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y) ≫
      eB.unitIso.inv.app Y =
    eB.inverse.map (η.hom.app Y) ≫ eB.unitIso.inv.app Y
⊢ eB.inverse.map (F.map (eA.unitIso.hom.app (G.obj Y))) ≫
      eB.inverse.map (F.map (eA.inverse.map (hG.inv.app Y))) ≫
        eB.inverse.map (hF.inv.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj Y)))) ≫
          eB.inverse.map (e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y)))) ≫
            eB.inverse.map (e'.counitIso.hom.app (eB.functor.obj Y)) ≫ eB.unitIso.inv.app Y =
    eB.inverse.map (η.hom.app Y) ≫ eB.unitIso.inv.app Y

Tactic:
simp only [equivalence₂_inverse, comp_obj, ← τ₀_hom_app, hη, τ₁_hom_app, ←
    eB.inverse.map_comp_assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.map_comp_assoc, AlgebraicTopology.DoldKan.Compatibility.τ₁_hom_app, AlgebraicTopology.DoldKan.Compatibility.τ₀_hom_app, AlgebraicTopology.DoldKan.Compatibility.equivalence₂_inverse, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
w :
  eB.inverse.map
        (hF.inv.app (G.obj Y) ≫
          (eA.functor ⋙ e'.functor).map (eA.unitIso.hom.app (G.obj Y)) ≫
            (eA.functor ⋙ e'.functor).map (eA.inverse.map (hG.inv.app Y)) ≫
              e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y) ≫
      eB.unitIso.inv.app Y =
    eB.inverse.map (η.hom.app Y) ≫ eB.unitIso.inv.app Y
⊢ eB.inverse.map
        (F.map (eA.unitIso.hom.app (G.obj Y)) ≫
          F.map (eA.inverse.map (hG.inv.app Y)) ≫
            hF.inv.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj Y))) ≫
              e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y) ≫
      eB.unitIso.inv.app Y =
    eB.inverse.map (η.hom.app Y) ≫ eB.unitIso.inv.app Y

Tactic:
rw [hF.inv.naturality_assoc, hF.inv.naturality_assoc]

Premises used: CategoryTheory.Iso.inv, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
w :
  hF.inv.app (G.obj Y) ≫
      (eA.functor ⋙ e'.functor).map (eA.unitIso.hom.app (G.obj Y)) ≫
        (eA.functor ⋙ e'.functor).map (eA.inverse.map (hG.inv.app Y)) ≫
          e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫
            e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y =
    η.hom.app Y
⊢ eB.inverse.map
        (hF.inv.app (G.obj Y) ≫
          (eA.functor ⋙ e'.functor).map (eA.unitIso.hom.app (G.obj Y)) ≫
            (eA.functor ⋙ e'.functor).map (eA.inverse.map (hG.inv.app Y)) ≫
              e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y) ≫
      eB.unitIso.inv.app Y =
    eB.inverse.map (η.hom.app Y) ≫ eB.unitIso.inv.app Y

Tactic:
congr 2
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
w :
  hF.inv.app (G.obj Y) ≫
      (eA.functor ⋙ e'.functor).map (eA.unitIso.hom.app (G.obj Y)) ≫
        (eA.functor ⋙ e'.functor).map (eA.inverse.map (hG.inv.app Y)) ≫
          e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y)) ≫ hG.hom.app Y) ≫
            hF.hom.app (G.obj Y) ≫ η.hom.app Y =
    η.hom.app Y
⊢ hF.inv.app (G.obj Y) ≫
      (eA.functor ⋙ e'.functor).map (eA.unitIso.hom.app (G.obj Y)) ≫
        (eA.functor ⋙ e'.functor).map (eA.inverse.map (hG.inv.app Y)) ≫
          e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫
            e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y =
    η.hom.app Y

Tactic:
simp only [← e'.functor.map_comp_assoc]

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
w :
  hF.inv.app (G.obj Y) ≫
      e'.functor.map (eA.functor.map (eA.unitIso.hom.app (G.obj Y))) ≫
        e'.functor.map (eA.counit.app (eA.functor.obj (G.obj Y))) ≫
          e'.functor.map (hG.inv.app Y) ≫
            e'.functor.map (eA.counitInv.app (e'.inverse.obj (eB.functor.obj Y))) ≫
              e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y =
    η.hom.app Y
⊢ hF.inv.app (G.obj Y) ≫
      (eA.functor ⋙ e'.functor).map (eA.unitIso.hom.app (G.obj Y)) ≫
        (eA.functor ⋙ e'.functor).map (eA.inverse.map (hG.inv.app Y)) ≫
          e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y)) ≫ hG.hom.app Y) ≫
            hF.hom.app (G.obj Y) ≫ η.hom.app Y =
    η.hom.app Y

Tactic:
simp only [Functor.comp_map, Equivalence.fun_inv_map, comp_obj, id_obj, map_comp, assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Equivalence.fun_inv_map, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
w :
  hF.inv.app (G.obj Y) ≫
      e'.functor.map
          (eA.functor.map (eA.unitIso.hom.app (G.obj Y)) ≫
            eA.counit.app (eA.functor.obj (G.obj Y)) ≫
              hG.inv.app Y ≫
                eA.counitInv.app (e'.inverse.obj (eB.functor.obj Y)) ≫
                  eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y)) ≫ hG.hom.app Y) ≫
        hF.hom.app (G.obj Y) ≫ η.hom.app Y =
    η.hom.app Y
⊢ hF.inv.app (G.obj Y) ≫
      e'.functor.map (eA.functor.map (eA.unitIso.hom.app (G.obj Y))) ≫
        e'.functor.map (eA.counit.app (eA.functor.obj (G.obj Y))) ≫
          e'.functor.map (hG.inv.app Y) ≫
            e'.functor.map (eA.counitInv.app (e'.inverse.obj (eB.functor.obj Y))) ≫
              e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y =
    η.hom.app Y

Tactic:
simp only [← e'.functor.map_comp_assoc]

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ hF.inv.app (G.obj Y) ≫
      e'.functor.map
          (eA.functor.map (eA.unitIso.hom.app (G.obj Y)) ≫
            eA.counit.app (eA.functor.obj (G.obj Y)) ≫
              hG.inv.app Y ≫
                eA.counitInv.app (e'.inverse.obj (eB.functor.obj Y)) ≫
                  eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y)) ≫ hG.hom.app Y) ≫
        hF.hom.app (G.obj Y) ≫ η.hom.app Y =
    η.hom.app Y

Tactic:
simp only [Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app, comp_obj, comp_id,
    Equivalence.functor_unit_comp, map_id, id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Equivalence.functor_unit_comp, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility
Goal:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} A'
inst_2 : Category.{v_3, u_3} B
inst_3 : Category.{v_4, u_4} B'
eA : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} A A'
eB : CategoryTheory.Equivalence.{v_3, v_4, u_3, u_4} B B'
e' : CategoryTheory.Equivalence.{v_2, v_4, u_2, u_4} A' B'
F : CategoryTheory.Functor.{v_1, v_4, u_1, u_4} A B'
hF : eA.functor ⋙ e'.functor ≅ F
G : CategoryTheory.Functor.{v_3, v_1, u_3, u_1} B A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
w : (equivalence hF hG).unitIso.hom = (equivalenceUnitIso hG ε).hom
⊢ (equivalence hF hG).unitIso = equivalenceUnitIso hG ε

Tactic:
ext1