mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ ((((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

Tactic:
dsimp

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) ≫
            (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
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
inst✝ : F.CommShift A
this : G.CommShift A := adj.rightAdjointCommShift A
a : A
X : C
⊢ ((Functor.commShiftIso (𝟭 C) a).hom ≫ Functor.whiskerRight adj.unit (shiftFunctor C a)).app X =
    ((shiftFunctor C a).whiskerLeft adj.unit ≫ (Functor.commShiftIso (F ⋙ G) a).hom).app X

Tactic:
dsimp

Goal state after:
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
inst✝ : F.CommShift A
this : G.CommShift A := adj.rightAdjointCommShift A
a : A
X : C
⊢ (Functor.commShiftIso (𝟭 C) a).hom.app X ≫ (shiftFunctor C a).map (adj.unit.app X) =
    adj.unit.app ((shiftFunctor C a).obj X) ≫ (Functor.commShiftIso (F ⋙ G) a).hom.app X
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₂
⊢ (Triangle.mk (Opposite.unop T₁).mor₂.op (Opposite.unop T₁).mor₁.op
          ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₁).obj₁) ≫
            (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₁).mor₃.op)).mor₃ ≫
      (shiftFunctor Cᵒᵖ 1).map φ.unop.hom₃.op =
    φ.unop.hom₁.op ≫
      (Triangle.mk (Opposite.unop T₂).mor₂.op (Opposite.unop T₂).mor₁.op
          ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₂).obj₁) ≫
            (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₂).mor₃.op)).mor₃

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : (Triangle C)ᵒᵖ
φ : T₁ ⟶ T₂
⊢ ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₁).obj₁) ≫
        (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₁).mor₃.op) ≫
      (shiftFunctor Cᵒᵖ 1).map φ.unop.hom₃.op =
    φ.unop.hom₁.op ≫
      (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₂).obj₁) ≫
        (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₂).mor₃.op
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₂
⊢ ((Triangle.mk T₂.mor₂.unop T₂.mor₁.unop
            (((opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁).unop ≫
              (shiftFunctor C 1).map T₂.mor₃.unop)).mor₃ ≫
        (shiftFunctor C 1).map φ.hom₃.unop).op =
    (φ.hom₁.unop ≫
        (Triangle.mk T₁.mor₂.unop T₁.mor₁.unop
            (((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫
              (shiftFunctor C 1).map T₁.mor₃.unop)).mor₃).op

Tactic:
dsimp

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 φ.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 ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁) ≫ φ.hom₁
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : Cᵒᵖ
⊢ IsZero ((triangleOpEquivalence C).functor.obj (Opposite.op (contractibleTriangle (Opposite.unop X)).invRotate)).obj₃

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : Cᵒᵖ
⊢ IsZero (Opposite.op ((shiftFunctor C (-1)).obj 0))
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
inst✝ : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
X : C
⊢ ((Functor.commShiftIso (𝟭 C) a).hom ≫ Functor.whiskerRight adj.unit (shiftFunctor C a)).app X =
    ((shiftFunctor C a).whiskerLeft adj.unit ≫ (Functor.commShiftIso (F ⋙ G) a).hom).app X

Tactic:
dsimp

Goal state after:
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
inst✝ : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
X : C
⊢ (Functor.commShiftIso (𝟭 C) a).hom.app X ≫ (shiftFunctor C a).map (adj.unit.app X) =
    adj.unit.app ((shiftFunctor C a).obj X) ≫ (Functor.commShiftIso (F ⋙ G) a).hom.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
E : C ≌ D
A : Type u_3
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift C A
inst✝⁸ : HasShift D A
inst✝⁷ : E.functor.CommShift A
inst✝⁶ : E.inverse.CommShift A
F : Type u_4
inst✝⁵ : Category.{v_3, u_4} F
inst✝⁴ : HasShift F A
E' : D ≌ F
inst✝³ : E.CommShift A
inst✝² : E'.functor.CommShift A
inst✝¹ : E'.inverse.CommShift A
inst✝ : E'.CommShift A
⊢ (E.trans E').functor.CommShift A

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
E : C ≌ D
A : Type u_3
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift C A
inst✝⁸ : HasShift D A
inst✝⁷ : E.functor.CommShift A
inst✝⁶ : E.inverse.CommShift A
F : Type u_4
inst✝⁵ : Category.{v_3, u_4} F
inst✝⁴ : HasShift F A
E' : D ≌ F
inst✝³ : E.CommShift A
inst✝² : E'.functor.CommShift A
inst✝¹ : E'.inverse.CommShift A
inst✝ : E'.CommShift A
⊢ (E.functor ⋙ E'.functor).CommShift A
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
E : C ≌ D
A : Type u_3
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift C A
inst✝⁸ : HasShift D A
inst✝⁷ : E.functor.CommShift A
inst✝⁶ : E.inverse.CommShift A
F : Type u_4
inst✝⁵ : Category.{v_3, u_4} F
inst✝⁴ : HasShift F A
E' : D ≌ F
inst✝³ : E.CommShift A
inst✝² : E'.functor.CommShift A
inst✝¹ : E'.inverse.CommShift A
inst✝ : E'.CommShift A
⊢ (E.trans E').inverse.CommShift A

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
E : C ≌ D
A : Type u_3
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift C A
inst✝⁸ : HasShift D A
inst✝⁷ : E.functor.CommShift A
inst✝⁶ : E.inverse.CommShift A
F : Type u_4
inst✝⁵ : Category.{v_3, u_4} F
inst✝⁴ : HasShift F A
E' : D ≌ F
inst✝³ : E.CommShift A
inst✝² : E'.functor.CommShift A
inst✝¹ : E'.inverse.CommShift A
inst✝ : E'.CommShift A
⊢ (E'.inverse ⋙ E.inverse).CommShift A
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: 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₃

Tactic:
dsimp

Goal state after:
case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((opShiftFunctorEquivalence C 1).counitIso.inv.app T.obj₃ ≫
        (shiftFunctor Cᵒᵖ 1).map
          (((shiftFunctor C 1).map T.mor₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app T.obj₁)) ≫
      (shiftFunctor Cᵒᵖ 1).map (𝟙 T.obj₁) =
    𝟙 T.obj₃ ≫ T.mor₃
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
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x : ↑(AddCommGrpCat.of (Ext X S.X₁ n))
⊢ (AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯) ≫ AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯)))
      x =
    (AddCommGrpCat.Hom.hom 0) x

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x : ↑(AddCommGrpCat.of (Ext X S.X₁ n))
⊢ (comp x (mk₀ S.f) ⋯).comp (mk₀ S.g) ⋯ = 0
Module: Mathlib.CategoryTheory.Localization.Linear

Goal state before:
pp: case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝¹ : Functor.Linear R (L ⋙ G)
this✝ : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this : r • 𝟙 X = e.inv ≫ (r • 𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
⊢ r • G.map e.inv ≫ 𝟙 ((L ⋙ G).obj (L.objPreimage X)) ≫ G.map e.hom = r • 𝟙 (G.obj X)

Tactic:
dsimp

Goal state after:
case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝¹ : Functor.Linear R (L ⋙ G)
this✝ : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this : r • 𝟙 X = e.inv ≫ (r • 𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
⊢ r • G.map e.inv ≫ 𝟙 (G.obj (L.obj (L.objPreimage X))) ≫ G.map e.hom = r • 𝟙 (G.obj X)
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
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
x : ↑(AddCommGrpCat.of (Ext X S.X₂ n₀))
⊢ (AddCommGrpCat.Hom.hom
        (AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯) ≫ AddCommGrpCat.ofHom (hS.extClass.postcomp X h)))
      x =
    (AddCommGrpCat.Hom.hom 0) x

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
x : ↑(AddCommGrpCat.of (Ext X S.X₂ n₀))
⊢ (comp x (mk₀ S.g) ⋯).comp hS.extClass h = 0
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
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
x : ↑(AddCommGrpCat.of (Ext X S.X₃ n₀))
⊢ (AddCommGrpCat.Hom.hom
        (AddCommGrpCat.ofHom (hS.extClass.postcomp X h) ≫ AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯)))
      x =
    (AddCommGrpCat.Hom.hom 0) x

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
x : ↑(AddCommGrpCat.of (Ext X S.X₃ n₀))
⊢ (comp x hS.extClass h).comp (mk₀ S.f) ⋯ = 0
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
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x₂ : Ext X S.X₂ n
hx₂ : x₂.comp (mk₀ S.g) ⋯ = 0
⊢ ∃ x₁, x₁.comp (mk₀ S.f) ⋯ = x₂

Tactic:
by
  have := covariant_sequence_exact₂' X hS n
  rw [ShortComplex.ab_exact_iff] at this
  exact this x₂ hx₂

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 : ℕ
x✝ : ↑(AddCommGrpCat.of (Ext S.X₃ Y n))
⊢ (AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯) ≫ AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯)))
      x✝ =
    (AddCommGrpCat.Hom.hom 0) x✝

Tactic:
dsimp

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 : ℕ
x✝ : ↑(AddCommGrpCat.of (Ext S.X₃ Y n))
⊢ (mk₀ S.f).comp ((mk₀ S.g).comp x✝ ⋯) ⋯ = 0
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₁
x✝ : ↑(AddCommGrpCat.of (Ext S.X₂ Y n₀))
⊢ (AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯) ≫ AddCommGrpCat.ofHom (hS.extClass.precomp Y h)))
      x✝ =
    (AddCommGrpCat.Hom.hom 0) x✝

Tactic:
dsimp

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₁
x✝ : ↑(AddCommGrpCat.of (Ext S.X₂ Y n₀))
⊢ hS.extClass.comp ((mk₀ S.f).comp x✝ ⋯) h = 0
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
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
this : f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient
⊢ f = f'

Tactic:
ext x
    obtain ⟨y, rfl⟩ := h.bijective.2 x
    exact DFunLike.congr_fun this y

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₁
x✝ : ↑(AddCommGrpCat.of (Ext S.X₁ Y n₀))
⊢ (AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (hS.extClass.precomp Y h) ≫ AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯)))
      x✝ =
    (AddCommGrpCat.Hom.hom 0) x✝

Tactic:
dsimp

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₁
x✝ : ↑(AddCommGrpCat.of (Ext S.X₁ Y n₀))
⊢ (mk₀ S.g).comp (hS.extClass.comp x✝ h) ⋯ = 0
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : g.Monic
⊢ (f %ₘ g).degree < g.degree

Tactic:
exact degree_modByMonic_lt _ hg

Goal state after:
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
h2 : ∀ (j : n), 0 < ∑ i, A i j
⊢ A.det ≠ 0

Tactic:
cases isEmpty_or_nonempty n
  · simp
  · contrapose! h2
    obtain ⟨v, ⟨h_vnz, h_vA⟩⟩ := Matrix.exists_vecMul_eq_zero_iff.mpr h2
    wlog h_sup : 0 < Finset.sup' Finset.univ Finset.univ_nonempty v
    · refine this h1 inferInstance h2 (-1 • v) (by simp [*]) ?_ ?_
      · rw [Matrix.smul_vecMul, h_vA, smul_zero]
      · obtain ⟨i, hi⟩ := Function.ne_iff.mp h_vnz
        simp_rw [Finset.lt_sup'_iff, Finset.mem_univ, true_and] at h_sup ⊢
        simp_rw [not_exists, not_lt] at h_sup
        refine ⟨i, ?_⟩
        rw [Pi.smul_apply, neg_smul, one_smul, Left.neg_pos_iff]
        exact Ne.lt_of_le hi (h_sup i)
    · obtain ⟨j₀, -, h_j₀⟩ := Finset.exists_mem_eq_sup' Finset.univ_nonempty v
      refine ⟨j₀, ?_⟩
      rw [← mul_le_mul_iff_right₀ (h_j₀ ▸ h_sup), Finset.mul_sum, mul_zero]
      rw [show 0 = ∑ i, v i * A i j₀ from (congrFun h_vA j₀).symm]
      refine Finset.sum_le_sum (fun i hi => ?_)
      by_cases h : i = j₀
      · rw [h]
      · exact (mul_le_mul_right_of_neg (h1 h)).mpr (h_j₀ ▸ Finset.le_sup' v hi)

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
A : SpecialLinearGroup n R
⊢ (↑A).det ^ (Fintype.card n - 1) = 1

Tactic:
A.prop,

Goal state after:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ 1 ^ (Fintype.card n - 1) = 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A B : SpecialLinearGroup n R
⊢ (↑A).det * (↑B).det = 1

Tactic:
A.prop,

Goal state after:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A B : SpecialLinearGroup n R
⊢ 1 * (↑B).det = 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
i : n
A B : ↥(center (SpecialLinearGroup n R))
⊢ rootsOfUnity.mkOfPowEq (↑↑(A * B) i i) ⋯ = rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯ * rootsOfUnity.mkOfPowEq (↑↑B i i) ⋯

Tactic:
dsimp

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
i : n
A B : ↥(center (SpecialLinearGroup n R))
⊢ rootsOfUnity.mkOfPowEq ((↑↑A * ↑↑B) i i) ⋯ = rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯ * rootsOfUnity.mkOfPowEq (↑↑B i i) ⋯
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Fact (Even (Fintype.card n))
g : SpecialLinearGroup n R
⊢ (-↑g).det = 1

Tactic:
by
    simpa [(@Fact.out <| Even <| Fintype.card n).neg_one_pow, g.det_coe]
      using det_smul (↑ₘg) (-1)

Goal state after:
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 • Pi.single j 1 = Pi.single j 1 + b • Pi.single i 1

Tactic:
by
  simp [SpecialLinearGroup.smul_def, transvection_coe, -mulVec_single,
    add_mulVec, single_mulVec_eq]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), f m * f m = (algebraMap R A) (Q m) }
x : M
⊢ ↑((fun F ↦ ⟨F.toLinearMap ∘ₗ ι Q, ⋯⟩) ((fun f ↦ (ringCon Q).liftₐ ((TensorAlgebra.lift R) ↑f) ⋯) f)) x = ↑f x

Tactic:
dsimp

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), f m * f m = (algebraMap R A) (Q m) }
x : M
⊢ ((ringCon Q).liftₐ ((TensorAlgebra.lift R) ↑f) ⋯) ((ι Q) x) = ↑f x
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : CliffordAlgebra Q →ₐ[R] A
x : M
⊢ ((((fun f ↦ (ringCon Q).liftₐ ((TensorAlgebra.lift R) ↑f) ⋯) ((fun F ↦ ⟨F.toLinearMap ∘ₗ ι Q, ⋯⟩) F)).comp
            (RingCon.mkₐ R (ringCon Q))).toLinearMap ∘ₗ
        TensorAlgebra.ι R)
      x =
    ((F.comp (RingCon.mkₐ R (ringCon Q))).toLinearMap ∘ₗ TensorAlgebra.ι R) x

Tactic:
dsimp

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : CliffordAlgebra Q →ₐ[R] A
x : M
⊢ ((ringCon Q).liftₐ ((TensorAlgebra.lift R) (F.toLinearMap ∘ₗ ι Q)) ⋯)
      ((RingCon.mkₐ R (ringCon Q)) ((TensorAlgebra.ι R) x)) =
    F ((RingCon.mkₐ R (ringCon Q)) ((TensorAlgebra.ι R) x))
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 : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
⊢ i2 ∈ ↑{i | i ≠ i₀} → i1 ≠ i2 → Function.onFun Commute (fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1) i1 i2

Tactic:
hi2

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
⊢ i1 ≠ i2 → Function.onFun Commute (fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1) i1 i2