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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.up ℕ).next n = n + 1

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{?u.4, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
⊢ (S.map' k (k + 1) ⋯ ⋯ ≫ hkf.lift (KernelFork.ofι (S.map' (k + 1) (k + 1 + 1) ⋯ ⋯) ⋯)) ≫ Fork.ι kf = 0 ≫ Fork.ι kf

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
⊢ shiftFunctor C 0 ≅ 𝟭 (DifferentialObject S C)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
⊢ Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = S.map' (k + 1) (k + 2) ⋯ ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
⊢ (eval C c j ⋙ coyoneda.obj (op X)).CorepresentableBy (evalCompCoyonedaCorepresentative c X j)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.embeddingUpIntGE 0).f (n - 1) = m - 1

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.embeddingUpIntGE 0).f n = m

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.embeddingUpIntGE 0).f (n + 1) = m + 1

Tactic:
by

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

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
i j : ι
h : ¬c.Rel i j
⊢ (C.d i j).app t = 0

Tactic:
by

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

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
i j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
⊢ (C.d i j).app t ≫ (C.d j k).app t = 0

Tactic:
by

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

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
⊢ { f := fun i ↦ (C.X i).map (𝟙 t), comm' := ⋯ } =
    𝟙 { X := fun i ↦ (C.X i).obj t, d := fun i j ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ }

Tactic:
by

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

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
X✝ Y✝ Z✝ : T
h₁ : X✝ ⟶ Y✝
h₂ : Y✝ ⟶ Z✝
⊢ { f := fun i ↦ (C.X i).map (h₁ ≫ h₂), comm' := ⋯ } =
    { f := fun i ↦ (C.X i).map h₁, comm' := ⋯ } ≫ { f := fun i ↦ (C.X i).map h₂, comm' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m₁ m₂ m₃ : S
X : DifferentialObject S C
⊢ (shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X ≫ (shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X) =
    eqToHom ⋯ ≫
      (shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X ≫ (shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.up ℤ).prev m = m - 1

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.up ℤ).next m = m + 1

Tactic:
by

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

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
X✝ Y✝ : HomologicalComplex (T ⥤ V) c
f : X✝ ⟶ Y✝
t t' : T
g : t ⟶ t'
⊢ X✝.asFunctor.map g ≫ { f := fun i ↦ (f.f i).app t', comm' := ⋯ } =
    { f := fun i ↦ (f.f i).app t, comm' := ⋯ } ≫ Y✝.asFunctor.map g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.down ℕ).prev n = n + 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ (shiftFunctorAdd C 0 n).hom.app X = eqToHom ⋯ ≫ (shiftFunctor C n).map ((shiftZero C).inv.app X)

Tactic:
by

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

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : Abelian V
S₁ S₂ : ShortComplex (T ⥤ V)
f : S₁ ⟶ S₂
hf : ∀ (j : T), QuasiIso (((evaluation T V).obj j).mapShortComplex.map f)
⊢ QuasiIso f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ (shiftFunctorAdd C n 0).hom.app X = eqToHom ⋯ ≫ (shiftZero C).inv.app ((shiftFunctor C n).obj X)

Tactic:
by

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

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : Abelian V
ι : Type u_3
c : ComplexShape ι
K₁ K₂ : HomologicalComplex (T ⥤ V) c
f : K₁ ⟶ K₂
i : ι
⊢ QuasiIsoAt f i ↔ ∀ (t : T), QuasiIsoAt ((((evaluation T V).obj t).mapHomologicalComplex c).map f) i

Tactic:
by

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

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : Abelian V
ι : Type u_3
c : ComplexShape ι
K₁ K₂ : HomologicalComplex (T ⥤ V) c
f : K₁ ⟶ K₂
⊢ QuasiIso f ↔ ∀ (t : T), QuasiIso ((((evaluation T V).obj t).mapHomologicalComplex c).map f)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.down ℕ).next n = n - 1

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this✝¹ : HasZeroObject C
this✝ : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
this : Epi h.f'
⊢ Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.HomologicalComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : (ObjectProperty.ofObj X).IsSeparating
K L : HomologicalComplex C c
f g : K ⟶ L
h : ∀ (G : HomologicalComplex C c), ObjectProperty.ofObj (separatingFamily c X) G → ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
a : α
p : X a ⟶ K.X j
H : (eval C c j ⋙ coyoneda.obj (Opposite.op (X a))).CorepresentableBy (evalCompCoyonedaCorepresentative c (X a) j)
⊢ H.homEquiv.symm (p ≫ f.f j) = H.homEquiv.symm (p ≫ g.f j)

Tactic:
simpa only [H.homEquiv_symm_comp] using! h _
    (ObjectProperty.ofObj_apply _ ⟨a, j⟩) (H.homEquiv.symm p)

Goal state after:
Module: Mathlib.CategoryTheory.Generator.HomologicalComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : (ObjectProperty.ofObj X).IsSeparating
⊢ (ObjectProperty.ofObj (separatingFamily c X)).IsSeparating

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.HomologicalComplex

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst✝³ : c.HasNoLoop
inst✝² : HasCoproductsOfShape ι C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
hX : IsSeparator X
φ : ι → HomologicalComplex C c := fun i ↦ separatingFamily c (fun x ↦ X) (PUnit.unit, i)
⊢ (ObjectProperty.ofObj fun x ↦ X).IsSeparating

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.HomologicalComplex

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst✝³ : c.HasNoLoop
inst✝² : HasCoproductsOfShape ι C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
hX : IsSeparator X
⊢ IsSeparator (∐ fun i ↦ separatingFamily c (fun x ↦ X) (PUnit.unit, i))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n + 1) = m - 1

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
⊢ Epi (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.embeddingUpIntLE (-1)).f n = m

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this✝¹ : HasZeroObject C
this✝ : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
this : Mono h.g'
⊢ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.g'

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n - 1) = m + 1

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.up ℤ).prev m = m - 1

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this✝¹ : HasZeroObject C
this✝ : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
this : Mono h.g'
fac : hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.g'
⊢ Mono (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
exact mono_of_mono_fac fac

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.up ℤ).next m = m + 1

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
⊢ Mono (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ (match Int.negSucc 0 with
      | Int.ofNat n => fL.f n
      | Int.negSucc n => fK.f n) ≫
      h'.cochainComplex.d (Int.negSucc 0) (Int.negSucc 0 + 1) =
    h.cochainComplex.d (Int.negSucc 0) (Int.negSucc 0 + 1) ≫
      match Int.negSucc 0 + 1 with
      | Int.ofNat n => fL.f n
      | Int.negSucc n => fK.f n

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : Balanced C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.Exact
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
⊢ IsIso (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : Small.{w, t} ι
K L : HomologicalComplex C c
emb : (K ⟶ L) → (i : Shrink.{w, t} ι) → Shrink.{w, v} (K.X ((equivShrink ι).symm i) ⟶ L.X ((equivShrink ι).symm i)) :=
  fun f i ↦ (equivShrink (K.X ((equivShrink ι).symm i) ⟶ L.X ((equivShrink ι).symm i))) (f.f ((equivShrink ι).symm i))
f g : K ⟶ L
h : emb f = emb g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ (𝟙 K).f 0 ≫ h.d₀ = h.d₀ ≫ (𝟙 L).f 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : Small.{w, t} ι
K L : HomologicalComplex C c
⊢ Small.{w, max t v} (K ⟶ L)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFilteredColimitsOfSize.{w, w', v, u} C
J : Type w'
x✝¹ : Category.{w, w'} J
x✝ : IsFiltered J
⊢ HasColimitsOfShape J (HomologicalComplex C c)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝⁴ : HasZeroMorphisms C
J : Type w
inst✝³ : Category.{w', w} J
inst✝² : HasFiniteLimits C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
F : K ⥤ J ⥤ HomologicalComplex C c
c✝ : Cone F
hc : IsLimit c✝
i : ι
⊢ IsLimit ((eval C c i).mapCone (colim.mapCone c✝))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝³ : HasZeroMorphisms C
inst✝² : HasFilteredColimitsOfSize.{w', w, v, u} C
inst✝¹ : HasFiniteLimits C
inst✝ : AB5OfSize.{w', w, v, u} C
J : Type w
x✝¹ : Category.{w', w} J
x✝ : IsFiltered J
⊢ HasExactColimitsOfShape J (HomologicalComplex C c)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
inst✝¹ : c.HasNoLoop
inst✝ : Small.{w, t} ι
⊢ HasSeparator (HomologicalComplex C c)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
⊢ h.map h (𝟙 K) (𝟙 L) ⋯ = 𝟙 h.cochainComplex

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ (fK ≫ fK').f 0 ≫ h''.d₀ = h.d₀ ≫ (fL ≫ fL').f 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm' = h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
K K' : ChainComplex C ℕ
L L' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst✝⁴ : NeZero n
m : ℤ
hmn : m = ↑n
inst✝³ : HasHomology h.cochainComplex m
inst✝² : HasHomology L n
inst✝¹ : HasHomology h'.cochainComplex m
inst✝ : HasHomology L' n
⊢ homologyMap (h.map h' fK fL f_comm) m =
    (h.homologyIsoPos n m hmn).hom ≫ homologyMap fL n ≫ (h'.homologyIsoPos n m hmn).inv

Tactic:
by

Goal state after: