awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Reduced (goal)
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Preadditive.{v_2, u_1} A
inst_4 : ι.Additive
X : A
h₁ :
  Karoubi.Hom.f
      (Arrow.Hom.left
        (Arrow.homMk
            { f := ι.map ((F' Λ).obj X).p, comm := ⋯ :
              (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
                      (NatTrans.app (π' Λ) X)).left.Hom
                (Arrow.mk (X := Functor.obj (toKaroubi A) ((Λ.F ⋙ ι).obj X))
                    (Functor.map (toKaroubi A) (Λ.π.app X))).left }
            (𝟙
              (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
                  (NatTrans.app (π' Λ) X)).right)
            ⋯ ≫
          Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := ⋯ }
            (𝟙
              (Arrow.mk (X := Functor.obj (toKaroubi A) ((Λ.F ⋙ ι).obj X))
                  (Functor.map (toKaroubi A) (Λ.π.app X))).right)
            ⋯)) =
    (Arrow.Hom.left
        (𝟙
          (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
            (NatTrans.app (π' Λ) X)))).f
⊢ Arrow.homMk
        { f := ι.map ((F' Λ).obj X).p, comm := ⋯ :
          (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
                  (NatTrans.app (π' Λ) X)).left.Hom
            (Arrow.mk (X := Functor.obj (toKaroubi A) ((Λ.F ⋙ ι).obj X)) (Functor.map (toKaroubi A) (Λ.π.app X))).left }
        (𝟙
          (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
              (NatTrans.app (π' Λ) X)).right)
        ⋯ ≫
      Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := ⋯ }
        (𝟙 (Arrow.mk (X := Functor.obj (toKaroubi A) ((Λ.F ⋙ ι).obj X)) (Functor.map (toKaroubi A) (Λ.π.app X))).right)
        ⋯ =
    𝟙 (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X) (NatTrans.app (π' Λ) X))
have h₂ : Karoubi.Hom.f
    (Arrow.Hom.right
      (Arrow.homMk
          { f := ι.map ((F' Λ).obj X).p, comm := sorry :
            (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
                    (NatTrans.app (π' Λ) X)).left.Hom
              (Arrow.mk (X := Functor.obj (toKaroubi A) ((Λ.F ⋙ ι).obj X))
                  (Functor.map (toKaroubi A) (Λ.π.app X))).left }
          (𝟙
            (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
                (NatTrans.app (π' Λ) X)).right)
          sorry ≫
        Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := sorry }
          (𝟙
            (Arrow.mk (X := Functor.obj (toKaroubi A) ((Λ.F ⋙ ι).obj X)) (Functor.map (toKaroubi A) (Λ.π.app X))).right)
          sorry)) =
  (Arrow.Hom.right
      (𝟙 (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X) (NatTrans.app (π' Λ) X)))).f
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Reduced (goal)
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Preadditive.{v_2, u_1} A
inst_4 : ι.Additive
X : A
⊢ Epi (X := (karoubi.F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj (Functor.obj (toKaroubi A) X))
    (NatTrans.app (karoubi.π Λ) (Functor.obj (toKaroubi A) X))
have rw : Epi (X := (karoubi.F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj (Functor.obj (toKaroubi A) X))
  (NatTrans.app (karoubi.π' Λ) X)
Tactic: rw [karoubi.π_app_toKaroubi_obj]
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Reduced (goal)
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Preadditive.{v_2, u_1} A
inst_4 : ι.Additive
inst_5 : IsIdempotentComplete.{v_2, u_1} A
inst_6 : IsIdempotentComplete.{v_1, u_2} C
⊢ Λ.reduced.F.PreservesZeroMorphisms
have dsimp : (Equivalence.functor (toKaroubiEquivalence A) ⋙
    karoubi.F Λ ⋙ Equivalence.inverse (toKaroubiEquivalence C)).PreservesZeroMorphisms
Tactic: dsimp [reduced, transport]
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Transport (goal)
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
A' : Type u_3
C' : Type u_4
inst_2 : Category.{v_3, u_4} C'
inst_3 : Category.{v_4, u_3} A'
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
ι' : Functor.{v_3, v_4, u_4, u_3} C' A'
eA : Equivalence.{v_4, v_2, u_3, u_1} A' A
eC : Equivalence.{v_3, v_1, u_4, u_2} C' C
e : ι' ⋙ eA.functor ≅ eC.functor ⋙ ι
x : A'
⊢ Epi (Y := obj.{v_4, v_4, u_3, u_3} (𝟭 A') x)
    (NatTrans.app
      (((eA.functor ⋙ Λ.F ⋙ eC.inverse) ⋙ ι').rightUnitor.inv ≫
        ((eA.functor ⋙ Λ.F ⋙ eC.inverse) ⋙ ι').whiskerLeft eA.unitIso.hom ≫
          ((eA.functor ⋙ Λ.F ⋙ eC.inverse).associator ι' (eA.functor ⋙ eA.inverse)).hom ≫
            (eA.functor ⋙ Λ.F ⋙ eC.inverse).whiskerLeft (ι'.associator eA.functor eA.inverse).inv ≫
              (eA.functor ⋙ Λ.F ⋙ eC.inverse).whiskerLeft (whiskerRight e.hom eA.inverse) ≫
                ((eA.functor ⋙ Λ.F ⋙ eC.inverse).associator (eC.functor ⋙ ι) eA.inverse).inv ≫
                  whiskerRight ((eA.functor ⋙ Λ.F ⋙ eC.inverse).associator eC.functor ι).inv eA.inverse ≫
                    whiskerRight (whiskerRight (eA.functor.associator (Λ.F ⋙ eC.inverse) eC.functor).hom ι) eA.inverse ≫
                      whiskerRight
                          (whiskerRight
                            (eA.functor.whiskerLeft
                              ((Λ.F.associator eC.inverse eC.functor).hom ≫
                                Λ.F.whiskerLeft eC.counitIso.hom ≫ Λ.F.rightUnitor.hom))
                            ι)
                          eA.inverse ≫
                        whiskerRight
                            ((eA.functor.associator Λ.F ι).hom ≫
                              eA.functor.whiskerLeft Λ.π ≫ eA.functor.rightUnitor.hom)
                            eA.inverse ≫
                          eA.unitIso.inv)
      x)
have dsimp : Epi (Y := x)
  (𝟙 (ι'.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x)))) ≫
    eA.unitIso.hom.app (ι'.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x)))) ≫
      𝟙 (eA.inverse.obj (eA.functor.obj (ι'.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x)))))) ≫
        𝟙 (eA.inverse.obj (eA.functor.obj (ι'.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x)))))) ≫
          eA.inverse.map (e.hom.app (eC.inverse.obj (Λ.F.obj (eA.functor.obj x)))) ≫
            𝟙 (eA.inverse.obj (ι.obj (eC.functor.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x)))))) ≫
              eA.inverse.map (𝟙 (ι.obj (eC.functor.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x)))))) ≫
                eA.inverse.map (ι.map (𝟙 (eC.functor.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x)))))) ≫
                  eA.inverse.map
                      (ι.map
                        (𝟙 (eC.functor.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x)))) ≫
                          eC.counitIso.hom.app (Λ.F.obj (eA.functor.obj x)) ≫ 𝟙 (Λ.F.obj (eA.functor.obj x)))) ≫
                    eA.inverse.map
                        (𝟙 (ι.obj (Λ.F.obj (eA.functor.obj x))) ≫ Λ.π.app (eA.functor.obj x) ≫ 𝟙 (eA.functor.obj x)) ≫
                      eA.unitIso.inv.app x)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Transport (goal)
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
A' : Type u_3
C' : Type u_4
inst_2 : Category.{v_3, u_4} C'
inst_3 : Category.{v_4, u_3} A'
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
ι' : Functor.{v_3, v_2, u_4, u_1} C' A
G : Functor.{v_1, v_3, u_2, u_4} C C'
e : G ⋙ ι' ≅ ι
x : A
⊢ Epi (((Λ.F.associator G ι').hom ≫ Λ.F.whiskerLeft e.hom ≫ Λ.π).app x)
have dsimp : Epi (𝟙 (ι'.obj (G.obj (Λ.F.obj x))) ≫ e.hom.app (Λ.F.obj x) ≫ Λ.π.app x)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Linear (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Category.{v_2, u_3} D
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : Linear.{u_1, v_1, u_2} R C
inst_6 : Linear.{u_1, v_2, u_3} R D
ι : Type u_4
c : ComplexShape ι
X_1 Y_1 X Y : HomologicalComplex.{v_1, u_2, u_4} C c
x x_1 : R
x_2 : X ⟶ Y
⊢ (x * x_1) • x_2 = x • x_1 • x_2
have h : ∀ (i : ι), ((x * x_1) • x_2).f i = (x • x_1 • x_2).f i
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.Linear (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Category.{v_2, u_3} D
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : Linear.{u_1, v_1, u_2} R C
inst_6 : Linear.{u_1, v_2, u_3} R D
ι : Type u_4
c : ComplexShape ι
X_1 Y_1 X Y : HomologicalComplex.{v_1, u_2, u_4} C c
x x_1 : R
x_2 : X ⟶ Y
⊢ (x + x_1) • x_2 = x • x_2 + x_1 • x_2
have h : ∀ (i : ι), ((x + x_1) • x_2).f i = (x • x_2 + x_1 • x_2).f i
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.LocalCohomology (goal)
Goal:
R : Type u
inst : CommRing R
J : Ideal R
k : ℕᵒᵖ
⊢ J ≤ ((idealPowersDiagram J).obj k).radical
have change : J ≤ (J ^ unop k).radical
Tactic: change _ ≤ (J ^ unop k).radical
-- Lean 4 proof step from Mathlib.Algebra.Homology.LocalCohomology (goal)
Goal:
R : Type u
inst : CommRing R
J : Ideal R
k : ℕᵒᵖ
⊢ J ≤ (J ^ unop k).radical
have zero : J ≤ (HPow.hPow (β := ℕ) J 0).radical
Tactic: rcases unop k with - | n
-- Lean 4 proof step from Mathlib.Algebra.Homology.LocalCohomology (goal)
Goal:
R : Type u
inst : CommRing R
J : Ideal R
k : ℕᵒᵖ
zero : J ≤ (HPow.hPow (β := ℕ) J 0).radical
⊢ J ≤ (J ^ unop k).radical
have succ : ∀ (n : ℕ), J ≤ (J ^ (n + 1)).radical
Tactic: rcases unop k with - | n
-- Lean 4 proof step from Mathlib.Algebra.Homology.LocalCohomology (goal)
Goal:
R : Type u
inst : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ IsConnected.{0, u} (CostructuredArrow (idealPowersToSelfLERadical J) J')
have inst : Nonempty.{u + 1} (CostructuredArrow (idealPowersToSelfLERadical J) J')
Tactic: apply +allowSynthFailures zigzag_isConnected
-- Lean 4 proof step from Mathlib.Algebra.Homology.LocalCohomology (goal)
Goal:
R : Type u
inst_1 : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
inst : Nonempty.{u + 1} (CostructuredArrow (idealPowersToSelfLERadical J) J')
⊢ IsConnected.{0, u} (CostructuredArrow (idealPowersToSelfLERadical J) J')
have h : ∀ (j₁ j₂ : CostructuredArrow (idealPowersToSelfLERadical J) J'), Zigzag j₁ j₂
Tactic: apply +allowSynthFailures zigzag_isConnected
-- Lean 4 proof step from Mathlib.Algebra.Homology.LocalCohomology (goal)
Goal:
R : Type u
inst : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ Nonempty.{u + 1} (CostructuredArrow (idealPowersToSelfLERadical J) J')
have inst : ∀ (k : ℕ) (hk : J ^ k ≤ J'.obj (P := fun (J' : Ideal R) ↦ J ≤ J'.radical)),
  Nonempty.{u + 1} (CostructuredArrow (idealPowersToSelfLERadical J) J')
Tactic: obtain ⟨k, hk⟩ := Ideal.exists_pow_le_of_le_radical_of_fg J'.2 (isNoetherian_def.mp hR _)
-- Lean 4 proof step from Mathlib.Algebra.Homology.LocalCohomology (goal)
Goal:
R : Type u
inst : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
⊢ Zigzag j1 j2
have h : Zag j1 j2
Tactic: apply Relation.ReflTransGen.single
-- Lean 4 proof step from Mathlib.Algebra.Homology.LocalCohomology (goal)
Goal:
R : Type u
inst : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
⊢ Zag j1 j2
have h : ∀ (h : unop j1.left ≤ unop j2.left), Zag j1 j2
Tactic: rcases le_total (unop j1.left) (unop j2.left) with h | h
-- Lean 4 proof step from Mathlib.Algebra.Homology.LocalCohomology (goal)
Goal:
R : Type u
inst : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : ∀ (h : unop j1.left ≤ unop j2.left), Zag j1 j2
⊢ Zag j1 j2
have h₁ : ∀ (h : unop j2.left ≤ unop j1.left), Zag j1 j2
Tactic: rcases le_total (unop j1.left) (unop j2.left) with h | h
-- Lean 4 proof step from Mathlib.Algebra.Homology.LocalCohomology (goal)
Goal:
R : Type u
inst : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : unop j1.left ≤ unop j2.left
⊢ Zag j1 j2
have h₁ : Nonempty (j2 ⟶ j1)
Tactic: right
-- Lean 4 proof step from Mathlib.Algebra.Homology.LocalCohomology (goal)
Goal:
R : Type u
inst : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : unop j2.left ≤ unop j1.left
⊢ Zag j1 j2
have h₁ : Nonempty (j1 ⟶ j2)
Tactic: left
-- Lean 4 proof step from Mathlib.Algebra.Homology.LocalCohomology (goal)
Goal:
R : Type u
inst : CommRing R
I J K : Ideal R
hJK : J.radical = K.radical
L : Ideal R
hL : J ≤ L.radical
⊢ K ≤ L.radical
have rw : ∀ (hL : J.radical ≤ L.radical), K.radical ≤ L.radical
Tactic: rw [← Ideal.radical_le_radical_iff] at hL ⊢
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
i : ι
x x_1 : HomologicalComplex.{v_1, u_1, u_2} C c
x_2 : x ⟶ x_1
hf : quasiIso C c x_2
⊢ IsIso (X := Functor.obj (homologyFunctor C c i) x) (CategoryTheory.Functor.map (homologyFunctor C c i) x_2)
have hf₁ : QuasiIso x_2
Tactic: rw [mem_quasiIso_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
i : ι
x x_1 : HomologicalComplex.{v_1, u_1, u_2} C c
x_2 : x ⟶ x_1
hf : QuasiIso x_2
⊢ IsIso (X := Functor.obj (homologyFunctor C c i) x) (CategoryTheory.Functor.map (homologyFunctor C c i) x_2)
have dsimp : IsIso (X := x.homology i) (Y := x_1.homology i) (homologyMap x_2 i)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
⊢ IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
      (CategoryTheory.Functor.map Q f) ↔
    HomologicalComplex.quasiIso C c f
have mp : IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
    (CategoryTheory.Functor.map Q f) →
  HomologicalComplex.quasiIso C c f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
mp :
  IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
      (CategoryTheory.Functor.map Q f) →
    HomologicalComplex.quasiIso C c f
⊢ IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
      (CategoryTheory.Functor.map Q f) ↔
    HomologicalComplex.quasiIso C c f
have mpr : HomologicalComplex.quasiIso C c f →
  IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
    (CategoryTheory.Functor.map Q f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
h :
  IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
    (CategoryTheory.Functor.map Q f)
⊢ HomologicalComplex.quasiIso C c f
have mp : ∀ (i : ι), QuasiIsoAt f i
Tactic: rw [HomologicalComplex.mem_quasiIso_iff, quasiIso_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
h :
  IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
    (CategoryTheory.Functor.map Q f)
i : ι
⊢ QuasiIsoAt f i
have mp : IsIso (X := K.homology i) (Y := L.homology i) (HomologicalComplex.homologyMap f i)
Tactic: rw [quasiIsoAt_iff_isIso_homologyMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
h :
  IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
    (CategoryTheory.Functor.map Q f)
i : ι
⊢ IsIso (X := K.homology i) (Y := L.homology i) (HomologicalComplex.homologyMap f i)
have mp : IsIso (X :=
  Functor.obj (Functor.comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) Q (homologyFunctor C c i)) K)
  (CategoryTheory.Functor.map
    (Functor.comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) Q (homologyFunctor C c i)) f)
Tactic: refine (NatIso.isIso_map_iff (homologyFunctorFactors C c i) f).1 ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
h :
  IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
    (CategoryTheory.Functor.map Q f)
i : ι
⊢ IsIso (X :=
    Functor.obj (Functor.comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) Q (homologyFunctor C c i))
      K)
    (CategoryTheory.Functor.map
      (Functor.comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) Q (homologyFunctor C c i)) f)
have mp : IsIso (X :=
  Functor.obj (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (homologyFunctor C c i) (Functor.obj Q K))
  (CategoryTheory.Functor.map (homologyFunctor C c i) (CategoryTheory.Functor.map Q f))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
⊢ quasiIso C c (X := Functor.obj (quotient C c) K) (CategoryTheory.Functor.map (quotient C c) f) ↔
    HomologicalComplex.quasiIso C c f
have eq : ∀ (i : ι),
  IsIso (X := Functor.obj (quotient C c ⋙ homologyFunctor C c i) K)
      (CategoryTheory.Functor.map (quotient C c ⋙ homologyFunctor C c i) f) ↔
    IsIso (X := Functor.obj (HomologicalComplex.homologyFunctor C c i) K)
      (CategoryTheory.Functor.map (HomologicalComplex.homologyFunctor C c i) f)
Tactic: have eq := fun (i : ι) => NatIso.isIso_map_iff (homologyFunctorFactors C c i) f
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
⊢ MorphismProperty.RespectsIso (C := HomotopyCategory.{v_1, u_1, u_2} C c) (quasiIso C c)
have hP : ∀ (f g : Arrow (HomotopyCategory.{v_1, u_1, u_2} C c)) (x : f ≅ g), quasiIso C c f.hom → quasiIso C c g.hom
Tactic: apply MorphismProperty.RespectsIso.of_respects_arrow_iso
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
X Y Z : HomotopyCategory.{v_1, u_1, u_2} C c
f : X ⟶ Y
g : Y ⟶ Z
hf : quasiIso C c f
hg : quasiIso C c g
⊢ quasiIso C c (f ≫ g)
have hf₁ : ∀ (n : ι), IsIso (X := Functor.obj (homologyFunctor C c n) X) (CategoryTheory.Functor.map (homologyFunctor C c n) f)
Tactic: rw [mem_quasiIso_iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
X Y Z : HomotopyCategory.{v_1, u_1, u_2} C c
f : X ⟶ Y
g : Y ⟶ Z
hf : quasiIso C c f
hg : quasiIso C c g
hf₁ :
  ∀ (n : ι), IsIso (X := Functor.obj (homologyFunctor C c n) X) (CategoryTheory.Functor.map (homologyFunctor C c n) f)
⊢ quasiIso C c (f ≫ g)
have hg₁ : ∀ (n : ι), IsIso (X := Functor.obj (homologyFunctor C c n) Y) (CategoryTheory.Functor.map (homologyFunctor C c n) g)
Tactic: rw [mem_quasiIso_iff] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
X Y Z : HomotopyCategory.{v_1, u_1, u_2} C c
f : X ⟶ Y
g : Y ⟶ Z
hf :
  ∀ (n : ι), IsIso (X := Functor.obj (homologyFunctor C c n) X) (CategoryTheory.Functor.map (homologyFunctor C c n) f)
hg :
  ∀ (n : ι), IsIso (X := Functor.obj (homologyFunctor C c n) Y) (CategoryTheory.Functor.map (homologyFunctor C c n) g)
⊢ ∀ (n : ι),
    IsIso (X := Functor.obj (homologyFunctor C c n) X) (CategoryTheory.Functor.map (homologyFunctor C c n) (f ≫ g))
have simp : ∀ (n : ι),
  IsIso (X := Functor.obj (homologyFunctor C c n) X)
    (CategoryTheory.Functor.map (homologyFunctor C c n) f ≫ CategoryTheory.Functor.map (homologyFunctor C c n) g)
Tactic: simp only [Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
⊢ Eq (α := MorphismProperty (HomotopyCategory.{v_1, u_1, u_2} C c)) (quasiIso C c)
    (MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c))
have h : ∀ (K L : HomologicalComplex.{v_1, u_1, u_2} C c)
  (f :
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, u_2} C c) (CategoryTheory.Quotient.mk (r := homotopic C c) K)
      (CategoryTheory.Quotient.mk (r := homotopic C c) L)),
  quasiIso C c f ↔ MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) f
Tactic: ext ⟨K⟩ ⟨L⟩ f