mathlib-initiative/mathlib-tactics huggingface dataset:
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'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.extend e).ExactAt j' ↔ K.ExactAt j

Tactic:
simp only [HomologicalComplex.exactAt_iff_isZero_homology]

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
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ IsZero ((K.extend e).homology j') ↔ IsZero (K.homology j)
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 : ι
hij : c.Rel i j
hi : ¬e.BoundaryGE i
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j

Tactic:
· 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.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'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.extendHomologyIso e hj').hom ≫ K.homologyι j = (K.extend e).homologyι j' ≫ (K.extendOpcyclesIso e hj').hom

Tactic:
simp only [← cancel_epi ((K.extend e).homologyπ j'),
    homologyπ_extendHomologyIso_hom_assoc, homology_π_ι, extendCyclesIso_hom_iCycles_assoc,
    homology_π_ι_assoc, pOpcycles_extendOpcyclesIso_hom]

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

Goal state before:
pp: case mp
ι : 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✝ : QuasiIso (K.πTruncGE e)
⊢ K.IsSupported e

Tactic:
refine ⟨fun i' hi' => ?_⟩

Goal state after:
case mp
ι : 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✝ : QuasiIso (K.πTruncGE e)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ K.ExactAt i'
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: case mpr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex C c
⊢ K.IsStrictlySupported e₂ → K.IsStrictlySupportedOutside e₁

Tactic:
· intro _
    exact ⟨fun i₁ => K.isZero_X_of_isStrictlySupported e₂ _
      (fun i₂ => (ac.disjoint i₁ i₂).symm)⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)).HasLeftCalculusOfFractions

Tactic:
rw [HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (HomotopyCategory.subcategoryAcyclic C).trW.HasLeftCalculusOfFractions
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)).HasRightCalculusOfFractions

Tactic:
rw [HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (HomotopyCategory.subcategoryAcyclic C).trW.HasRightCalculusOfFractions
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 B : C
f : A ⟶ B
⊢ (singleObjHomologySelfIso c j A).inv ≫ homologyMap ((single C c j).map f) j = f ≫ (singleObjHomologySelfIso c j B).inv

Tactic:
rw [← cancel_mono (singleObjHomologySelfIso c j B).hom, assoc, assoc,
    singleObjHomologySelfIso_hom_naturality,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]

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

Goal state before:
pp: C₁ : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst✝⁹ : AddMonoid M
inst✝⁸ : HasShift C₁ M
inst✝⁷ : HasShift C₂ M
inst✝⁶ : Φ.functor.CommShift M
X₁ Y₁ : C₁
X₂ Y₂ : C₂
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst✝² : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor.obj X₁ ≅ X₂
eY : Φ.functor.obj Y₁ ≅ Y₂
inst✝¹ : W₁.IsCompatibleWithShift M
inst✝ : W₂.IsCompatibleWithShift M
m : M
f : ShiftedHom X₁ Y₁ m
⊢ Φ.smallShiftedHomMap eX eY (SmallShiftedHom.mk W₁ f) =
    SmallShiftedHom.mk W₂ ((ShiftedHom.mk₀ 0 ⋯ eX.inv).comp ((f.map Φ.functor).comp (ShiftedHom.mk₀ 0 ⋯ eY.hom) ⋯) ⋯)

Tactic:
apply (SmallShiftedHom.equiv W₂ W₂.Q).injective
  let e := CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
  simp only [Φ.equiv_smallShiftedHomMap W₁.Q W₂.Q _ _ (Φ.localizedFunctor W₁.Q W₂.Q) e,
    Functor.comp_obj, ShiftedHom.map, SmallShiftedHom.equiv_mk, Functor.map_comp, assoc,
    ShiftedHom.comp_mk₀, NatTrans.shift_app, Functor.commShiftIso_comp_inv_app,
    Functor.commShiftIso_comp_hom_app, Iso.hom_inv_id_app_assoc, ShiftedHom.mk₀_comp,
    Functor.commShiftIso_hom_naturality]
  nth_rw 2 [← Functor.map_comp_assoc]
  simp [reassoc_of% (NatIso.naturality_2 e f)]

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
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Ext S.X₃ S.X₁ 1

Tactic:
have := hS.hasSmallLocalizedShiftedHom_K_S'_X₁

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Ext S.X₃ S.X₁ 1
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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
eq :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y))
⊢ adj.unit.app (G.obj ((shiftFunctor D a).obj Y)) ≫ G.map (adj.counit.app ((shiftFunctor D a).obj Y)) =
    e₂.hom.app Y ≫
      (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ (shiftFunctor C a).map (G.map (adj.counit.app Y)) ≫ e₂.inv.app Y

Tactic:
simp only [right_triangle_components, ← Functor.map_comp_assoc, Functor.map_id, id_comp,
    Iso.hom_inv_id_app, Functor.comp_obj]

Goal state after:
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ᵒᵖ
m n p : ℤ
h : m + n = p
⊢ 𝟙 (((opShiftFunctorEquivalence C p).functor ⋙ (opShiftFunctorEquivalence C p).inverse).obj X) =
    (((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op ≫
        ((shiftFunctorAdd' C m n p h).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m).obj X))).op ≫
          ((shiftFunctor C n).map
                ((opShiftFunctorEquivalence C m).unitIso.inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
            (opShiftFunctorEquivalence C n).unitIso.inv.app X) ≫
      (opShiftFunctorEquivalence C p).unitIso.hom.app X

Tactic:
opShiftFunctorEquivalence_add_unitIso_hom_app_eq _ _ _ _ h,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ 𝟙 (((opShiftFunctorEquivalence C p).functor ⋙ (opShiftFunctorEquivalence C p).inverse).obj X) =
    (((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op ≫
        ((shiftFunctorAdd' C m n p h).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m).obj X))).op ≫
          ((shiftFunctor C n).map
                ((opShiftFunctorEquivalence C m).unitIso.inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
            (opShiftFunctorEquivalence C n).unitIso.inv.app X) ≫
      (opShiftFunctorEquivalence C n).unitIso.hom.app X ≫
        ((shiftFunctor C n).map
              ((opShiftFunctorEquivalence C m).unitIso.hom.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
          ((shiftFunctorAdd' C m n p h).hom.app
                (Opposite.unop ((opShiftFunctorEquivalence C m).functor.obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
            ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).inv.app X).unop).op
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ᵒᵖ
m n p : ℤ
h : m + n = p
⊢ (opShiftFunctorEquivalence C p).unitIso.inv.app X =
    ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op ≫
      ((shiftFunctorAdd' C m n p h).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m).obj X))).op ≫
        ((shiftFunctor C n).map
              ((opShiftFunctorEquivalence C m).unitIso.inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
          (opShiftFunctorEquivalence C n).unitIso.inv.app X

Tactic:
rw [← cancel_mono ((opShiftFunctorEquivalence C p).unitIso.hom.app X), Iso.inv_hom_id_app,
    opShiftFunctorEquivalence_add_unitIso_hom_app_eq _ _ _ _ h,
    Category.assoc, Category.assoc, Category.assoc, Iso.inv_hom_id_app_assoc]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ 𝟙 (((opShiftFunctorEquivalence C p).functor ⋙ (opShiftFunctorEquivalence C p).inverse).obj X) =
    ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op ≫
      ((shiftFunctorAdd' C m n p h).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m).obj X))).op ≫
        ((shiftFunctor C n).map
              ((opShiftFunctorEquivalence C m).unitIso.inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
          ((shiftFunctor C n).map
                ((opShiftFunctorEquivalence C m).unitIso.hom.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
            ((shiftFunctorAdd' C m n p h).hom.app
                  (Opposite.unop ((opShiftFunctorEquivalence C m).functor.obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
              ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).inv.app X).unop).op
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
⊢ a + b = 0

Tactic:
rw [eq_neg_of_add_eq_zero_left h, add_neg_cancel]

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 Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app
            (Opposite.unop ((shiftFunctor Cᵒᵖ a).obj ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X)))) ≫
          (shiftFunctor C c).map ((shiftFunctor Cᵒᵖ a).map g).unop ≫ (shiftFunctor C c).map (Quiver.Hom.unop f) =
    ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map (Quiver.Hom.unop g) ≫
        (shiftFunctor C b).map ((opEquiv a).symm f) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z

Tactic:
← NatTrans.naturality_assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
        (shiftFunctor C a ⋙ shiftFunctor C b).map ((shiftFunctor Cᵒᵖ a).map g).unop ≫
          (shiftFunctorAdd' C a b c ⋯).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ a).obj (Opposite.op Y))) ≫
            (shiftFunctor C c).map (Quiver.Hom.unop f) =
    ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map (Quiver.Hom.unop g) ≫
        (shiftFunctor C b).map ((opEquiv a).symm f) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z
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₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 isComplex₂_iff._proof_2 ⋯)
      ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact

Tactic:
refine exact₂_mk _ (by simp) ?_
      rw [ShortComplex.exact_iff_mono _ (by simp)]
      infer_instance

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

Goal state before:
pp: case succ
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughProjectives C
this✝¹ : HasDerivedCategory C := HasDerivedCategory.standard C
this✝ : HasExt C
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex C :=
  { X₁ := kernel (Projective.π X), X₂ := Projective.over X, X₃ := X, f := kernel.ι (Projective.π X),
    g := Projective.π X, zero := ⋯ }
hS : S.ShortExact
this : Function.Surjective ⇑(hS.extClass.precomp Y ⋯)
⊢ Small.{w, max u v} (Ext X Y (n + 1))

Tactic:
exact small_of_surjective.{w} this

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := ⋯
α : I ⟶ L.X i := ⋯
this : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α
⊢ (ι ≫ mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯).f i = (𝟙 ((singleFunctor C i).obj I)).f i

Tactic:
rw [comp_f, mkHomToSingle_f, id_f, this, assoc, Injective.comp_factorThru_assoc,
        id_comp, Iso.hom_inv_id]

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

Goal state before:
pp: case succ
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughInjectives C
this✝¹ : HasDerivedCategory C := HasDerivedCategory.standard C
this✝ : HasExt C
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex C :=
  { X₁ := Y, X₂ := Injective.under Y, X₃ := cokernel (Injective.ι Y), f := Injective.ι Y,
    g := cokernel.π (Injective.ι Y), zero := ⋯ }
hS : S.ShortExact
this : Function.Surjective ⇑(hS.extClass.postcomp X ⋯)
⊢ Small.{w, max u v} (Ext X Y (n + 1))

Tactic:
exact small_of_surjective.{w} this

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
x : relations.R →₀ A
⊢ (solution.π ∘ₗ relations.map) x = 0

Tactic:
rw [π_comp_map, LinearMap.zero_apply]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
⊢ M.Nondegenerate ↔ (∀ (v : m → R), v ᵥ* M = 0 → v = 0) ∧ ∀ (v : n → R), M *ᵥ v = 0 → v = 0

Tactic:
rw [nondegenerate_iff, separatingLeft_iff_forall_vecMul_eq_zero,
    separatingRight_iff_forall_mulVec_eq_zero]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
e : Basis ι R M
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
v : Basis ι' R M
i : ι'
⊢ ((toLin v e) (e.toMatrix ⇑v)) (v i) = LinearMap.id (v i)

Tactic:
by cases nonempty_fintype ι; rw [toLin_self, id_apply, e.sum_toMatrix_smul_self]

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

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ ((b₁.repr x).sum fun i xi ↦ (b₂.repr y).sum fun j yj ↦ ρ₁₂ xi • σ₁₂ yj • (B (b₁ i)) (b₂ j)) = (B x) y

Tactic:
conv_rhs => rw [← b₁.linearCombination_repr x, ← b₂.linearCombination_repr y]

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ ((b₁.repr x).sum fun i xi ↦ (b₂.repr y).sum fun j yj ↦ ρ₁₂ xi • σ₁₂ yj • (B (b₁ i)) (b₂ j)) =
    (B ((Finsupp.linearCombination R ⇑b₁) (b₁.repr x))) ((Finsupp.linearCombination S ⇑b₂) (b₂.repr y))
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

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

Tactic:
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.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 κ
j : κ
F' : Finset κ
hF2 : j ∉ F'
h3 : (∀ k ∈ F', g k ∈ A (i k)) → ∏ k ∈ F', g k ∈ A (∑ k ∈ F', i k)
hF : ∀ k ∈ insert j F', g k ∈ A (i k)
⊢ ∏ k ∈ insert j F', g k ∈ A (∑ k ∈ insert j F', i k)

Tactic:
rw [Finset.prod_insert hF2, Finset.sum_insert hF2]

Goal state after:
ι : 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 κ
j : κ
F' : Finset κ
hF2 : j ∉ F'
h3 : (∀ k ∈ F', g k ∈ A (i k)) → ∏ k ∈ F', g k ∈ A (∑ k ∈ F', i k)
hF : ∀ k ∈ insert j F', g k ∈ A (i k)
⊢ g j * ∏ x ∈ F', g x ∈ A (i j + ∑ x ∈ F', i x)
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x y z : Rᵐᵒᵖ
⊢ associator x y z = -op (associator (unop z) (unop y) (unop x))

Tactic:
simp only [associator_apply, ← unop_mul, ← unop_sub, op_unop, neg_sub]

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

Goal state before:
pp: case «1»
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
⊢ P (diag2n hij c hc)

Tactic:
· obtain rfl : j = 0 := by fin_cases j <;> tauto
    rw [show diag2n hij c hc = diag2 c⁻¹ (inv_ne_zero hc) by
      ext; simp [diag2n_coe, diagonal_apply]; grind, diag2_decompose c⁻¹ (inv_ne_zero hc)]
    refine hmul _ _ (hmul _ _ (hmul _ _ (hmul _ _ (hmul _ _ ?_ ?_) ?_) ?_) ?_) ?_
    all_goals exact htransvec _ _ _ _

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
xi : ι
xv : A xi
yi : ι
yv : A yi
⊢ (f (xi + yi)) (GradedMonoid.GMul.mul xv yv) = (f xi) xv * (f yi) yv

Tactic:
exact hmul _ _

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), ↥(𝒜 i)
right_inv : (coeAlgHom 𝒜).comp decompose = AlgHom.id R A
left_inv : ∀ (i : ι) (x : ↥(𝒜 i)), decompose ↑x = (of (fun i ↦ ↥(𝒜 i)) i) x
⊢ decompose.comp (coeAlgHom 𝒜) = AlgHom.id R (⨁ (i : ι), ↥(𝒜 i))

Tactic:
ext i x : 2

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), ↥(𝒜 i)
right_inv : (coeAlgHom 𝒜).comp decompose = AlgHom.id R A
left_inv : ∀ (i : ι) (x : ↥(𝒜 i)), decompose ↑x = (of (fun i ↦ ↥(𝒜 i)) i) x
i : ι
x : ↥(𝒜 i)
⊢ ((decompose.comp (coeAlgHom 𝒜)).toLinearMap ∘ₗ lof R ι (fun i ↦ ↥(𝒜 i)) i) x =
    ((AlgHom.id R (⨁ (i : ι), ↥(𝒜 i))).toLinearMap ∘ₗ lof R ι (fun i ↦ ↥(𝒜 i)) i) x