awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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
⊢ 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

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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
⊢ Karoubi.Hom.f
      (Arrow.Hom.right
        (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.right
        (𝟙
          (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
            (NatTrans.app (π' Λ) X)))).f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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 := (toKaroubi A ⋙ karoubi.F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X) (NatTrans.app (karoubi.π' Λ) X)

Tactic:
of_retract (P := epimorphisms _) (karoubi.retractArrow Λ X)
    (epimorphisms.infer_property _)

Premises used: CategoryTheory.Abelian.LeftResolution.karoubi.retractArrow, CategoryTheory.MorphismProperty.epimorphisms.infer_property, CategoryTheory.MorphismProperty.of_retract
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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
⊢ Eq (α :=
    (F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj (Functor.obj (toKaroubi A) X) ⟶
      Functor.obj (𝟭 (Karoubi.{v_2, u_1} A)) (Functor.obj (toKaroubi A) X))
    (NatTrans.app (π Λ) (Functor.obj (toKaroubi A) X)) (NatTrans.app (π' Λ) X)

Tactic:
simp [π, whiskeringLeftObjToKaroubiFullyFaithful]

Premises used: CategoryTheory.Idempotents.whiskeringLeftObjToKaroubiFullyFaithful, CategoryTheory.Abelian.LeftResolution.karoubi.π
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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
rw :
  Epi (X := (karoubi.F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj (Functor.obj (toKaroubi A) X))
    (NatTrans.app (karoubi.π' Λ) X)
⊢ Epi (X := (karoubi.F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj (Functor.obj (toKaroubi A) X))
    (NatTrans.app (karoubi.π Λ) (Functor.obj (toKaroubi A) X))

Tactic:
rw [karoubi.π_app_toKaroubi_obj]

Premises used: CategoryTheory.Abelian.LeftResolution.karoubi.π_app_toKaroubi_obj
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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.π' Λ) X)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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 : Karoubi.{v_2, u_1} A
⊢ Epi (X := (karoubi.F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X) (NatTrans.app (karoubi.π Λ) X)

Tactic:
of_retract (P := epimorphisms _) (NatTrans.retractArrowApp (karoubi.π Λ) X.retract)
    (epimorphisms.infer_property _)

Premises used: CategoryTheory.Idempotents.Karoubi.retract, CategoryTheory.NatTrans.retractArrowApp, CategoryTheory.MorphismProperty.epimorphisms.infer_property, CategoryTheory.MorphismProperty.of_retract, CategoryTheory.Abelian.LeftResolution.karoubi.π
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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
dsimp :
  (Equivalence.functor (toKaroubiEquivalence A) ⋙
      karoubi.F Λ ⋙ Equivalence.inverse (toKaroubiEquivalence C)).PreservesZeroMorphisms
⊢ Λ.reduced.F.PreservesZeroMorphisms

Tactic:
dsimp [reduced, transport]

Premises used: CategoryTheory.Abelian.LeftResolution.transport, CategoryTheory.Abelian.LeftResolution.reduced
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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
⊢ (Equivalence.functor (toKaroubiEquivalence A) ⋙
      karoubi.F Λ ⋙ Equivalence.inverse (toKaroubiEquivalence C)).PreservesZeroMorphisms

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.LeftResolution.Transport
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 := 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:
infer_instance
-- Module: Mathlib.Algebra.Homology.LeftResolution.Transport
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
dsimp : Epi (𝟙 (ι'.obj (G.obj (Λ.F.obj x))) ≫ e.hom.app (Λ.F.obj x) ≫ Λ.π.app x)
⊢ Epi (((Λ.F.associator G ι').hom ≫ Λ.F.whiskerLeft e.hom ≫ Λ.π).app x)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.LeftResolution.Transport
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 (𝟙 (ι'.obj (G.obj (Λ.F.obj x))) ≫ e.hom.app (Λ.F.obj x) ≫ Λ.π.app x)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Linear
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
ι : Type u_4
c : ComplexShape ι
X Y : HomologicalComplex.{v_1, u_2, u_4} C c
r : R
f : X ⟶ Y
n : ι
⊢ (r • f).f n = r • f.f n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Linear
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
ι : Type u_4
c : ComplexShape ι
X Y : HomologicalComplex.{v_1, u_2, u_4} C c
r : Rˣ
f : X ⟶ Y
n : ι
⊢ (r • f).f n = r • f.f n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Linear
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
h : ∀ (i : ι), ((x * x_1) • x_2).f i = (x • x_1 • x_2).f i
⊢ (x * x_1) • x_2 = x • x_1 • x_2

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.Linear
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
i : ι
⊢ ((x * x_1) • x_2).f i = (x • x_1 • x_2).f i

Tactic:
apply mul_smul

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Homology.Linear
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
h : ∀ (i : ι), ((x + x_1) • x_2).f i = (x • x_2 + x_1 • x_2).f i
⊢ (x + x_1) • x_2 = x • x_2 + x_1 • x_2

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.Linear
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
i : ι
⊢ ((x + x_1) • x_2).f i = (x • x_2 + x_1 • x_2).f i

Tactic:
apply add_smul

Premises used: add_smul
-- Module: Mathlib.Algebra.Homology.LocalCohomology
Goal:
R : Type (max u v)
inst : CommRing R
D : Type v
inst_1 : SmallCategory D
I : D ⥤ Ideal R
i : ℕ
⊢ HasColimit (diagram I i)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Homology.LocalCohomology
Goal:
R : Type u
inst : CommRing R
J : Ideal R
k : ℕᵒᵖ
change : J ≤ (J ^ unop k).radical
⊢ J ≤ ((idealPowersDiagram J).obj k).radical

Tactic:
change _ ≤ (J ^ unop k).radical

Premises used: HPow.hPow, Opposite.unop, Ideal.radical
-- Module: Mathlib.Algebra.Homology.LocalCohomology
Goal:
R : Type u
inst : CommRing R
J : Ideal R
k : ℕᵒᵖ
zero : J ≤ (HPow.hPow (β := ℕ) J 0).radical
succ : ∀ (n : ℕ), J ≤ (J ^ (n + 1)).radical
⊢ J ≤ (J ^ unop k).radical

Tactic:
rcases unop k with - | n

Premises used: Opposite.unop
-- Module: Mathlib.Algebra.Homology.LocalCohomology
Goal:
R : Type u
inst : CommRing R
J : Ideal R
k : ℕᵒᵖ
⊢ J ≤ (HPow.hPow (β := ℕ) J 0).radical

Tactic:
simp [Ideal.radical_top, pow_zero, Ideal.one_eq_top, le_top]

Premises used: Ideal.one_eq_top, pow_zero, le_top, Ideal.radical_top
-- Module: Mathlib.Algebra.Homology.LocalCohomology
Goal:
R : Type u
inst : CommRing R
J : Ideal R
k : ℕᵒᵖ
n : ℕ
⊢ J ≤ (J ^ (n + 1)).radical

Tactic:
simp only [J.radical_pow n.succ_ne_zero, Ideal.le_radical]

Premises used: Ideal.le_radical, Nat.succ_ne_zero, Ideal.radical_pow
-- Module: Mathlib.Algebra.Homology.LocalCohomology
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')
h : ∀ (j₁ j₂ : CostructuredArrow (idealPowersToSelfLERadical J) J'), Zigzag j₁ j₂
⊢ IsConnected.{0, u} (CostructuredArrow (idealPowersToSelfLERadical J) J')

Tactic:
apply +allowSynthFailures zigzag_isConnected

Premises used: CategoryTheory.zigzag_isConnected
-- Module: Mathlib.Algebra.Homology.LocalCohomology
Goal:
R : Type u
inst_1 : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
inst :
  ∀ (k : ℕ) (hk : J ^ k ≤ J'.obj (P := fun (J' : Ideal R) ↦ J ≤ J'.radical)),
    Nonempty.{u + 1} (CostructuredArrow (idealPowersToSelfLERadical J) J')
⊢ 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 _)

Premises used: Ideal.exists_pow_le_of_le_radical_of_fg, CategoryTheory.ObjectProperty.FullSubcategory.property, isNoetherian_def, Iff.mp
-- Module: Mathlib.Algebra.Homology.LocalCohomology
Goal:
R : Type u
inst : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
k : ℕ
hk : J ^ k ≤ J'.obj (P := fun (J' : Ideal R) ↦ J ≤ J'.radical)
⊢ Nonempty.{u + 1} (CostructuredArrow (idealPowersToSelfLERadical J) J')

Tactic:
⟨CostructuredArrow.mk (⟨⟨⟨hk⟩⟩⟩ : (idealPowersToSelfLERadical J).obj (op k) ⟶ J')⟩

Premises used: Nonempty.intro, PLift.up, CategoryTheory.InducedCategory.Hom.mk, CategoryTheory.CostructuredArrow.mk, ULift.up
-- Module: Mathlib.Algebra.Homology.LocalCohomology
Goal:
R : Type u
inst : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
k : ℕ
hk : J ^ k ≤ J'.obj (P := fun (J' : Ideal R) ↦ J ≤ J'.radical)
⊢ Nonempty.{u + 1} (CostructuredArrow (idealPowersToSelfLERadical J) J')

Tactic:
exact ⟨CostructuredArrow.mk (⟨⟨⟨hk⟩⟩⟩ : (idealPowersToSelfLERadical J).obj (op k) ⟶ J')⟩
-- Module: Mathlib.Algebra.Homology.LocalCohomology
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 : Zag j1 j2
⊢ Zigzag j1 j2

Tactic:
apply Relation.ReflTransGen.single

Premises used: Relation.ReflTransGen.single
-- Module: Mathlib.Algebra.Homology.LocalCohomology
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
h₁ : ∀ (h : unop j2.left ≤ unop j1.left), Zag j1 j2
⊢ Zag j1 j2

Tactic:
rcases le_total (unop j1.left) (unop j2.left) with h | h

Premises used: le_total, CategoryTheory.CostructuredArrow.left, Opposite.unop
-- Module: Mathlib.Algebra.Homology.LocalCohomology
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
h₁ : Nonempty (j2 ⟶ j1)
⊢ Zag j1 j2

Tactic:
right
-- Module: Mathlib.Algebra.Homology.LocalCohomology
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
⊢ Nonempty (j2 ⟶ j1)

Tactic:
⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩

Premises used: Quiver.Hom.op, CategoryTheory.CostructuredArrow.homMk, Nonempty.intro, CategoryTheory.homOfLE, rfl
-- Module: Mathlib.Algebra.Homology.LocalCohomology
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
⊢ Nonempty (j2 ⟶ j1)

Tactic:
exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩
-- Module: Mathlib.Algebra.Homology.LocalCohomology
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
h₁ : Nonempty (j1 ⟶ j2)
⊢ Zag j1 j2

Tactic:
left
-- Module: Mathlib.Algebra.Homology.LocalCohomology
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
⊢ Nonempty (j1 ⟶ j2)

Tactic:
⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩

Premises used: Quiver.Hom.op, CategoryTheory.CostructuredArrow.homMk, Nonempty.intro, CategoryTheory.homOfLE, rfl
-- Module: Mathlib.Algebra.Homology.LocalCohomology
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
⊢ Nonempty (j1 ⟶ j2)

Tactic:
exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩
-- Module: Mathlib.Algebra.Homology.LocalCohomology
Goal:
R : Type u
inst : CommRing R
I J K : Ideal R
⊢ HasColimitsOfSize.{0, 0, u, u + 1} (ModuleCat R)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Homology.LocalCohomology
Goal:
R : Type u
inst : CommRing R
I J K : Ideal R
hJK : J.radical = K.radical
L : Ideal R
hL : J ≤ L.radical
rw : ∀ (hL : J.radical ≤ L.radical), K.radical ≤ L.radical
⊢ K ≤ L.radical

Tactic:
rw [← Ideal.radical_le_radical_iff] at hL ⊢

Premises used: Ideal.radical_le_radical_iff
-- Module: Mathlib.Algebra.Homology.LocalCohomology
Goal:
R : Type u
inst : CommRing R
I J K : Ideal R
hJK : J.radical = K.radical
L : Ideal R
hL : J.radical ≤ L.radical
⊢ K.radical ≤ L.radical

Tactic:
hJK.symm.trans_le hL

Premises used: Eq.trans_le, Eq.symm
-- Module: Mathlib.Algebra.Homology.LocalCohomology
Goal:
R : Type u
inst : CommRing R
I J K : Ideal R
hJK : J.radical = K.radical
L : Ideal R
hL : J.radical ≤ L.radical
⊢ K.radical ≤ L.radical

Tactic:
exact hJK.symm.trans_le hL

Premises used: Eq.trans_le, Eq.symm
-- Module: Mathlib.Algebra.Homology.LocalCohomology
Goal:
R : Type u
inst : CommRing R
I J K : Ideal R
hJK : J.radical = K.radical
⊢ (cast hJK).IsEquivalence

Tactic:
(castEquivalence hJK).isEquivalence_functor

Premises used: localCohomology.SelfLERadical.castEquivalence, CategoryTheory.ObjectProperty.ιOfLE, localCohomology.SelfLERadical.cast, CategoryTheory.Equivalence.isEquivalence_functor
-- Module: Mathlib.Algebra.Homology.Localization
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
⊢ QuasiIso x_2

Tactic:
rw [mem_quasiIso_iff] at hf

Premises used: HomologicalComplex.mem_quasiIso_iff
-- Module: Mathlib.Algebra.Homology.Localization
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
dsimp : IsIso (X := x.homology i) (Y := x_1.homology i) (homologyMap x_2 i)
⊢ IsIso (X := Functor.obj (homologyFunctor C c i) x) (CategoryTheory.Functor.map (homologyFunctor C c i) x_2)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Localization
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 := x.homology i) (Y := x_1.homology i) (homologyMap x_2 i)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Localization
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
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)
⊢ 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
-- Module: Mathlib.Algebra.Homology.Localization
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)
mp : ∀ (i : ι), QuasiIsoAt f i
⊢ HomologicalComplex.quasiIso C c f

Tactic:
rw [HomologicalComplex.mem_quasiIso_iff, quasiIso_iff]

Premises used: HomologicalComplex.mem_quasiIso_iff, quasiIso_iff
-- Module: Mathlib.Algebra.Homology.Localization
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 : ι
mp : IsIso (X := K.homology i) (Y := L.homology i) (HomologicalComplex.homologyMap f i)
⊢ QuasiIsoAt f i

Tactic:
rw [quasiIsoAt_iff_isIso_homologyMap]

Premises used: quasiIsoAt_iff_isIso_homologyMap