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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ Q.map S.f ≫ 𝟙 (Q.obj S.X₂) = 𝟙 (Q.obj S.X₁) ≫ Q.map S.f

Tactic:
simp only [comp_id, id_comp]

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

Goal state before:
pp: case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp ((mk₀ biprod.fst).comp α ⋯).hom ⋯ = α.hom

Tactic:
comp_hom,

Goal state after:
case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp ((mk₀ biprod.fst).hom.comp α.hom ⋯) ⋯ = α.hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp ((mk₀ biprod.snd).comp β ⋯).hom ⋯ = β.hom

Tactic:
comp_hom,

Goal state after:
case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp ((mk₀ biprod.snd).hom.comp β.hom ⋯) ⋯ = β.hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (ShiftedHom.mk₀ 0 mk₀._proof_1 ((singleFunctor C 0).map (biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.snd))).comp β.hom ⋯ = β.hom

Tactic:
biprod.lift_snd,

Goal state after:
case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (ShiftedHom.mk₀ 0 mk₀._proof_1 ((singleFunctor C 0).map (𝟙 X))).comp β.hom ⋯ = β.hom
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
⊢ HasExt C ↔ ∀ (X Y : C) (n : ℕ), Small.{w', w} (Ext X Y n)

Tactic:
let := HasDerivedCategory.standard C
  simp only [hasExt_iff, small_congr Ext.homEquiv]
  constructor
  · intro h X Y n
    exact h X Y n (by simp)
  · intro h X Y n hn
    lift n to ℕ using hn
    exact h X Y n

Goal state after:
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 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (φ.app 0)
h₁ : IsIso (φ.app 1)
h₃ : IsIso (φ.app 3)
h₄ : Mono (φ.app 4)
⊢ Mono (app' φ 2 ⋯)

Tactic:
apply mono_of_epi_of_mono_of_mono (δlastFunctor.map φ) (R₁.exact_iff_δlast.1 hR₁).1
      (R₂.exact_iff_δlast.1 hR₂).1

Goal state after:
case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (φ.app 0)
h₁ : IsIso (φ.app 1)
h₃ : IsIso (φ.app 3)
h₄ : Mono (φ.app 4)
⊢ Epi (app' (δlastFunctor.map φ) 0 mono_of_epi_of_mono_of_mono'._proof_13)

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (φ.app 0)
h₁ : IsIso (φ.app 1)
h₃ : IsIso (φ.app 3)
h₄ : Mono (φ.app 4)
⊢ Mono (app' (δlastFunctor.map φ) 1 mono_of_epi_of_mono_of_mono'._proof_11)

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (φ.app 0)
h₁ : IsIso (φ.app 1)
h₃ : IsIso (φ.app 3)
h₄ : Mono (φ.app 4)
⊢ Mono (app' (δlastFunctor.map φ) 3 mono_of_epi_of_mono_of_mono'._proof_7)
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_1.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ {
      X₁ :=
        (mk₂ ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨0, ⋯⟩,
      X₂ :=
        (mk₂ ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨1, ⋯⟩,
      X₃ :=
        (mk₂ ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨2, ⋯⟩,
      f :=
        (mk₂ ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
          0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
      g :=
        (mk₂ ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
          1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
      zero := ⋯ }.Exact

Tactic:
rwa [ShortComplex.exact_iff_epi _ (by simp)]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_2.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ {
      X₁ :=
        (mk₂ ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨0, ⋯⟩,
      X₂ :=
        (mk₂ ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨1, ⋯⟩,
      X₃ :=
        (mk₂ ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨2, ⋯⟩,
      f :=
        (mk₂ ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
          0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
      g :=
        (mk₂ ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
          1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
      zero := ⋯ }.Exact

Tactic:
rwa [ShortComplex.exact_iff_epi _ (by simp)]

Goal state after:
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
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ ((opEquiv a).symm f).comp z h = (opEquiv a).symm (Quiver.Hom.op z ≫ f) ≫ (shiftFunctorAdd' C b a c h).inv.app Z

Tactic:
rw [ShiftedHom.opEquiv_symm_apply, ShiftedHom.opEquiv_symm_apply,
    ShiftedHom.comp]
  dsimp
  simp only [assoc, Functor.map_comp]

Goal state after:
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)
⊢ (opEquiv' (m + n) a a'' ⋯).symm x =
    (opEquiv' m a' a'' ha'').symm
      (Quiver.Hom.op ((opEquiv' n a a' ha').symm (x ≫ (shiftFunctorAdd Cᵒᵖ m n).hom.app (Opposite.op X))))

Tactic:
simp only [opEquiv'_symm_apply, opEquiv_symm_apply,
    opShiftFunctorEquivalence_add_unitIso_inv_app_eq _ _ _ _ (add_comm n m)]

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)
⊢ ((((shiftFunctor C (m + n)).map ((shiftFunctorAdd' Cᵒᵖ m n (m + n) ⋯).hom.app (Opposite.op X)).unop).op ≫
            ((shiftFunctorAdd' C n m (m + n) ⋯).inv.app
                  (Opposite.unop ((shiftFunctor Cᵒᵖ m ⋙ shiftFunctor Cᵒᵖ n).obj (Opposite.op X)))).op ≫
              ((shiftFunctor C m).map
                    ((opShiftFunctorEquivalence C n).unitIso.inv.app
                        ((shiftFunctor Cᵒᵖ m).obj (Opposite.op X))).unop).op ≫
                (opShiftFunctorEquivalence C m).unitIso.inv.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
                              ((Discrete.addMonoidalFunctor (AddMonoidHom.mk' (fun n ↦ -n) ⋯)).obj { as := m }).as).obj
                          X))).unop ≫
                  (shiftFunctor C n).map (x ≫ (shiftFunctorAdd Cᵒᵖ m n).hom.app (Opposite.op X)).unop) ≫
                (shiftFunctorAdd' C a n a' ⋯).inv.app Y).op.unop) ≫
      (shiftFunctorAdd' C a' m a'' ⋯).inv.app Y
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
inst✝ : HasDerivedCategory C
X : C
n₀ : ℕ
x : Ext X S.X₃ n₀
n₁ : ℕ
h : n₀ + 1 = n₁
⊢ x.hom ≫
      (shiftFunctor (DerivedCategory C) ↑n₀).map hS.singleTriangle.mor₃ ≫
        (shiftFunctorAdd' (DerivedCategory C) 1 ↑n₀ ↑n₁ ⋯).inv.app hS.singleTriangle.obj₁ =
    (x.comp hS.extClass h).hom

Tactic:
comp_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
X : C
n₀ : ℕ
x : Ext X S.X₃ n₀
n₁ : ℕ
h : n₀ + 1 = n₁
⊢ x.hom ≫
      (shiftFunctor (DerivedCategory C) ↑n₀).map hS.singleTriangle.mor₃ ≫
        (shiftFunctorAdd' (DerivedCategory C) 1 ↑n₀ ↑n₁ ⋯).inv.app hS.singleTriangle.obj₁ =
    x.hom.comp hS.extClass.hom ⋯
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Goal state before:
pp: R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y : C
n : ℕ
x : Ext X Y n
r : R
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ r • homEquiv x = (x.comp (mk₀ (r • 𝟙 Y)) ⋯).hom

Tactic:
comp_hom,

Goal state after:
R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y : C
n : ℕ
x : Ext X Y n
r : R
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ r • homEquiv x = x.hom.comp (mk₀ (r • 𝟙 Y)).hom ⋯
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
inst✝ : HasDerivedCategory C
Y : C
n₀ : ℕ
x : Ext S.X₁ Y n₀
n₁ : ℕ
h : 1 + n₀ = n₁
⊢ hS.singleTriangle.mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map x.hom ≫
        (shiftFunctorAdd' (DerivedCategory C) (↑n₀) 1 ↑n₁ ⋯).inv.app ((singleFunctor C 0).obj Y) =
    (hS.extClass.comp x h).hom

Tactic:
comp_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
Y : C
n₀ : ℕ
x : Ext S.X₁ Y n₀
n₁ : ℕ
h : 1 + n₀ = n₁
⊢ hS.singleTriangle.mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map x.hom ≫
        (shiftFunctorAdd' (DerivedCategory C) (↑n₀) 1 ↑n₁ ⋯).inv.app ((singleFunctor C 0).obj Y) =
    hS.extClass.hom.comp x.hom ⋯
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
ζ : Rˣ
⊢ ζ ^ (p ^ k * m) = 1 ↔ ζ ∈ rootsOfUnity m R

Tactic:
rw [← mem_rootsOfUnity, mem_rootsOfUnity_prime_pow_mul_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

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
f : R →+* S
g : GL n R
⊢ (map f) g⁻¹ = ((map f) g)⁻¹

Tactic:
by
  simp only [map_inv]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
R : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Fact (Even (Fintype.card n))
g : ↥(GLPos n R)
⊢ -↑g ∈ GLPos n R

Tactic:
rw [mem_glpos, GeneralLinearGroup.val_det_apply, Units.val_neg, det_neg,
        (Fact.out (p := Even <| Fintype.card n)).neg_one_pow, one_mul]

Goal state after:
n : Type u
R : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Fact (Even (Fintype.card n))
g : ↥(GLPos n R)
⊢ 0 < (↑↑g).det
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
M : Matrix n n A
inst✝ : DecidableEq n
⊢ M.SeparatingRight ↔ M.det ≠ 0

Tactic:
grind [separatingRight_iff_forall_mulVec_eq_zero, exists_mulVec_eq_zero_iff]

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

Goal state before:
pp: case h
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : ↑⟨!![a, b; c, d], ⋯⟩ 1 0 = 0
⊢ ∃ a_1 b_1, ∃ (h : a_1 ≠ 0), ⟨!![a, b; c, d], ⋯⟩ = ⟨!![a_1, b_1; 0, a_1⁻¹], ⋯⟩

Tactic:
replace hg : c = 0 := by simpa using hg

Goal state after:
case h
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
⊢ ∃ a_1 b_1, ∃ (h : a_1 ≠ 0), ⟨!![a, b; c, d], ⋯⟩ = ⟨!![a_1, b_1; 0, a_1⁻¹], ⋯⟩
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : D i₀ = (∏ x with x ≠ i₀, D x)⁻¹
⊢ (∏ i with i ≠ i₀, fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) = D

Tactic:
← Finset.prod_inv_distrib

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : D i₀ = ∏ x with x ≠ i₀, (D x)⁻¹
⊢ (∏ i with i ≠ i₀, fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) = D
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' : List (TransvectionStruct ι F)
D : ι → F
hM : ↑M = (List.map TransvectionStruct.toMatrix L).prod * diagonal D * (List.map TransvectionStruct.toMatrix L').prod
⊢ ↑M =
    (List.map (fun x ↦ ↑x.toSpecialLinearGroup) L).prod * diagonal D *
      (List.map (fun x ↦ ↑x.toSpecialLinearGroup) L').prod

Tactic:
TransvectionStruct.toSpecialLinearGroup_coe,

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : SpecialLinearGroup ι F
L L' : List (TransvectionStruct ι F)
D : ι → F
hM : ↑M = (List.map TransvectionStruct.toMatrix L).prod * diagonal D * (List.map TransvectionStruct.toMatrix L').prod
⊢ ↑M = (List.map (fun x ↦ x.toMatrix) L).prod * diagonal D * (List.map (fun x ↦ x.toMatrix) L').prod
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : CommMonoid R
inst✝¹ : AddCommMonoid ι
A : ι → S
inst✝ : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
hF : ∀ k ∈ F, g k ∈ A (i k)
⊢ ∏ k ∈ F, g k ∈ A (∑ k ∈ F, i k)

Tactic:
induction F using Finset.induction_on

Goal state after:
case empty
ι : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : CommMonoid R
inst✝¹ : AddCommMonoid ι
A : ι → S
inst✝ : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
hF : ∀ k ∈ ∅, g k ∈ A (i k)
⊢ ∏ k ∈ ∅, g k ∈ A (∑ k ∈ ∅, i k)

case insert
ι : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : CommMonoid R
inst✝¹ : AddCommMonoid ι
A : ι → S
inst✝ : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
a✝² : κ
s✝ : Finset κ
a✝¹ : a✝² ∉ s✝
a✝ : (∀ k ∈ s✝, g k ∈ A (i k)) → ∏ k ∈ s✝, g k ∈ A (∑ k ∈ s✝, i k)
hF : ∀ k ∈ insert a✝² s✝, g k ∈ A (i k)
⊢ ∏ k ∈ insert a✝² s✝, g k ∈ A (∑ k ∈ insert a✝² s✝, i k)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
j : Fin 2
c : F
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ j = 1

Tactic:
fin_cases j <;> tauto

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
j : Fin 2
c : F
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ j = 0

Tactic:
fin_cases j <;> tauto

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
j : Fin 2
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ j = 1

Tactic:
fin_cases j <;> tauto

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
j : Fin 2
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ j = 0

Tactic:
fin_cases j <;> tauto

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
⊢ ∀ (y : A i), ((mulHom A) One.one) ((of A i) y) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) y)

Tactic:
xi

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ((mulHom A) One.one) ((of A i) xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
⊢ ∀ (y : A i), ((mulHom A).flip One.one) ((of A i) y) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) y)

Tactic:
xi

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ((mulHom A).flip One.one) ((of A i) xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)
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
a : R
x y : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ (a * a) • Q x + Q y + (B (a • x)) y - (a * a) • Q x - Q y = a • (Q x + Q y + (B x) y - Q x - Q y)

Tactic:
LinearMap.map_smul₂,

Goal state after:
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
a : R
x y : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ (a * a) • Q x + Q y + a • (B x) y - (a * a) • Q x - Q y = a • (Q x + Q y + (B x) y - Q x - Q y)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
⊢ (of A 0) (a ^ 0) = (of A 0) a ^ 0

Tactic:
by rw [pow_zero, pow_zero, DirectSum.of_zero_one]

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ ↦ if i₁ + i = n then ↑x₁ * ↑0 else 0) = 0

Tactic:
simp_rw [ZeroMemClass.coe_zero, mul_zero, ite_self]

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ ↦ 0) = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: V : Type u
K : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hK : Invertible 2
B : BilinForm K V
hB₂ : IsSymm B
⊢ ∀ (d : ℕ), finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v

Tactic:
intro d hd

Goal state after:
V : Type u
K : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hK : Invertible 2
B : BilinForm K V
hB₂ : IsSymm B
d : ℕ
hd : finrank K V = d
⊢ ∃ v, IsOrthoᵢ B ⇑v