mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
x✝ : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
W : C
a : W ⟶ X
b : Y ⟶ (shiftFunctor C 1).obj W
hT : Triangle.mk a s b ∈ Pretriangulated.distinguishedTriangles
hW : B W
W' : C
c : W ⟶ W'
d : W' ⟶ X
h₁ : A W'
h₂ : B W'
fac : c ≫ d = a
U : C
hU : A U
e : X ⟶ U
f : U ⟶ (shiftFunctor C 1).obj W'
hT' : Triangle.mk d e f ∈ Pretriangulated.distinguishedTriangles
g : (Triangle.mk a s b).obj₃ ⟶ (Triangle.mk d e f).obj₃
hg : (Triangle.mk a s b).mor₂ ≫ g = 𝟙 (Triangle.mk a s b).obj₂ ≫ (Triangle.mk d e f).mor₂
right✝ : (Triangle.mk a s b).mor₃ ≫ (shiftFunctor C 1).map c = g ≫ (Triangle.mk d e f).mor₃
⊢ (A ⊓ B).trW e

Tactic:
rw [ObjectProperty.trW_iff']

Goal state after:
case refine_1
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
x✝ : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
W : C
a : W ⟶ X
b : Y ⟶ (shiftFunctor C 1).obj W
hT : Triangle.mk a s b ∈ Pretriangulated.distinguishedTriangles
hW : B W
W' : C
c : W ⟶ W'
d : W' ⟶ X
h₁ : A W'
h₂ : B W'
fac : c ≫ d = a
U : C
hU : A U
e : X ⟶ U
f : U ⟶ (shiftFunctor C 1).obj W'
hT' : Triangle.mk d e f ∈ Pretriangulated.distinguishedTriangles
g : (Triangle.mk a s b).obj₃ ⟶ (Triangle.mk d e f).obj₃
hg : (Triangle.mk a s b).mor₂ ≫ g = 𝟙 (Triangle.mk a s b).obj₂ ≫ (Triangle.mk d e f).mor₂
right✝ : (Triangle.mk a s b).mor₃ ≫ (shiftFunctor C 1).map c = g ≫ (Triangle.mk d e f).mor₃
⊢ ∃ X_1 f h, ∃ (_ : Triangle.mk f e h ∈ Pretriangulated.distinguishedTriangles), (A ⊓ B) X_1
Module: Mathlib.Algebra.Homology.Factorizations.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
hL : IsZero L
n : ℤ
⊢ epiWithInjectiveKernel (f.f n) ↔ Injective (K.X n)

Tactic:
by
    rw [epiWithInjectiveKernel_iff_of_isZero]
    exact (HomologicalComplex.eval _ _ n).map_isZero hL

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLT n).obj X
h : f₁ ≫ (t.truncLTι n).app X = f₂ ≫ (t.truncLTι n).app X
inst✝ : t.IsLE Y (n - 1)
f : Y ⟶ (t.truncLT n).obj X
hf : f ≫ (t.truncLTι n).app X = 0
g : Y ⟶ ((t.triangleLTGE n).obj X).invRotate.obj₁
hg : f = g ≫ ((t.triangleLTGE n).obj X).invRotate.mor₁
⊢ t.IsGE ((t.triangleLTGE n).obj X).invRotate.obj₁ (n + 1)

Tactic:
by dsimp; apply (t.isGE_shift _ n (-1) (n + 1) (by lia))

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Lifting

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this✝¹ : Epi π
this✝ : Mono ι
n : ℤ
this :
  (↑(cocycle₁' sq hsq)).v n (n + 1) ⋯ ≫ X.d (n + 1) (n + 2) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq)).v (n + 1) (n + 2) ⋯ =
    0
⊢ π.f n ≫ (cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2) +
      π.f n ≫ Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯ ≫ ι.f (n + 2) =
    π.f n ≫ 0 ≫ ι.f (n + 2)

Tactic:
HomologicalComplex.Hom.comm_assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this✝¹ : Epi π
this✝ : Mono ι
n : ℤ
this :
  (↑(cocycle₁' sq hsq)).v n (n + 1) ⋯ ≫ X.d (n + 1) (n + 2) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq)).v (n + 1) (n + 2) ⋯ =
    0
⊢ π.f n ≫ (cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2) +
      B.d n (n + 1) ≫ π.f (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯ ≫ ι.f (n + 2) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : Mono f
T : ShortComplex C :=
  { X₁ := homology K n, X₂ := homology L n, X₃ := homology (cokernel f) n, f := homologyMap f n,
    g := homologyMap (cokernel.π f) n, zero := ⋯ }
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ Mono φ.τ₃ ∧ IsIso φ.τ₂ ∧ Epi φ.τ₁

Tactic:
by
    dsimp [φ]
    rw [homologyMap_comp]
    exact ⟨inferInstance, inferInstance, inferInstance⟩

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: case mp
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_4, u_4} D₁
inst✝ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
α : L ≅ L'
β : R ≅ R'
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact → w.GuitartExact

pp: case mpr
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_4, u_4} D₁
inst✝ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
α : L ≅ L'
β : R ≅ R'
⊢ w.GuitartExact → (w.whiskerVertical α.hom β.inv).GuitartExact

Tactic:
· intro h
    have : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom := by
      ext X₁
      simp only [Functor.comp_obj, whiskerVertical_app, assoc, Iso.hom_inv_id_app_assoc,
        ← B.map_comp, Iso.hom_inv_id_app, B.map_id, comp_id]
    rw [this]
    exact whiskerVertical (w.whiskerVertical α.hom β.inv) α.symm β.symm

Goal state after:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_4, u_4} D₁
inst✝ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
α : L ≅ L'
β : R ≅ R'
⊢ w.GuitartExact → (w.whiskerVertical α.hom β.inv).GuitartExact
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case inr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝² : EnoughInjectives C
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
hq : n ≤ n
this✝ : Mono (homologyMap (π f n) n)
this : Mono (homologyMap (mappingCocone.triangle (α f n)).mor₁ n)
h₁ : IsLimit (KernelFork.ofι (homologyShortComplex f n).f ⋯)
h₂ :
  IsLimit
    (KernelFork.ofι
      { X₁ := homology (mappingCocone.triangle (α f n)).obj₁ n, X₂ := homology (mappingCocone.triangle (α f n)).obj₂ n,
          X₃ := homology (mappingCocone.triangle (α f n)).obj₃ n,
          f := homologyMap (mappingCocone.triangle (α f n)).mor₁ n,
          g := homologyMap (mappingCocone.triangle (α f n)).mor₂ n, zero := ⋯ }.f
      ⋯)
⊢ QuasiIsoAt (ι f n) n

Tactic:
have : homologyMap (ι f n) n = (IsLimit.conePointUniqueUpToIso h₁ h₂).hom := by
      simp [← cancel_mono (homologyMap (π f n) n),
        dsimp% IsLimit.conePointUniqueUpToIso_hom_comp h₁ h₂ .zero,
        ← homologyMap_comp, mappingCocone.lift_fst]

Goal state after:
case inr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝² : EnoughInjectives C
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
hq : n ≤ n
this✝¹ : Mono (homologyMap (π f n) n)
this✝ : Mono (homologyMap (mappingCocone.triangle (α f n)).mor₁ n)
h₁ : IsLimit (KernelFork.ofι (homologyShortComplex f n).f ⋯)
h₂ :
  IsLimit
    (KernelFork.ofι
      { X₁ := homology (mappingCocone.triangle (α f n)).obj₁ n, X₂ := homology (mappingCocone.triangle (α f n)).obj₂ n,
          X₃ := homology (mappingCocone.triangle (α f n)).obj₃ n,
          f := homologyMap (mappingCocone.triangle (α f n)).mor₁ n,
          g := homologyMap (mappingCocone.triangle (α f n)).mor₂ n, zero := ⋯ }.f
      ⋯)
this : homologyMap (ι f n) n = (h₁.conePointUniqueUpToIso h₂).hom
⊢ QuasiIsoAt (ι f n) n
Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived

Goal state before:
pp: C : Type u_3
D : Type u_1
H : Type u_2
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : Category.{v_3, u_1} D
inst✝² : Category.{v_5, u_2} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
G : D ⥤ H
β : F ⟶ L ⋙ G
⊢ G.IsLeftKanExtension β ↔ IsIso (RF.rightDerivedDesc α W G β)

Tactic:
have := IsRightDerivedFunctor.isLeftKanExtension _ α W

Goal state after:
C : Type u_3
D : Type u_1
H : Type u_2
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : Category.{v_3, u_1} D
inst✝² : Category.{v_5, u_2} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
G : D ⥤ H
β : F ⟶ L ⋙ G
this : RF.IsLeftKanExtension α
⊢ G.IsLeftKanExtension β ↔ IsIso (RF.rightDerivedDesc α W G β)
Module: Mathlib.CategoryTheory.Localization.StructuredArrow

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g ↦ P ((structuredArrowEquiv W W.Q L) g)
Y₁ Y₂ : C
f : Y₁ ⟶ Y₂
φ : W.Q.obj X ⟶ W.Q.obj Y₁
hφ : P' (StructuredArrow.mk φ)
⊢ (structuredArrowEquiv W W.Q L) (StructuredArrow.mk (φ ≫ W.Q.map f)) =
    StructuredArrow.mk ((homEquiv W W.Q L) φ ≫ L.map f)

Tactic:
simp [homEquiv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.KanExtension

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
inst✝² : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝¹ : w.GuitartExact
inst✝ : B.EssSurj
F : C₂ ⥤ D
h : ∀ (Y : C₃), R.HasPointwiseLeftKanExtensionAt F (B.obj Y)
X₄ : C₄
⊢ R.HasPointwiseLeftKanExtensionAt F X₄

Tactic:
rw [← Functor.hasPointwiseLeftKanExtensionAt_iff_of_iso _ _ (B.objObjPreimageIso X₄)]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
inst✝² : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝¹ : w.GuitartExact
inst✝ : B.EssSurj
F : C₂ ⥤ D
h : ∀ (Y : C₃), R.HasPointwiseLeftKanExtensionAt F (B.obj Y)
X₄ : C₄
⊢ R.HasPointwiseLeftKanExtensionAt F (B.obj (B.objPreimage X₄))
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ F'
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cocone (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app (CostructuredArrow.mk φ) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk φ)
⊢ ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app
        (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ))

Tactic:
· have : IsIso (F.map w) := by
        have := Localization.inverts L W w hw
        rw [← NatIso.naturality_2 e w]
        dsimp
        infer_instance
      have eq := s.ι.naturality
        (CostructuredArrow.homMk w : CostructuredArrow.mk φ ⟶ CostructuredArrow.mk
          ((Localization.isoOfHom L W w hw).inv ≫ φ))
      dsimp at eq hφ ⊢
      rw [comp_id] at eq
      rw [assoc] at hφ
      rw [map_comp, assoc, assoc, ← cancel_epi (F.map w), eq, ← hφ,
        NatTrans.naturality_assoc, comp_map, ← G.map_comp_assoc]
      simp

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor

Goal state before:
pp: C₁ : Type u₁
inst✝¹² : Category.{v₁, u₁} C₁
inst✝¹¹ : Abelian C₁
inst✝¹⁰ : HasDerivedCategory C₁
C₂ : Type u₂
inst✝⁹ : Category.{v₂, u₂} C₂
inst✝⁸ : Abelian C₂
inst✝⁷ : HasDerivedCategory C₂
F : C₁ ⥤ C₂
inst✝⁶ : F.Additive
inst✝⁵ : PreservesFiniteLimits F
inst✝⁴ : PreservesFiniteColimits F
R : Type u_1
inst✝³ : Ring R
inst✝² : CategoryTheory.Linear R C₁
inst✝¹ : CategoryTheory.Linear R C₂
inst✝ : Linear R F
⊢ Linear R F.mapDerivedCategory

Tactic:
rw [← Localization.functor_linear_iff DerivedCategory.Qh (HomotopyCategory.quasiIso C₁
    (ComplexShape.up ℤ)) R ((F.mapHomotopyCategory (ComplexShape.up ℤ)).comp DerivedCategory.Qh)]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.DifferentialObject

Goal state before:
pp: β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i : β
⊢ ((if h : i + b = i + b then X.d i ≫ X.objEqToHom ⋯ else 0) ≫
      if h : i + b + b = i + b + b then X.d (i + b) ≫ X.objEqToHom ⋯ else 0) =
    0

Tactic:
simp [objEqToHom_d_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Generator.HomologicalComplex

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst✝³ : c.HasNoLoop
inst✝² : HasCoproductsOfShape ι C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
hX : IsSeparator X
⊢ IsSeparator (∐ fun i ↦ separatingFamily c (fun x ↦ X) (PUnit.unit, i))

Tactic:
by
  let φ (i : ι) := separatingFamily c (fun (_ : Unit) ↦ X) ⟨⟨⟩, i⟩
  refine isSeparator_of_isColimit_cofan
    (isSeparating_separatingFamily c (X := fun (_ : Unit) ↦ X) (by simpa using! hX))
      (c := Cofan.mk (∐ φ) (fun ⟨_, i⟩ ↦ Sigma.ι φ i)) ?_
  exact IsColimit.ofWhiskerEquivalence
    (Discrete.equivalence (Equiv.punitProd.{0} ι).symm) (coproductIsCoproduct φ)

Goal state after:
Module: Mathlib.Algebra.Homology.LocalCohomology

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ ∀ (j₁ j₂ : CostructuredArrow (idealPowersToSelfLERadical J) J'), Zigzag j₁ j₂

Tactic:
intro j1 j2

Goal state after:
case h
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
Module: Mathlib.Algebra.Homology.SpectralObject.Differentials

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯) = 0

Tactic:
Ψ_fromOpcycles_assoc ..,

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.iCycles f₂ f₃ n₀ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯) = 0
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: case convert_3
I : Type u
inst✝¹¹ : AddMonoid I
C : Type u_1
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : DecidableEq I
inst✝⁷ : HasInitial C
inst✝⁶ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁵ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
X₁ X₃ : GradedObject I C
inst✝⁴ : X₁.HasTensor X₃
inst✝³ : (tensorObj X₁ tensorUnit).HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj tensorUnit X₃)
inst✝¹ : X₁.HasGoodTensor₁₂Tensor tensorUnit X₃
inst✝ : X₁.HasGoodTensorTensor₂₃ tensorUnit X₃
⊢ HasGoodTrifunctor₁₂Obj (curriedTensor C) (curriedTensor C) (triangleIndexData I).ρ₁₂ X₁ ((single₀ I).obj (𝟙_ C)) X₃

pp: case convert_4
I : Type u
inst✝¹¹ : AddMonoid I
C : Type u_1
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : DecidableEq I
inst✝⁷ : HasInitial C
inst✝⁶ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁵ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
X₁ X₃ : GradedObject I C
inst✝⁴ : X₁.HasTensor X₃
inst✝³ : (tensorObj X₁ tensorUnit).HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj tensorUnit X₃)
inst✝¹ : X₁.HasGoodTensor₁₂Tensor tensorUnit X₃
inst✝ : X₁.HasGoodTensorTensor₂₃ tensorUnit X₃
⊢ HasGoodTrifunctor₂₃Obj (curriedTensor C) (curriedTensor C) (triangleIndexData I).ρ₂₃ X₁ ((single₀ I).obj (𝟙_ C)) X₃

Tactic:
all_goals assumption

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : autoParam (n + 1 = n') spectralSequence_first_page_d_eq._auto_1
⊢ data.i₁ pq = data.i₀ r₀ pq ⋯

Tactic:
data.hi₀₁ pq

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq pq' : κ
hpq : (c r₀).Rel pq pq'
i j k : ι
hi : i = data.i₁ pq'
hj : j = data.i₁ pq
hk : k = data.i₂ pq
n n' : ℤ
hn : n = data.deg pq
hn' : autoParam (n + 1 = n') spectralSequence_first_page_d_eq._auto_1
⊢ data.i₁ pq = data.i₁ pq
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩)
hn : n = (coreE₂CohomologicalFin l).deg (p, ⟨q, hq⟩) - 1
this : ↑q + r ≤ ↑l
⊢ False

Tactic:
obtain ⟨t, ht⟩ := Int.le.dest this

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩)
hn : n = (coreE₂CohomologicalFin l).deg (p, ⟨q, hq⟩) - 1
this : ↑q + r ≤ ↑l
t : ℕ
ht : ↑q + r + ↑t = ↑l
⊢ False
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx✝ :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
hx : x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
⊢ x = 0

Tactic:
← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) (by cat_disch) n₁),

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx✝ :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
hx : x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
⊢ x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0 ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsArtinianRing R
a b : R
hab : a * b = 1
c : R
hca : (LinearMap.toSpanSingleton R R a) c = 1
⊢ b * a = 1

Tactic:
rwa [← left_inv_eq_right_inv hca hab]

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: case refine_2
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0
x y : L
hxy : (toEnd R L M) x = (toEnd R L M) y
m : M
⊢ ⁅x - y, m⁆ = 0

Tactic:
rw [sub_lie, sub_eq_zero, ← toEnd_apply_apply R, ← toEnd_apply_apply R, hxy]

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
⊢ K = ⊥ ↔ ∀ x ∈ K, x = 0

Tactic:
_root_.eq_bot_iff

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
⊢ K ≤ ⊥ ↔ ∀ x ∈ K, x = 0
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
hx : x ∈ I
⊢ f x ∈ map f I

Tactic:
apply LieSubmodule.subset_lieSpan
  use x
  exact ⟨hx, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ ⇑f '' ↑I ⊆ ↑J ↔ I ≤ comap f J

Tactic:
exact Set.image_subset_iff

Goal state after:
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ LieIdeal.map f I ≤ f.idealRange

Tactic:
f.idealRange_eq_map

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ LieIdeal.map f I ≤ LieIdeal.map f ⊤