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
⊢ ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'

Tactic:
obtain ⟨g, hg, _⟩ := Pretriangulated.complete_distinguished_triangle_morphism _ _ hT hT'
      c (𝟙 _) (by cat_disch)

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₃
⊢ ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
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
a b : ℤ
h : a ≤ b
X : C
⊢ (t.natTransTruncLTOfLE a b h).app X ≫ (t.truncLTι b).app X = (t.truncLTι a).app X

Tactic:
simpa using! ((TruncAux.triangleFunctorNatTransOfLE t a b h).app X).comm₁.symm

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

Goal state before:
pp: case mp
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 : ℤ
X : C
h : t.IsGE X n
⊢ IsIso ((t.truncGEπ n).app X)

Tactic:
obtain ⟨e, he⟩ := t.triangle_iso_exists
      (inv_rot_of_distTriang _ (contractible_distinguished X))
      (t.triangleLTGE_distinguished n X) (Iso.refl X) (n - 1) n
      (t.isLE_of_iso (shiftFunctor C (-1 : ℤ)).mapZeroObject.symm _)
      (by dsimp; infer_instance) (by dsimp; infer_instance) (by dsimp; infer_instance)

Goal state after:
case mp
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 : ℤ
X : C
h : t.IsGE X n
e : (contractibleTriangle X).invRotate ≅ (t.triangleLTGE n).obj X
he : e.hom.hom₂ = (Iso.refl X).hom
⊢ IsIso ((t.truncGEπ n).app X)
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₁ = f₂

Tactic:
suffices ∀ (f : Y ⟶ (t.truncLT n).obj X) (_ : f ≫ (t.truncLTι n).app X = 0), f = 0 by
    rw [← sub_eq_zero, this (f₁ - f₂) (by cat_disch)]

Goal state after:
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), f ≫ (t.truncLTι n).app X = 0 → f = 0
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ι)
α : Cochain Q K 0
p : ℤ
hα : ((Cochain.ofHom π).comp ((δ 0 1 α).comp (Cochain.ofHom ι) ⋯) ⋯).v p (p + 1) ⋯ = (↑(cocycle₁' sq hsq)).v p (p + 1) ⋯
⊢ (δ 0 1 (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯)).v p (p + 1) ⋯ =
    Cochain.v 0 p (p + 1) ⋯

Tactic:
simp only [Cochain.zero_cochain_comp_v, Cochain.ofHom_v, Cochain.comp_zero_cochain_v,
              δ_zero_cochain_v, Preadditive.sub_comp, Category.assoc, Preadditive.comp_sub,
              HomologicalComplex.Hom.comm_assoc, cocycle₁', Cocycle.mk_coe, Cochain.ofHoms_v,
              HomologicalComplex.eval_obj, HomologicalComplex.eval_map] at hα

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ι)
α : Cochain Q K 0
p : ℤ
hα :
  π.f p ≫ α.v p p ⋯ ≫ K.d p (p + 1) ≫ ι.f (p + 1) - B.d p (p + 1) ≫ π.f (p + 1) ≫ α.v (p + 1) (p + 1) ⋯ ≫ ι.f (p + 1) =
    (hsq p).l ≫ X.d p (p + 1) - B.d p (p + 1) ≫ (hsq (p + 1)).l
⊢ (δ 0 1 (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯)).v p (p + 1) ⋯ =
    Cochain.v 0 p (p + 1) ⋯
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f : { obj := K, property := ⋯ }.obj ⟶ { obj := L, property := ⋯ }.obj
d : ℤ
left✝ : K.IsStrictlyGE (d + 1)
right✝ : L.IsStrictlyGE d
⊢ Nonempty ((trivialCofibrations (Plus C)).MapFactorizationData (fibrations (Plus C)) { hom := f })

Tactic:
obtain ⟨K', _, i, p, _, _, hp, fac⟩ := cm5a f d

Goal state after:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f : { obj := K, property := ⋯ }.obj ⟶ { obj := L, property := ⋯ }.obj
d : ℤ
left✝² : K.IsStrictlyGE (d + 1)
right✝ : L.IsStrictlyGE d
K' : CochainComplex C ℤ
w✝ : K'.IsStrictlyGE d
i : { obj := K, property := ⋯ }.obj ⟶ K'
p : K' ⟶ { obj := L, property := ⋯ }.obj
left✝¹ : Mono i
left✝ : QuasiIso i
hp : degreewiseEpiWithInjectiveKernel p
fac : i ≫ p = f
⊢ Nonempty ((trivialCofibrations (Plus C)).MapFactorizationData (fibrations (Plus C)) { hom := f })
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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
i : ℤ
hi : i < n
⊢ ExactAt (cokernel f) i

Tactic:
rw [exactAt_iff_isZero_homology]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
i : ℤ
hi : i < n
⊢ IsZero (homology (cokernel f) i)
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this✝ : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ := (CatCommSq.vInvEquiv H₂ eL eR H₃) inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ L₁.isoWhiskerLeft eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ R₁.isoWhiskerLeft eR.unitIso.symm ≪≫ R₁.rightUnitor
X₁ : C₁
⊢ w.natTrans.app X₁ =
    w.natTrans.app X₁ ≫
      eR.unit.app (H₂.obj (L₁.obj X₁)) ≫
        eR.inverse.map
            ((natTrans w'.hom).app (L₁.obj X₁) ≫
              H₃.map (eL.functor.map (eL.unit.app (L₁.obj X₁))) ≫
                w'.inv.app (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
          eR.unitIso.inv.app (H₂.obj (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
            H₂.map (eL.unitIso.inv.app (L₁.obj X₁))

Tactic:
← Functor.comp_map,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this✝ : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ := (CatCommSq.vInvEquiv H₂ eL eR H₃) inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ L₁.isoWhiskerLeft eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ R₁.isoWhiskerLeft eR.unitIso.symm ≪≫ R₁.rightUnitor
X₁ : C₁
⊢ w.natTrans.app X₁ =
    w.natTrans.app X₁ ≫
      eR.unit.app (H₂.obj (L₁.obj X₁)) ≫
        eR.inverse.map
            ((natTrans w'.hom).app (L₁.obj X₁) ≫
              (eL.functor ⋙ H₃).map (eL.unit.app (L₁.obj X₁)) ≫
                w'.inv.app (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
          eR.unitIso.inv.app (H₂.obj (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
            H₂.map (eL.unitIso.inv.app (L₁.obj X₁))
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
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
q : ℕ
⊢ ι f n₀ ≫ midπ f n₀ q = ((functor f n₀).obj (op q)).obj.ι

Tactic:
by
  simp [ι, midπ]

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

Goal state before:
pp: 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
T' : C₁ ⥤ D₁
B' : C₂ ⥤ D₂
α : T ≅ T'
β : B ≅ B'
⊢ (w.whiskerHorizontal α.inv β.hom).GuitartExact ↔ w.GuitartExact

Tactic:
rw [← guitartExact_op_iff, ← w.guitartExact_op_iff,
    ← whiskerVertical_iff w.op (NatIso.op α.symm) (NatIso.op β.symm)]
  rfl

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
inst✝¹ : K.IsKProjective
inst✝ : L.IsKProjective
f : K ⟶ L
x✝ : QuasiIso f
g : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K
hg : Qh.map g = (quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K
⊢ Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f ≫ g) =
    Qh.map (𝟙 ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K))

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
inst✝¹ : K.IsKProjective
inst✝ : L.IsKProjective
f : K ⟶ L
x✝ : QuasiIso f
g : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K
hg : Qh.map g = (quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K
⊢ Qh.map (g ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f) =
    Qh.map (𝟙 ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L))

Tactic:
· simp [hg]

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
inst✝¹ : K.IsKProjective
inst✝ : L.IsKProjective
f : K ⟶ L
x✝ : QuasiIso f
g : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K
hg : Qh.map g = (quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K
⊢ Qh.map (g ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f) =
    Qh.map (𝟙 ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L))
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
K : HomologicalComplex C c
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
k : ι
h : k = i₀ ∨ k = i₁
⊢ φ.f k = φ'.f k

pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
K : HomologicalComplex C c
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
k : ι
h : ¬(k = i₀ ∨ k = i₁)
⊢ φ.f k = φ'.f k

Tactic:
· obtain rfl | rfl := h <;> assumption

Goal state after:
case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
K : HomologicalComplex C c
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
k : ι
h : ¬(k = i₀ ∨ k = i₁)
⊢ φ.f k = φ'.f k
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
K : HomologicalComplex C c
φ φ' : K ⟶ double f hi₀₁
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
k : ι
h : k = i₀ ∨ k = i₁
⊢ φ.f k = φ'.f k

pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
K : HomologicalComplex C c
φ φ' : K ⟶ double f hi₀₁
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
k : ι
h : ¬(k = i₀ ∨ k = i₁)
⊢ φ.f k = φ'.f k

Tactic:
· obtain rfl | rfl := h <;> assumption

Goal state after:
case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
K : HomologicalComplex C c
φ φ' : K ⟶ double f hi₀₁
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
k : ι
h : ¬(k = i₀ ∨ k = i₁)
⊢ φ.f k = φ'.f k
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ (ofComplex Z).d 1 0 = d (Projective.π Z)

Tactic:
by
  simp [ofComplex]

Goal state after:
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₂
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.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
y₂ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂)
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.pOpcycles f₁₂ f₃ n₁
⊢ y₂ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g = 0

Tactic:
simpa only [Category.assoc, p_opcyclesToE, hx₂, comp_zero]
        using! hy₂.symm =≫ X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Semiprimary

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝¹ : RingHomSurjective τ₁₂
inst✝ : IsSemisimpleModule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Submodule.comap f ⊥ ≤ f.ker

Tactic:
LinearMap.ker,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝¹ : RingHomSurjective τ₁₂
inst✝ : IsSemisimpleModule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Submodule.comap f ⊥ ≤ Submodule.comap f ⊥
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
g : L₂ → L₁
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
⊢ ∀ {x y : L₂}, ((↑f).inverse g h₁ h₂).toFun ⁅x, y⁆ = ⁅((↑f).inverse g h₁ h₂).toFun x, ((↑f).inverse g h₁ h₂).toFun y⁆

Tactic:
by
      intro x y
      calc
        g ⁅x, y⁆ = g ⁅f (g x), f (g y)⁆ := by conv_lhs => rw [← h₂ x, ← h₂ y]
        _ = g (f ⁅g x, g y⁆) := by rw [map_lie]
        _ = ⁅g x, g y⁆ := h₁ _

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

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₂
⊢ Injective toLinearEquiv

Tactic:
rintro ⟨⟨⟨⟨f, -⟩, -⟩, -⟩, f_inv⟩ ⟨⟨⟨⟨g, -⟩, -⟩, -⟩, g_inv⟩

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_inv : L₂ → L₁
f : L₁ → L₂
map_add'✝¹ : ∀ (x y : L₁), f (x + y) = f x + f y
map_smul'✝¹ :
  ∀ (m : R) (x : L₁),
    { toFun := f, map_add' := map_add'✝¹ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := f, map_add' := map_add'✝¹ }.toFun x
map_lie'✝¹ :
  ∀ {x y : L₁},
    { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun ⁅x, y⁆ =
      ⁅{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun x,
        { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun y⁆
left_inv✝¹ :
  LeftInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun
right_inv✝¹ :
  RightInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun
g_inv : L₂ → L₁
g : L₁ → L₂
map_add'✝ : ∀ (x y : L₁), g (x + y) = g x + g y
map_smul'✝ :
  ∀ (m : R) (x : L₁),
    { toFun := g, map_add' := map_add'✝ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := g, map_add' := map_add'✝ }.toFun x
map_lie'✝ :
  ∀ {x y : L₁},
    { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun ⁅x, y⁆ =
      ⁅{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun x,
        { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun y⁆
left_inv✝ :
  LeftInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun
right_inv✝ :
  RightInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun
⊢ { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹, invFun := f_inv,
          left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toLinearEquiv =
      { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝, invFun := g_inv,
          left_inv := left_inv✝, right_inv := right_inv✝ }.toLinearEquiv →
    { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹, invFun := f_inv,
        left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
      { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝, invFun := g_inv,
        left_inv := left_inv✝, right_inv := right_inv✝ }
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : LieRingModule L M
inst✝ : LieRingModule L N
⊢ Injective toEquiv

Tactic:
rintro ⟨⟨⟨⟨f, -⟩, -⟩, -⟩, f_inv⟩ ⟨⟨⟨⟨g, -⟩, -⟩, -⟩, g_inv⟩

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : LieRingModule L M
inst✝ : LieRingModule L N
f_inv : N → M
f : M → N
map_add'✝¹ : ∀ (x y : M), f (x + y) = f x + f y
map_smul'✝¹ :
  ∀ (m : R) (x : M),
    { toFun := f, map_add' := map_add'✝¹ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := f, map_add' := map_add'✝¹ }.toFun x
map_lie'✝¹ :
  ∀ {x : L} {m : M},
    { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun ⁅x, m⁆ =
      ⁅x, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun m⁆
left_inv✝¹ :
  LeftInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun
right_inv✝¹ :
  RightInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun
g_inv : N → M
g : M → N
map_add'✝ : ∀ (x y : M), g (x + y) = g x + g y
map_smul'✝ :
  ∀ (m : R) (x : M),
    { toFun := g, map_add' := map_add'✝ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := g, map_add' := map_add'✝ }.toFun x
map_lie'✝ :
  ∀ {x : L} {m : M},
    { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun ⁅x, m⁆ =
      ⁅x, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun m⁆
left_inv✝ :
  LeftInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun
right_inv✝ :
  RightInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun
⊢ { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹, invFun := f_inv,
          left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toEquiv =
      { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝, invFun := g_inv,
          left_inv := left_inv✝, right_inv := right_inv✝ }.toEquiv →
    { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹, invFun := f_inv,
        left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
      { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝, invFun := g_inv,
        left_inv := left_inv✝, right_inv := right_inv✝ }