mathlib-initiative/mathlib-tactics huggingface dataset:
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₁ Z₁ : C₁
X₂ Y₂ Z₂ : 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₂
eZ : Φ.functor.obj Z₁ ≅ Z₂
inst✝⁷ : W₁.IsCompatibleWithShift M
inst✝⁶ : W₂.IsCompatibleWithShift M
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst✝² : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst✝¹ : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst✝ : HasSmallLocalizedShiftedHom W₂ M X₂ Z₂
a b c : M
f : SmallShiftedHom W₁ X₁ Y₁ a
g : SmallShiftedHom W₁ Y₁ Z₁ b
h : b + a = c
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
⊢ 0 + b + a = c

Tactic:
simpa

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₁ Z₁ : C₁
X₂ Y₂ Z₂ : 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₂
eZ : Φ.functor.obj Z₁ ≅ Z₂
inst✝⁷ : W₁.IsCompatibleWithShift M
inst✝⁶ : W₂.IsCompatibleWithShift M
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst✝² : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst✝¹ : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst✝ : HasSmallLocalizedShiftedHom W₂ M X₂ Z₂
a b c : M
f : SmallShiftedHom W₁ X₁ Y₁ a
g : SmallShiftedHom W₁ Y₁ Z₁ b
h : b + a = c
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
⊢ b + a + 0 = c

Tactic:
simpa

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₁ Z₁ : C₁
X₂ Y₂ Z₂ : 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₂
eZ : Φ.functor.obj Z₁ ≅ Z₂
inst✝⁷ : W₁.IsCompatibleWithShift M
inst✝⁶ : W₂.IsCompatibleWithShift M
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst✝² : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst✝¹ : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst✝ : HasSmallLocalizedShiftedHom W₂ M X₂ Z₂
a b c : M
f : SmallShiftedHom W₁ X₁ Y₁ a
g : SmallShiftedHom W₁ Y₁ Z₁ b
h : b + a = c
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
⊢ b + 0 + a = c

Tactic:
simpa

Goal state after:
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 : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ triangleOfSES hS ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)

Tactic:
refine Iso.symm (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))) ?_ ?_ ?_)

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₁ ≫
      (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₂).hom =
    (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₁).hom ≫ (triangleOfSES hS).mor₁

case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₂ ≫
      (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom =
    (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₂).hom ≫ (triangleOfSES hS).mor₂

case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map
        (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₁).hom =
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom ≫ (triangleOfSES hS).mor₃
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 : C
n : ℕ
inst✝ : HasDerivedCategory C
α : Ext X Y n
⊢ (-α).hom = -α.hom

Tactic:
by
  rw [← add_right_inj α.hom, ← add_hom, add_neg_cancel, add_neg_cancel, zero_hom]

Goal state after:
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₁ Y₂ : C
n : ℕ
e : Ext X (Y₁ ⊞ Y₂) n
⊢ (fun e ↦ e.1.comp (mk₀ biprod.inl) ⋯ + e.2.comp (mk₀ biprod.inr) ⋯)
      ((fun e ↦ (e.comp (mk₀ biprod.fst) ⋯, e.comp (mk₀ biprod.snd) ⋯)) e) =
    e

Tactic:
by
    simp only [comp_assoc_of_second_deg_zero, mk₀_comp_mk₀, ← comp_add, ← mk₀_add,
      biprod.total, comp_mk₀_id]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
⊢ R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0

Tactic:
by simpa only [map'_comp R₁ 0 1 2] using hR₁.toIsComplex.zero 0

Goal state after:
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₁ e₁' : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁' e₂
x✝ : C
⊢ e₁.hom.app x✝ = e₁'.hom.app x✝

Tactic:
compatibilityCounit_left adj e₁ e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ 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₁ e₁' : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁' e₂
x✝ : C
⊢ F.map ((shiftFunctor C a).map (adj.unit.app x✝)) ≫
      F.map (e₂.inv.app (F.obj x✝)) ≫ adj.counit.app ((shiftFunctor D a).obj (F.obj x✝)) =
    e₁'.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
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
a b : A
⊢ CommShift.CompatibilityUnit adj (Functor.commShiftIso F (a + b)) (Functor.CommShift.isoAdd (iso adj a) (iso adj b))

Tactic:
rw [F.commShiftIso_add]

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
a b : A
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoAdd (Functor.commShiftIso F a) (Functor.commShiftIso F b))
    (Functor.CommShift.isoAdd (iso adj a) (iso adj b))
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
      rw [Functor.map_id, comp_id, id_comp, Functor.map_comp,
        ← opShiftFunctorEquivalence_counitIso_inv_naturality_assoc,
        opShiftFunctorEquivalence_counitIso_inv_app_shift, ← Functor.map_comp,
        Iso.hom_inv_id_app, Functor.map_id]
      simp only [Functor.id_obj, comp_id]

Goal state after:
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
T₁ T₂ : Triangle Cᵒᵖ
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃
hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop
hc₂ :
  (shiftFunctor C 1).map T₂.mor₃.unop ≫ (shiftFunctor C 1).map c =
    ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫
      a.unop ≫ ((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop
⊢ (shiftFunctor C 1).map (T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a).unop = (shiftFunctor C 1).map (c.op ≫ T₂.mor₃).unop

Tactic:
rw [unop_comp, unop_comp, Functor.map_comp, Functor.map_comp,
    Quiver.Hom.unop_op, hc₂, ← unop_comp_assoc, ← unop_comp_assoc,
    ← opShiftFunctorEquivalence_unitIso_inv_naturality]

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
T₁ T₂ : Triangle Cᵒᵖ
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃
hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop
hc₂ :
  (shiftFunctor C 1).map T₂.mor₃.unop ≫ (shiftFunctor C 1).map c =
    ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫
      a.unop ≫ ((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop
⊢ (shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map a).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop =
    (((shiftFunctor C 1).map
              ((shiftFunctor Cᵒᵖ 1).map (a ≫ (opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁)).unop).op ≫
          (opShiftFunctorEquivalence C 1).unitIso.inv.app
            (Opposite.op ((shiftFunctor C 1).obj (Opposite.unop ((shiftFunctor Cᵒᵖ 1).obj T₂.obj₁))))).unop ≫
      (shiftFunctor C 1).map T₁.mor₃.unop
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ iCycles K i ≫ π.f i =
    cyclesMap π i ≫
      homologyπ ((single C (ComplexShape.up ℤ) i).obj P) i ≫
        (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv

Tactic:
rw [homologyπ_singleObjHomologySelfIso_hom_assoc,
      ← singleObjCyclesSelfIso_inv_iCycles, Iso.hom_inv_id_assoc, ← cyclesMap_i]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
this : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
⊢ mkHomFromSingle (Projective.factorThru (𝟙 P) α) ⋯ ≫ π = 𝟙 ((singleFunctor C i).obj P)

Tactic:
apply HomologicalComplex.from_single_hom_ext
      rw [comp_f, mkHomFromSingle_f, assoc, id_f, this, Projective.factorThru_comp_assoc,
        id_comp, Iso.hom_inv_id]
      rfl

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
⊢ 0 x = 0

Tactic:
LinearMap.zero_apply

Goal state after:
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
⊢ 0 = 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
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
r : relations.R
this : π = Finsupp.linearCombination A fun g ↦ π (Finsupp.single g 1)
⊢ (Finsupp.linearCombination A fun g ↦ π (Finsupp.single g 1)) (relations.relation r) = 0

Tactic:
← this

Goal state after:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
r : relations.R
this : π = Finsupp.linearCombination A fun g ↦ π (Finsupp.single g 1)
⊢ π (relations.relation r) = 0
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: m : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
hM : M.det ∈ R⁰
⊢ Mᵀ.det ∈ R⁰

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: ι : Type u_2
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i ∈ s, f i = c ^ n
⊢ ∀ i ∈ s, ∃ d, f i = d ^ n

Tactic:
intro i hi

Goal state after:
ι : Type u_2
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i ∈ s, f i = c ^ n
i : ι
hi : i ∈ s
⊢ ∃ d, f i = d ^ n
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✝¹ : DecidableEq ι
inst✝ : Fintype ι'
⊢ b.toMatrix ⇑b = 1

Tactic:
toMatrix_self

Goal state after:
ι : 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✝¹ : DecidableEq ι
inst✝ : Fintype ι'
⊢ 1 = 1
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
inst✝ : Algebra R S
g : SpecialLinearGroup n R
⊢ GeneralLinearGroup.det ((mapGL S) g) = 1

Tactic:
by
  simp [mapGL]

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

Goal state before:
pp: case mpr
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
⊢ ∃ v, v ≠ 0 ∧ M *ᵥ v = 0

Tactic:
let := Classical.decEq K
    obtain ⟨⟨b, hb⟩, ba_eq⟩ :=
      IsLocalization.exist_integer_multiples_of_finset (nonZeroDivisors A) (Finset.univ.image v)
    choose f hf using ba_eq
    refine
      ⟨fun i => f _ (Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩),
        mt (fun h => funext fun i => ?_) hv, ?_⟩
    · have := congr_arg (algebraMap A K) (congr_fun h i)
      rw [hf, Subtype.coe_mk, Pi.zero_apply, map_zero, Algebra.smul_def, mul_eq_zero,
        IsFractionRing.to_map_eq_zero_iff] at this
      exact this.resolve_left (nonZeroDivisors.ne_zero hb)
    · ext i
      refine IsFractionRing.injective A K ?_
      calc
        algebraMap A K ((M *ᵥ (fun i : n => f (v i) _)) i) =
            ((algebraMap A K).mapMatrix M *ᵥ algebraMap _ K b • v) i := ?_
        _ = 0 := ?_
        _ = algebraMap A K 0 := (map_zero _).symm
      · simp_rw [RingHom.map_mulVec, mulVec, dotProduct, Function.comp_apply, hf,
          RingHom.mapMatrix_apply, Pi.smul_apply, smul_eq_mul, Algebra.smul_def]
      · rw [mulVec_smul, mul_eq, Pi.smul_apply, Pi.zero_apply, smul_zero]

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).adjugate.det = 1

Tactic:
det_adjugate,

Goal state after:
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
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 b : M
h : QuadraticMap.IsOrtho Q a b
⊢ (ι Q) a * (ι Q) b + (ι Q) b * (ι Q) a = 0

Tactic:
ι_mul_ι_add_swap,

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 b : M
h : QuadraticMap.IsOrtho Q a b
⊢ (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) = 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case cons
F : Type u_1
inst✝³ : Field F
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial ι
P : SpecialLinearGroup ι F → Prop
M : SpecialLinearGroup ι F
hdiag : ∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (diag2n hij c hc)
htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F), P (transvection hij a)
hmul : ∀ (A B : SpecialLinearGroup ι F), P A → P B → P (A * B)
i₀ j₀ : ι
hij₀ : i₀ ≠ j₀
hP1 : P 1
hdiagonal : ∀ (D : ι → F) (hD : (diagonal D).det = 1), P ⟨diagonal D, hD⟩
t : TransvectionStruct ι F
L : List (TransvectionStruct ι F)
ih : P (List.map TransvectionStruct.toSpecialLinearGroup L).prod
⊢ P (List.map TransvectionStruct.toSpecialLinearGroup (t :: L)).prod

Tactic:
List.map_cons,

Goal state after:
case cons
F : Type u_1
inst✝³ : Field F
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial ι
P : SpecialLinearGroup ι F → Prop
M : SpecialLinearGroup ι F
hdiag : ∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (diag2n hij c hc)
htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F), P (transvection hij a)
hmul : ∀ (A B : SpecialLinearGroup ι F), P A → P B → P (A * B)
i₀ j₀ : ι
hij₀ : i₀ ≠ j₀
hP1 : P 1
hdiagonal : ∀ (D : ι → F) (hD : (diagonal D).det = 1), P ⟨diagonal D, hD⟩
t : TransvectionStruct ι F
L : List (TransvectionStruct ι F)
ih : P (List.map TransvectionStruct.toSpecialLinearGroup L).prod
⊢ P (t.toSpecialLinearGroup :: List.map TransvectionStruct.toSpecialLinearGroup L).prod
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : AddMonoid ι
l : List α
fι : α → ι
⊢ l.dProdIndex fι = (map fι l).sum

Tactic:
match l with
  | [] => simp
  | head::tail => simp [List.dProdIndex_eq_map_sum tail fι]

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
⊢ GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA) = (map fA (head :: tail)).prod

Tactic:
List.map_cons,

Goal state after:
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
⊢ GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA) = (fA head :: map fA tail).prod
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ (List.map r (head :: tail)).prod ∈ A (List.map i (head :: tail)).sum

Tactic:
List.map_cons,

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ (List.map r (head :: tail)).prod ∈ A (i head :: List.map i tail).sum
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ (List.map r (head :: tail)).prod ∈ A (i head :: List.map i tail).sum

Tactic:
List.map_cons,

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ (r head :: List.map r tail).prod ∈ A (i head :: List.map i tail).sum
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
head : α
tail : List α
⊢ ↑(fA head) * ↑(tail.dProd fι fA) = (List.map (fun a ↦ ↑(fA a)) (head :: tail)).prod

Tactic:
List.map_cons,

Goal state after:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
head : α
tail : List α
⊢ ↑(fA head) * ↑(tail.dProd fι fA) = (↑(fA head) :: List.map (fun a ↦ ↑(fA a)) tail).prod