mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso ((snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).castSucc, (snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).succ)
    ((snoc s₂ x₂ hsat₂).toFun (e (Fin.last s₁.length)).castSucc, (snoc s₂ x₂ hsat₂).toFun (e (Fin.last s₁.length)).succ)

Tactic:
rw [he_last]

Goal state after:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso ((snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).castSucc, (snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).succ)
    ((snoc s₂ x₂ hsat₂).toFun (Fin.last s₂.length).castSucc, (snoc s₂ x₂ hsat₂).toFun (Fin.last s₂.length).succ)
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
⊢ (∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)) ↔ ∀ (x : R), x ≠ 0 → IsUnit x

Tactic:
by
    refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ (h x hx).unit.mulRight_bijective.surjective⟩
    obtain ⟨y, hyx : y * x = 1⟩ := h x hx 1
    have hy : y ≠ 0 := left_ne_zero_of_mul (hyx.symm ▸ one_ne_zero)
    obtain ⟨z, hzy : z * y = 1⟩ := h y hy 1
    exact ⟨⟨x, y, left_inv_eq_right_inv hzy hyx ▸ hzy, hyx⟩, rfl⟩

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

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
J : Ideal R
f : Module.End R R
idem : IsIdempotentElem f
h : IsCompl (LinearMap.range f) J
⊢ Submodule.map f ⊤ = Ideal.span {f 1}

Tactic:
← Ideal.span_one,

Goal state after:
R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
J : Ideal R
f : Module.End R R
idem : IsIdempotentElem f
h : IsCompl (LinearMap.range f) J
⊢ Submodule.map f (Ideal.span 1) = Ideal.span {f 1}
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ torsionOf R M m = ⊤ ↔ m = 0

Tactic:
refine ⟨fun h => ?_, fun h => by simp [h]⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
h : torsionOf R M m = ⊤
⊢ m = 0
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : R
dvd : a ∣ b
⊢ torsionBy R M a ≤ torsionBy R M b

Tactic:
← torsionBySet_span_singleton_eq,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : R
dvd : a ∣ b
⊢ torsionBySet R M ↑(R ∙ a) ≤ torsionBy R M b
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case empty
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
r : R
hr1 : r - 1 ∈ I
right✝ : ∅ ⊆ ↑N
n : M
hrn : ((LinearMap.lsmul R M) r) n ∈ I • ⊥
hn : n ∈ N
⊢ r • n = 0

Tactic:
smul_bot,

Goal state after:
case empty
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
r : R
hr1 : r - 1 ∈ I
right✝ : ∅ ⊆ ↑N
n : M
hrn : ((LinearMap.lsmul R M) r) n ∈ ⊥
hn : n ∈ N
⊢ r • n = 0
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
i : ℕ
h : ¬i = 0
⊢ 0 ∈ I ^ i

Tactic:
· simp

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
h : ¬i = 0
⊢ 0 ∈ I ^ i

Tactic:
· simp

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case a
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) ≤ reesAlgebra I

Tactic:
apply Algebra.adjoin_le _

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ ↑(Submodule.map (monomial 1) I) ⊆ ↑(reesAlgebra I)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
⊢ (fun i ↦ torsionBySet R M ↑(p i)) i ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i) = ⊥

Tactic:
have := GaloisConnection.u_inf
    (b₁ := OrderDual.toDual (p i)) (b₂ := OrderDual.toDual (⨅ i ∈ T, p i)) (torsion_gc R M)

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
this :
  torsionBySet R M ↑(OrderDual.ofDual (OrderDual.toDual (p i) ⊓ OrderDual.toDual (⨅ i ∈ T, p i))) =
    torsionBySet R M ↑(OrderDual.ofDual (OrderDual.toDual (p i))) ⊓
      torsionBySet R M ↑(OrderDual.ofDual (OrderDual.toDual (⨅ i ∈ T, p i)))
⊢ (fun i ↦ torsionBySet R M ↑(p i)) i ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i) = ⊥
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ ⨆ i ∈ S, torsionBy R M (q i) = torsionBy R M (∏ i ∈ S, q i)

Tactic:
← torsionBySet_span_singleton_eq,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ ⨆ i ∈ S, torsionBy R M (q i) = torsionBySet R M ↑(R ∙ ∏ i ∈ S, q i)
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this : map N.mkQ (I • N') = map N.mkQ N'
⊢ N ⊔ N' = N ⊔ J • N'

Tactic:
have :=
    @Submodule.eq_smul_of_le_smul_of_le_jacobson _ _ _ _ _ I J (N'.map N.mkQ) (hN'.map _)
      (by rw [← map_smul'', this]) hIJ

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this✝ : map N.mkQ (I • N') = map N.mkQ N'
this : map N.mkQ N' = J • map N.mkQ N'
⊢ N ⊔ N' = N ⊔ J • N'
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsTorsionFree R M ↔ torsion R M = ⊥

Tactic:
by
  simp [torsion, torsion', subset_antisymm_iff, exists_ne, isTorsionFree_iff_smul_eq_zero]
  grind

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
⊢ (F ⊓ F').submodule = F.submodule ⊓ F'.submodule

Tactic:
ext
  exact forall_and

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mpr.succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, single R i '' ↑(F.N i) ⊆ ↑F'
j : ℕ
hj : single R j '' ↑(F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
⊢ single R (j + 1) '' ↑(F.N (j + 1)) ⊆
    ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))

Tactic:
| succ j hj =>

Goal state after:
case mpr.succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, single R i '' ↑(F.N i) ⊆ ↑F'
j : ℕ
hj : single R j '' ↑(F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
⊢ single R (j + 1) '' ↑(F.N (j + 1)) ⊆
    ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Submodule.span R (⇑(maximalIdeal R).toCotangent '' s) = Submodule.restrictScalars R ⊤ ↔
    Submodule.map (maximalIdeal R).toCotangent (Submodule.span R s) = ⊤

pp: case hsur
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Function.Surjective ⇑(algebraMap R (ResidueField R))

Tactic:
· simp

Goal state after:
case hsur
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Function.Surjective ⇑(algebraMap R (ResidueField R))
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : J.toCotangent x' = x
this : Function.Surjective ⇑(Algebra.ofId A B)
hx : ↑x' ∈ comap (algebraMap A B) (map (algebraMap A B) (J ^ 2))
⊢ x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))

Tactic:
Ideal.comap_map_of_surjective' _ surj

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : J.toCotangent x' = x
this : Function.Surjective ⇑(Algebra.ofId A B)
hx : ↑x' ∈ J ^ 2 ⊔ RingHom.ker (algebraMap A B)
⊢ x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : J.toCotangent x' = x
this : Function.Surjective ⇑(Algebra.ofId A B)
hx : ↑x' ∈ J ^ 2 ⊔ RingHom.ker (algebraMap A B)
y : A
hy : y ∈ J ^ 2
z : A
hz : z ∈ RingHom.ker (algebraMap A B)
hyz : y + z = ↑x'
⊢ x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))

Tactic:
have : y + z ∈ J := by simp [hyz]

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : J.toCotangent x' = x
this✝ : Function.Surjective ⇑(Algebra.ofId A B)
hx : ↑x' ∈ J ^ 2 ⊔ RingHom.ker (algebraMap A B)
y : A
hy : y ∈ J ^ 2
z : A
hz : z ∈ RingHom.ker (algebraMap A B)
hyz : y + z = ↑x'
this : y + z ∈ J
⊢ x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
X : Cᵒᵖ
hX : Limits.IsInitial X
M : PresheafOfModules R
Y Z : Cᵒᵖ
f : Y ⟶ Z
r : ↑(R.obj X)
x : ↑(forgetToPresheafModuleCatObjObj X hX M Y)
⊢ (ConcreteCategory.hom (R.map f)) ((RingCat.Hom.hom (R.map (hX.to Y))) r) • (ConcreteCategory.hom (M.map f)) x =
    (RingCat.Hom.hom (R.map (hX.to Z))) r • (ConcreteCategory.hom (M.map f)) x

Tactic:
← RingCat.comp_apply,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
X : Cᵒᵖ
hX : Limits.IsInitial X
M : PresheafOfModules R
Y Z : Cᵒᵖ
f : Y ⟶ Z
r : ↑(R.obj X)
x : ↑(forgetToPresheafModuleCatObjObj X hX M Y)
⊢ (ConcreteCategory.hom (R.map (hX.to Y) ≫ R.map f)) r • (ConcreteCategory.hom (M.map f)) x =
    (RingCat.Hom.hom (R.map (hX.to Z))) r • (ConcreteCategory.hom (M.map f)) x
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: case neg
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
X✝ Y✝ Z✝ : V
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
i✝ : ι
h : ¬i✝ = j
⊢ 0 = 0 ≫ 0

Tactic:
· simp

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C D : HomologicalComplex V c
f g : C ⟶ D
h : ∀ (i : ι), f.f i = g.f i
⊢ f = g

Tactic:
apply Hom.ext

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C D : HomologicalComplex V c
f g : C ⟶ D
h : ∀ (i : ι), f.f i = g.f i
⊢ f.f = g.f
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
i k : ι
hik : c.Rel i k
⊢ (if hi : i = j then (singleObjXIsoOfEq c j A i hi).hom ≫ φ ≫ (K.XIsoOfEq hi).inv else 0) ≫ K.d i k =
    ((single V c j).obj A).d i k ≫
      if hi : k = j then (singleObjXIsoOfEq c j A k hi).hom ≫ φ ≫ (K.XIsoOfEq hi).inv else 0

Tactic:
by
    dsimp
    rw [zero_comp]
    split_ifs with hi
    · subst hi
      simp only [XIsoOfEq_rfl, Iso.refl_inv, comp_id, assoc, hφ k hik, comp_zero]
    · apply (isZero_single_obj_X c j A i hi).eq_of_src

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : c.Rel i j
⊢ C.dFrom i = C.d i j ≫ (C.xNextIso r).inv

Tactic:
obtain rfl := c.next_eq' r

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
r : c.Rel i (c.next i)
⊢ C.dFrom i = C.d i (c.next i) ≫ (C.xNextIso r).inv
Module: Mathlib.Algebra.Homology.Additive

Goal state before:
pp: case pos
ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f : C ⟶ D
i✝ : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
i : ι
h : i = j
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = 𝟙 (F.obj (((single W₁ c j).obj X).X i))

pp: case neg
ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f : C ⟶ D
i✝ : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
i : ι
h : ¬i = j
⊢ 0 ≫ 0 = 𝟙 (F.obj (((single W₁ c j).obj X).X i))

Tactic:
· simp

Goal state after:
case neg
ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f : C ⟶ D
i✝ : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
i : ι
h : ¬i = j
⊢ 0 ≫ 0 = 𝟙 (F.obj (((single W₁ c j).obj X).X i))
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ n' + m' + p = p' + p

Tactic:
hp,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ n' + m' + p = 0
Module: Mathlib.Algebra.Homology.Additive

Goal state before:
pp: case pos
ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f : C ⟶ D
i✝ : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
i : ι
h : i = j
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = 𝟙 (((single W₂ c j).obj (F.obj X)).X i)

pp: case neg
ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f : C ⟶ D
i✝ : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
i : ι
h : ¬i = j
⊢ 0 ≫ 0 = 𝟙 (((single W₂ c j).obj (F.obj X)).X i)

Tactic:
· simp

Goal state after:
case neg
ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f : C ⟶ D
i✝ : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
i : ι
h : ¬i = j
⊢ 0 ≫ 0 = 𝟙 (((single W₂ c j).obj (F.obj X)).X i)
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i : ι
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesLimitsOfShape J (single C c i)

Tactic:
by intros; infer_instance

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i : ι
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesColimitsOfShape J (single C c i)

Tactic:
by intros; infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝² : HasFiniteLimits C
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits F
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesLimitsOfShape J (F.mapHomologicalComplex c)

Tactic:
by intros; infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝² : HasFiniteColimits C
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesFiniteColimits F
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesColimitsOfShape J (F.mapHomologicalComplex c)

Tactic:
by intros; infer_instance

Goal state after: