mathlib-initiative/mathlib-tactics huggingface dataset:
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'
⊢ QuasiIsoAt (K.πTruncGE e) j'

Tactic:
rw [quasiIsoAt_iff]
  by_cases hj : e.BoundaryGE j
  · rw [(truncGE.rightHomologyMapData K e hj' rfl rfl hj).quasiIso_iff]
    dsimp
    infer_instance
  · let φ := (shortComplexFunctor C c' j').map (K.πTruncGE e)
    have : Epi φ.τ₁ := by
      by_cases hi : ∃ i, e.f i = c'.prev j'
      · obtain ⟨i, hi⟩ := hi
        dsimp [φ, πTruncGE]
        rw [e.epi_liftExtend_f_iff _ _ hi]
        infer_instance
      · apply IsZero.epi (isZero_extend_X _ _ _ (by simpa using hi))
    have : IsIso φ.τ₂ := by
      dsimp [φ, πTruncGE]
      rw [e.isIso_liftExtend_f_iff _ _ hj']
      exact K.isIso_restrictionToTruncGE' e j hj
    have : IsIso φ.τ₃ := by
      dsimp [φ, πTruncGE]
      have : c'.next j' = e.f (c.next j) := by simpa only [← hj'] using e.next_f rfl
      rw [e.isIso_liftExtend_f_iff _ _ this.symm]
      exact K.isIso_restrictionToTruncGE' e _ (e.not_boundaryGE_next' hj rfl)
    exact ShortComplex.quasiIso_of_epi_of_isIso_of_mono φ

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'
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : HasZeroObject C
hK : K.Acyclic
e : c.Embedding c'
inst✝ : e.IsTruncGE
⊢ (K.truncGE e).Acyclic

Tactic:
by
  rw [acyclic_truncGE_iff_isSupportedOutside]
  exact ⟨fun _ ↦ hK _⟩

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
hi : ∃ j', c'.Rel (e.f i) j'
⊢ IsZero ((K.shortComplexTruncLE e).X₃.homology (e.f i))

Tactic:
obtain ⟨j', hj'⟩ := hi

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ IsZero ((K.shortComplexTruncLE e).X₃.homology (e.f i))
Module: Mathlib.CategoryTheory.Localization.HomEquiv

Goal state before:
pp: C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{v_2, u_2} C₁
inst✝⁴ : Category.{v_3, u_3} C₂
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X : C₁
⊢ Φ.homMap L₁ L₂ (𝟙 (L₁.obj X)) = 𝟙 (L₂.obj (Φ.functor.obj X))

Tactic:
by
  simpa using Φ.homMap_map L₁ L₂ (𝟙 X)

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

Goal state before:
pp: C₁ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁶ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
D₁ : Type u₃
inst✝⁵ : Category.{v₃, u₃} D₁
D₂ : Type u₄
inst✝⁴ : Category.{v₄, u₄} D₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝² : L₂.IsLocalization W₂
X Y : C₁
inst✝¹ : HasSmallLocalizedHom W₁ X Y
inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
g : W₁.Q.obj X ⟶ W₁.Q.obj Y
G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
β : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso Φ.functor W₁.Q W₂.Q G'
E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor
α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor
α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
⊢ (SmallHom.equiv W₂ L₂)
      ((SmallHom.equiv W₂ W₂.Q).symm
        ((((CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).symm.app X).homCongr
            ((CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).symm.app Y))
          ((Φ.localizedFunctor W₁.Q W₂.Q).map g))) =
    e.hom.app X ≫ G.map (α₁.inv.app X ≫ E₁.map g ≫ α₁.hom.app Y) ≫ e.inv.app Y

Tactic:
SmallHom.equiv_equiv_symm W₂ W₂.Q L₂ E₂ α₂

Goal state after:
C₁ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁶ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
D₁ : Type u₃
inst✝⁵ : Category.{v₃, u₃} D₁
D₂ : Type u₄
inst✝⁴ : Category.{v₄, u₄} D₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝² : L₂.IsLocalization W₂
X Y : C₁
inst✝¹ : HasSmallLocalizedHom W₁ X Y
inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
g : W₁.Q.obj X ⟶ W₁.Q.obj Y
G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
β : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso Φ.functor W₁.Q W₂.Q G'
E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor
α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor
α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
⊢ α₂.inv.app (Φ.functor.obj X) ≫
      E₂.map
          ((((CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).symm.app X).homCongr
              ((CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).symm.app Y))
            ((Φ.localizedFunctor W₁.Q W₂.Q).map g)) ≫
        α₂.hom.app (Φ.functor.obj Y) =
    e.hom.app X ≫ G.map (α₁.inv.app X ≫ E₁.map g ≫ α₁.hom.app Y) ≫ e.inv.app Y
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
n : ℕ
α : Ext Z T n
⊢ (mk₀ f).comp ((mk₀ g).comp α ⋯) ⋯ = (mk₀ (f ≫ g)).comp α ⋯

Tactic:
← mk₀_comp_mk₀,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
n : ℕ
α : Ext Z T n
⊢ (mk₀ f).comp ((mk₀ g).comp α ⋯) ⋯ = ((mk₀ f).comp (mk₀ g) ⋯).comp α ⋯
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
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
h₁ : (mk₀ biprod.inl).comp α ⋯ = (mk₀ biprod.inl).comp β ⋯
h₂ : (mk₀ biprod.inr).comp α ⋯ = (mk₀ biprod.inr).comp β ⋯
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α = β

Tactic:
rw [Ext.ext_iff] at h₁ h₂ ⊢

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₂ : ((mk₀ biprod.inr).comp α ⋯).hom = ((mk₀ biprod.inr).comp β ⋯).hom
h₁ : ((mk₀ biprod.inl).comp α ⋯).hom = ((mk₀ biprod.inl).comp β ⋯).hom
⊢ α.hom = β.hom
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n k : ℕ
h : k + 3 ≤ n
R₁ R₂ : ComposableArrows C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ k₁ k₂ k₃ : ℕ
hk₀ : k₀ = k
hk₁ : k₁ = k + 1
hk₂ : k₂ = k + 2
hk₃ : k₃ = k + 3
h₀ : Epi (app' φ k₀ ⋯)
h₁ : Mono (app' φ k₁ ⋯)
h₃ : Mono (app' φ k₃ ⋯)
⊢ Mono (app' φ k₂ ⋯)

Tactic:
by
  subst_vars
  change Epi (app' φ (k₀ + 0)) at h₀
  rw [← natAddLEFunctor_app' h] at h₀ h₁ h₃ ⊢
  exact mono_of_epi_of_mono_of_mono _ (natAddLEFunctor_obj_exact h hR₁)
    (natAddLEFunctor_obj_exact h hR₂) h₀ h₁ h₃

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w :
  a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧
    a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ ((↑(fst S.f)).v n₀ n₁ h ≫ S.f.f n₁ + (snd S.f).v n₀ n₀ ⋯ ≫ S.X₂.d n₀ n₁) +
        b ≫ S.X₂.d n₀ n₁ =
      0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h

Tactic:
comp_add,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w :
  a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧
    a ≫
          ((inl S.f).v n₁ n₀ ⋯ ≫ (↑(fst S.f)).v n₀ n₁ h ≫ S.f.f n₁ +
            (inl S.f).v n₁ n₀ ⋯ ≫ (snd S.f).v n₀ n₀ ⋯ ≫ S.X₂.d n₀ n₁) +
        b ≫ S.X₂.d n₀ n₁ =
      0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
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ᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₃ b₃ ⋯).hom.app X ≫
      (shiftFunctorAdd' (OppositeShift C ℤ) b₁ b₂ b₃ ⋯).hom.app X ≫
        (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₂ b₂ ⋯).inv.app
            ((shiftFunctor (OppositeShift C ℤ) b₁).obj X) ≫
          (shiftFunctor (PullbackShift (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯)) a₂).map
            ((pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₁ b₁ ⋯).inv.app X) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).1 (Opposite.unop X))) ≫
          (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).inv.app X)

Tactic:
oppositeShiftFunctorAdd'_hom_app

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₃ b₃ ⋯).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₂ b₂ ⋯).inv.app
            ((shiftFunctor (OppositeShift C ℤ) b₁).obj X) ≫
          (shiftFunctor (PullbackShift (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯)) a₂).map
            ((pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₁ b₁ ⋯).inv.app X) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).1 (Opposite.unop X))) ≫
          (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).inv.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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift C A
inst✝⁸ : HasShift D A
inst✝⁷ : F.CommShift A
inst✝⁶ : G.CommShift A
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
F' : D ⥤ E
G' : E ⥤ D
adj' : F' ⊣ G'
inst✝⁴ : HasShift E A
inst✝³ : F'.CommShift A
inst✝² : G'.CommShift A
inst✝¹ : adj.CommShift A
inst✝ : adj'.CommShift A
⊢ NatTrans.CommShift (adj.comp adj').counit A

Tactic:
by
    rw [comp_counit]
    infer_instance

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
inst✝² : HasDerivedCategory C
I : C
inst✝¹ : Injective I
K : CochainComplex C ℤ
i n : ℤ
hn : i < n
inst✝ : K.IsStrictlyGE n
L : CochainComplex C ℤ
w✝ : L.IsStrictlyGE i
g : K ⟶ L
ι : (CochainComplex.singleFunctor C i).obj I ⟶ L
h : IsIso (Q.map ι)
hπ : IsSplitMono ι
⊢ 𝟙 (Q.obj ((CochainComplex.singleFunctor C i).obj I)) = Q.map (ι ≫ retraction ι)

Tactic:
IsSplitMono.id,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
I : C
inst✝¹ : Injective I
K : CochainComplex C ℤ
i n : ℤ
hn : i < n
inst✝ : K.IsStrictlyGE n
L : CochainComplex C ℤ
w✝ : L.IsStrictlyGE i
g : K ⟶ L
ι : (CochainComplex.singleFunctor C i).obj I ⟶ L
h : IsIso (Q.map ι)
hπ : IsSplitMono ι
⊢ 𝟙 (Q.obj ((CochainComplex.singleFunctor C i).obj I)) = Q.map (𝟙 ((CochainComplex.singleFunctor C i).obj I))
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: case mpr
K : Type u_7
V : Type u_9
V₂ : Type u_11
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (B x) y = 0 → ∀ (n : V), (∃ a, a • x = n) → (B n) y = 0

Tactic:
rintro h _ ⟨z, rfl⟩
    rw [map_smulₛₗ₂, smul_eq_zero]
    exact Or.intro_right _ h

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₁
⊢ AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯) ≫ AddCommGrpCat.ofHom (hS.extClass.precomp Y h) = 0

Tactic:
by
        ext
        dsimp
        simp only [ShortComplex.ShortExact.extClass_comp_assoc]

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
hA : A ∈ center (SpecialLinearGroup n R)
i : n
r : R
hr : (scalar n) r = ↑A
⊢ (scalar n) (↑A i i) = ↑A

Tactic:
simp [← congr_fun₂ hr i i, ← hr]

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:
rw [transvection_coe]
  simp [-mulVec_single, add_mulVec, single_mulVec_eq]

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 * transvection hij (-b)) = ↑1

Tactic:
by
  simp [transvection_coe, mul_add, add_mul,
    single_mul_single_of_ne _ _ _ _ hij.symm, ← single_neg]

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
g : CliffordAlgebra Q →ₐ[R] A
⊢ (lift Q) ⟨g.toLinearMap ∘ₗ ι Q, ⋯⟩ = g

Tactic:
exact (lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).apply_symm_apply g

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ Q (-x) = Q x

Tactic:
by
  rw [← @neg_one_smul R _ _ _ _ x, Q.map_smul, neg_one_mul, neg_neg, one_smul]

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

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a b : A
b_mem : b ∈ 𝒜 j
⊢ ↑(((decompose 𝒜) (a * b)) (i + j)) = ↑(((decompose 𝒜) a) i) * b

Tactic:
lift b to 𝒜 j using b_mem
  rw [decompose_mul, decompose_coe, coe_mul_of_apply_add]

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

Goal state before:
pp: case refine_2.refine_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
m✝ m'✝ : A
⊢ ↑(((decompose 𝒜) (↑⟨c, hc⟩ * m✝)) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) m✝) 0) →
    ↑(((decompose 𝒜) (↑⟨c, hc⟩ * m'✝)) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) m'✝) 0) →
      ↑(((decompose 𝒜) (↑⟨c, hc⟩ * (m✝ + m'✝))) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) (m✝ + m'✝)) 0)

Tactic:
hd

Goal state after:
case refine_2.refine_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
m✝ m'✝ : A
hd : ↑(((decompose 𝒜) (↑⟨c, hc⟩ * m✝)) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) m✝) 0)
⊢ ↑(((decompose 𝒜) (↑⟨c, hc⟩ * m'✝)) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) m'✝) 0) →
    ↑(((decompose 𝒜) (↑⟨c, hc⟩ * (m✝ + m'✝))) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) (m✝ + m'✝)) 0)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommRing R
inst✝⁷ : DecidableEq m
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
M : Matrix m n R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ ((toLinearMap₂' R) M).SeparatingLeft ↔ M.SeparatingLeft

Tactic:
separatingLeft_toLinearMap₂'_iff

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommRing R
inst✝⁷ : DecidableEq m
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
M : Matrix m n R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ M.SeparatingLeft ↔ M.SeparatingLeft
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommRing R
inst✝⁷ : DecidableEq m
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
M : Matrix m n R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ ((toLinearMap₂' R) M).SeparatingRight ↔ M.SeparatingRight

Tactic:
separatingRight_toLinearMap₂'_iff

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommRing R
inst✝⁷ : DecidableEq m
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
M : Matrix m n R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ M.SeparatingRight ↔ M.SeparatingRight
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:
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
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case succ.inl
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hd : finrank K V = d + 1
hB₂ : IsSymm 0
b : Basis (Fin (finrank K V)) K V := finBasis K V
⊢ ∃ v, IsOrthoᵢ 0 ⇑v

Tactic:
hd

Goal state after:
case succ.inl
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hd : finrank K V = d + 1
hB₂ : IsSymm 0
b : Basis (Fin (d + 1)) K V
⊢ ∃ v, IsOrthoᵢ 0 ⇑v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
l : List M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldr Q f hf) n) (List.map (⇑(ι Q)) l).prod = List.foldr (fun m n ↦ (f m) n) n l

Tactic:
induction l with
  | nil => rw [List.map_nil, List.prod_nil, List.foldr_nil, foldr_one]
  | cons hd tl ih => rw [List.map_cons, List.prod_cons, List.foldr_cons, foldr_mul, foldr_ι, ih]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
l : List M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldr Q f hf) n) (reverse (List.map (⇑(ι Q)) l).prod) = List.foldl (fun m n ↦ (f n) m) n l

Tactic:
reverse_prod_map_ι,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
l : List M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldr Q f hf) n) (List.map (⇑(ι Q)) l).reverse.prod = List.foldl (fun m n ↦ (f n) m) n l
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ (DirectSum.coeAlgHom (evenOdd Q)).comp ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) = AlgHom.id R (CliffordAlgebra Q)

Tactic:
by
      ext m
      dsimp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply, AlgHom.comp_apply,
        AlgHom.id_apply]
      rw [lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.coeAlgHom_of, Subtype.coe_mk]

Goal state after: