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
⊢ (K.truncGE e).Acyclic ↔ K.IsSupportedOutside e

Tactic:
constructor
  · intro hK
    exact ⟨fun i ↦ by simpa only [exactAt_iff_of_quasiIsoAt (K.πTruncGE e)] using hK (e.f i)⟩
  · intro hK i'
    by_cases hi' : ∃ i, e.f i = i'
    · obtain ⟨i, rfl⟩ := hi'
      simpa only [← exactAt_iff_of_quasiIsoAt (K.πTruncGE e)] using hK.exactAt i
    · exact exactAt_of_isSupported _ e i' (by simpa using hi')

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

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✝⁶ : 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✝¹ : HasZeroObject C
inst✝ : K.IsStrictlySupported e
i' : ι'
i : ι
hi : e.f i = i'
⊢ IsIso ((e.liftExtend (K.restrictionToTruncGE' e) ⋯).f i')

Tactic:
rw [e.isIso_liftExtend_f_iff _ _ 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✝⁶ : 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✝¹ : HasZeroObject C
inst✝ : K.IsStrictlySupported e
i' : ι'
i : ι
hi : e.f i = i'
⊢ IsIso ((K.restrictionToTruncGE' e).f i)
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ opcyclesMap ((single C c j).map f) j ≫ (singleObjOpcyclesSelfIso c j B).inv = (singleObjOpcyclesSelfIso c j A).inv ≫ f

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

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

Goal state before:
pp: case e_β
C₁ : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁹ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁸ : HasSmallLocalizedHom W₁ X Y
inst✝⁷ : HasSmallLocalizedHom W₁ Y Z
inst✝⁶ : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst✝⁵ : HasSmallLocalizedHom W₂ X' X'
inst✝⁴ : HasSmallLocalizedHom W₂ Y' Y'
inst✝³ : HasSmallLocalizedHom W₂ Z' Z'
inst✝² : HasSmallLocalizedHom W₂ X' Y'
inst✝¹ : HasSmallLocalizedHom W₂ Y' Z'
inst✝ : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor.obj X ≅ X'
eY : Φ.functor.obj Y ≅ Y'
eZ : Φ.functor.obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this✝⁵ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
this✝⁴ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Y'
this✝³ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) Z'
this✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)
this✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Z'
this✝ : HasSmallLocalizedHom W₂ Y' (Φ.functor.obj Y)
this : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Y)
⊢ (Φ.smallHomMap g).comp (SmallHom.mk W₂ eZ.hom) =
    ((SmallHom.mk W₂ eY.hom).comp (SmallHom.mk W₂ eY.inv)).comp ((Φ.smallHomMap g).comp (SmallHom.mk W₂ eZ.hom))

Tactic:
SmallHom.mk_comp_mk,

Goal state after:
case e_β
C₁ : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁹ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁸ : HasSmallLocalizedHom W₁ X Y
inst✝⁷ : HasSmallLocalizedHom W₁ Y Z
inst✝⁶ : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst✝⁵ : HasSmallLocalizedHom W₂ X' X'
inst✝⁴ : HasSmallLocalizedHom W₂ Y' Y'
inst✝³ : HasSmallLocalizedHom W₂ Z' Z'
inst✝² : HasSmallLocalizedHom W₂ X' Y'
inst✝¹ : HasSmallLocalizedHom W₂ Y' Z'
inst✝ : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor.obj X ≅ X'
eY : Φ.functor.obj Y ≅ Y'
eZ : Φ.functor.obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this✝⁵ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
this✝⁴ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Y'
this✝³ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) Z'
this✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)
this✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Z'
this✝ : HasSmallLocalizedHom W₂ Y' (Φ.functor.obj Y)
this : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Y)
⊢ (Φ.smallHomMap g).comp (SmallHom.mk W₂ eZ.hom) =
    (SmallHom.mk W₂ (eY.hom ≫ eY.inv)).comp ((Φ.smallHomMap g).comp (SmallHom.mk W₂ eZ.hom))
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos.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
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 0
      mono_of_epi_of_mono_of_mono'._proof_13)

pp: case pos.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
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 1
      mono_of_epi_of_mono_of_mono'._proof_11)

pp: case pos.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
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 3
      mono_of_epi_of_mono_of_mono'._proof_7)

Tactic:
· exact h₁

Goal state after:
case pos.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
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 1
      mono_of_epi_of_mono_of_mono'._proof_11)

case pos.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
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 3
      mono_of_epi_of_mono_of_mono'._proof_7)
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos.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
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 0
      mono_of_epi_of_mono_of_mono'._proof_13)

pp: case pos.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
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 2
      mono_of_epi_of_mono_of_mono'._proof_4)

pp: case pos.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
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 3
      mono_of_epi_of_mono_of_mono'._proof_7)

Tactic:
· exact h₁

Goal state after:
case pos.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
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 2
      mono_of_epi_of_mono_of_mono'._proof_4)

case pos.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
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 3
      mono_of_epi_of_mono_of_mono'._proof_7)
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
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Mono (homologyMap φ.τ₁ j)

Tactic:
have := h₃ j hij

Goal state after:
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
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
this : IsIso (homologyMap φ.τ₁ j)
⊢ Mono (homologyMap φ.τ₁ j)
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
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
this : Mono (homologyMap φ.τ₃ i)
j : ι
hij : c.Rel i j
⊢ Epi (homologyMap φ.τ₁ j)

Tactic:
have := h₃ j hij

Goal state after:
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
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
this✝ : Mono (homologyMap φ.τ₃ i)
j : ι
hij : c.Rel i j
this : IsIso (homologyMap φ.τ₁ j)
⊢ Epi (homologyMap φ.τ₁ j)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ ((SmallHom.equiv W Q)
          (SmallHom.mkInv (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯) ≫
        (SmallHom.equiv W Q)
          (SmallHom.mk W (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃)) ≫
      (Functor.commShiftIso Q 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    hS.singleδ

Tactic:
SmallHom.equiv_mkInv,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ ((isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
        (SmallHom.equiv W Q)
          (SmallHom.mk W (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃)) ≫
      (Functor.commShiftIso Q 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    hS.singleδ
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ᵒᵖ
⊢ (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).inv.app X).unop ≫
      (shiftFunctorCompIsoId C 0 0 ⋯).hom.app (Opposite.unop X) =
    (shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).inv.app X).unop ≫ (shiftFunctorZero C ℤ).hom.app (Opposite.unop X)

Tactic:
shiftFunctorZero_op_inv_app,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).inv.app X).unop ≫
      (shiftFunctorCompIsoId C 0 0 ⋯).hom.app (Opposite.unop X) =
    (shiftFunctor C 0).map
        (((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C 0 0 ⋯).inv.app X).unop ≫
      (shiftFunctorZero C ℤ).hom.app (Opposite.unop X)
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) α) ⋯).f i ≫ π.f i = (𝟙 ((singleFunctor C i).obj P)).f i

Tactic:
mkHomFromSingle_f,

Goal state after:
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
⊢ ((singleObjXSelf (ComplexShape.up ℤ) i P).hom ≫ Projective.factorThru (𝟙 P) α) ≫ π.f i =
    (𝟙 ((singleFunctor C i).obj P)).f i
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

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

Tactic:
apply HomologicalComplex.to_single_hom_ext

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := ⋯
α : I ⟶ L.X i := ⋯
this : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α
⊢ (ι ≫ mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯).f i = (𝟙 ((singleFunctor C i).obj I)).f i
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 ι
h₁ : inv (Q.map ι) = Q.map (retraction ι)
⊢ g ≫ retraction ι = 0

Tactic:
apply HomologicalComplex.to_single_hom_ext

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 ι
h₁ : inv (Q.map ι) = Q.map (retraction ι)
⊢ (g ≫ retraction ι).f i = HomologicalComplex.Hom.f 0 i
Module: Mathlib.Algebra.CharP.Reduced

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p n : ℕ
inst✝ : ExpChar R p
x y : R
H : (iterateFrobenius R p n) x = (iterateFrobenius R p n) y
⊢ x = y

Tactic:
rw [← sub_eq_zero] at H ⊢
  simp_rw [iterateFrobenius_def, ← sub_pow_expChar_pow] at H
  exact IsReduced.eq_zero _ ⟨_, H⟩

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Mᵀ.SeparatingLeft ↔ M.SeparatingRight

Tactic:
by
  have := Fintype.ofFinite m
  have := Fintype.ofFinite n
  simp_rw [separatingLeft_def, separatingRight_def, dotProduct_transpose_mulVec]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
e : Basis ι R M
v w : ι → M
⊢ e.toMatrix (v + w) = e.toMatrix v + e.toMatrix w

Tactic:
by
    ext i j
    rw [Matrix.add_apply, e.toMatrix_apply, Pi.add_apply, map_add]
    rfl

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
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ det
      { val := diagonal fun j ↦ if j = i then ↑r else 1, inv := diagonal fun j ↦ if j = i then ↑r⁻¹ else 1,
        val_inv := ?m.57, inv_val := ?m.58 } =
    r

Tactic:
by simp [det]

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

Tactic:
rw [← Matrix.map_mul]

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
f : R →+* S
g : GL n R
⊢ (↑g * (↑g)⁻¹).map ⇑f = 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
f : R →+* S
g : GL n R
⊢ (↑g)⁻¹.map ⇑f * (↑g).map ⇑f = 1

Tactic:
rw [← Matrix.map_mul]

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
f : R →+* S
g : GL n R
⊢ ((↑g)⁻¹ * ↑g).map ⇑f = 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
T : Type u_2
inst✝⁴ : CommRing S
inst✝³ : CommRing T
f : R✝ →+* S
R : Type u_3
m : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x : GL n R
y : GL m R
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) ↑x⁻¹ ↑y⁻¹ * kroneckerMap (fun x1 x2 ↦ x1 * x2) ↑x ↑y = 1

Tactic:
simp only [← mul_kronecker_mul, Units.inv_mul, one_kronecker_one]

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 rw [← transvection_mul_neg hij (-b), neg_neg]

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c : F
⊢ SpecialLinearGroup.transvection ⋯ c ∈ commutator SL(2, F)

Tactic:
have (b c' : F) (hc : c' = b * (a ^ 2 - 1)) :
      ⁅diag2 a⁻¹ (inv_ne_zero ha), SpecialLinearGroup.transvection one_ne_zero b⁆ =
      (SpecialLinearGroup.transvection one_ne_zero c' : SL(2, F)) := by
    rw [commutatorElement_def, diag2_inv a⁻¹ (inv_ne_zero ha),
      SpecialLinearGroup.transvection_inv one_ne_zero b]
    refine Subtype.ext <| Matrix.ext fun i j ↦ ?_
    fin_cases i <;> fin_cases j <;>
    simp [hc, SpecialLinearGroup.transvection_coe, diag2_coe, inv_inv, mul_add, add_mul,
      mul_inv_cancel₀ ha, inv_mul_cancel₀ ha, mul_comm a b, mul_assoc b a a, ← pow_two,
      mul_sub_one, ← sub_eq_add_neg]

Goal state after:
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c : F
this :
  ∀ (b c' : F),
    c' = b * (a ^ 2 - 1) → ⁅diag2 a⁻¹ ⋯, SpecialLinearGroup.transvection ⋯ b⁆ = SpecialLinearGroup.transvection ⋯ c'
⊢ SpecialLinearGroup.transvection ⋯ c ∈ commutator SL(2, F)
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: case pos
ι : 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
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : i + j = 0
⊢ ↑(((decompose 𝒜) (c * c')) 0) = ↑(((decompose 𝒜) c) 0) * ↑(((decompose 𝒜) c') 0)

pp: case neg
ι : 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
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
⊢ ↑(((decompose 𝒜) (c * c')) 0) = ↑(((decompose 𝒜) c) 0) * ↑(((decompose 𝒜) c') 0)

Tactic:
· rw [decompose_of_mem_same 𝒜
              (show c * c' ∈ 𝒜 0 from h ▸ SetLike.GradedMul.mul_mem hc hc'),
            decompose_of_mem_same 𝒜 (show c ∈ 𝒜 0 from (add_eq_zero.mp h).1 ▸ hc),
            decompose_of_mem_same 𝒜 (show c' ∈ 𝒜 0 from (add_eq_zero.mp h).2 ▸ hc')]

Goal state after:
case neg
ι : 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
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
⊢ ↑(((decompose 𝒜) (c * c')) 0) = ↑(((decompose 𝒜) c) 0) * ↑(((decompose 𝒜) c') 0)