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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ { X₁ := S.X₁.cycles i, X₂ := S.X₂.cycles i, X₃ := S.X₃.cycles i, f := cyclesMap S.f i, g := cyclesMap S.g i,
      zero := ⋯ }.Exact

Tactic:
by
  have : Mono (ShortComplex.map S (eval C c i)).f := by dsimp; infer_instance
  have hi := (hS.map (HomologicalComplex.eval C c i)).fIsKernel
  apply ShortComplex.exact_of_f_is_kernel
  exact KernelFork.IsLimit.ofι' _ _ (fun {A} k hk => by
    dsimp at k hk ⊢
    have H := KernelFork.IsLimit.lift' hi (k ≫ S.X₂.iCycles i) (by
      dsimp
      rw [assoc, ← cyclesMap_i, reassoc_of% hk, zero_comp])
    dsimp at H
    refine ⟨S.X₁.liftCycles H.1 _ rfl ?_, ?_⟩
    · rw [← cancel_mono (S.f.f _), assoc, zero_comp, ← Hom.comm, reassoc_of% H.2,
        iCycles_d, comp_zero]
    · rw [← cancel_mono (S.X₂.iCycles i), liftCycles_comp_cyclesMap, liftCycles_i, H.2])

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

Goal state before:
pp: case refine_2.inr.refine_1
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : W.Q.map w = (wIso w hw✝).hom
hw' : G₁.map (wIso w hw✝).hom = eqToHom ⋯ ≫ G₂.map (wIso w hw✝).hom ≫ eqToHom ⋯
⊢ G₁.obj (W.Q.obj Y) = G₂.obj (W.Q.obj Y)

pp: case refine_2.inr.refine_2
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : W.Q.map w = (wIso w hw✝).hom
hw' : G₁.map (wIso w hw✝).hom = eqToHom ⋯ ≫ G₂.map (wIso w hw✝).hom ≫ eqToHom ⋯
⊢ G₁.obj (W.Q.obj X) = G₂.obj (W.Q.obj X)

Tactic:
all_goals apply Functor.congr_obj h

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

Goal state before:
pp: case mpr
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂ : Paths (LocQuiver W)
⊢ ∀ (f : X₁ ⟶ X₂), P (G.map f)

Tactic:
p

Goal state after:
case mpr
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂ : Paths (LocQuiver W)
p : X₁ ⟶ X₂
⊢ P (G.map p)
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝ Y✝ Z✝ : W.FunctorsInverting D
τ₁ : X✝ ⟶ Y✝
τ₂ : Y✝ ⟶ Z✝
X : C
⊢ (𝟙 W.Q ◫ natTransExtension (eqToHom ⋯ ≫ (τ₁ ≫ τ₂).hom ≫ eqToHom ⋯)).app X =
    (𝟙 W.Q ◫
          (natTransExtension (eqToHom ⋯ ≫ τ₁.hom ≫ eqToHom ⋯) ≫ natTransExtension (eqToHom ⋯ ≫ τ₂.hom ≫ eqToHom ⋯))).app
      X

Tactic:
simp only [natTransExtension_hcomp, NatTrans.comp_app, eqToHom_app, eqToHom_refl,
          id_comp, comp_id, NatTrans.hcomp_app, NatTrans.id_app, Functor.map_id,
          natTransExtension_app, NatTransExtension.app_eq]

Goal state after:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝ Y✝ Z✝ : W.FunctorsInverting D
τ₁ : X✝ ⟶ Y✝
τ₂ : Y✝ ⟶ Z✝
X : C
⊢ (τ₁ ≫ τ₂).hom.app X = τ₁.hom.app X ≫ τ₂.hom.app X
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type v
X : ι → Type u
inst✝¹ : Small.{w, v} ι
inst✝ : ∀ (i : ι), Small.{w, u} (X i)
⊢ ∃ κ, κ.IsRegular ∧ ∀ (i : ι), HasCardinalLT (X i) κ

Tactic:
by
  obtain ⟨κ, hκ, h⟩ := exists_regular_cardinal.{w} (Sigma X)
  exact ⟨κ, hκ, fun i ↦ h.of_injective _ sigma_mk_injective⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
H : ∀ (J : Type w) [Finite J], P.IsClosedUnderLimitsOfShape (Discrete J)
J : Type
x✝ : Finite J
⊢ P.IsClosedUnderLimitsOfShape (Discrete J)

Tactic:
by
    rw [P.isClosedUnderLimitsOfShape_iff_of_equivalence (Discrete.equivalence (equivShrink.{w} _))]
    exact H _

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

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
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ { Y' := z₁₂.Y', f := z₁.f ≫ z₁₂.f, s := z₂.s ≫ z₁₂.s, hs := ⋯ }.comp z₃ =
    z₁.comp { Y' := z₂₃.Y', f := z₂.f ≫ z₂₃.f, s := z₃.s ≫ z₂₃.s, hs := ⋯ }

Tactic:
comp_eq _ z₃ (mk z'.f (z₂₃.s ≫ z'.s) (W.comp_mem _ _ z₂₃.hs z'.hs))
        (by dsimp; rw [assoc, reassoc_of% fac₂₃, fac]),

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
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ Hom.mk
      ({ Y' := z₁₂.Y', f := z₁.f ≫ z₁₂.f, s := z₂.s ≫ z₁₂.s, hs := ⋯ }.comp₀ z₃
        { Y' := z'.Y', f := z'.f, s := z₂₃.s ≫ z'.s, hs := ⋯ }) =
    z₁.comp { Y' := z₂₃.Y', f := z₂.f ≫ z₂₃.f, s := z₃.s ≫ z₂₃.s, hs := ⋯ }
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ P.trW f

Tactic:
by
  refine (P.trW.arrow_mk_iso_iff ?_).1 (MorphismProperty.id_mem _ X)
  exact Arrow.isoMk (Iso.refl _) (asIso f)

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

Goal state before:
pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : ¬i = a
⊢ (if i + n = a + n then X else 0) = if i = a then X else 0

Tactic:
if_neg h,

Goal state after:
case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : ¬i = a
⊢ (if i + n = a + n then X else 0) = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X ⟶ Y
hf : IsIso (Qh.map f)
⊢ ∀ (n : ℤ), IsIso ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n).map f)

Tactic:
intro n

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X ⟶ Y
hf : IsIso (Qh.map f)
n : ℤ
⊢ IsIso ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n).map f)
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : DerivedCategory C
f : K ⟶ L
hf : ∀ (n : ℤ), IsIso ((homologyFunctor C n).map f)
g : Arrow (HomotopyCategory C (ComplexShape.up ℤ)) := Qh.mapArrow.objPreimage (Arrow.mk f)
⊢ ∀ (n : ℤ), IsIso ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n).map g.hom)

Tactic:
intro n

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : DerivedCategory C
f : K ⟶ L
hf : ∀ (n : ℤ), IsIso ((homologyFunctor C n).map f)
g : Arrow (HomotopyCategory C (ComplexShape.up ℤ)) := Qh.mapArrow.objPreimage (Arrow.mk f)
n : ℤ
⊢ IsIso ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n).map g.hom)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ Cochain.ofHom (inv f g ≫ hom f g) =
    -((snd (mappingConeCompTriangle f g).mor₁).comp
            ((↑(fst (f ≫ g))).comp
              ((inl f).comp
                  (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁)) ⋯ +
                -(Cochain.ofHom (f ≫ inr f)).comp (inl (mappingConeCompTriangle f g).mor₁) ⋯)
              ⋯)
            ⋯ +
          -
            -((↑(fst (mappingConeCompTriangle f g).mor₁)).comp (Cochain.ofHom (mappingConeCompTriangle f g).mor₁)
                    ⋯).comp
                ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1)
                  ⋯)
                ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))

Tactic:
neg_neg

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ Cochain.ofHom (inv f g ≫ hom f g) =
    -((snd (mappingConeCompTriangle f g).mor₁).comp
            ((↑(fst (f ≫ g))).comp
              ((inl f).comp
                  (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁)) ⋯ +
                -(Cochain.ofHom (f ≫ inr f)).comp (inl (mappingConeCompTriangle f g).mor₁) ⋯)
              ⋯)
            ⋯ +
          ((↑(fst (mappingConeCompTriangle f g).mor₁)).comp (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) ⋯).comp
            ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
            ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : HomologicalComplex Vᵒᵖ c
x✝⁴ x✝³ x✝² : ι
x✝¹ : c.symm.Rel x✝⁴ x✝³
x✝ : c.symm.Rel x✝³ x✝²
⊢ (X.d x✝³ x✝⁴).unop ≫ (X.d x✝² x✝³).unop = 0

Tactic:
rw [← unop_comp, X.d_comp_d, unop_zero]

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

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : HomologicalComplex Vᵒᵖ c.symm
x✝⁴ x✝³ x✝² : ι
x✝¹ : c.Rel x✝⁴ x✝³
x✝ : c.Rel x✝³ x✝²
⊢ (X.d x✝³ x✝⁴).unop ≫ (X.d x✝² x✝³).unop = 0

Tactic:
rw [← unop_comp, X.d_comp_d, unop_zero]

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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
hjk : ¬c.Rel j k
⊢ ¬c.Rel j (c.next j)

Tactic:
simpa only [hk] using hjk

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

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
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.extendCyclesIso e hj').hom ≫ K.iCycles j = (K.extend e).iCycles j' ≫ (K.extendXIso e hj').hom

Tactic:
by
  rw [← cancel_epi (K.extendCyclesIso e hj').inv, Iso.inv_hom_id_assoc]
  dsimp [extendCyclesIso, iCycles]
  rw [assoc, ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles_assoc]
  dsimp
  rw [assoc, Iso.inv_hom_id, comp_id,
    ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i]

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

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
inst✝³ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝² : ∀ (j : ι), K.HasHomology j
inst✝¹ : ∀ (j : ι), L.HasHomology j
inst✝ : QuasiIso φ
⊢ QuasiIso (extendMap φ e)

Tactic:
quasiIso_extendMap_iff

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
inst✝³ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝² : ∀ (j : ι), K.HasHomology j
inst✝¹ : ∀ (j : ι), L.HasHomology j
inst✝ : QuasiIso φ
⊢ QuasiIso φ
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: case right
ι : 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₂
⊢ Function.Surjective (fromSum e₁ e₂)

Tactic:
intro n

Goal state after:
case right
ι : 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₂
n : ι
⊢ ∃ a, fromSum e₁ e₂ a = n
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (HomologicalComplex.homologyMap S.f j)
⊢ IsZero (S.X₃.homology i)

Tactic:
apply (hS.homology_exact₃ i j hij).isZero_X₂

Goal state after:
case pos.hf
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (HomologicalComplex.homologyMap S.f j)
⊢ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ }.f =
    0

case pos.hg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (HomologicalComplex.homologyMap S.f j)
⊢ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ }.g =
    0
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
⊢ Q.map (CochainComplex.mappingCone.descShortComplex S) ≫ triangleOfSESδ hS =
    Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S.X₁

Tactic:
by
  simp [triangleOfSESδ]

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₂.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Epi (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
⊢ Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)

Tactic:
by
  let ψ : mk₃ (0 : R₁.obj' 0 ⟶ _) (R₁.map' 0 1) (R₁.map' 1 2) ⟶
    mk₃ (0 : R₁.obj' 0 ⟶ _) (R₂.map' 0 1) (R₂.map' 1 2) := homMk₃ (𝟙 _) (app' φ 0) (app' φ 1)
      (app' φ 2) (by simp) (naturality' φ 0 1) (naturality' φ 1 2)
  refine epi_of_epi_of_epi_of_mono' ψ (hR₁.exact 0).exact_toComposableArrows
    (exact₂_mk _ (by simp) ?_) ?_ (by dsimp [ψ]; infer_instance) h₀ h₁
  · rw [ShortComplex.exact_iff_mono _ (by simp)]
    exact hR₂'
  · dsimp
    rw [← Functor.map_comp]
    exact hR₂

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
X : Cᵒᵖ
⊢ ((shiftFunctor C (-1)).map (𝟙 0)).op = 0

Tactic:
id_zero,

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : Cᵒᵖ
⊢ ((shiftFunctor C (-1)).map 0).op = 0
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 ≫ ((single C (ComplexShape.up ℤ) i).obj P).iCycles i

Tactic:
← cyclesMap_i

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
⊢ cyclesMap π i ≫ iCycles ((single C (ComplexShape.up ℤ) i).obj P) i =
    cyclesMap π i ≫ ((single C (ComplexShape.up ℤ) i).obj P).iCycles i
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ { X₁ := AddCommGrpCat.of (Ext X S.X₃ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₁ n₁),
      X₃ := AddCommGrpCat.of (Ext X S.X₂ n₁), f := AddCommGrpCat.ofHom (hS.extClass.postcomp X h),
      g := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯), zero := ⋯ }.Exact

Tactic:
let := HasDerivedCategory.standard C
  have := (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequence_exact₁ _
    (hS.singleTriangle_distinguished) n₀ n₁ (by lia)
  rw [ShortComplex.ab_exact_iff_function_exact] at this ⊢
  apply Function.Exact.of_ladder_addEquiv_of_exact' (e₁ := Ext.homAddEquiv)
    (e₂ := Ext.homAddEquiv) (e₃ := Ext.homAddEquiv) (H := this)
  · ext x
    exact preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply hS x h
  · ext x; apply hom_comp_singleFunctor_map_shift (C := C)

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
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ : ℕ
x₃ : Ext X S.X₃ n₀
n₁ : ℕ
hn₁ : n₀ + 1 = n₁
hx₃ : x₃.comp hS.extClass hn₁ = 0
⊢ ∃ x₂, x₂.comp (mk₀ S.g) ⋯ = x₃

Tactic:
have := covariant_sequence_exact₃' X hS n₀ n₁ hn₁

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ : ℕ
x₃ : Ext X S.X₃ n₀
n₁ : ℕ
hn₁ : n₀ + 1 = n₁
hx₃ : x₃.comp hS.extClass hn₁ = 0
this :
  { X₁ := AddCommGrpCat.of (Ext X S.X₂ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₃ n₀),
      X₃ := AddCommGrpCat.of (Ext X S.X₁ n₁), f := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.postcomp X hn₁), zero := ⋯ }.Exact
⊢ ∃ x₂, x₂.comp (mk₀ S.g) ⋯ = x₃
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Fintype n
this : Fintype m
h : ∀ (v : n → R), M *ᵥ v = 0 → v = 0
w : n → R
hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0
i : m
⊢ (M *ᵥ w) i = 0 i

Tactic:
· classical simpa using hw <| Pi.single i 1

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
c : R
v : ι → M
i j : ι
⊢ (e.repr (c • v j)) i = ((RingHom.id R) c • e.toMatrix v) i j

Tactic:
map_smul

Goal state after:
ι : 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
c : R
v : ι → M
i j : ι
⊢ (c • e.repr (v j)) i = ((RingHom.id R) c • e.toMatrix v) i j
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case intro
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ⇑f
val✝ : Fintype G
⊢ ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n

Tactic:
intro n

Goal state after:
case intro
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ⇑f
val✝ : Fintype G
n : ℕ
⊢ 0 < n → #{a | a ^ n = 1} ≤ n
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 : ℕ
M : Type u_7
inst✝ : CommMonoid M
n : ℕ
ζ : ↥(rootsOfUnity n M)
⊢ ↑ζ ^ n = 1

Tactic:
exact (mem_rootsOfUnity ..).mp ζ.prop

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ˣ
⊢ ∃ a, det a = r

Tactic:
obtain ⟨i⟩ := ‹Nonempty n›

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ ∃ a, det a = r
Module: Mathlib.LinearAlgebra.Basis.Bilinear

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
Rₗ : Type u_10
Mₗ : Type u_11
Nₗ : Type u_12
Pₗ : Type u_13
inst✝⁶ : CommSemiring Rₗ
inst✝⁵ : AddCommMonoid Mₗ
inst✝⁴ : AddCommMonoid Nₗ
inst✝³ : AddCommMonoid Pₗ
inst✝² : Module Rₗ Mₗ
inst✝¹ : Module Rₗ Nₗ
inst✝ : Module Rₗ Pₗ
b₁' : Basis ι₁ Rₗ Mₗ
b₂' : Basis ι₂ Rₗ Nₗ
B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ
x : Mₗ
y : Nₗ
⊢ ∑ x_1 ∈ (b₁'.repr x).support,
      ∑ x_2 ∈ (b₂'.repr y).support, (b₁'.repr x) x_1 • (b₂'.repr y) x_2 • (B (b₁' x_1)) (b₂' x_2) =
    ∑ x_1 ∈ (b₁'.repr x).support,
      ∑ x_2 ∈ (b₂'.repr y).support, (b₁'.repr x) x_1 • (B (b₁' x_1)) ((b₂'.repr y) x_2 • b₂' x_2)

Tactic:
map_smul

Goal state after: