mathlib-initiative/mathlib-tactics huggingface dataset:
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 W' : Subspace K V₁
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
let F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (Submodule.mkQ W).prod (Submodule.mkQ W')

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
b : Basis (↑(hli.extend ⋯)) K V := Basis.mk ⋯ ⋯
i : ι
hi : v i ∈ hli.extend ⋯
ri : ↑(hli.extend ⋯) := ⟨v i, hi⟩
⊢ ((b.constr K) 1) (v i) = 1

Tactic:
have : b ri = v i := by simp [b, ri]

Goal state after:
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
b : Basis (↑(hli.extend ⋯)) K V := Basis.mk ⋯ ⋯
i : ι
hi : v i ∈ hli.extend ⋯
ri : ↑(hli.extend ⋯) := ⟨v i, hi⟩
this : b ri = v i
⊢ ((b.constr K) 1) (v i) = 1
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

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

Tactic:
rw [sub_def, ← Category.comp_id a, ← prod.comp_lift, Category.assoc, diag_σ, comp_zero]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (imageIsoImage f).hom ≫ Limits.image.ι f = kernel.ι (cokernel.π f)

Tactic:
simp only [IsImage.isoExt_hom, IsImage.lift_ι, imageStrongEpiMonoFactorisation_m]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
⊢ S.g.op ≫ S.f.op = 0

Tactic:
by simp only [← op_comp, S.zero]; rfl

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

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
eq1 : (h b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
eq2 : (g b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩
⊢ (h b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = (g b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩)

Tactic:
DFunLike.congr_fun hb

Goal state after:
A B : GrpCat
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
eq1 : (h b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
eq2 : (g b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩
⊢ (g b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = (g b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩)
Module: Mathlib.Algebra.Homology.ShortComplex.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S✝ S₁ S₂ S₃ : ShortComplex C
S : ShortComplex Cᵒᵖ
⊢ S.g.unop ≫ S.f.unop = 0

Tactic:
simp only [← unop_comp, S.zero]; rfl

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

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
inst✝ : Epi f
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
dsimp [Function.Surjective]

Goal state after:
A B : GrpCat
f : A ⟶ B
inst✝ : Epi f
⊢ ∀ (b : ↑B), ∃ a, (ConcreteCategory.hom f) a = b
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
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
T : C
φ : T ⟶ S.X₂
⊢ φ ≫ S.g = 0

Tactic:
simp [hg]

Goal state after:
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
h : S.RightHomologyData
A : C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ Cofork.π c ≫ 𝟙 c.pt ≫ (hc.ofIsoColimit (Cofork.ext (Iso.refl c.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯) =
    Cofork.π c ≫ 0

Tactic:
simp [hg]

Goal state after:
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
h : S.RightHomologyData
A : C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ Cofork.π c ≫ (hc.ofIsoColimit (Cofork.ext (Iso.refl c.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯) = Cofork.π c ≫ 0

Tactic:
simp [hg]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ h.leftHomologyIso.hom ≫ h.homologyIso.inv = S.leftHomologyIso.hom

Tactic:
dsimp only [homologyIso]
  simp only [Iso.trans_inv, Iso.symm_inv, Iso.hom_inv_id_assoc]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ h.rightHomologyIso.hom ≫ h.homologyIso.inv = S.rightHomologyIso.hom

Tactic:
dsimp only [homologyIso]
  simp only [Iso.trans_inv, Iso.symm_inv, Iso.hom_inv_id_assoc]

Goal state after:
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 : ShortComplex C
inst✝¹ : S.HasRightHomology
inst✝ : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
⊢ HasKernel (cokernel.desc S.f S.g ⋯)

Tactic:
have : HasLimit (parallelPair h.g' 0) := ⟨⟨⟨_, h.hι'⟩⟩⟩

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasRightHomology
inst✝ : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
this : HasLimit (parallelPair h.g' 0)
⊢ HasKernel (cokernel.desc S.f S.g ⋯)
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 : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ F.map (leftRightHomologyComparison' hₗ hᵣ) = leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)

Tactic:
apply Cofork.IsColimit.hom_ext (hₗ.map F).hπ

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ Cofork.π (CokernelCofork.ofπ (hₗ.map F).π ⋯) ≫ F.map (leftRightHomologyComparison' hₗ hᵣ) =
    Cofork.π (CokernelCofork.ofπ (hₗ.map F).π ⋯) ≫ leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (-a + a).τ₁ = Hom.τ₁ 0

Tactic:
apply neg_add_cancel

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

Goal state before:
pp: case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (-a + a).τ₂ = Hom.τ₂ 0

Tactic:
apply neg_add_cancel

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

Goal state before:
pp: case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (-a + a).τ₃ = Hom.τ₃ 0

Tactic:
apply neg_add_cancel

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = kernel.lift γ f' ⋯ ≫ kernel.ι γ
wπ : f' ≫ cokernel.π (kernel.ι γ) = 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso (limit.isLimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0))
he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel
fac : f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ
hπ : IsColimit (CokernelCofork.ofπ (cokernel.π (kernel.ι γ)) wπ)
⊢ S.LeftHomologyData

Tactic:
exact
    { K := kernel S.g,
      H := Abelian.coimage (kernel.ι S.g ≫ cokernel.π S.f)
      i := kernel.ι _,
      π := cokernel.π _
      wi := kernel.condition _
      hi := kernelIsKernel _
      wπ := wπ
      hπ := hπ }

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₂
h₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ S₁.g ≫ h₁₂.h₂ + h₁₂.h₁ ≫ S₂.f + (S₁.g ≫ h₂₃.h₂ + h₂₃.h₁ ≫ S₂.f + φ₃.τ₂) =
    S₁.g ≫ h₁₂.h₂ + S₁.g ≫ h₂₃.h₂ + (h₁₂.h₁ + h₂₃.h₁) ≫ S₂.f + φ₃.τ₂

Tactic:
add_comp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ S₁.g ≫ h₁₂.h₂ + h₁₂.h₁ ≫ S₂.f + (S₁.g ≫ h₂₃.h₂ + h₂₃.h₁ ≫ S₂.f + φ₃.τ₂) =
    S₁.g ≫ h₁₂.h₂ + S₁.g ≫ h₂₃.h₂ + (h₁₂.h₁ ≫ S₂.f + h₂₃.h₁ ≫ S₂.f) + φ₃.τ₂
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₂
h₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ h₁₂.h₃ + h₁₂.h₂ ≫ S₂.g + (h₂₃.h₃ + h₂₃.h₂ ≫ S₂.g + φ₃.τ₃) = h₁₂.h₃ + h₂₃.h₃ + (h₁₂.h₂ + h₂₃.h₂) ≫ S₂.g + φ₃.τ₃

Tactic:
add_comp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ h₁₂.h₃ + h₁₂.h₂ ≫ S₂.g + (h₂₃.h₃ + h₂₃.h₂ ≫ S₂.g + φ₃.τ₃) = h₁₂.h₃ + h₂₃.h₃ + (h₁₂.h₂ ≫ S₂.g + h₂₃.h₂ ≫ S₂.g) + φ₃.τ₃
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₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ + (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
    S₁.g ≫ h.h₂ + S₁.g ≫ h'.h₂ + (h.h₁ + h'.h₁) ≫ S₂.f + (φ₂.τ₂ + φ₄.τ₂)

Tactic:
add_comp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ + (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
    S₁.g ≫ h.h₂ + S₁.g ≫ h'.h₂ + (h.h₁ ≫ S₂.f + h'.h₁ ≫ S₂.f) + (φ₂.τ₂ + φ₄.τ₂)
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₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ + (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) = h.h₃ + h'.h₃ + (h.h₂ + h'.h₂) ≫ S₂.g + (φ₂.τ₃ + φ₄.τ₃)

Tactic:
add_comp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ + (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) =
    h.h₃ + h'.h₃ + (h.h₂ ≫ S₂.g + h'.h₂ ≫ S₂.g) + (φ₂.τ₃ + φ₄.τ₃)
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
⊢ ∃ f', f' ≫ g = f

Tactic:
by
    rcases hP.factors (adj.unit.app P ≫ G.map f) (G.map g) with ⟨f', hf'⟩
    use F.map f' ≫ adj.counit.app _
    rw [Category.assoc, ← Adjunction.counit_naturality, ← Category.assoc, ← F.map_comp, hf']
    simp

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

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : Retract X Y
p : Projective Y
A B : C
f : X ⟶ B
e : A ⟶ B
x✝ : Epi e
g : Y ⟶ A
hg : g ≫ e = h.r ≫ f
⊢ (h.i ≫ g) ≫ e = f

Tactic:
simp [hg]

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₂
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₂ = S₁.g ≫ h₂ + h₁ ≫ S₂.f + Hom.τ₂ 0

Tactic:
by rw [nullHomotopic_τ₂, zero_τ₂, add_zero]; abel

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₂
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃ = h₃ + h₂ ≫ S₂.g + Hom.τ₃ 0

Tactic:
rw [nullHomotopic_τ₃, zero_τ₃, add_zero]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ h₂ ≫ S₂.g + h₃ = h₃ + h₂ ≫ S₂.g
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: 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

Tactic:
exact sup_factors_of_factors_right (ih ⟨j, ⟨m, h⟩⟩)

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

Goal state before:
pp: case some
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
Z✝ : C
u v : Z✝ ⟶ widePullback s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
val✝ : ↑(⇑(equivShrink (Subobject A)) '' s)
⊢ u ≫ limit.π (wideCospan s) (some val✝) ≫ ((equivShrink (Subobject A)).symm ↑val✝).arrow =
    v ≫ limit.π (wideCospan s) (some val✝) ≫ ((equivShrink (Subobject A)).symm ↑val✝).arrow

Tactic:
limit.w (wideCospan s) (WidePullbackShape.Hom.term _)

Goal state after:
case some
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
Z✝ : C
u v : Z✝ ⟶ widePullback s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
val✝ : ↑(⇑(equivShrink (Subobject A)) '' s)
⊢ u ≫ limit.π (wideCospan s) none = v ≫ limit.π (wideCospan s) none
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

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
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F₁ F₂ : D ⥤ H
G : C ⥤ H
β : F₁ ⟶ F₂
f : F₂ ⟶ L.ran.obj G
⊢ ((L.ran.obj G).homEquivOfIsRightKanExtension (L.ranCounit.app G) F₁).symm.symm (β ≫ f) =
    ((whiskeringLeft C D H).obj L).map β ≫
      ((L.ran.obj G).homEquivOfIsRightKanExtension (L.ranCounit.app G) F₂).symm.symm f

Tactic:
dsimp [homEquivOfIsRightKanExtension]

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
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F₁ F₂ : D ⥤ H
G : C ⥤ H
β : F₁ ⟶ F₂
f : F₂ ⟶ L.ran.obj G
⊢ (L.whiskerLeft β ≫ L.whiskerLeft f) ≫ L.ranCounit.app G = L.whiskerLeft β ≫ L.whiskerLeft f ≫ L.ranCounit.app G
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

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
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : D ⥤ H
G₁ G₂ : C ⥤ H
β : ((whiskeringLeft C D H).obj L).obj F ⟶ G₁
f : G₁ ⟶ G₂
X : C
⊢ (L.whiskerLeft (((L.ran.obj G₂).homEquivOfIsRightKanExtension (L.ranCounit.app G₂) F).symm (β ≫ f)) ≫
          L.ranCounit.app G₂).app
      X =
    (L.whiskerLeft (((L.ran.obj G₁).homEquivOfIsRightKanExtension (L.ranCounit.app G₁) F).symm β ≫ L.ran.map f) ≫
          L.ranCounit.app G₂).app
      X

Tactic:
dsimp [homEquivOfIsRightKanExtension]

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
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : D ⥤ H
G₁ G₂ : C ⥤ H
β : ((whiskeringLeft C D H).obj L).obj F ⟶ G₁
f : G₁ ⟶ G₂
X : C
⊢ ((L.ran.obj G₂).liftOfIsRightKanExtension (L.ranCounit.app G₂) F (β ≫ f)).app (L.obj X) ≫ (L.ranCounit.app G₂).app X =
    (((L.ran.obj G₁).liftOfIsRightKanExtension (L.ranCounit.app G₁) F β).app (L.obj X) ≫ (L.ran.map f).app (L.obj X)) ≫
      (L.ranCounit.app G₂).app X
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
⊢ IsColimit ((prod.functor.obj F ⋙ (evaluation C D).obj k).mapCocone c)

Tactic:
let :=
              isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t

Goal state after:
C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) :=
  isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
⊢ IsColimit ((prod.functor.obj F ⋙ (evaluation C D).obj k).mapCocone c)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ L.whiskerLeft e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) := ⋯
⊢ F₂'.IsLeftKanExtension α₂ → F₁'.IsLeftKanExtension α₁

Tactic:
exact fun _ => ⟨⟨eq.2 (isUniversalOfIsLeftKanExtension F₂' α₂)⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
⊢ Unique ((precomp₂ L' α).obj b ⟶ y)

Tactic:
let u : L'.LeftExtension F₁ :=
      mk y.right <|
        hα.desc <| LeftExtension.mk _ <|
          y.hom ≫ (L.associator L' y.right).hom

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
⊢ Unique ((precomp₂ L' α).obj b ⟶ y)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsSeparating
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g

pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCoseparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g

Tactic:
· refine Quiver.Hom.op_inj (hP _ _ fun G hG h => Quiver.Hom.unop_inj ?_)
    simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ hG _

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCoseparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsCoseparating
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g

pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsSeparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g

Tactic:
· refine Quiver.Hom.op_inj (hP _ _ fun G hG h => Quiver.Hom.unop_inj ?_)
    simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ hG _

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsSeparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case refine_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk f) ≤
    { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk g)

Tactic:
· refine Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).right ?_
      exact congr_arg CommaMorphism.right (Subobject.ofMkLEMk_comp h)

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

Goal state before:
pp: case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ IsSeparator (AddCommGrpCat.of (ULift.{u, 0} ℤ))

Tactic:
intro A B f g h

Goal state after:
case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
A B : AddCommGrpCat
f g : A ⟶ B
h : ∀ (G : AddCommGrpCat), ObjectProperty.singleton (AddCommGrpCat.of (ULift.{u, 0} ℤ)) G → ∀ (h : G ⟶ A), h ≫ f = h ≫ g
⊢ f = g