mathlib-initiative/mathlib-tactics huggingface dataset:
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₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ + φ₃.τ₁ = S₁.f ≫ (h.h₁ + h'.h₁) + (h.h₀ + h'.h₀) + (φ₂.τ₁ + φ₄.τ₁)

Tactic:
h'.comm₁,

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₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ + (S₁.f ≫ h'.h₁ + h'.h₀ + φ₄.τ₁) = S₁.f ≫ (h.h₁ + h'.h₁) + (h.h₀ + h'.h₀) + (φ₂.τ₁ + φ₄.τ₁)
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₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ - φ₃.τ₁ = S₁.f ≫ (h.h₁ - h'.h₁) + (h.h₀ - h'.h₀) + (φ₂.τ₁ - φ₄.τ₁)

Tactic:
h'.comm₁,

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₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ - (S₁.f ≫ h'.h₁ + h'.h₀ + φ₄.τ₁) = S₁.f ≫ (h.h₁ - h'.h₁) + (h.h₀ - h'.h₀) + (φ₂.τ₁ - φ₄.τ₁)
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : F.PreservesEpimorphisms
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
g : P ⟶ X✝
f : E✝ ⟶ X✝
x✝ : Epi f
⊢ ∃ f', f' ≫ f = g

Tactic:
obtain ⟨h, fac⟩ := hP.factors (F.map g) (F.map f)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : F.PreservesEpimorphisms
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
g : P ⟶ X✝
f : E✝ ⟶ X✝
x✝ : Epi f
h : F.obj P ⟶ F.obj E✝
fac : h ≫ F.map f = F.map g
⊢ ∃ f', f' ≫ f = g
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : EnoughInjectives C
X : C
h : IsZero X
this : Injective X
⊢ IsZero X → IsZero { J := X, injective := ⋯, f := 𝟙 X, mono := ⋯ }.J

Tactic:
tauto

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : EnoughInjectives C
X : C
h : ¬IsZero X
⊢ IsZero X → IsZero ⋯.some.J

Tactic:
tauto

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
⊢ h₁ ≫ S₂.f + S₁.g ≫ h₂ = S₁.g ≫ h₂ + h₁ ≫ S₂.f + Hom.τ₂ 0

Tactic:
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₂.f + S₁.g ≫ h₂ = S₁.g ≫ h₂ + h₁ ≫ S₂.f + 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
⊢ S.op.Exact

Tactic:
by
  obtain ⟨h, z⟩ := h
  exact ⟨⟨h.op, (IsZero.of_iso z h.iso.symm).op⟩⟩

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

Goal state before:
pp: case mp
S : ShortComplex Ab
x₁ : ↑S.X₁
h :
  (ConcreteCategory.hom S.g) ((ConcreteCategory.hom S.f) x₁) = 0 →
    ∃ x₁_1, (ConcreteCategory.hom S.f) x₁_1 = (ConcreteCategory.hom S.f) x₁
⊢ (ConcreteCategory.hom S.g) ((ConcreteCategory.hom S.f) x₁) = 0

Tactic:
simp only [ab_zero_apply]

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

Goal state before:
pp: case mpr
S : ShortComplex Ab
x₂ : ↑S.X₂
⊢ ((ConcreteCategory.hom S.g) x₂ = 0 ↔ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f)) →
    (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂

Tactic:
tauto

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 S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ e.inv.τ₁ ≫ e.hom.τ₁ = 𝟙 S₂.X₁

Tactic:
← comp_τ₁,

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 S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ (e.inv ≫ e.hom).τ₁ = 𝟙 S₂.X₁
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: case inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ False

Tactic:
apply hf

Goal state after:
case inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ IsIso f
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : HasPullbacks C
x : Subobject X
⊢ (pullback (𝟙 X)).obj x = x

Tactic:
induction x using Quotient.inductionOn' with | _ f
   =>  _ 

Goal state after:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : HasPullbacks C
f : MonoOver X
⊢ (pullback (𝟙 X)).obj (Quotient.mk'' f) = Quotient.mk'' f
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
x : Subobject X
⊢ (map (𝟙 X)).obj x = x

Tactic:
induction x using Quotient.inductionOn' with | _ f
   =>  _ 

Goal state after:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
f : MonoOver X
⊢ (map (𝟙 X)).obj (Quotient.mk'' f) = Quotient.mk'' f
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₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
this : Mono φ.τ₂.op ↔ Epi φ.τ₂
⊢ { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := ⋯ }.unop.Exact ∧
      Mono (opMap φ).τ₂ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ }.Exact ∧ Epi φ.τ₂

Tactic:
tauto

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ f ≫ g ≫ h = 0

Tactic:
by simp [reassoc_of% w]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasCokernels C
X : C
⊢ ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g],
    Subobject.mk f ≤ Subobject.mk g →
      Subobject.lift (fun x f x_1 ↦ Subobject.mk (cokernel.π f).op) ⋯ (Subobject.mk f) ≤
        Subobject.lift (fun x f x_1 ↦ Subobject.mk (cokernel.π f).op) ⋯ (Subobject.mk g)

Tactic:
by
      intro A B f g hf hg h
      dsimp only [Subobject.lift_mk]
      refine Subobject.mk_le_mk_of_comm (cokernel.desc f (cokernel.π g) ?_).op ?_
      · rw [← Subobject.ofMkLEMk_comp h, Category.assoc, cokernel.condition, comp_zero]
      · exact Quiver.Hom.unop_inj (cokernel.π_desc _ _ _)

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✝¹ : HasInitial C
inst✝ : InitialMonoClass C
X : C
⊢ ∀ (a : Subobject X), Quotient.mk'' ⊥ ≤ a

Tactic:
refine Quotient.ind' fun f => ?_
    exact ⟨MonoOver.botLE f⟩

Goal state after:
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_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g),
      ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g),
      ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F, PreservesFiniteColimits F].TFAE

Tactic:
tfae_have 2 → 3
  | hF, X, Y, f => by
    refine preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f) ?_
    apply (CokernelCofork.isColimitMapCoconeEquiv _ F).2
    let S := ShortComplex.mk _ _ (cokernel.condition f)
    let hS := hF S ⟨exact_cokernel f, inferInstance⟩
    have : Epi (S.map F).g := hS.2
    exact hS.1.gIsCokernel

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_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
tfae_2_to_3 :
  (∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)) →
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g),
      ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g),
      ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F, PreservesFiniteColimits F].TFAE
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsInitial X
this : ∀ (S : Subobject X), S = mk (𝟙 X)
⊢ ∀ (a b : Subobject X), a = b

Tactic:
simp [this]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : C ⥤ D
d : D
⊢ (map (𝟙 d)).toCatHom = 𝟙 (Cat.of (CostructuredArrow T d))

Tactic:
by
    ext
    exact Functor.ext (fun ⟨_, _, _⟩ => by simp [CostructuredArrow.map, Comma.mapRight])

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

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
a✝ : L'.HasPointwiseRightKanExtensionAt F Y'
⊢ L.HasPointwiseRightKanExtensionAt F Y

Tactic:
exact hasPointwiseRightKanExtensionAt_of_equivalence L' L F E.symm
      (isoWhiskerRight eL.symm _ ≪≫ Functor.associator _ _ _ ≪≫
        isoWhiskerLeft L E.unitIso.symm ≪≫ L.rightUnitor) Y' Y
      (E.inverse.mapIso e.symm ≪≫ E.unitIso.symm.app Y)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : CostructuredArrow L Y₁
⊢ colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j ≫
      colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
        { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
          ι :=
            { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map (f ≫ f')).obj g),
              naturality := ⋯ } } =
    colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j ≫
      colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
          { pt := colimit (CostructuredArrow.proj L Y₂ ⋙ F),
            ι :=
              { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g),
                naturality := ⋯ } } ≫
        colimit.desc (CostructuredArrow.proj L Y₂ ⋙ F)
          { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
            ι :=
              { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map f').obj g),
                naturality := ⋯ } }

Tactic:
simp only [colimit.ι_desc, colimit.ι_desc_assoc, comp_obj, CostructuredArrow.proj_obj]

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : CostructuredArrow L Y₁
⊢ colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map (f ≫ f')).obj j) =
    colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map f').obj ((CostructuredArrow.map f).obj j))
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 ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
t : C
this :
  α.app t ≫ b.hom.app (L.obj t) ≫ (StructuredArrow.Hom.right u).app (L'.obj (L.obj t)) = α.app t ≫ y.hom.app (L.obj t)
⊢ (StructuredArrow.hom (mk F₁ α) ≫
          ((whiskeringLeft C D H).obj L).map
            (StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (StructuredArrow.Hom.right u))).app
      t =
    (StructuredArrow.hom (mk F₁ α) ≫ ((whiskeringLeft C D H).obj L).map (StructuredArrow.hom y)).app t

Tactic:
simp [this]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝² : HasFiniteLimits C
this✝¹ : HasProductsOfShape (Subtype P) C
this✝ : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
⊢ (A : C) → Unique (Subobject.underlying.obj ⊥ ⟶ A)

Tactic:
have := hP.mono_productTo

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝³ : HasFiniteLimits C
this✝² : HasProductsOfShape (Subtype P) C
this✝¹ : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this✝ : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
this : ∀ (X : C) [inst : HasProduct (P.productToFamily X)], Mono (P.productTo X)
⊢ (A : C) → Unique (Subobject.underlying.obj ⊥ ⟶ A)
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono

Goal state before:
pp: K : Type u
inst✝⁵ : Category.{v, u} K
C : Type u'
inst✝⁴ : Category.{v', u'} C
D : Type u''
inst✝³ : Category.{v'', u''} D
F G : K ⥤ C
f : F ⟶ G
inst✝² : HasPushouts C
inst✝¹ : Epi f
H : C ⥤ D
inst✝ : H.PreservesEpimorphisms
⊢ Epi (whiskerRight f H)

Tactic:
have : ∀ X, Epi ((whiskerRight f H).app X) := by intros; dsimp; infer_instance

Goal state after:
K : Type u
inst✝⁵ : Category.{v, u} K
C : Type u'
inst✝⁴ : Category.{v', u'} C
D : Type u''
inst✝³ : Category.{v'', u''} D
F G : K ⥤ C
f : F ⟶ G
inst✝² : HasPushouts C
inst✝¹ : Epi f
H : C ⥤ D
inst✝ : H.PreservesEpimorphisms
this : ∀ (X : K), Epi ((whiskerRight f H).app X)
⊢ Epi (whiskerRight f H)
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx : (AddCommGrpCat.Hom.hom (colimMap S.g)) ((ConcreteCategory.hom (colimit.ι S.X₂ j)) y) = 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range

Tactic:
rw [← ConcreteCategory.comp_apply, colimMap_eq, colimit.ι_map, ConcreteCategory.comp_apply,
      ← map_zero (colimit.ι S.X₃ j).hom] at hx

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.g.app k)) ((ConcreteCategory.hom (S.X₂.map e₁)) y) = 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range

