mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj' : ¬∃ j, e.f j = j'
⊢ ((K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

Tactic:
apply (L.isZero_extend_X e j' (by simpa using hj')).eq_of_tgt

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ i, e.f i = i'
this : (L.extend e).d i' j' = 0
hj' : ¬∃ j, e.f j = j'
⊢ f φ j' = 0

Tactic:
apply (L.isZero_extend_X e j' (by simpa using hj')).eq_of_tgt

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L L' : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
β : L ⟶ L'
i : ι
⊢ (e.homRestrict (ψ ≫ extendMap β e)).f i = (e.homRestrict ψ ≫ β).f i

Tactic:
simp [homRestrict_f _ _ rfl, extendMap_f β e rfl]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
⊢ Epi φ.τ₁

Tactic:
by_cases hi : ∃ i, e.f i = c'.prev j'

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✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
hi : ∃ i, e.f i = c'.prev j'
⊢ Epi φ.τ₁

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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
hi : ¬∃ i, e.f i = c'.prev j'
⊢ Epi φ.τ₁
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
this✝¹ : Epi φ.τ₁
this✝ : IsIso φ.τ₂
this : c'.next j' = e.f (c.next j)
⊢ IsIso ((e.liftExtend (K.restrictionToTruncGE' e) ⋯).f (c'.next j'))

Tactic:
e.isIso_liftExtend_f_iff _ _ this.symm

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
this✝¹ : Epi φ.τ₁
this✝ : IsIso φ.τ₂
this : c'.next j' = e.f (c.next j)
⊢ IsIso ((K.restrictionToTruncGE' e).f (c.next 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 L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncGE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : K.IsStrictlySupported e
i : ι
hi : ¬e.BoundaryGE i
⊢ IsIso ((K.restrictionToTruncGE' e).f i)

Tactic:
rw [K.restrictionToTruncGE'_f_eq_iso_hom_iso_inv e rfl hi]
    infer_instance

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
⊢ QuasiIso (K.πTruncGE e) ↔ K.IsSupported e

Tactic:
by
  constructor
  · intro
    refine ⟨fun i' hi' => ?_⟩
    rw [exactAt_iff_of_quasiIsoAt (K.πTruncGE e) i']
    exact (K.truncGE e).exactAt_of_isSupported e i' hi'
  · intro
    rw [quasiIso_iff]
    intro i'
    by_cases hi' : ∃ i, e.f i = i'
    · obtain ⟨i, rfl⟩ := hi'
      infer_instance
    · 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.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ : ι₁
h₁ : c.Rel (e₁.f i₁) (c.next (e₁.f i₁))
h₂ : ∀ (k : ι₁), ¬c.Rel (e₁.f i₁) (e₁.f k)
⊢ ∃ i₂, ac.Boundary i₁ i₂

Tactic:
obtain ⟨i₂, hi₂⟩ := ac.exists_i₂ (c.next (e₁.f i₁))
    (fun i₁' hi₁' => h₂ i₁' (by simpa only [← hi₁'] using! h₁))

Goal state after:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ : ι₁
h₁ : c.Rel (e₁.f i₁) (c.next (e₁.f i₁))
h₂ : ∀ (k : ι₁), ¬c.Rel (e₁.f i₁) (e₁.f k)
i₂ : ι₂
hi₂ : c.next (e₁.f i₁) = e₂.f i₂
⊢ ∃ i₂, ac.Boundary i₁ i₂
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
⊢ HasSmallLocalizedShiftedHom W M X Y ↔
    ∀ (a b : M), Small.{w, v₂} ((shiftFunctor D a).obj (L.obj X) ⟶ (shiftFunctor D b).obj (L.obj Y))

Tactic:
dsimp [HasSmallLocalizedShiftedHom]
  have eq := fun (a b : M) ↦ small_congr.{w}
    (Iso.homCongr ((L.commShiftIso a).app X) ((L.commShiftIso b).app Y))
  dsimp at eq
  simp only [hasSmallLocalizedHom_iff _ L, eq]

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

Goal state before:
pp: 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
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
i : ι
⊢ IsIso (homologyMap φ.τ₃ i)

Tactic:
apply isIso_homologyMap_τ₃ φ hS₁ hS₂

Goal state after:
case h₁
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
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
i : ι
⊢ Epi (homologyMap φ.τ₁ i)

case h₂
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
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
i : ι
⊢ IsIso (homologyMap φ.τ₂ i)

case h₃
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
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
i : ι
⊢ ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)

case h₄
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
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
i : ι
⊢ ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Q.map (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ Q.map ((shiftFunctor (CochainComplex C ℤ) 1).map f.τ₁) =
    Q.map (CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯) ≫ Q.map (CochainComplex.mappingCone.triangle S₂.f).mor₃

Tactic:
rw [← Q.map_comp, ← Q.map_comp]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Q.map ((CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1).map f.τ₁) =
    Q.map (CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ (CochainComplex.mappingCone.triangle S₂.f).mor₃)
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : (OppositeShift.functor A F).CommShift A
a b : A
x✝ : C
⊢ (NatIso.removeOp
            (CommShift.isoAdd (commShiftIso (OppositeShift.functor A F) a)
                (commShiftIso (OppositeShift.functor A F) b)).symm).hom.app
      x✝ =
    (CommShift.isoAdd (NatIso.removeOp (commShiftIso (OppositeShift.functor A F) a).symm)
            (NatIso.removeOp (commShiftIso (OppositeShift.functor A F) b).symm)).hom.app
      x✝

Tactic:
simp only [NatIso.removeOp_hom, Iso.symm_hom, NatTrans.removeOp_app,
      CommShift.isoAdd_inv_app, unop_comp, Category.assoc,
      CommShift.isoAdd_hom_app]

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : (OppositeShift.functor A F).CommShift A
a b : A
x✝ : C
⊢ ((OppositeShift.functor A F).map ((shiftFunctorAdd Cᵒᵖ a b).inv.app (Opposite.op x✝))).unop ≫
      ((commShiftIso (OppositeShift.functor A F) b).inv.app ((shiftFunctor Cᵒᵖ a).obj (Opposite.op x✝))).unop ≫
        ((shiftFunctor Dᵒᵖ b).map ((commShiftIso (OppositeShift.functor A F) a).inv.app (Opposite.op x✝))).unop ≫
          ((shiftFunctorAdd Dᵒᵖ a b).hom.app ((OppositeShift.functor A F).obj (Opposite.op x✝))).unop =
    F.map ((shiftFunctorAdd C a b).hom.app x✝) ≫
      ((commShiftIso (OppositeShift.functor A F) b).inv.app (Opposite.op ((shiftFunctor C a).obj x✝))).unop ≫
        (shiftFunctor D b).map ((commShiftIso (OppositeShift.functor A F) a).inv.app (Opposite.op x✝)).unop ≫
          (shiftFunctorAdd D a b).inv.app (F.obj x✝)
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
⊢ φ a₁ + φ a₂ = b₃

Tactic:
h₃,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
⊢ φ a₁ + φ a₂ = φ a₃
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ : A
b₃ : B
h₃ : b₃ = φ (a₁ + a₂)
⊢ b₃ = φ a₁ + φ a₂

Tactic:
h₃,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ : A
b₃ : B
h₃ : b₃ = φ (a₁ + a₂)
⊢ φ (a₁ + a₂) = φ a₁ + φ 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
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₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
x✝ : D
⊢ adj.unit.app ((shiftFunctor C a).obj (G.obj x✝)) ≫
      G.map (e₁.hom.app (G.obj x✝)) ≫ G.map ((shiftFunctor D a).map (adj.counit.app x✝)) =
    e₂'.inv.app x✝

Tactic:
compatibilityUnit_right adj e₁ e₂' h'

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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
x✝ : D
⊢ adj.unit.app ((shiftFunctor C a).obj (G.obj x✝)) ≫
      G.map (e₁.hom.app (G.obj x✝)) ≫ G.map ((shiftFunctor D a).map (adj.counit.app x✝)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj x✝)) ≫
      G.map (e₁.hom.app (G.obj x✝)) ≫ G.map ((shiftFunctor D a).map (adj.counit.app x✝))
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X I : C
n : ℕ
inst✝ : Injective I
e : Ext X I (n + 1)
K : CochainComplex C ℤ := (CochainComplex.singleFunctor C 0).obj X
this✝ : K.IsStrictlyGE (-↑n)
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ homEquiv e ≫ ((singleFunctors C).shiftIso (↑n + 1) (-(↑n + 1)) 0 ⋯).hom.app I = 0

Tactic:
exact to_singleFunctor_obj_eq_zero_of_injective (K := K) (n := -n) _ (by lia)

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
b : Basis ι R M
b' : Basis ι' R M
inst✝¹ : Fintype ι
inst✝ : Finite ι'
m : M
⊢ b'.toMatrix ⇑b *ᵥ ⇑(b.repr m) = ⇑(b'.repr m)

Tactic:
by
  classical
  cases nonempty_fintype ι'
  simp [← LinearMap.toMatrix_id_eq_basis_toMatrix, LinearMap.toMatrix_mulVec_repr]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
ξ : ↥(rootsOfUnity n R)
⊢ (Units.map ↑σ) ↑ξ ∈ rootsOfUnity n S

Tactic:
rw [mem_rootsOfUnity, ← map_pow, Units.ext_iff, Units.coe_map, ξ.prop]
      exact map_one σ

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
⊢ ((↑g)⁻¹ * ↑g).map ⇑f = 1

Tactic:
simp only [isUnits_det_units, nonsing_inv_mul, map_zero, map_one, Matrix.map_one]

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

Goal state before:
pp: case mpr.refine_2.calc_2
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ ((algebraMap A K).mapMatrix M *ᵥ (algebraMap A K) b • v) i = 0

Tactic:
mulVec_smul,

Goal state after:
case mpr.refine_2.calc_2
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ ((algebraMap A K) b • (algebraMap A K).mapMatrix M *ᵥ v) i = 0
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
⊢ 1 * (↑B).det = 1

Tactic:
B.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 * 1 = 1
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_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ (algebraMap R A) (Q (a + b)) - (algebraMap R A) (Q a) - (algebraMap R A) (Q b) =
    (algebraMap R A) (Q (a + b) - Q a - Q b)

Tactic:
by rw [← map_sub, ← map_sub]

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

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ (toMatrix₂' R) (B.compl₁₂ l r) i j = ((toMatrix' l)ᵀ * (toMatrix₂' R) B * toMatrix' r) i j

Tactic:
simp only [LinearMap.toMatrix₂'_apply, LinearMap.compl₁₂_apply, transpose_apply, Matrix.mul_apply,
    LinearMap.toMatrix', LinearEquiv.coe_mk, LinearMap.coe_mk, AddHom.coe_mk, sum_mul]

Goal state after:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ (B (l (Pi.single i 1))) (r (Pi.single j 1)) =
    ∑ x,
      ∑ i_1,
        of (fun i j ↦ l (Pi.single j 1) i) i_1 i * (B (Pi.single i_1 1)) (Pi.single x 1) *
          of (fun i j ↦ r (Pi.single j 1) i) x j
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
σ₁ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
k : n
x✝ : k ∈ univ
hk : k ≠ i
⊢ ∑ x, σ₁ ((Finsupp.single i 1) k) •> (Finsupp.single j 1) x •> M k x = 0

Tactic:
simp [hk]

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
σ₁ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j k : m
x✝ : k ∈ univ
hk : k ≠ j
⊢ σ₁ ((Finsupp.single i 1) i) •> (Finsupp.single j 1) k •> M i k = 0

Tactic:
simp [hk]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i j : ι
hx : x ∈ ℳ i
hij : i ≠ j
⊢ ↑(((decompose ℳ) x) j) = 0

Tactic:
rw [decompose_of_mem _ hx, DirectSum.of_eq_of_ne _ _ _ hij.symm, ZeroMemClass.coe_zero]

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

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
Q : QuadraticMap R M N
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
x y : M
⊢ -(Q x + Q y + (B x) y) = -Q x + -Q y + ((-B) x) y

Tactic:
LinearMap.neg_apply,

Goal state after:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
Q : QuadraticMap R M N
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
x y : M
⊢ -(Q x + Q y + (B x) y) = -Q x + -Q y + -(B x) y
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
f g : M →ₗ[R] R
x✝¹ x✝ : M
⊢ ((associated (linMulLin f g)) x✝¹) x✝ = ((⅟2 • ((mul R R).compl₁₂ f g + (mul R R).compl₁₂ g f)) x✝¹) x✝

Tactic:
simp only [associated_apply, linMulLin_apply, map_add, smul_add, LinearMap.add_apply,
    LinearMap.smul_apply, compl₁₂_apply, mul_apply', smul_eq_mul, invOf_smul_eq_iff]

Goal state after:
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
f g : M →ₗ[R] R
x✝¹ x✝ : M
⊢ (f x✝¹ + f x✝) * (g x✝¹ + g x✝) - f x✝¹ * g x✝¹ - f x✝ * g x✝ = 2 • (⅟2 * (f x✝¹ * g x✝)) + 2 • (⅟2 * (g x✝¹ * f x✝))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' x y : CliffordAlgebra Q
hx : x ∈ ⨆ i, (ι Q).range ^ ↑i
hy : y ∈ ⨆ i, (ι Q).range ^ ↑i
ihx : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨x, hx⟩
ihy : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) y = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨y, hy⟩
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) (x + y) = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨x + y, ⋯⟩

Tactic:
| add x y hx hy ihx ihy =>

Goal state after: