mathlib-initiative/mathlib-tactics huggingface dataset:
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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
hi : ¬e.BoundaryGE i
⊢ (truncGE'.XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (truncGE'.XIso K e ⋯).inv =
    (K.truncGE'XIso e ⋯ hi).hom ≫ K.d (e.f i) (e.f j) ≫ (K.truncGE'XIso e ⋯ ⋯).inv

Tactic:
simp [truncGE'XIso]

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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
⊢ (K.restrictionToTruncGE' e).f i =
    (K.restrictionXIso e hi').hom ≫ K.pOpcycles i' ≫ (K.truncGE'XIsoOpcycles e hi' hi).inv

Tactic:
by
  apply restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv

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

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.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
this✝ : Epi φ.τ₁
this : IsIso φ.τ₂
⊢ IsIso ((e.liftExtend (K.restrictionToTruncGE' e) ⋯).f (c'.next j'))

Tactic:
have : c'.next j' = e.f (c.next j) := by simpa only [← hj'] using e.next_f rfl

Goal state after:
ι : 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'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
this✝¹ : Epi φ.τ₁
this✝ : IsIso φ.τ₂
this : c'.next j' = e.f (c.next j)
⊢ IsIso ((e.liftExtend (K.restrictionToTruncGE' e) ⋯).f (c'.next j'))
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

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
i : ι
⊢ QuasiIsoAt (K.πTruncGE e ≫ truncGEMap φ e) (e.f i) ↔ QuasiIsoAt φ (e.f i)

Tactic:
πTruncGE_naturality φ e,

Goal state after:
ι : 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
i : ι
⊢ QuasiIsoAt (φ ≫ L.πTruncGE e) (e.f i) ↔ QuasiIsoAt φ (e.f i)
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case inl
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝² : HasZeroObject C
n : ℤ
inst✝¹ : K.IsStrictlyGE n
inst✝ : K.IsStrictlyLE n
i : ℤ
hi : i < n
⊢ (mkHomToSingle (𝟙 (K.X n)) ⋯ ≫ mkHomFromSingle (𝟙 (K.X n)) ⋯).f i = (𝟙 K).f i

pp: case inr.inl
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝² : HasZeroObject C
i : ℤ
inst✝¹ : K.IsStrictlyGE i
inst✝ : K.IsStrictlyLE i
⊢ (mkHomToSingle (𝟙 (K.X i)) ⋯ ≫ mkHomFromSingle (𝟙 (K.X i)) ⋯).f i = (𝟙 K).f i

pp: case inr.inr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝² : HasZeroObject C
n : ℤ
inst✝¹ : K.IsStrictlyGE n
inst✝ : K.IsStrictlyLE n
i : ℤ
hi : n < i
⊢ (mkHomToSingle (𝟙 (K.X n)) ⋯ ≫ mkHomFromSingle (𝟙 (K.X n)) ⋯).f i = (𝟙 K).f i

Tactic:
· apply (K.isZero_of_isStrictlyGE n i (by lia)).eq_of_src

Goal state after:
case inr.inl
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝² : HasZeroObject C
i : ℤ
inst✝¹ : K.IsStrictlyGE i
inst✝ : K.IsStrictlyLE i
⊢ (mkHomToSingle (𝟙 (K.X i)) ⋯ ≫ mkHomFromSingle (𝟙 (K.X i)) ⋯).f i = (𝟙 K).f i

case inr.inr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝² : HasZeroObject C
n : ℤ
inst✝¹ : K.IsStrictlyGE n
inst✝ : K.IsStrictlyLE n
i : ℤ
hi : n < i
⊢ (mkHomToSingle (𝟙 (K.X n)) ⋯ ≫ mkHomFromSingle (𝟙 (K.X n)) ⋯).f i = (𝟙 K).f i
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ ((single C c j).obj A).homologyπ j ≫ ((single C c j).obj A).homologyι j =
    (singleObjCyclesSelfIso c j A).hom ≫ (singleObjOpcyclesSelfIso c j A).hom

Tactic:
homology_π_ι,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ ((single C c j).obj A).iCycles j ≫ ((single C c j).obj A).pOpcycles j =
    (singleObjCyclesSelfIso c j A).hom ≫ (singleObjOpcyclesSelfIso c j A).hom
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 Z : C
inst✝² : HasSmallLocalizedHom W X Y
inst✝¹ : HasSmallLocalizedHom W Y Z
inst✝ : HasSmallLocalizedHom W X Z
this✝ : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := small_of_hasSmallLocalizedHom W W.Q X Y
this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := small_of_hasSmallLocalizedHom W W.Q Y Z
α : W.Q.obj X ⟶ W.Q.obj Y
β : W.Q.obj Y ⟶ W.Q.obj Z
⊢ (homEquiv W W.Q L)
      ((equivShrink (W.Q.obj X ⟶ W.Q.obj Z)).symm
        ((equivShrink (W.Q.obj X ⟶ W.Q.obj Z))
          ((homEquiv W W.Q W.Q)
            ((homEquiv W W.Q W.Q)
                ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α)) ≫
              (homEquiv W W.Q W.Q)
                ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)).symm ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) β)))))) =
    (homEquiv W W.Q L) ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α)) ≫
      (homEquiv W W.Q L) ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)).symm ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) β))

Tactic:
rw [Equiv.symm_apply_apply]

Goal state after:
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 Z : C
inst✝² : HasSmallLocalizedHom W X Y
inst✝¹ : HasSmallLocalizedHom W Y Z
inst✝ : HasSmallLocalizedHom W X Z
this✝ : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := small_of_hasSmallLocalizedHom W W.Q X Y
this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := small_of_hasSmallLocalizedHom W W.Q Y Z
α : W.Q.obj X ⟶ W.Q.obj Y
β : W.Q.obj Y ⟶ W.Q.obj Z
⊢ (homEquiv W W.Q L)
      ((homEquiv W W.Q W.Q)
        ((homEquiv W W.Q W.Q) ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α)) ≫
          (homEquiv W W.Q W.Q)
            ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)).symm ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) β)))) =
    (homEquiv W W.Q L) ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) α)) ≫
      (homEquiv W W.Q L) ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)).symm ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) β))
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos.hR₁
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ ((δ₀Functor ⋙ δlastFunctor).obj (composableArrows₅ hS₁ i j hij)).Exact

Tactic:
exact (composableArrows₅_exact hS₁ i j hij).δ₀.δlast

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
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := ⋯
⊢ ((-α).comp β h).hom = (-α.comp β h).hom

Tactic:
simp [this, neg_hom']

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
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := ⋯
⊢ (α.comp (-β) h).hom = (-α.comp β h).hom

Tactic:
simp [this, neg_hom']

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
S₁ S₂ : ShortComplex C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ ((singleFunctorsPostcompQIso C).hom.hom 0).app S₁.X₃ ≫
      triangleOfSESδ ⋯ ≫
        (shiftFunctor (DerivedCategory C) 1).map (((CochainComplex.singleFunctors C).functor 0 ⋙ Q).map f.τ₁) ≫
          (shiftFunctor (DerivedCategory C) 1).map (((singleFunctorsPostcompQIso C).inv.hom 0).app S₂.X₁) =
    (singleFunctor C 0).map f.τ₃ ≫
      ((singleFunctorsPostcompQIso C).hom.hom 0).app S₂.X₃ ≫
        triangleOfSESδ ⋯ ≫
          (shiftFunctor (DerivedCategory C) 1).map (((singleFunctorsPostcompQIso C).inv.hom 0).app S₂.X₁)

Tactic:
dsimp [CochainComplex.singleFunctors]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
S₁ S₂ : ShortComplex C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ ((singleFunctorsPostcompQIso C).hom.hom 0).app S₁.X₃ ≫
      triangleOfSESδ ⋯ ≫
        (shiftFunctor (DerivedCategory C) 1).map
            (Q.map ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map f.τ₁)) ≫
          (shiftFunctor (DerivedCategory C) 1).map (((singleFunctorsPostcompQIso C).inv.hom 0).app S₂.X₁) =
    (singleFunctor C 0).map f.τ₃ ≫
      ((singleFunctorsPostcompQIso C).hom.hom 0).app S₂.X₃ ≫
        triangleOfSESδ ⋯ ≫
          (shiftFunctor (DerivedCategory C) 1).map (((singleFunctorsPostcompQIso C).inv.hom 0).app S₂.X₁)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ 𝟙 ((shiftFunctor Cᵒᵖ 0).obj X) =
    (shiftFunctorOpIso C 0 0 ⋯).hom.app X ≫
      ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op ≫
        ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C 0 0 ⋯).inv.app X

Tactic:
← op_comp_assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ 𝟙 ((shiftFunctor Cᵒᵖ 0).obj X) =
    (shiftFunctorOpIso C 0 0 ⋯).hom.app X ≫
      ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X) ≫ (shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op ≫
        (shiftFunctorOpIso C 0 0 ⋯).inv.app X
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ a₃).obj X) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X

Tactic:
← op_comp_assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ a₃).obj X) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X) ≫
            (shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X
Module: Mathlib.CategoryTheory.Shift.Adjunction

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a b : A
h : b + a = 0
inst✝ : F.CommShift A
Y : D
⊢ (iso adj a).inv.app Y =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D b a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a b ⋯).hom.app (F.obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map (adj.counit.app Y))

Tactic:
obtain rfl : b = -a := by rw [← add_left_inj a, h, neg_add_cancel]
  simp only [iso, iso', shiftEquiv', Equiv.toFun_as_coe, conjugateIsoEquiv_apply_inv,
    conjugateEquiv_apply_app, Functor.comp_obj, comp_unit_app, Functor.id_obj,
    Equivalence.toAdjunction_unit, Equivalence.Equivalence_mk'_unit, Iso.symm_hom, Functor.comp_map,
    comp_counit_app, Equivalence.toAdjunction_counit, Equivalence.Equivalence_mk'_counit,
    Functor.map_shiftFunctorCompIsoId_hom_app, assoc, Functor.map_comp]
  slice_lhs 3 4 => rw [← Functor.map_comp, ← Functor.map_comp, Iso.inv_hom_id_app]
  simp only [Functor.comp_obj, Functor.map_id, id_comp, assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : Triangle Cᵒᵖ
φ : T₁ ⟶ T₂
⊢ ((shiftFunctor C 1).map φ.hom₃.unop).op ≫
      ((shiftFunctor C 1).map T₂.mor₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁ =
    ((shiftFunctor C 1).map T₁.mor₃.unop).op ≫
      ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map φ.hom₁).unop).op ≫
        (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁

Tactic:
← op_comp_assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : Triangle Cᵒᵖ
φ : T₁ ⟶ T₂
⊢ ((shiftFunctor C 1).map T₂.mor₃.unop ≫ (shiftFunctor C 1).map φ.hom₃.unop).op ≫
      (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁ =
    ((shiftFunctor C 1).map T₁.mor₃.unop).op ≫
      ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map φ.hom₁).unop).op ≫
        (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁
Module: Mathlib.CategoryTheory.Triangulated.Yoneda

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
B : C
T : Triangle Cᵒᵖ
hT : T ∈ distinguishedTriangles
x₂ : unop T.obj₂ ⟶ B
hx₂ : T.mor₂.unop ≫ x₂ = 0
⊢ ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).f) x₁ = x₂

Tactic:
obtain ⟨x₃, hx₃⟩ := Triangle.yoneda_exact₂ _ (unop_distinguished T hT) x₂ hx₂

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
B : C
T : Triangle Cᵒᵖ
hT : T ∈ distinguishedTriangles
x₂ : unop T.obj₂ ⟶ B
hx₂ : T.mor₂.unop ≫ x₂ = 0
x₃ : (unop ((triangleOpEquivalence C).inverse.obj T)).obj₃ ⟶ B
hx₃ : x₂ = (unop ((triangleOpEquivalence C).inverse.obj T)).mor₂ ≫ x₃
⊢ ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).f) x₁ = x₂
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution solution' : relations.Solution M
h : solution = solution'
g : relations.G
⊢ solution.var g = solution'.var g

Tactic:
rw [h]

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

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution M
h : solution = solution'
f : M →ₗ[A] N
⊢ solution.postcomp f = solution'.postcomp f

Tactic:
rw [h]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
inst✝³ : CommSemiring R
S : Type u_9
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
v : ι' → S
i : ι'
⊢ ∑ x, b x * (b.toMatrix v).map (⇑(algebraMap R S)) x i = v i

Tactic:
Matrix.map_apply,

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_5
inst✝³ : CommSemiring R
S : Type u_9
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
v : ι' → S
i : ι'
⊢ ∑ x, b x * (algebraMap R S) (b.toMatrix v x i) = v i
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝¹¹ : CommRing R₂
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
S : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : Algebra R₂ S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R₂ S M₂
inst✝¹ : IsDomain R₂
inst✝ : IsTorsionFree R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range ⇑b))
i✝ j✝ : ι
⊢ ((restrictScalars R₂ b).toMatrix v).map (⇑(algebraMap R₂ S)) i✝ j✝ = b.toMatrix (fun i ↦ ↑(v i)) i✝ j✝

Tactic:
Matrix.map_apply,

Goal state after:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝¹¹ : CommRing R₂
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
S : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : Algebra R₂ S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R₂ S M₂
inst✝¹ : IsDomain R₂
inst✝ : IsTorsionFree R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range ⇑b))
i✝ j✝ : ι
⊢ (algebraMap R₂ S) ((restrictScalars R₂ b).toMatrix v i✝ j✝) = b.toMatrix (fun i ↦ ↑(v i)) i✝ j✝
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 : ℕ
M : Type u_7
inst✝ : CommMonoid M
n : ℕ
ζ : ↥(rootsOfUnity n M)
⊢ (fun ζ ↦ ⟨↑↑ζ, ⋯⟩) ((fun ζ ↦ ⟨toUnits ↑ζ, ⋯⟩) ζ) = ζ

Tactic:
by simp only [val_toUnits_apply, Subtype.coe_eta]

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

Goal state before:
pp: case pos
n✝ : Type u_1
inst✝⁵ : Fintype n✝
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.univ.sup' ⋯ v
j₀ : n
h_j₀ : Finset.univ.sup' ⋯ v = v j₀
i : n
hi : i ∈ Finset.univ
h : i = j₀
⊢ v j₀ * A i j₀ ≤ v i * A i j₀

Tactic:
rw [h]

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
inst✝ : CharZero R
g h : SpecialLinearGroup n ℤ
⊢ (∀ (i j : n), (↑g).map (fun x ↦ ↑x) i j = (↑h).map (fun x ↦ ↑x) i j) → ∀ (i j : n), ↑g i j = ↑h i j

Tactic:
Matrix.map_apply,

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : CharZero R
g h : SpecialLinearGroup n ℤ
⊢ (∀ (i j : n), ↑(↑g i j) = ↑(↑h i j)) → ∀ (i j : n), ↑g i j = ↑h i j
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
⊢ transvection hij b ∈ Subgroup.center (SpecialLinearGroup ι F) ↔ b = 0

Tactic:
refine ⟨fun h ↦ ?_, fun hb ↦ ?_⟩
  · obtain ⟨r, _, hr⟩ := mem_center_iff.1 h
    simpa [transvection_coe, hij] using congr($hr i j).symm
  · simp only [hb, mem_center_iff, scalar_apply, transvection_coe, single_zero,
      add_zero, diagonal_eq_one]
    exact ⟨1, one_pow _, rfl⟩

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : SpecialLinearGroup ι F
⊢ ∃ L L' D,
    ∃ (hD : (diagonal D).det = 1),
      M =
        (List.map TransvectionStruct.toSpecialLinearGroup L).prod * ⟨diagonal D, hD⟩ *
          (List.map TransvectionStruct.toSpecialLinearGroup L').prod

Tactic:
obtain ⟨L, L', D, hM⟩ := Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec M.1
  refine ⟨L, L', D, by simpa [hM] using M.2, Subtype.ext <| ?_⟩
  simp_rw [coe_mul, ← coeMonoidHom_apply, map_list_prod, List.map_map, Function.comp_def,
    coeMonoidHom_apply, TransvectionStruct.toSpecialLinearGroup_coe, hM]

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
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ (((Pi.basisFun R n).repr (l (Pi.single i 1))).sum fun i xi ↦
      ((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj ↦
        xi •> yj •> (B ((Pi.basisFun R n) i)) ((Pi.basisFun R m) j)) =
    ∑ y,
      ∑ x,
        of (fun i j ↦ l (Pi.single j 1) i) y i * (B (Pi.single y 1)) (Pi.single x 1) *
          of (fun i j ↦ r (Pi.single j 1) i) x j

Tactic:
rw [Finsupp.sum_fintype]

Goal state after:
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
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ (∑ i_1,
      ((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj ↦
        ((Pi.basisFun R n).repr (l (Pi.single i 1))) i_1 •> yj •> (B ((Pi.basisFun R n) i_1)) ((Pi.basisFun R m) j)) =
    ∑ y,
      ∑ x,
        of (fun i j ↦ l (Pi.single j 1) i) y i * (B (Pi.single y 1)) (Pi.single x 1) *
          of (fun i j ↦ r (Pi.single j 1) i) x j

case h
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
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ ∀ (i : n),
    (((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj ↦
        0 •> yj •> (B ((Pi.basisFun R n) i)) ((Pi.basisFun R m) j)) =
      0