mathlib-initiative/mathlib-tactics huggingface dataset:
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
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.sc j').iCycles ≫
      (𝟙 (K.X j') ≫ (K.restrictionXIso e hj').inv ≫ 𝟙 (K.X (e.f j))) ≫ ((K.restriction e).sc j).pOpcycles =
    (K.sc j').homologyπ ≫ K.homologyι j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv

Tactic:
rw [comp_id, id_comp]

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.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
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.sc j').iCycles ≫ (K.restrictionXIso e hj').inv ≫ ((K.restriction e).sc j).pOpcycles =
    (K.sc j').homologyπ ≫ K.homologyι j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

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.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
⊢ QuasiIso (K.ιTruncLE e) ↔ K.IsSupported e

Tactic:
rw [← quasiIso_opFunctor_map_iff, ← isSupported_op_iff]
  exact K.op.quasiIso_πTruncGE_iff_isSupported e.op

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

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'
inst✝ : HasZeroObject C
a✝ : K.IsSupported e
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ QuasiIsoAt (K.πTruncGE e) i'

Tactic:
· rw [quasiIsoAt_iff_exactAt (K.πTruncGE e) i']
      all_goals exact exactAt_of_isSupported _ e i' (by simpa using hi')

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

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✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i' : ι'
j : ι
hij' : c'.Rel i' (e.f j)
⊢ ⋯.δ i' (e.f j) hij' ≫ homologyMap (K.ιTruncLE e) (e.f j) = 0 ≫ homologyMap (K.ιTruncLE e) (e.f j)

Tactic:
zero_comp

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i' : ι'
j : ι
hij' : c'.Rel i' (e.f j)
⊢ ⋯.δ i' (e.f j) hij' ≫ homologyMap (K.ιTruncLE e) (e.f j) = 0
Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
L : C ⥤ D
inst✝³ : L.IsLocalization W
inst✝² : L.CommShift M
X Y : C
m : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M X Y
e : SmallShiftedHom W X Y m
⊢ (equiv W L) (chgUniv e) = (equiv W L) e

Tactic:
dsimp [equiv]
  congr
  apply SmallHom.equiv_chgUniv

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

Goal state before:
pp: case pos
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)
hi : ∃ j, c.Rel i j
⊢ Epi (homologyMap φ.τ₃ i)

pp: case neg
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)
hi : ¬∃ j, c.Rel i j
⊢ Epi (homologyMap φ.τ₃ i)

Tactic:
· obtain ⟨j, hij⟩ := hi
    apply epi_of_epi_of_epi_of_mono
      ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij))
    · exact (composableArrows₅_exact hS₁ i j hij).δ₀.δlast
    · exact (composableArrows₅_exact hS₂ i j hij).δ₀.δlast
    · exact h₁
    · exact h₂ j hij
    · exact h₃ j hij

Goal state after:
case neg
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)
hi : ¬∃ j, c.Rel i j
⊢ Epi (homologyMap φ.τ₃ i)
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁✝ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
f₂ : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
⊢ 0 = 0 ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7

Tactic:
zero_comp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁✝ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
f₂ : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
⊢ 0 = 0
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))
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)
⊢ (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)

Tactic:
apply (subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE _ _ (-a) (-b) (by
        lia)).elim

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
A : C
x₂ x₂' : A ⟶ K.X j
hx₂ : x₂ ≫ K.d j k = 0
hx₂' : x₂' ≫ K.d j k = 0
⊢ K.liftCycles x₂ k hk hx₂ ≫ K.homologyπ j = K.liftCycles x₂' k hk hx₂' ≫ K.homologyπ j ↔
    ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = π ≫ x₂' + x₁ ≫ K.d i j

Tactic:
subst hi hk
  exact (K.sc j).liftCycles_comp_homologyπ_eq_iff_up_to_refinements x₂ x₂' hx₂ hx₂'

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 : C
n : ℕ
inst✝ : HasDerivedCategory C
β : Ext 0 Y n := 0
hβ : β.hom = 0
this : 0 = comp 0 β ⋯
⊢ hom 0 = 0

Tactic:
rw [this, comp_hom, hβ, ShiftedHom.comp_zero]

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
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x✝ : (i : J) → Ext (X i) Y n
i b✝ : J
a✝ : b✝ ∈ Finset.univ
hij : b✝ ≠ i
⊢ comp 0 (x✝ b✝) ⋯ = 0

Tactic:
zero_comp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x✝ : (i : J) → Ext (X i) Y n
i b✝ : J
a✝ : b✝ ∈ Finset.univ
hij : b✝ ≠ i
⊢ 0 = 0
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₁) =
    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
            ((𝟙 (((CochainComplex.singleFunctors C).postcomp Q).functor 0)).app S.X₁)

Tactic:
NatTrans.id_app

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₁) =
    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
            (𝟙 ((((CochainComplex.singleFunctors C).postcomp Q).functor 0).obj S.X₁))
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ (m + n)).obj (Opposite.op X)
⊢ ((((((opShiftFunctorEquivalence C m).unitIso.inv.app (Opposite.op X)).unop ≫
              (shiftFunctor C m).map
                ((opShiftFunctorEquivalence C n).unitIso.inv.app ((shiftFunctor Cᵒᵖ m).obj (Opposite.op X))).unop) ≫
            (shiftFunctorAdd' C n m (m + n) ⋯).inv.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj ((shiftFunctor Cᵒᵖ m).obj (Opposite.op X))))) ≫
          (shiftFunctor C (m + n)).map ((shiftFunctorAdd' Cᵒᵖ m n (m + n) ⋯).hom.app (Opposite.op X)).unop) ≫
        (shiftFunctor C (m + n)).map x.unop) ≫
      (shiftFunctorAdd' C a (m + n) a'' ⋯).inv.app Y =
    (((opShiftFunctorEquivalence C m).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C m).map
          ((((opShiftFunctorEquivalence C n).unitIso.inv.app
                  (Opposite.op ((shiftFunctor C ((AddMonoidHom.mk' (fun n ↦ -n) ⋯) m)).obj X))).unop ≫
              (shiftFunctor C n).map (((shiftFunctorAdd Cᵒᵖ m n).hom.app (Opposite.op X)).unop ≫ x.unop)) ≫
            (shiftFunctorAdd' C a n a' ⋯).inv.app Y)) ≫
      (shiftFunctorAdd' C a' m a'' ⋯).inv.app Y

Tactic:
simp only [assoc, Functor.map_comp, ← shiftFunctorAdd'_eq_shiftFunctorAdd,
    ← NatTrans.naturality_assoc,
    shiftFunctorAdd'_assoc_inv_app a n m a' (m + n) a'' (by lia) (by lia) (by lia)]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ (m + n)).obj (Opposite.op X)
⊢ ((opShiftFunctorEquivalence C m).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C m).map
          ((opShiftFunctorEquivalence C n).unitIso.inv.app ((shiftFunctor Cᵒᵖ m).obj (Opposite.op X))).unop ≫
        (shiftFunctor C n ⋙ shiftFunctor C m).map ((shiftFunctorAdd' Cᵒᵖ m n (m + n) ⋯).hom.app (Opposite.op X)).unop ≫
          (shiftFunctor C n ⋙ shiftFunctor C m).map x.unop ≫
            (shiftFunctorAdd' C n m (m + n) ⋯).inv.app ((shiftFunctor C a).obj Y) ≫
              (shiftFunctorAdd' C a (m + n) a'' ⋯).inv.app Y =
    ((opShiftFunctorEquivalence C m).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C m).map
          ((opShiftFunctorEquivalence C n).unitIso.inv.app
              (Opposite.op ((shiftFunctor C ((AddMonoidHom.mk' (fun n ↦ -n) ⋯) m)).obj X))).unop ≫
        (shiftFunctor C m).map
            ((shiftFunctor C n).map ((shiftFunctorAdd' Cᵒᵖ m n (m + n) ⋯).hom.app (Opposite.op X)).unop) ≫
          (shiftFunctor C m).map ((shiftFunctor C n).map x.unop) ≫
            (shiftFunctorAdd' C n m (m + n) ⋯).inv.app ((shiftFunctor C a).obj Y) ≫
              (shiftFunctorAdd' C a (m + n) a'' ⋯).inv.app Y
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 : Triangle Cᵒᵖ
⊢ (inverse C ⋙ functor C).obj T ≅ (𝟭 (Triangle Cᵒᵖ)).obj T

Tactic:
refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((inverse C ⋙ functor C).obj T).mor₁ ≫ (Iso.refl ((inverse C ⋙ functor C).obj T).obj₂).hom =
    (Iso.refl ((inverse C ⋙ functor C).obj T).obj₁).hom ≫ ((𝟭 (Triangle Cᵒᵖ)).obj T).mor₁

case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((inverse C ⋙ functor C).obj T).mor₂ ≫ (Iso.refl ((inverse C ⋙ functor C).obj T).obj₃).hom =
    (Iso.refl ((inverse C ⋙ functor C).obj T).obj₂).hom ≫ ((𝟭 (Triangle Cᵒᵖ)).obj T).mor₂

case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((inverse C ⋙ functor C).obj T).mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map (Iso.refl ((inverse C ⋙ functor C).obj T).obj₁).hom =
    (Iso.refl ((inverse C ⋙ functor C).obj T).obj₃).hom ≫ ((𝟭 (Triangle Cᵒᵖ)).obj T).mor₃
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
⊢ ((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).Exact

Tactic:
by
    rw [ShortComplex.ab_exact_iff]
    intro (x₂ : T.obj₂.unop ⟶ B) (hx₂ : T.mor₂.unop ≫ x₂ = 0)
    obtain ⟨x₃, hx₃⟩ := Triangle.yoneda_exact₂ _ (unop_distinguished T hT) x₂ hx₂
    exact ⟨x₃, hx₃.symm⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ { X₁ := AddCommGrpCat.of (Ext S.X₁ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₃ Y n₁),
      X₃ := AddCommGrpCat.of (Ext S.X₂ Y n₁), f := AddCommGrpCat.ofHom (hS.extClass.precomp Y h),
      g := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), zero := ⋯ }.Exact

Tactic:
have := (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequence_exact₁ _
    (op_distinguished _ hS.singleTriangle_distinguished) n₀ n₁ (by lia)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  {
      X₁ :=
        ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₀).obj
          ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₃,
      X₂ :=
        ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).obj
          ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₁,
      X₃ :=
        ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).obj
          ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₂,
      f :=
        (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
          ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯,
      g :=
        ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift ↑n₁).map
          ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).mor₁,
      zero := ⋯ }.Exact
⊢ { X₁ := AddCommGrpCat.of (Ext S.X₁ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₃ Y n₁),
      X₃ := AddCommGrpCat.of (Ext S.X₂ Y n₁), f := AddCommGrpCat.ofHom (hS.extClass.precomp Y h),
      g := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), zero := ⋯ }.Exact
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
c : R
v : ι → M
i j : ι
⊢ e.toMatrix (c • v) i j = ((RingHom.id R) c • e.toMatrix v) i j

Tactic:
rw [e.toMatrix_apply, Pi.smul_apply, map_smul]

Goal state after:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
c : R
v : ι → M
i j : ι
⊢ (c • e.repr (v j)) i = ((RingHom.id R) c • e.toMatrix v) i j
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: 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
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
    [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
    (Pairwise fun i j ↦ A i j < 0) →
      ∀ (h : Nonempty n), A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i, A i j ≤ 0
h_sup : ¬0 < Finset.univ.sup' ⋯ v
⊢ -1 • v ≠ 0

Tactic:
simp [*]

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

Goal state before:
pp: 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₀
⊢ ∃ j, ∑ i, A i j ≤ 0

Tactic:
refine ⟨j₀, ?_⟩

Goal state after:
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, A i j₀ ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹¹ : Semiring R₁
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : Module S₁ N₂
inst✝⁵ : Module S₂ N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
i : n
j : m
⊢ ((toLinearMap₂'Aux σ₁ σ₂ f) (Pi.single i 1)) (Pi.single j 1) = f i j

Tactic:
by
  rw [Matrix.toLinearMap₂'Aux, mk₂'ₛₗ_apply]
  have : (∑ i', ∑ j', (if i = i' then (1 : S₁) else (0 : S₁)) •
        (if j = j' then (1 : S₂) else (0 : S₂)) • f i' j') =
      f i j := by
    simp_rw [← Finset.smul_sum]
    simp only [ite_smul, one_smul, zero_smul, sum_ite_eq, mem_univ, ↓reduceIte]
  rw [← this]
  exact Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by aesop

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ polar (-f) x y = -polar f x y

Tactic:
by
  simp only [polar, Pi.neg_apply, sub_eq_add_neg, neg_add]

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✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x y : M
⊢ polar (⇑Q) x (-y) = -polar (⇑Q) x y

Tactic:
rw [← neg_one_smul R y, polar_smul_right, neg_one_smul]

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✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ polar (⇑Q) x x = 2 • Q x

Tactic:
by
  rw [polar, map_add_self, sub_sub, sub_eq_iff_eq_add, ← two_smul ℕ, ← two_smul ℕ, ← mul_smul]
  simp

Goal state after: