awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f (CategoryTheory.Functor.map N₁ f ≫ inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₁ X))) i)
⊢ ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f) ≫ CategoryTheory.Functor.map N₁ f)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₁ Y))) i)

Tactic:
have h₂ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.inv_hom_id (N₁.map f)))
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f (CategoryTheory.Functor.map N₁ f ≫ inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₁ X))) i)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f) ≫ CategoryTheory.Functor.map N₁ f)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₁ Y))) i)
⊢ ∀ (n : ℕ),
    Eq (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f (Karoubi.p (Functor.obj N₁ Y)) n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f (Karoubi.p (Functor.obj N₁ X)) n ≫ f.app (op ⦋n⦌))

Tactic:
have h₃ := fun n =>
      Karoubi.HomologicalComplex.p_comm_f_assoc (inv (N₁.map f)) n (f.app (op ⦋n⦌))
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f (CategoryTheory.Functor.map N₁ f ≫ inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₁ X))) i)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f) ≫ CategoryTheory.Functor.map N₁ f)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₁ Y))) i)
h₃ :
  ∀ (n : ℕ),
    Eq (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f (Karoubi.p (Functor.obj N₁ Y)) n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f (Karoubi.p (Functor.obj N₁ X)) n ≫ f.app (op ⦋n⦌))
⊢ ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)

Tactic:
simp only [N₁_map_f, Karoubi.comp_f, HomologicalComplex.comp_f,
      AlternatingFaceMapComplex.map_f, N₁_obj_p, Karoubi.id_f, assoc] at h₁ h₂ h₃

Premises used: CategoryTheory.Category.assoc, AlgebraicTopology.DoldKan.N₁_map_f, AlgebraicTopology.DoldKan.N₁_obj_p, AlgebraicTopology.AlternatingFaceMapComplex.map_f, CategoryTheory.Idempotents.Karoubi.id_f, CategoryTheory.Idempotents.Karoubi.comp_f, HomologicalComplex.comp_f
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i ≫
        HomologicalComplex.Hom.f PInfty i ≫ f.app (op ⦋i⦌))
      (HomologicalComplex.Hom.f PInfty i)
h₃ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)
h :
  f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 = 𝟙 (X _⦋0⦌) ∧
    Eq (α := Y _⦋0⦌ ⟶ Y _⦋0⦌)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 ≫ f.app (op ⦋0⦌) :
        Y _⦋0⦌ ⟶ Y _⦋0⦌)
      (𝟙 (Y _⦋0⦌) : Y _⦋0⦌ ⟶ Y _⦋0⦌)
⊢ IsIso (X := X _⦋0⦌) (f.app (op ⦋0⦌))

Tactic:
use (inv (N₁.map f)).f.f 0

Premises used: CategoryTheory.Idempotents.Karoubi.Hom.f, HomologicalComplex.Hom.f, CategoryTheory.Functor.map, AlgebraicTopology.DoldKan.N₁, CategoryTheory.inv, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i ≫
        HomologicalComplex.Hom.f PInfty i ≫ f.app (op ⦋i⦌))
      (HomologicalComplex.Hom.f PInfty i)
h₃ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) 0 ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) 0)
    (HomologicalComplex.Hom.f PInfty 0 ≫
      f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0)
    (HomologicalComplex.Hom.f PInfty 0)

Tactic:
have h₁₀ := h₁ 0
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i ≫
        HomologicalComplex.Hom.f PInfty i ≫ f.app (op ⦋i⦌))
      (HomologicalComplex.Hom.f PInfty i)
h₃ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)
h₁₀ :
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) 0 ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) 0)
    (HomologicalComplex.Hom.f PInfty 0 ≫
      f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0)
    (HomologicalComplex.Hom.f PInfty 0)
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) 0 ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) 0)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 ≫
      HomologicalComplex.Hom.f PInfty 0 ≫ f.app (op ⦋0⦌))
    (HomologicalComplex.Hom.f PInfty 0)

Tactic:
have h₂₀ := h₂ 0
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i ≫
        HomologicalComplex.Hom.f PInfty i ≫ f.app (op ⦋i⦌))
      (HomologicalComplex.Hom.f PInfty i)
h₃ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)
h₁₀ :
  𝟙 (X _⦋0⦌) ≫ f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 =
    𝟙 (X _⦋0⦌)
h₂₀ :
  Eq (α := Y _⦋0⦌ ⟶ Y _⦋0⦌)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 ≫ 𝟙 (X _⦋0⦌) ≫ f.app (op ⦋0⦌) :
      Y _⦋0⦌ ⟶ Y _⦋0⦌)
    (𝟙 (Y _⦋0⦌) : Y _⦋0⦌ ⟶ Y _⦋0⦌)
⊢ f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 = 𝟙 (X _⦋0⦌)

Tactic:
simp only [id_comp] at h₁₀ h₂₀

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i ≫
        HomologicalComplex.Hom.f PInfty i ≫ f.app (op ⦋i⦌))
      (HomologicalComplex.Hom.f PInfty i)
h₃ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)
h₁₀ :
  𝟙 (X _⦋0⦌) ≫ f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 =
    𝟙 (X _⦋0⦌)
h₂₀ :
  Eq (α := Y _⦋0⦌ ⟶ Y _⦋0⦌)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 ≫ 𝟙 (X _⦋0⦌) ≫ f.app (op ⦋0⦌) :
      Y _⦋0⦌ ⟶ Y _⦋0⦌)
    (𝟙 (Y _⦋0⦌) : Y _⦋0⦌ ⟶ Y _⦋0⦌)
h₁₁ : f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 = 𝟙 (X _⦋0⦌)
⊢ Eq (α := Y _⦋0⦌ ⟶ Y _⦋0⦌)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 ≫ f.app (op ⦋0⦌) :
      Y _⦋0⦌ ⟶ Y _⦋0⦌)
    (𝟙 (Y _⦋0⦌) : Y _⦋0⦌ ⟶ Y _⦋0⦌)

Tactic:
simp only [id_comp] at h₁₀ h₂₀

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i ≫
        HomologicalComplex.Hom.f PInfty i ≫ f.app (op ⦋i⦌))
      (HomologicalComplex.Hom.f PInfty i)
h₃ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)
h₁₀ : f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 = 𝟙 (X _⦋0⦌)
h₂₀ :
  Eq (α := Y _⦋0⦌ ⟶ Y _⦋0⦌)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 ≫ f.app (op ⦋0⦌) :
      Y _⦋0⦌ ⟶ Y _⦋0⦌)
    (𝟙 (Y _⦋0⦌) : Y _⦋0⦌ ⟶ Y _⦋0⦌)
h : f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 = 𝟙 (X _⦋0⦌)
h₄ :
  Eq (α := Y _⦋0⦌ ⟶ Y _⦋0⦌)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 ≫ f.app (op ⦋0⦌) :
      Y _⦋0⦌ ⟶ Y _⦋0⦌)
    (𝟙 (Y _⦋0⦌) : Y _⦋0⦌ ⟶ Y _⦋0⦌)
⊢ f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 = 𝟙 (X _⦋0⦌) ∧
    Eq (α := Y _⦋0⦌ ⟶ Y _⦋0⦌)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 ≫ f.app (op ⦋0⦌) :
        Y _⦋0⦌ ⟶ Y _⦋0⦌)
      (𝟙 (Y _⦋0⦌) : Y _⦋0⦌ ⟶ Y _⦋0⦌)

Tactic:
tauto
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i ≫
        HomologicalComplex.Hom.f PInfty i ≫ f.app (op ⦋i⦌))
      (HomologicalComplex.Hom.f PInfty i)
h₃ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)
n : ℕ
hn : IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))
h :
  f.app (op ⦋n + 1⦌) ≫
        φ
          {
            a :=
              CategoryStruct.comp (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj Y) (n + 1))
                (HomologicalComplex.Hom.f PInfty (n + 1))
                (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) (n + 1)),
            b := fun (i : Fin (n + 1)) ↦ inv (f.app (op ⦋n⦌)) ≫ X.σ i } =
      𝟙 (X _⦋n + 1⦌) ∧
    φ
          {
            a :=
              CategoryStruct.comp (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj Y) (n + 1))
                (HomologicalComplex.Hom.f PInfty (n + 1))
                (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) (n + 1)),
            b := fun (i : Fin (n + 1)) ↦ inv (f.app (op ⦋n⦌)) ≫ X.σ i } ≫
        f.app (op ⦋n + 1⦌) =
      𝟙 (Y _⦋n + 1⦌)
⊢ IsIso (X := X _⦋n + 1⦌) (f.app (op ⦋n + 1⦌))

Tactic:
use φ { a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1)
              b := fun i => inv (f.app (op ⦋n⦌)) ≫ X.σ i }

Premises used: CategoryTheory.Idempotents.Karoubi.Hom.f, HomologicalComplex.Hom.f, AlgebraicTopology.DoldKan.MorphComponents.mk, AlgebraicTopology.DoldKan.PInfty, CategoryTheory.Functor.map, HAdd.hAdd, SimplexCategory.mk, Opposite.op, CategoryTheory.CategoryStruct.comp, AlgebraicTopology.DoldKan.N₁, CategoryTheory.inv, OfNat.ofNat, AlgebraicTopology.DoldKan.MorphComponents.φ, CategoryTheory.NatTrans.app, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i ≫
        HomologicalComplex.Hom.f PInfty i ≫ f.app (op ⦋i⦌))
      (HomologicalComplex.Hom.f PInfty i)
h₃ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)
n : ℕ
hn : IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))
⊢ f.app (op ⦋n + 1⦌) ≫
        φ
          {
            a :=
              CategoryStruct.comp (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj Y) (n + 1))
                (HomologicalComplex.Hom.f PInfty (n + 1))
                (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) (n + 1)),
            b := fun (i : Fin (n + 1)) ↦ inv (f.app (op ⦋n⦌)) ≫ X.σ i } =
      𝟙 (X _⦋n + 1⦌) ∧
    φ
          {
            a :=
              CategoryStruct.comp (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj Y) (n + 1))
                (HomologicalComplex.Hom.f PInfty (n + 1))
                (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) (n + 1)),
            b := fun (i : Fin (n + 1)) ↦ inv (f.app (op ⦋n⦌)) ≫ X.σ i } ≫
        f.app (op ⦋n + 1⦌) =
      𝟙 (Y _⦋n + 1⦌)

Tactic:
simp only [MorphComponents.id, ← id_φ, ← preComp_φ, preComp, ← postComp_φ, postComp,
        PInfty_f_naturality_assoc, IsIso.hom_inv_id_assoc, assoc, IsIso.inv_hom_id_assoc,
        SimplicialObject.σ_naturality, h₁, h₂, h₃, and_self]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SimplicialObject.σ_naturality, and_self, AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc, AlgebraicTopology.DoldKan.MorphComponents.id_φ, CategoryTheory.IsIso.hom_inv_id_assoc, AlgebraicTopology.DoldKan.MorphComponents.postComp, AlgebraicTopology.DoldKan.MorphComponents.preComp_φ, AlgebraicTopology.DoldKan.MorphComponents.preComp, AlgebraicTopology.DoldKan.MorphComponents.postComp_φ, AlgebraicTopology.DoldKan.MorphComponents.id, CategoryTheory.IsIso.inv_hom_id_assoc