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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Projective R (M ⧸ p)
⊢ ∃ f, f x ≠ 0 ∧ map f p = ⊥

Tactic:
suffices ∃ f : Dual R (M ⧸ p), f (p.mkQ x) ≠ 0 by
    obtain ⟨f, hf⟩ := this; exact ⟨f.comp p.mkQ, hf, by simp [Submodule.map_comp]⟩

Goal state after:
R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Projective R (M ⧸ p)
⊢ ∃ f, f (p.mkQ x) ≠ 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
⊢ (domRestrict₁₂ B W W).Nondegenerate ↔ Disjoint W (ker B)

Tactic:
by
  refine ⟨disjoint_ker_of_nondegenerate_restrict, fun hW ↦ ?_⟩
  have hB' : (B.domRestrict₁₂ W W).IsRefl := fun x y ↦ hB.isRefl (W.subtype x) (W.subtype y)
  rw [IsRefl.nondegenerate_iff_separatingLeft hB']
  intro ⟨x, hx⟩ h
  simp_rw [Subtype.forall, domRestrict₁₂_apply] at h
  specialize h x hx
  rw [B.apply_apply_same_eq_zero_iff hs hB] at h
  have key : x ∈ W ⊓ LinearMap.ker B := ⟨hx, h⟩
  simpa [hW.eq_bot] using key

Goal state after:
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
W : Subspace K V
v : V
x✝ : ∃ φ, φ (Submodule.Quotient.mk v) ≠ 0
φ : Dual K (V ⧸ W)
hφ : φ (Submodule.Quotient.mk v) ≠ 0
w : V
hw : w ∈ W
⊢ φ (Submodule.Quotient.mk w) = 0

Tactic:
(Quotient.mk_eq_zero W).mpr hw,

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
x✝ : ∃ φ, φ (Submodule.Quotient.mk v) ≠ 0
φ : Dual K (V ⧸ W)
hφ : φ (Submodule.Quotient.mk v) ≠ 0
w : V
hw : w ∈ W
⊢ φ 0 = 0
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
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V) W

Tactic:
by
  have : _ = W := Subspace.dualAnnihilator_dualCoannihilator_eq
  rw [dualCoannihilator, ← Module.mapEvalEquiv_symm_apply] at this
  rwa [← OrderIso.symm_apply_eq]

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

Goal state before:
pp: case left
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (↑W.quotAnnihilatorEquiv).ker = ⊥

Tactic:
apply LinearEquiv.ker

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

Goal state before:
pp: case left
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (↑(dualQuotEquivDualAnnihilator W).symm).ker = ⊥

Tactic:
apply LinearEquiv.ker

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
P Q : C
f✝ : P ⟶ Q
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
f g : Arrow C
η : f ⟶ g
⊢ cokernel.map (kernel.ι f.hom) (kernel.ι g.hom) (kernel.map f.hom g.hom (Arrow.Hom.left η) (Arrow.Hom.right η) ⋯)
        (Arrow.Hom.left η) ⋯ ≫
      (Arrow.mk (coimageImageComparison g.hom)).hom =
    (Arrow.mk (coimageImageComparison f.hom)).hom ≫
      kernel.map (cokernel.π f.hom) (cokernel.π g.hom) (Arrow.Hom.right η)
        (cokernel.map f.hom g.hom (Arrow.Hom.left η) (Arrow.Hom.right η) ⋯) ⋯

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasKernels C
inst✝² : IsNormalMonoCategory C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
⊢ ((s.snd ≫ b) ≫ prod.lift f g) ≫ prod.snd = s.snd ≫ b ≫ g

Tactic:
by
                    simp only [prod.lift_snd, Category.assoc]

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

Goal state before:
pp: G H : AddCommGrpCat
⊢ ∀ {T : AddCommGrpCat} (f : T ⟶ G) (g : T ⟶ H)
    (m : T ⟶ (BinaryFan.mk (ofHom (AddMonoidHom.fst ↑G ↑H)) (ofHom (AddMonoidHom.snd ↑G ↑H))).pt),
    m ≫ (BinaryFan.mk (ofHom (AddMonoidHom.fst ↑G ↑H)) (ofHom (AddMonoidHom.snd ↑G ↑H))).fst = f →
      m ≫ (BinaryFan.mk (ofHom (AddMonoidHom.fst ↑G ↑H)) (ofHom (AddMonoidHom.snd ↑G ↑H))).snd = g →
        m = ofHom ((Hom.hom f).prod (Hom.hom g))

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ -(a - b) = -a + b

Tactic:
by
  rw [neg_def, neg_def]
  conv_lhs => rw [← sub_self (0 : X ⟶ Y)]
  rw [sub_sub_sub, add_def, neg_def]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
⊢ π₁Toπ₂ ≫ π₂Toπ₃ = 0

Tactic:
by cat_disch

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

Goal state before:
pp: A : Type u
B : Type v
inst✝¹ : Group A
inst✝ : Group B
f : A →* B
h : ∀ (u v : ↥f.ker →* A), f.comp u = f.comp v → u = v
⊢ f.comp f.ker.subtype = f.comp 1

Tactic:
by cat_disch

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

Goal state before:
pp: A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : (QuotientGroup.mk' f.range).ker = ker 1
⊢ f.range = ⊤

Tactic:
ker_one,

Goal state after:
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : (QuotientGroup.mk' f.range).ker = ⊤
⊢ f.range = ⊤
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: case neg
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∉ (Hom.hom f).range
⊢ (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, ⋯⟩, ⋯⟩

Tactic:
rw [h_apply_fromCoset_nin_range f (f a) ⟨_, rfl⟩ _ m]
        simp only [leftCoset_assoc]

Goal state after:
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₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
⊢ QuasiIso φ'

Tactic:
by
  let α : S₃ ⟶ S₁ := e.inv.left
  let β : S₂ ⟶ S₄ := e.hom.right
  suffices φ' = α ≫ φ ≫ β by
    rw [this]
    infer_instance
  simp only [α, β, Arrow.w_mk_right_assoc, Arrow.mk_hom,
    ← Arrow.comp_right, e.inv_hom_id, Arrow.id_right, comp_id]

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₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
⊢ cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φK ≫ cyclesMap' φ₂ h₂ h₃

Tactic:
γ₂.cyclesMap'_eq,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
⊢ cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φK ≫ γ₂.φK
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₂
inst✝⁴ : S₁.HasLeftHomology
inst✝³ : S₂.HasLeftHomology
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ IsIso (leftHomologyMap φ)

Tactic:
dsimp only [leftHomologyMap]

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₂
inst✝⁴ : S₁.HasLeftHomology
inst✝³ : S₂.HasLeftHomology
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ IsIso (leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData)
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 : ShortComplex C
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
A' : C
α : A' ⟶ A
⊢ α ≫ S.liftCycles k hk = S.liftCycles (α ≫ k) ⋯

Tactic:
by cat_disch

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 : ShortComplex C
inst✝¹ : S.HasLeftHomology
inst✝ : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
this : HasColimit (parallelPair h.f' 0)
⊢ (parallelPair (kernel.lift S.g S.f ⋯) 0).map WalkingParallelPairHom.left ≫
      ((kernelIsKernel S.g).conePointUniqueUpToIso h.hi).hom =
    (Iso.refl ((parallelPair (kernel.lift S.g S.f ⋯) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair h.f' 0).map WalkingParallelPairHom.left

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
⊢ limMap (F.whiskerLeft π₁Toπ₂) ≫ limMap (F.whiskerLeft π₂Toπ₃) = 0

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
⊢ ∀ (j : J),
    (limit.cone (F ⋙ π₁)).π.app j = (Iso.refl (limit.cone (F ⋙ π₁)).pt).hom ≫ (π₁.mapCone (limitCone F)).π.app j

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
⊢ ∀ (j : J),
    (limit.cone (F ⋙ π₂)).π.app j = (Iso.refl (limit.cone (F ⋙ π₂)).pt).hom ≫ (π₂.mapCone (limitCone F)).π.app j

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
⊢ ∀ (j : J),
    (limit.cone (F ⋙ π₃)).π.app j = (Iso.refl (limit.cone (F ⋙ π₃)).pt).hom ≫ (π₃.mapCone (limitCone F)).π.app j

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ (π₁.mapCocone c).ι.app j ≫ h₁.desc (π₁.mapCocone s) ≫ s.pt.f =
    (π₁.mapCocone c).ι.app j ≫ c.pt.f ≫ h₂.desc (π₂.mapCocone s)

Tactic:
have eq₁ := h₁.fac (π₁.mapCocone s)
        have eq₂ := h₂.fac (π₂.mapCocone s)
        have eq₁₂ := fun j => (c.ι.app j).comm₁₂
        have eq₁₂' := fun j => (s.ι.app j).comm₁₂
        dsimp at eq₁ eq₂ eq₁₂ eq₁₂' ⊢
        rw [reassoc_of% (eq₁ j), eq₁₂', reassoc_of% eq₁₂, eq₂]

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

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
⊢ F.map (leftHomologyMap' φ hl₁ hl₂) = leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)

Tactic:
have γ : ShortComplex.LeftHomologyMapData φ hl₁ hl₂ := default
  rw [γ.leftHomologyMap'_eq, (γ.map F).leftHomologyMap'_eq,
    ShortComplex.LeftHomologyMapData.map_φH]

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
⊢ colimMap (F.whiskerLeft π₁Toπ₂) ≫ colimMap (F.whiskerLeft π₂Toπ₃) = 0

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
⊢ ∀ (j : J),
    (colimit.cocone (F ⋙ π₁)).ι.app j ≫ (Iso.refl (colimit.cocone (F ⋙ π₁)).pt).hom =
      (π₁.mapCocone (colimitCocone F)).ι.app j

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
⊢ ∀ (j : J),
    (colimit.cocone (F ⋙ π₂)).ι.app j ≫ (Iso.refl (colimit.cocone (F ⋙ π₂)).pt).hom =
      (π₂.mapCocone (colimitCocone F)).ι.app j

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
⊢ ∀ (j : J),
    (colimit.cocone (F ⋙ π₃)).ι.app j ≫ (Iso.refl (colimit.cocone (F ⋙ π₃)).pt).hom =
      (π₃.mapCocone (colimitCocone F)).ι.app j

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P Q : C
inst✝² : HasBinaryCoproduct P Q
inst✝¹ : Projective P
inst✝ : Projective Q
E✝ X✝ : C
f : P ⨿ Q ⟶ X✝
e : E✝ ⟶ X✝
epi : Epi e
⊢ coprod.desc (factorThru (coprod.inl ≫ f) e) (factorThru (coprod.inr ≫ f) e) ≫ e = f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
β : Type v
g : β → C
inst✝¹ : HasCoproduct g
inst✝ : ∀ (b : β), Projective (g b)
E✝ X✝ : C
f : ∐ g ⟶ X✝
e : E✝ ⟶ X✝
epi : Epi e
⊢ (Sigma.desc fun b ↦ factorThru (Sigma.ι g b ≫ f) e) ≫ e = f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P Q : C
inst✝³ : HasZeroMorphisms C
inst✝² : HasBinaryBiproduct P Q
inst✝¹ : Projective P
inst✝ : Projective Q
E✝ X✝ : C
f : P ⊞ Q ⟶ X✝
e : E✝ ⟶ X✝
epi : Epi e
⊢ biprod.desc (factorThru (biprod.inl ≫ f) e) (factorThru (biprod.inr ≫ f) e) ≫ e = f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
β : Type v
g : β → C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBiproduct g
inst✝ : ∀ (b : β), Projective (g b)
E✝ X✝ : C
f : ⨁ g ⟶ X✝
e : E✝ ⟶ X✝
epi : Epi e
⊢ (biproduct.desc fun b ↦ factorThru (biproduct.ι g b ≫ f) e) ≫ e = f

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
⊢ Function.LeftInverse (fun h ↦ ((ofEq ⋯).trans (h.add (refl φ₂))).trans (ofEq ⋯)) fun h ↦
    (h.sub (refl φ₂)).trans (ofEq ⋯)

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
⊢ Function.RightInverse (fun h ↦ ((ofEq ⋯).trans (h.add (refl φ₂))).trans (ofEq ⋯)) fun h ↦
    (h.sub (refl φ₂)).trans (ofEq ⋯)

Tactic:
by cat_disch

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

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
⊢ PreservesColimit (parallelPair S.f 0) F

Tactic:
rw [hf]
      infer_instance

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
⊢ Mono S₂.f

Tactic:
by
    suffices Mono (S₂.f ≫ e.inv.τ₂) by
      exact mono_of_mono _ e.inv.τ₂
    have := h.mono_f
    rw [← e.inv.comm₁₂]
    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✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
S' : ShortComplex C := { X₁ := h.left.K, X₂ := S.X₂, X₃ := S.X₃, f := h.left.i, g := S.g, zero := ⋯ }
S'' : ShortComplex C := { X₁ := h.left.K, X₂ := S.X₂, X₃ := h.right.Q, f := h.left.i, g := h.right.p, zero := ⋯ }
a : S ⟶ S' := { τ₁ := h.left.f', τ₂ := 𝟙 S.X₂, τ₃ := 𝟙 S.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ { X₁ := h.left.K, X₂ := S.X₂, X₃ := h.right.Q, f := h.left.i, g := h.right.p, zero := ⋯ }.Exact

Tactic:
let b : S'' ⟶ S' :=
      { τ₁ := 𝟙 _
        τ₂ := 𝟙 _
        τ₃ := h.right.g' }

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
S' : ShortComplex C := { X₁ := h.left.K, X₂ := S.X₂, X₃ := S.X₃, f := h.left.i, g := S.g, zero := ⋯ }
S'' : ShortComplex C := { X₁ := h.left.K, X₂ := S.X₂, X₃ := h.right.Q, f := h.left.i, g := h.right.p, zero := ⋯ }
a : S ⟶ S' := { τ₁ := h.left.f', τ₂ := 𝟙 S.X₂, τ₃ := 𝟙 S.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
b : S'' ⟶ S' := { τ₁ := 𝟙 S''.X₁, τ₂ := 𝟙 S''.X₂, τ₃ := h.right.g', comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ { X₁ := h.left.K, X₂ := S.X₂, X₃ := h.right.Q, f := h.left.i, g := h.right.p, zero := ⋯ }.Exact
Module: Mathlib.CategoryTheory.Preadditive.LeftExact

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y Z : C
π₁ : Z ⟶ X
π₂ : Z ⟶ Y
inst✝ : PreservesLimit (parallelPair π₂ 0) F
i : IsLimit (BinaryFan.mk π₁ π₂)
⊢ IsLimit (F.mapCone (BinaryFan.mk π₁ π₂))

Tactic:
let bc := BinaryBicone.ofLimitCone i
  let presf : PreservesLimit (parallelPair bc.snd 0) F := by simpa
  let hf : IsLimit bc.sndKernelFork := BinaryBicone.isLimitSndKernelFork i
  exact (isLimitMapConeBinaryFanEquiv F π₁ π₂).invFun
    (BinaryBicone.isBilimitOfKernelInl (F.mapBinaryBicone bc)
    (isLimitMapConeForkEquiv' F bc.inl_snd (isLimitOfPreserves F hf))).isLimit

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
a✝ : Mono S.g
⊢ IsZero
    (HomologyData.ofIsLimitKernelFork S hf (KernelFork.ofι 0 ⋯)
          (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι 0 ⋯) ⋯ ⋯)).left.H

Tactic:
exact isZero_zero C

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hg : S.g = 0
a✝ : Epi S.f
⊢ IsZero
    (HomologyData.ofIsColimitCokernelCofork S hg (CokernelCofork.ofπ 0 ⋯)
          (CokernelCofork.IsColimit.ofEpiOfIsZero (CokernelCofork.ofπ 0 ⋯) ⋯ ⋯)).left.H

Tactic:
exact isZero_zero C

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasKernel S.g
⊢ (Iso.refl (Arrow.mk S.toCycles).left).hom ≫ (Arrow.mk (kernel.lift S.g S.f ⋯)).hom =
    (Arrow.mk S.toCycles).hom ≫ S.cyclesIsoKernel.hom

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasCokernel S.f
⊢ S.opcyclesIsoCokernel.symm.hom ≫ (Arrow.mk S.fromOpcycles).hom =
    (Arrow.mk (cokernel.desc S.f S.g ⋯)).hom ≫ (Iso.refl (Arrow.mk (cokernel.desc S.f S.g ⋯)).right).hom

Tactic:
by cat_disch

Goal state after:
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✝¹ : Preadditive C
inst✝ : Preadditive D
S✝ : ShortComplex C
S : ShortComplex Cᵒᵖ
h : S.Splitting
⊢ (h.s.unop ≫ S.unop.f + S.unop.g ≫ h.r.unop).op = (𝟙 S.unop.X₂).op

Tactic:
simp only [unop_X₂, Opposite.op_unop, unop_X₁, unop_f, unop_X₃, unop_g, op_add,
      op_comp, Quiver.Hom.op_unop, op_id, ← h.id]

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✝¹ : Preadditive C
inst✝ : Preadditive D
S✝ : ShortComplex C
S : ShortComplex Cᵒᵖ
h : S.Splitting
⊢ S.g ≫ h.s + h.r ≫ S.f = h.r ≫ S.f + S.g ≫ h.s
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
W : C
h : W ⟶ X
w : (equalizerSubobject f g).Factors h
⊢ h ≫ f = h ≫ g

Tactic:
rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, equalizerSubobject_arrow_comp,
      Category.assoc]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ kernelSubobjectMap (𝟙 (Arrow.mk f)) = 𝟙 (underlying.obj (kernelSubobject f))

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasKernel f'
sq : Arrow.mk f ⟶ Arrow.mk f'
⊢ kernel.map f f' sq.left sq.right ⋯ ≫ (kernelSubobjectIso f').inv = (kernelSubobjectIso f).inv ≫ kernelSubobjectMap sq

Tactic:
by cat_disch

Goal state after:
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✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
⊢ (f ⟶ h) → (g ⟶ h) → ((sup.obj f).obj g ⟶ h)

Tactic:
intro k₁ k₂

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ (sup.obj f).obj g ⟶ h