Tactic:
rcases hS k hk with ⟨t, ht⟩

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.g.app k)) ((ConcreteCategory.hom (S.X₂.map e₁)) y) = 0
t : ↑(S.map ((evaluation J AddCommGrpCat).obj k)).X₁
ht : (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj k)).f) t = (ConcreteCategory.hom (S.X₂.map e₁)) y
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
c : Cofan f
hc : IsColimit c
⊢ IsSeparator c.pt ↔ (ObjectProperty.ofObj f).IsSeparating

Tactic:
by
  refine ⟨fun h X Y u v huv => ?_, fun h => isSeparator_of_isColimit_cofan h hc⟩
  refine h.def _ _ fun g => hc.hom_ext fun b => ?_
  simpa using! huv (f b.as) (by simp) (c.inj _ ≫ g)

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

Goal state before:
pp: case e'_2.mpr.left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ G = WalkingPair.rec G H WalkingPair.left ∨ H = WalkingPair.rec G H WalkingPair.left

Tactic:
tauto

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

Goal state before:
pp: case e'_2.mpr.right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ G = WalkingPair.rec G H WalkingPair.right ∨ H = WalkingPair.rec G H WalkingPair.right

Tactic:
tauto

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

Goal state before:
pp: case e'_2.mpr.left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ G = WalkingPair.rec G H WalkingPair.left ∨ H = WalkingPair.rec G H WalkingPair.left

Tactic:
tauto

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

Goal state before:
pp: case e'_2.mpr.right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ G = WalkingPair.rec G H WalkingPair.right ∨ H = WalkingPair.rec G H WalkingPair.right

Tactic:
tauto

Goal state after:
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case pos
n₁ n₂ : ℤ
h₂ : Even n₂
⊢ Even n₁ ↔ (Even n₁ ↔ Even n₂)

Tactic:
tauto

Goal state after:
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case neg
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ Odd n₁ ↔ (¬Odd n₁ ↔ ¬Odd n₂)

Tactic:
tauto

Goal state after:
Module: Mathlib.Data.Nat.Periodic

Goal state before:
pp: n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ (filter p (Ico n (n + a))).card = {x ∈ Finset.range a | p x}.card

Tactic:
Finset.card,

Goal state after:
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ (filter p (Ico n (n + a))).card = {x ∈ Finset.range a | p x}.val.card
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case basic
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s✝ : Set α
h : s✝ ∈ insert A S
⊢ s✝ ∈ S ∨ ∃ Q ∈ S, s✝ = A ∩ Q

Tactic:
cases h

Goal state after:
case basic.inl
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s✝ : Set α
h✝ : s✝ = A
⊢ s✝ ∈ S ∨ ∃ Q ∈ S, s✝ = A ∩ Q

case basic.inr
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s✝ : Set α
h✝ : s✝ ∈ S
⊢ s✝ ∈ S ∨ ∃ Q ∈ S, s✝ = A ∩ Q
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case inter
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
a✝ : finiteInterClosure (insert A S) T2
h1 : T1 ∈ S ∨ ∃ Q ∈ S, T1 = A ∩ Q
h2 : T2 ∈ S ∨ ∃ Q ∈ S, T2 = A ∩ Q
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q

Tactic:
rcases h1 with (h | ⟨Q, hQ, rfl⟩) <;> rcases h2 with (i | ⟨R, hR, rfl⟩)

Goal state after:
case inter.inl.inl
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
a✝ : finiteInterClosure (insert A S) T2
h : T1 ∈ S
i : T2 ∈ S
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q

case inter.inl.inr
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
h : T1 ∈ S
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ T1 ∩ (A ∩ R) ∈ S ∨ ∃ Q ∈ S, T1 ∩ (A ∩ R) = A ∩ Q

case inter.inr.inl
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T2
Q : Set α
hQ : Q ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ Q)
i : T2 ∈ S
⊢ A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ T2 = A ∩ Q_1

case inter.inr.inr
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
a✝¹ : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ A ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ (A ∩ R) = A ∩ Q_1
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atTop

Tactic:
rw [← prod_atTop_atTop_eq]
  exact hf.prodMap hg

Goal state after: