mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X Y : (HomologicalComplex V c)ᵒᵖ
f : X ⟶ Y
⊢ (𝟭 (HomologicalComplex V c)ᵒᵖ).map f ≫ (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop Y).op.unopSymm.X x)) ⋯).op.hom =
    (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯).op.hom ≫ (opFunctor V c ⋙ opInverse V c).map f

Tactic:
refine Quiver.Hom.unop_inj ?_

Goal state after:
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X Y : (HomologicalComplex V c)ᵒᵖ
f : X ⟶ Y
⊢ ((𝟭 (HomologicalComplex V c)ᵒᵖ).map f ≫
        (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop Y).op.unopSymm.X x)) ⋯).op.hom).unop =
    ((Hom.isoOfComponents (fun x ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯).op.hom ≫
        (opFunctor V c ⋙ opInverse V c).map f).unop
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ inr (map f (f ≫ g) (𝟙 X₁) g ⋯) ≫ (mappingConeCompHomotopyEquiv f g).inv = (mappingConeCompTriangle f g).mor₂

Tactic:
by
  simp [map, mappingConeCompHomotopyEquiv, MappingConeCompHomotopyEquiv.inv]

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

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X Y : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
f : X ⟶ Y
⊢ (𝟭 (HomologicalComplex Vᵒᵖ c)ᵒᵖ).map f ≫
      (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop Y).op.unopSymm.X x)) ⋯).op.hom =
    (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯).op.hom ≫
      (unopFunctor V c ⋙ unopInverse V c).map f

Tactic:
refine Quiver.Hom.unop_inj ?_

Goal state after:
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X Y : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
f : X ⟶ Y
⊢ ((𝟭 (HomologicalComplex Vᵒᵖ c)ᵒᵖ).map f ≫
        (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop Y).op.unopSymm.X x)) ⋯).op.hom).unop =
    ((Hom.isoOfComponents (fun x ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯).op.hom ≫
        (unopFunctor V c ⋙ unopInverse V c).map f).unop
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : ¬c.Rel i j
⊢ ((if hij : c.Rel i j then
        if hi : e.BoundaryGE i then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
        else (XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
      else 0) ≫
      if hij : c.Rel j k then
        if hi : e.BoundaryGE j then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
        else (XIso K e hi).hom ≫ K.d (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
      else 0) =
    0

Tactic:
rw [dif_neg hij, zero_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ ((K.restriction e).iCycles j ≫ (K.restrictionXIso e hj').hom) ≫ K.d j' k' = 0

Tactic:
by
      rw [assoc, ← cancel_mono (K.restrictionXIso e hk').inv, assoc, assoc, ← restriction_d_eq,
        iCycles_d, zero_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
φ : W ⟶ cocone.pt
⊢ (K.extendXIso e hj').hom ≫
      Cofork.π cocone ≫
        (isColimitCokernelCofork K e hj' hi hi' cocone hcocone).desc (CokernelCofork.ofπ ((K.extend e).d j' k') ⋯) =
    (K.extend e).d j' k'

Tactic:
by
    simpa using! (isColimitCokernelCofork K e hj' hi hi' cocone hcocone).fac _
      WalkingParallelPair.one

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j

Tactic:
by_cases hi : e.BoundaryGE i
    · rw [f_eq_iso_hom_pOpcycles_iso_inv K e rfl hi,
        f_eq_iso_hom_iso_inv K e rfl (e.not_boundaryGE_next hij),
        K.truncGE'_d_eq_fromOpcycles e hij rfl rfl hi]
      simp [restrictionXIso]
    · rw [f_eq_iso_hom_iso_inv K e rfl hi,
        f_eq_iso_hom_iso_inv K e rfl (e.not_boundaryGE_next hij),
        K.truncGE'_d_eq e hij rfl rfl hi]
      simp [restrictionXIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ K.πTruncGE e ≫ truncGEMap φ e = φ ≫ L.πTruncGE e

Tactic:
apply (e.homEquiv _ _).injective
  ext1
  dsimp [truncGEMap, πTruncGE]
  rw [e.homRestrict_comp_extendMap, e.homRestrict_liftExtend, e.homRestrict_precomp,
    e.homRestrict_liftExtend, restrictionToTruncGE'_naturality]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncLE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁷ : Category.{v_1, u_3} C
inst✝⁶ : HasZeroMorphisms C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁵ : e.IsTruncLE
inst✝⁴ : ∀ (i' : ι'), K.HasHomology i'
inst✝³ : ∀ (i' : ι'), L.HasHomology i'
inst✝² : ∀ (i' : ι'), M.HasHomology i'
inst✝¹ : HasZeroObject C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
⊢ (K.truncLE e).IsStrictlySupported e'

Tactic:
rw [← isStrictlySupported_op_iff]
  exact inferInstanceAs ((K.op.truncGE e.op).IsStrictlySupported e'.op)

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: case right.inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ : ι₂
⊢ ∃ a, fromSum e₁ e₂ a = e₂.f i₂

Tactic:
· exact ⟨Sum.inr i₂, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ : ι₁
h : e₁.BoundaryLE i₁
⊢ ∃ i₂, ac.Boundary i₁ i₂

Tactic:
by
  obtain ⟨h₁, h₂⟩ := h
  obtain ⟨i₂, hi₂⟩ := ac.exists_i₂ (c.next (e₁.f i₁))
    (fun i₁' hi₁' => h₂ i₁' (by simpa only [← hi₁'] using! h₁))
  exact ⟨i₂, by simpa only [hi₂] using! h₁⟩

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ : ι₂
h₁ : c.Rel (c.prev (e₂.f i₂)) (e₂.f i₂)
h₂ : ∀ (i : ι₂), ¬c.Rel (e₂.f i) (e₂.f i₂)
⊢ ∃ i₁, ac.Boundary i₁ i₂

Tactic:
obtain ⟨i₁, hi₁⟩ := ac.exists_i₁ (c.prev (e₂.f i₂))
    (fun i₂' hi₂' => h₂ i₂' (by simpa only [← hi₂'] using! h₁))

Goal state after:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ : ι₂
h₁ : c.Rel (c.prev (e₂.f i₂)) (e₂.f i₂)
h₂ : ∀ (i : ι₂), ¬c.Rel (e₂.f i) (e₂.f i₂)
i₁ : ι₁
hi₁ : c.prev (e₂.f i₂) = e₁.f i₁
⊢ ∃ i₁, ac.Boundary i₁ i₂
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : CochainComplex C ℤ
f : Q.obj X ⟶ Q.obj Y
φ : (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)).LeftFraction { as := X } { as := Y }
hφ : f = φ.map Qh ⋯
⊢ ∃ Y' g s, ∃ (x : IsIso (Q.map s)), f = Q.map g ≫ inv (Q.map s)

Tactic:
obtain ⟨X', g, s, hs, rfl⟩ := φ.cases

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : CochainComplex C ℤ
f : Q.obj X ⟶ Q.obj Y
X' : HomotopyCategory C (ComplexShape.up ℤ)
g : { as := X } ⟶ X'
s : { as := Y } ⟶ X'
hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) s
hφ : f = { Y' := X', f := g, s := s, hs := hs }.map Qh ⋯
⊢ ∃ Y' g s, ∃ (x : IsIso (Q.map s)), f = Q.map g ≫ inv (Q.map s)
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝³ : HasZeroObject C
inst✝² : ∀ (i : ℤ), HasHomology K i
inst✝¹ : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst✝ : K.IsGE n
⊢ QuasiIso (K.πTruncGE n)

Tactic:
rw [quasiIso_πTruncGE_iff]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
h : Small.{w, v₂} (L.obj X ⟶ L.obj Y)
⊢ HasSmallLocalizedHom W X Y

Tactic:
exact ⟨small_map (homEquiv W W.Q L)⟩

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n : ℤ
⊢ (embeddingUpIntGE n).BoundaryGE 0

Tactic:
rw [boundaryGE_embeddingUpIntGE_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝² : L.IsLocalization W
X Y : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W X Y
e : SmallHom W X Y
⊢ (equiv W L) (chgUniv e) = (equiv W L) e

Tactic:
obtain ⟨f, rfl⟩ := (equiv W W.Q).symm.surjective e
  dsimp [chgUniv]
  simp only [Equiv.apply_symm_apply,
    equiv_equiv_symm W _ _ _ (Localization.compUniqFunctor W.Q L W)]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mpr.inr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
x y :
  (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
    (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))
⊢ x ≫ (Functor.commShiftIso Q b).inv.app ((CochainComplex.singleFunctor C 0).obj Y) =
    y ≫ (Functor.commShiftIso Q b).inv.app ((CochainComplex.singleFunctor C 0).obj Y)

Tactic:
← cancel_epi ((Q.commShiftIso a).hom.app _)

Goal state after:
case mpr.inr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
x y :
  (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
    (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))
⊢ (Functor.commShiftIso Q a).hom.app ((CochainComplex.singleFunctor C 0).obj X) ≫
      x ≫ (Functor.commShiftIso Q b).inv.app ((CochainComplex.singleFunctor C 0).obj Y) =
    (Functor.commShiftIso Q a).hom.app ((CochainComplex.singleFunctor C 0).obj X) ≫
      y ≫ (Functor.commShiftIso Q b).inv.app ((CochainComplex.singleFunctor C 0).obj Y)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
x y :
  (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
    (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))
this✝ : ((shiftFunctor (CochainComplex C ℤ) a).obj ((CochainComplex.singleFunctor C 0).obj X)).IsStrictlyLE (-a)
this : ((shiftFunctor (CochainComplex C ℤ) b).obj ((CochainComplex.singleFunctor C 0).obj Y)).IsStrictlyGE (-b)
⊢ -a < -b

Tactic:
by
        lia

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

Goal state before:
pp: case pos.hg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (HomologicalComplex.homologyMap S.f j)
⊢ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ }.g =
    0

Tactic:
· simp [← cancel_mono (HomologicalComplex.homologyMap S.f j)]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
α : ↑((extFunctorObj (Opposite.unop X₁) n).obj Y₁)
⊢ 0 + n + 0 = n

Tactic:
all_goals lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    ((singleFunctorsPostcompQIso C).hom.hom 0).app S.X₃ ≫
      inv
          (Q.map
            (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
        Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
          (Functor.commShiftIso Q 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁) ≫
            (shiftFunctor (DerivedCategory C) 1).map (((singleFunctorsPostcompQIso C).inv.hom 0).app S.X₁)

Tactic:
singleFunctorsPostcompQIso_hom_hom,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    (𝟙 ((singleFunctors C).functor 0)).app S.X₃ ≫
      inv
          (Q.map
            (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
        Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
          (Functor.commShiftIso Q 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁) ≫
            (shiftFunctor (DerivedCategory C) 1).map (((singleFunctorsPostcompQIso C).inv.hom 0).app S.X₁)
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
X : C
⊢ CatCenter.app { app := fun X ↦ (a * b) • 𝟙 X, naturality := ⋯ } X = a • b • 𝟙 X ≫ 𝟙 X

Tactic:
smul_smul

Goal state after:
R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
X : C
⊢ CatCenter.app { app := fun X ↦ (a * b) • 𝟙 X, naturality := ⋯ } X = (a * b) • 𝟙 X ≫ 𝟙 X
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughProjectives C
⊢ HasExt C

Tactic:
by
  let := HasDerivedCategory.standard C
  have := hasExt_of_hasDerivedCategory C
  rw [hasExt_iff_small_ext.{w}]
  intro X Y n
  induction n generalizing X Y with
  | zero =>
    rw [small_congr Ext.homEquiv₀]
    infer_instance
  | succ n hn =>
    let S := ShortComplex.mk _ _ (kernel.condition (Projective.π X))
    have hS : S.ShortExact :=
      { exact := ShortComplex.exact_of_f_is_kernel _ (kernelIsKernel S.g) }
    have : Function.Surjective (Ext.precomp hS.extClass Y (add_comm 1 n)) := fun x₃ ↦
      Ext.contravariant_sequence_exact₃ hS Y x₃
        (Ext.eq_zero_of_projective _) (by lia)
    exact small_of_surjective.{w} this

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

Goal state before:
pp: case mp
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : Function.Injective ⇑solution.fromQuotient
⊢ (solution.fromQuotient ∘ₗ relations.toQuotient).ker = relations.toQuotient.ker

Tactic:
LinearMap.ker_comp,

Goal state after:
case mp
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : Function.Injective ⇑solution.fromQuotient
⊢ Submodule.comap relations.toQuotient solution.fromQuotient.ker = relations.toQuotient.ker
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : CommMonoid R
inst✝¹ : CommMonoid S
inst✝ : FunLike F R S
σ : R ≃* S
n : ℕ
ξ : ↥(rootsOfUnity n S)
⊢ ↑↑((_root_.restrictRootsOfUnity σ n) ((_root_.restrictRootsOfUnity σ.symm n) ξ)) = ↑↑ξ

Tactic:
exact σ.apply_symm_apply _

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
inst✝ : CommMonoid R
⊢ val '' ↑(rootsOfUnity 1 R) = {1}

Tactic:
by
  simp

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
inst✝ : CommRing R
k : ℕ
ζ : Rˣ
⊢ ζ ∈ rootsOfUnity k R ↔ (X ^ k - 1).IsRoot ↑ζ

Tactic:
by
  simp [-mem_rootsOfUnity, mem_rootsOfUnity', sub_eq_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)

Tactic:
by
  obtain ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm K Q)
  have hv₂ := hv₁.not_isOrtho_basis_self_of_separatingLeft hQ
  simp_rw [associated_eq_self_apply] at hv₂
  exact ⟨fun i => Units.mk0 _ (hv₂ i), ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
hn : IsEmpty n
⊢ ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)

Tactic:
rw [center_eq_bot_of_subsingleton, Fintype.card_eq_zero, max_eq_right_of_lt zero_lt_one,
      rootsOfUnity_one]
    exact MulEquiv.ofUnique

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
M : Matrix n' n R
N : Matrix m m' R
⊢ M * (toMatrix₂' R) B * N = (toMatrix₂' R) (B.compl₁₂ (toLin' Mᵀ) (toLin' N))

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ ((mulHom A) ((of A i) a)) ((of A j) b) = (of A (i + j)) (GradedMonoid.GMul.mul a b)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
a b : R
⊢ ((of A 0).comp GAlgebra.toFun) (a * b) = ((of A 0).comp GAlgebra.toFun) a * ((of A 0).comp GAlgebra.toFun) b

Tactic:
by
      simp only [AddMonoidHom.comp_apply]
      rw [of_mul_of]
      apply DFinsupp.single_eq_of_sigma_eq (GAlgebra.map_mul a b)

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
⊢ Q 0 = 0

Tactic:
← @zero_smul R _ _ _ _ (0 : M),

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
⊢ Q (0 • 0) = 0
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
this : mulHom A = (mulHom A).flip
⊢ ((mulHom A) b) a = b * a

Tactic:
mulHom_apply

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
this : mulHom A = (mulHom A).flip
⊢ b * a = b * a
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike σ M
inst✝ : AddSubmonoidClass σ M
ℳ : ι → σ
x y : Decomposition ℳ
⊢ x = y

Tactic:
by
    obtain ⟨_, _, xr⟩ := x
    obtain ⟨_, yl, _⟩ := y
    congr
    exact Function.LeftInverse.eq_rightInverse xr yl

Goal state after: