awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
s : Cone.{w, v, w, u} (wideCospan ι X)
f :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := WidePullbackShape ι) (F := wideCospan ι X)
      { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
        π :=
          {
            app := fun (X_1 : WidePullbackShape ι) ↦
              Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                Functor.obj.{w, v, w, u}
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                  Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                X_1
                (terminal.from
                  (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
            naturality := ⋯ } }
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          (Cone.π
            { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
              π :=
                {
                  app := fun (X_1 : WidePullbackShape ι) ↦
                    Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                      Functor.obj.{w, v, w, u}
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                        Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                      X_1
                      (terminal.from
                        (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                      fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
                  naturality := ⋯ } })
          j =
      s.π.app j
j : ι
⊢ f ≫ Pi.π (fun (x : ι) ↦ X) j = NatTrans.app (Cone.π (Fan.mk s.pt fun (j : ι) ↦ s.π.app (some j))) { as := j }
have h₁ : f ≫ Pi.π (fun (x : ι) ↦ X) j = s.π.app (some j)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
s : Cone.{w, v, w, u} (wideCospan ι X)
f :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := WidePullbackShape ι) (F := wideCospan ι X)
      { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
        π :=
          {
            app := fun (X_1 : WidePullbackShape ι) ↦
              Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                Functor.obj.{w, v, w, u}
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                  Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                X_1
                (terminal.from
                  (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                    (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
            naturality := ⋯ } }
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          (Cone.π
            { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
              π :=
                {
                  app := fun (X_1 : WidePullbackShape ι) ↦
                    Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                      Functor.obj.{w, v, w, u}
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                        Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                      X_1
                      (terminal.from
                        (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                      fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
                  naturality := ⋯ } })
          j =
      s.π.app j
j : ι
⊢ f ≫ Pi.π (fun (x : ι) ↦ X) j = s.π.app (some j)
have h₁ : f ≫ Pi.π (fun (x : ι) ↦ X) j =
  f ≫
    NatTrans.app
      (Cone.π
        { pt := piObj.{w, v, u} fun (x : ι) ↦ X,
          π :=
            {
              app := fun (X_1 : WidePullbackShape ι) ↦
                Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
                  Functor.obj.{w, v, w, u}
                      (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
                    Functor.obj.{w, v, w, u} (wideCospan ι X) x)
                  X_1
                  (terminal.from
                    (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                      (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
                  fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i },
              naturality := sorry } })
      (some j)
Tactic: rw [← h (some j)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
⊢ HasWidePullback.{w, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
    (fun (x : ι) ↦ Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) fun (x : ι) ↦
    Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))
have intro : ∀ (val : Fintype ι),
  HasWidePullback.{w, v, u} (Arrow.right.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X)))
    (fun (x : ι) ↦ Arrow.left.{v, u} (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))) fun (x : ι) ↦
    Arrow.hom (Arrow.mk (Y := terminal.{v, u} C) (terminal.from X))
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
j : ι
⊢ Eq.{v + 1} (α := limit.{w, w, v, u} (wideCospan ι X) ⟶ X)
    (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ι) ↦ X)
        (Iso.hom (limitIsoPi ι X) : limit.{w, w, v, u} (wideCospan ι X) ⟶ piObj.{w, v, u} fun (x : ι) ↦ X)
        (Pi.π (fun (x : ι) ↦ X) j : (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ X) :
      limit.{w, w, v, u} (wideCospan ι X) ⟶ X)
    (WidePullback.π (fun (x : ι) ↦ terminal.from X) j :
      (widePullback.{w, v, u} (terminal.{v, u} C) (fun (x : ι) ↦ X) fun (x : ι) ↦ terminal.from X) ⟶ X)
have rw : Eq.{v + 1} (α := limit.{w, w, v, u} (wideCospan ι X) ⟶ X)
  (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ι) ↦ X)
      (Iso.hom (limitIsoPi ι X) : limit.{w, w, v, u} (wideCospan ι X) ⟶ piObj.{w, v, u} fun (x : ι) ↦ X)
      (CategoryStruct.comp (Y := limit.{w, w, v, u} (wideCospan ι X))
          (Iso.inv (limitIsoPi ι X) : (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ limit.{w, w, v, u} (wideCospan ι X))
          (WidePullback.π (fun (x : ι) ↦ terminal.from X) j :
            (widePullback.{w, v, u} (terminal.{v, u} C) (fun (x : ι) ↦ X) fun (x : ι) ↦ terminal.from X) ⟶ X) :
        (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ X) :
    limit.{w, w, v, u} (wideCospan ι X) ⟶ X)
  (WidePullback.π (fun (x : ι) ↦ terminal.from X) j :
    (widePullback.{w, v, u} (terminal.{v, u} C) (fun (x : ι) ↦ X) fun (x : ι) ↦ terminal.from X) ⟶ X)
Tactic: rw [← wideCospan.limitIsoPi_inv_comp_pi, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
j : ι
rw :
  Eq.{v + 1} (α := limit.{w, w, v, u} (wideCospan ι X) ⟶ X)
    (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ι) ↦ X)
        (Iso.hom (limitIsoPi ι X) : limit.{w, w, v, u} (wideCospan ι X) ⟶ piObj.{w, v, u} fun (x : ι) ↦ X)
        (CategoryStruct.comp (Y := limit.{w, w, v, u} (wideCospan ι X))
            (Iso.inv (limitIsoPi ι X) : (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ limit.{w, w, v, u} (wideCospan ι X))
            (WidePullback.π (fun (x : ι) ↦ terminal.from X) j :
              (widePullback.{w, v, u} (terminal.{v, u} C) (fun (x : ι) ↦ X) fun (x : ι) ↦ terminal.from X) ⟶ X) :
          (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ X) :
      limit.{w, w, v, u} (wideCospan ι X) ⟶ X)
    (WidePullback.π (fun (x : ι) ↦ terminal.from X) j :
      (widePullback.{w, v, u} (terminal.{v, u} C) (fun (x : ι) ↦ X) fun (x : ι) ↦ terminal.from X) ⟶ X)
⊢ Eq.{v + 1} (α := limit.{w, w, v, u} (wideCospan ι X) ⟶ X)
    (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ι) ↦ X)
        (Iso.hom (limitIsoPi ι X) : limit.{w, w, v, u} (wideCospan ι X) ⟶ piObj.{w, v, u} fun (x : ι) ↦ X)
        (Pi.π (fun (x : ι) ↦ X) j : (piObj.{w, v, u} fun (x : ι) ↦ X) ⟶ X) :
      limit.{w, w, v, u} (wideCospan ι X) ⟶ X)
    (WidePullback.π (fun (x : ι) ↦ terminal.from X) j :
      (widePullback.{w, v, u} (terminal.{v, u} C) (fun (x : ι) ↦ X) fun (x : ι) ↦ terminal.from X) ⟶ X)
have rw₁ : Eq.{v + 1} (α := limit.{w, w, v, u} (wideCospan ι X) ⟶ X) (WidePullback.π (fun (x : ι) ↦ terminal.from X) j)
  (WidePullback.π (fun (x : ι) ↦ terminal.from X) j)
Tactic: rw [← wideCospan.limitIsoPi_inv_comp_pi, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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
⊢ (equivalence₁ hF).counitIso = equivalence₁CounitIso hF
have w : ∀ (Y : B'), (equivalence₁ hF).counitIso.hom.app Y = (equivalence₁CounitIso hF).hom.app Y
Tactic: ext Y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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
⊢ (equivalence₁ hF).unitIso = equivalence₁UnitIso hF
have w : ∀ (X : A), (equivalence₁ hF).unitIso.hom.app X = (equivalence₁UnitIso hF).hom.app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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).counitIso = equivalence₂CounitIso eB hF
have w : ∀ (Y' : B), (equivalence₂ eB hF).counitIso.hom.app Y' = (equivalence₂CounitIso eB hF).hom.app Y'
Tactic: ext Y'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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).unitIso = equivalence₂UnitIso eB hF
have w : ∀ (X : A), (equivalence₂ eB hF).unitIso.hom.app X = (equivalence₂UnitIso eB hF).hom.app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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 η
⊢ (equivalence hF hG).counitIso = equivalenceCounitIso η
have w : (equivalence hF hG).counitIso.hom = (equivalenceCounitIso η).hom
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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 η
⊢ (equivalence hF hG).counitIso.hom = (equivalenceCounitIso η).hom
have w : (equivalence hF hG).counitIso.hom.app = (equivalenceCounitIso η).hom.app
Tactic: apply NatTrans.ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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 η
⊢ (equivalence hF hG).counitIso.hom.app = (equivalenceCounitIso η).hom.app
have w : ∀ (Y : B), (equivalence hF hG).counitIso.hom.app Y = (equivalenceCounitIso η).hom.app Y
Tactic: ext Y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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
⊢ (equivalence hF hG).counitIso.hom.app Y = (equivalenceCounitIso η).hom.app Y
have 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
Tactic: dsimp [equivalence]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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
⊢ 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
have 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
Tactic: simp only [comp_id, id_comp, Functor.map_comp, equivalence₂CounitIso_eq,
    equivalence₂CounitIso_hom_app, assoc, equivalenceCounitIso_hom_app]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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
⊢ 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
have 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
Tactic: simp only [equivalence₂_inverse, comp_obj, ← τ₀_hom_app, hη, τ₁_hom_app, ←
    eB.inverse.map_comp_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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
⊢ 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
have 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
Tactic: rw [hF.inv.naturality_assoc, hF.inv.naturality_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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
⊢ 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
have 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
Tactic: congr 2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Compatibility (goal)
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) ≫
      (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
have 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
Tactic: simp only [← e'.functor.map_comp_assoc]