mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case hr.fst
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : Dual R M
p : P
x✝ : N
⊢ ((((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap 0 ∘ₗ inr R M N) x✝).1 =
    (((dualTensorHom R (M × N) (P × Q)) ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q) p) ∘ₗ inr R M N) x✝).1

Tactic:
simp only [coe_comp, coe_inl, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      fst_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case hr.snd
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : Dual R M
p : P
x✝ : N
⊢ ((((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap 0 ∘ₗ inr R M N) x✝).2 =
    (((dualTensorHom R (M × N) (P × Q)) ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q) p) ∘ₗ inr R M N) x✝).2

Tactic:
simp only [coe_comp, coe_inl, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      fst_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case inl
K : Type uK
V : Type uV
inst✝³ : CommSemiring K
inst✝² : AddCommMonoid V
inst✝¹ : Module K V
inst✝ : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
h✝ : Finite ι
⊢ Module.Finite K V

Tactic:
exact .of_basis b

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type uK
V : Type uV
inst✝³ : CommSemiring K
inst✝² : AddCommMonoid V
inst✝¹ : Module K V
inst✝ : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
h✝ : Infinite ι
a✝ : Nontrivial K
n : ℕ
hn : ∀ (f : Dual K V →ₗ[K] Fin n → K), ¬Function.Surjective ⇑f
⊢ Module.Finite K V

Tactic:
let g := Finsupp.llift K K K ι ≪≫ₗ b.repr.dualMap

Goal state after:
K : Type uK
V : Type uV
inst✝³ : CommSemiring K
inst✝² : AddCommMonoid V
inst✝¹ : Module K V
inst✝ : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
h✝ : Infinite ι
a✝ : Nontrivial K
n : ℕ
hn : ∀ (f : Dual K V →ₗ[K] Fin n → K), ¬Function.Surjective ⇑f
g : (ι → K) ≃ₗ[K] Dual K V := Finsupp.llift K K K ι ≪≫ₗ b.repr.dualMap
⊢ Module.Finite K V
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
⊢ h ≫ t.rightSection ≫ s.π = s.π

Tactic:
rw [← t.leftSection_top_assoc, s.condition, t.leftSection_bottom_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Projective R M
⊢ ⊤.dualCoannihilator = ⊥

Tactic:
dualCoannihilator,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Projective R M
⊢ comap (Dual.eval R M) ⊤.dualAnnihilator = ⊥
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
W : Subspace K V
this : (dualAnnihilator W).dualCoannihilator = W
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V) W

Tactic:
dualCoannihilator,

Goal state after:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
W : Subspace K V
this : comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator = W
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V) W
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ φ ∈ W.dualAnnihilator → ∃ y, W.mkQ.dualMap y = φ

Tactic:
intro hφ
    exists W.dualCopairing ⟨φ, hφ⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
v : V₁
⊢ ∃ y ∈ LinearMap.ker f, ∃ z ∈ p, y + z = v

Tactic:
have : v ∈ (⊤ : Submodule K V₁) := Submodule.mem_top
    rwa [← (isCompl_ker_of_disjoint_of_ne_bot hf hpf hp).sup_eq_top, Submodule.mem_sup] at this

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ G.map (Fork.ι c) ≫ G.map f = 0

Tactic:
by
  rw [← G.map_comp, c.condition, G.map_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ G.map f ≫ G.map (Cofork.π c) = 0

Tactic:
by
  rw [← G.map_comp, c.condition, G.map_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (biprod.lift f (-g)) 0
⊢ (f ≫ biprod.inl + (-g) ≫ biprod.inr) ≫ s.π = 0

Tactic:
←
            biprod.lift_eq,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (biprod.lift f (-g)) 0
⊢ biprod.lift f (-g) ≫ s.π = 0
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
s : PullbackCone f g
hs : IsLimit s
⊢ Epi s.snd

Tactic:
by
  have : Epi (NatTrans.app (limit.cone (cospan f g)).π WalkingCospan.right) :=
    Abelian.epi_pullback_of_epi_f f g
  apply epi_of_epi_fac (IsLimit.conePointUniqueUpToIso_hom_comp (limit.isLimit _) hs _)

Goal state after:
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: case refine_1.fromCoset
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩) =
    (g ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩)

Tactic:
rw [g_apply_fromCoset]

Goal state after:
case refine_1.fromCoset
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩) =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: case mp
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
⊢ QuasiIso (φ ≫ φ') → QuasiIso φ

pp: case mpr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
⊢ QuasiIso φ → QuasiIso (φ ≫ φ')

Tactic:
· intro
    exact quasiIso_of_comp_right φ φ'

Goal state after:
case mpr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
⊢ QuasiIso φ → QuasiIso (φ ≫ φ')
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: C : Type ?u.2
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ φ.τ₂ ≫ S₂.g = 0

Tactic:
φ.comm₂₃,

Goal state after:
C : Type ?u.2
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ S₁.g ≫ φ.τ₃ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ φ.τ₂ ≫ S₂.g = 0

Tactic:
φ.comm₂₃,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ S₁.g ≫ φ.τ₃ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
⊢ ψ₁ = ψ₂

Tactic:
have hK : ψ₁.φK = ψ₂.φK := by rw [← cancel_mono h₂.i, commi, commi]
    have hH : ψ₁.φH = ψ₂.φH := by rw [← cancel_epi h₁.π, commπ, commπ, hK]
    cases ψ₁
    cases ψ₂
    congr

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ h₁.i ≫ φ.τ₂ ≫ S₂.g = 0

Tactic:
φ.comm₂₃,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ h₁.i ≫ S₁.g ≫ φ.τ₃ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
⊢ φ.τ₂ ≫ S₂.g = h₁.p ≫ h₁.g' ≫ φ.τ₃

Tactic:
φ.comm₂₃,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
⊢ S₁.g ≫ φ.τ₃ = h₁.p ≫ h₁.g' ≫ φ.τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W'✝ : C
x : W'✝ ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
⊢ x ≫ φ.τ₂ ≫ S₂.g = 0

Tactic:
φ.comm₂₃,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W'✝ : C
x : W'✝ ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
⊢ x ≫ S₁.g ≫ φ.τ₃ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝¹ : S.HasLeftHomology
φ : S ⟶ S₁
inst✝ : S₁.HasLeftHomology
⊢ k ≫ φ.τ₂ ≫ S₁.g = 0

Tactic:
φ.comm₂₃,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝¹ : S.HasLeftHomology
φ : S ⟶ S₁
inst✝ : S₁.HasLeftHomology
⊢ k ≫ S.g ≫ φ.τ₃ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Mono (opcyclesMap φ)
⊢ Mono (S₁.homologyι ≫ opcyclesMap φ)

Tactic:
apply mono_comp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
h : S₁.ShortExact
this : Mono S₁.f
⊢ Mono (e.inv.τ₁ ≫ S₁.f)

Tactic:
apply mono_comp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
this✝¹ : S.HasHomology
h : IsZero S.homology
this✝ : IsIso S.pOpcycles
this : Mono S.fromOpcycles
⊢ Mono (S.pOpcycles ≫ S.fromOpcycles)

Tactic:
apply mono_comp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
a✝ : Epi S.f
⊢ S.g = 0

Tactic:
← cancel_epi S.f,

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
a✝ : Epi S.f
⊢ S.f ≫ S.g = S.f ≫ 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ φ.τ₂ ≫ S₂.g = 0

Tactic:
φ.comm₂₃,

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
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ S₁.g ≫ φ.τ₃ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ φ.τ₂ ≫ S₂.g = 0

Tactic:
φ.comm₂₃,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ S₁.g ≫ φ.τ₃ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
⊢ Mono (S₂.liftCycles φ.τ₂ w ≫ S₂.iCycles)

Tactic:
apply mono_comp

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
W : C
h : W ⟶ X
inst✝ : HasPullbacks C
this :
  pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h
⊢ ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ f =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ g

Tactic:
← reassoc_of% (Subobject.isPullback h (equalizerSubobject f g)).w,

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
W : C
h : W ⟶ X
inst✝ : HasPullbacks C
this :
  pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h
⊢ pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow ≫ f =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ g
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
W : C
h : W ⟶ X
inst✝ : HasPullbacks C
this :
  pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h
⊢ pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow ≫ f =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ g

Tactic:
← reassoc_of% (Subobject.isPullback h (equalizerSubobject f g)).w,

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
W : C
h : W ⟶ X
inst✝ : HasPullbacks C
this :
  pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h
⊢ pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow ≫ f =
    pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow ≫ g
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ pullback.fst ((forget A).obj g).hom X✝.arrow ≫ ((forget A).obj g).hom =
    (pullback.snd ((forget A).obj g).hom X✝.arrow ≫ Over.Hom.left k.hom) ≫ Y✝.arrow

Tactic:
rw [pullback.condition, assoc, w k]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (imageSubobjectIso f).hom ≫ image.map sq ≫ image.ι g = (imageSubobject f).arrow ≫ Arrow.Hom.right sq

Tactic:
rw [dsimp% image.map_ι sq]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (imageSubobjectIso f).hom ≫ image.ι f ≫ Arrow.Hom.right sq = (imageSubobject f).arrow ≫ Arrow.Hom.right sq
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : S.Exact
⊢ IsColimit (CokernelCofork.ofπ (Abelian.coimage.π S.g) ⋯)

Tactic:
rw [exact_iff_kernel_ι_comp_cokernel_π_zero] at h
  refine CokernelCofork.IsColimit.ofπ _ _
    (fun u hu => cokernel.desc (kernel.ι S.g) u
      (by rw [← cokernel.π_desc S.f u hu, ← Category.assoc, h, zero_comp]))
    (by simp) ?_
  intro _ _ _ _ hm
  ext
  rw [hm, cokernel.π_desc]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : (S.map F).Exact
⊢ S.Exact

Tactic:
ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (S.map F).g ≫ cokernel.π (S.map F).f = 0
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case insert
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
i✝ : I
m : i✝ = a✝¹ ∨ i✝ ∈ s✝
⊢ (P i✝).Factors (P a✝¹ ⊓ s✝.inf P).arrow

Tactic:
rcases m with (rfl | m)

Goal state after:
case insert.inl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
s✝ : Finset I
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
i✝ : I
a✝ : i✝ ∉ s✝
⊢ (P i✝).Factors (P i✝ ⊓ s✝.inf P).arrow

case insert.inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
i✝ : I
m : i✝ ∈ s✝
⊢ (P i✝).Factors (P a✝¹ ⊓ s✝.inf P).arrow
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

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
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
tfae_2_to_1 :
  (∀ (S : ShortComplex C), S.Exact → (S.map F).Exact) → ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
tfae_3_to_4 : F.PreservesHomology → PreservesFiniteLimits F ∧ PreservesFiniteColimits F
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact,
      F.PreservesHomology, PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE

Tactic:
tfae_have 4 → 2
  | ⟨h1, h2⟩, _, h => h.map F

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
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
tfae_2_to_1 :
  (∀ (S : ShortComplex C), S.Exact → (S.map F).Exact) → ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
tfae_3_to_4 : F.PreservesHomology → PreservesFiniteLimits F ∧ PreservesFiniteColimits F
tfae_4_to_2 : PreservesFiniteLimits F ∧ PreservesFiniteColimits F → ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact,
      F.PreservesHomology, PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE
Module: Mathlib.CategoryTheory.Limits.Filtered

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ Nonempty (Cocone F)

Tactic:
· obtain ⟨c⟩ := h F
    exact ⟨c.pt, ⟨(limitCompYonedaIsoCocone F c.pt).inv c.ι⟩⟩

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ Nonempty (Cocone F)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case insert
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : (∃ i ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
j : I
h : (P j).Factors f
m : j = a✝¹ ∨ j ∈ s✝
⊢ (P a✝¹ ⊔ s✝.sup P).Factors f

Tactic:
rcases m with (rfl | m)

Goal state after:
case insert.inl
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
s✝ : Finset I
ih : (∃ i ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
j : I
h : (P j).Factors f
a✝ : j ∉ s✝
⊢ (P j ⊔ s✝.sup P).Factors f

case insert.inr
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : (∃ i ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
j : I
h : (P j).Factors f
m : j ∈ s✝
⊢ (P a✝¹ ⊔ s✝.sup P).Factors f