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

Tactic:
comp_add

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₁ + S₁.f ≫ h₂₃.h₁ + (h₁₂.h₀ + h₂₃.h₀) + φ₃.τ₁
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₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ (S₁.mapCyclesIso F).hom ≫ F.map (cyclesMap φ) ≫ (S₂.mapCyclesIso F).inv =
    (S₁.mapCyclesIso F).hom ≫ (S₁.mapCyclesIso F).inv ≫ cyclesMap (F.mapShortComplex.map φ)

Tactic:
← mapCyclesIso_hom_naturality_assoc,

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ cyclesMap (F.mapShortComplex.map φ) ≫ (S₂.mapCyclesIso F).hom ≫ (S₂.mapCyclesIso F).inv =
    (S₁.mapCyclesIso F).hom ≫ (S₁.mapCyclesIso F).inv ≫ cyclesMap (F.mapShortComplex.map φ)
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₀ + φ₄.τ₁) = S₁.f ≫ (h.h₁ + h'.h₁) + (h.h₀ + h'.h₀) + (φ₂.τ₁ + φ₄.τ₁)

Tactic:
comp_add

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₁ + S₁.f ≫ h'.h₁ + (h.h₀ + h'.h₀) + (φ₂.τ₁ + φ₄.τ₁)
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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt ≫ π ≫ (isoHomology S hkf hcc fac).hom = 0 ≫ (isoHomology S hkf hcc fac).hom

Tactic:
id_comp,

Goal state after:
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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ hkf.lift (KernelFork.ofι S.f ⋯) ≫ π ≫ (isoHomology S hkf hcc fac).hom = 0 ≫ (isoHomology S hkf hcc fac).hom
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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ ι ≫ 𝟙 cc.pt ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) = 0

Tactic:
id_comp,

Goal state after:
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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ ι ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) = 0
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

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.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
⊢ IsIso S.f → IsZero S.X₃

pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
⊢ IsZero S.X₃ → IsIso S.f

Tactic:
· intro hf
    simp only [IsZero.iff_id_eq_zero, ← cancel_epi S.g, ← cancel_epi S.f,
      S.zero_assoc, zero_comp]

Goal state after:
case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
⊢ IsZero S.X₃ → IsIso S.f
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
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : S.Exact
⊢ a ≫ b = 0

Tactic:
rw [exact_iff_iCycles_pOpcycles_zero] at eq

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : S.iCycles ≫ S.pOpcycles = 0
⊢ a ≫ b = 0
Module: Mathlib.CategoryTheory.Adjunction.Restrict

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ R.obj Y
⊢ (Trans.trans
          (Trans.trans
            (Trans.trans (Trans.trans hiD.homEquiv ((comm1.symm.app X').homCongr (Iso.refl (iD.obj Y))))
              (adj.homEquiv (iC.obj X') (iD.obj Y)))
            ((Iso.refl (iC.obj X')).homCongr (comm2.app Y)))
          hiC.homEquiv.symm).symm
      (f ≫ g) =
    L.map f ≫
      (Trans.trans
            (Trans.trans
              (Trans.trans (Trans.trans hiD.homEquiv ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y))))
                (adj.homEquiv (iC.obj X) (iD.obj Y)))
              ((Iso.refl (iC.obj X)).homCongr (comm2.app Y)))
            hiC.homEquiv.symm).symm
        g

Tactic:
apply hiD.map_injective
        simpa [Trans.trans] using (comm1.inv.naturality_assoc f _).symm

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₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = e.inv.τ₂ ≫ 𝟙 S₁.X₂ ≫ e.hom.τ₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂

Tactic:
id_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₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = e.inv.τ₂ ≫ e.hom.τ₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝³ : Mono S₁.op.f
this✝² : Mono S₂.op.f
this✝¹ : Mono (opMap φ).τ₁
this✝ : Mono (opMap φ).τ₃
this : Mono (opMap φ).τ₂
⊢ Epi φ.τ₂

Tactic:
exact unop_epi_of_mono (opMap φ).τ₂

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✝ : Balanced C
S : ShortComplex C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
⊢ 𝟙 S.X₂ ≫ S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃

Tactic:
id_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✝ : Balanced C
S : ShortComplex C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
⊢ S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsInitial X
A : C
i : A ⟶ X
w✝ : Mono i
fac : hX.to A ≫ i = 𝟙 X
⊢ i ≫ 𝟙 X = 𝟙 A ≫ i

Tactic:
id_comp,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsInitial X
A : C
i : A ⟶ X
w✝ : Mono i
fac : hX.to A ≫ i = 𝟙 X
⊢ i ≫ 𝟙 X = i
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
E E' : L.RightExtension F
Y : D
g₁ g₂ : StructuredArrow Y L
φ : g₁ ⟶ g₂
⊢ 𝟙 ((CostructuredArrow.left E).obj Y) ≫
      (CostructuredArrow.left E).map g₂.hom ≫ (CostructuredArrow.hom E).app g₂.right =
    (CostructuredArrow.left E).map g₁.hom ≫ (CostructuredArrow.hom E).app g₁.right ≫ F.map φ.right

Tactic:
id_comp,

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
E E' : L.RightExtension F
Y : D
g₁ g₂ : StructuredArrow Y L
φ : g₁ ⟶ g₂
⊢ (CostructuredArrow.left E).map g₂.hom ≫ (CostructuredArrow.hom E).app g₂.right =
    (CostructuredArrow.left E).map g₁.hom ≫ (CostructuredArrow.hom E).app g₁.right ≫ F.map φ.right
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✝³ : L.Full
inst✝² : L.Faithful
F : C ⥤ H
inst✝¹ : L.HasPointwiseRightKanExtension F
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
⊢ IsIso ((L.ranAdjunction H).counit.app F)

Tactic:
rw [ranAdjunction_counit]

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✝³ : L.Full
inst✝² : L.Faithful
F : C ⥤ H
inst✝¹ : L.HasPointwiseRightKanExtension F
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
⊢ IsIso (L.ranCounit.app F)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: case e_7
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₁
⊢ (CostructuredArrow.map (f ≫ f')).obj j = (CostructuredArrow.map f').obj ((CostructuredArrow.map f).obj j)

Tactic:
apply CostructuredArrow.map_comp

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

Goal state before:
pp: case e_7
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
X : D
j : CostructuredArrow L X
⊢ j = CostructuredArrow.mk (𝟙 (L.obj j.left) ≫ j.hom)

Tactic:
id_comp,

Goal state after:
case e_7
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
X : D
j : CostructuredArrow L X
⊢ j = CostructuredArrow.mk j.hom
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : HasColimitsOfShape J D
F : C ⥤ E
K : J ⥤ E ⥤ D
c : Cocone K
hc : IsColimit c
⊢ IsColimit (((whiskeringLeft C E D).obj F).mapCocone c)

Tactic:
apply evaluationJointlyReflectsColimits

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : HasColimitsOfShape J D
F : C ⥤ E
K : J ⥤ E ⥤ D
c : Cocone K
hc : IsColimit c
⊢ (k : C) → IsColimit (((evaluation C D).obj k).mapCocone (((whiskeringLeft C E D).obj F).mapCocone c))
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: 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
α₁ : L ⋙ F₁' ⟶ F₁
α₂ : L ⋙ F₂' ⟶ F₂
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : L.whiskerLeft e'.hom ≫ α₂ = α₁ ≫ e.hom
⊢ F₁'.IsRightKanExtension α₁ ↔ F₂'.IsRightKanExtension α₂

Tactic:
by
  let eq := RightExtension.isUniversalEquivOfIso₂ (RightExtension.mk _ α₁)
    (RightExtension.mk _ α₂) e e' h
  constructor
  · exact fun _ => ⟨⟨eq.1 (isUniversalOfIsRightKanExtension F₁' α₁)⟩⟩
  · exact fun _ => ⟨⟨eq.2 (isUniversalOfIsRightKanExtension F₂' α₂)⟩⟩

Goal state after:
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✝² : HasPullbacks C
inst✝¹ : Mono f
H : C ⥤ D
inst✝ : H.PreservesMonomorphisms
⊢ Mono (whiskerRight f H)

Tactic:
by
  have : ∀ X, Mono ((whiskerRight f H).app X) := by intros; dsimp; infer_instance
  apply NatTrans.mono_of_mono_app

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

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

Tactic:
rintro ⟨⟨_ | _⟩, rfl⟩

Goal state after:
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

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
Module: Mathlib.CategoryTheory.Generator.Basic

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

Tactic:
rintro ⟨⟨_ | _⟩, rfl⟩

Goal state after:
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

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
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
i j : C
f : { as := i } ⟶ { as := j }
⊢ (fun x ↦
        match { as := j }, x with
        | { as := i }, x => ⟨i, x⟩) ∘
      ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
    fun x ↦
    match { as := i }, x with
    | { as := i }, x => ⟨i, x⟩

Tactic:
obtain rfl : i = j := by simpa using Discrete.eq_of_hom f

Goal state after:
C : Type u
F : C → Type v
i : C
f : { as := i } ⟶ { as := i }
⊢ (fun x ↦
        match { as := i }, x with
        | { as := i }, x => ⟨i, x⟩) ∘
      ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
    fun x ↦
    match { as := i }, x with
    | { as := i }, x => ⟨i, x⟩
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C✝ : Type u
F✝ : C✝ → Type v
C : Type u
F : C → Type v
c : Cofan F
i j : C
f : { as := i } ⟶ { as := j }
⊢ (match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) { as := j } with
      | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))) ∘
      ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
    match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) { as := i } with
    | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))

Tactic:
obtain rfl : i = j := by simpa using Discrete.eq_of_hom f

Goal state after:
C✝ : Type u
F✝ : C✝ → Type v
C : Type u
F : C → Type v
c : Cofan F
i : C
f : { as := i } ⟶ { as := i }
⊢ (match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) { as := i } with
      | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))) ∘
      ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
    match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) { as := i } with
    | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
X Y : Type u
x✝¹ : Cocone (pair X Y)
x✝ : (binaryCoproductCocone X Y).pt ⟶ x✝¹.pt
w : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone X Y).ι.app j ≫ x✝ = x✝¹.ι.app j
⊢ x✝ = ↾Sum.elim ⇑(ConcreteCategory.hom (BinaryCofan.inl x✝¹)) ⇑(ConcreteCategory.hom (BinaryCofan.inr x✝¹))

Tactic:
by
    ext ⟨⟩
    exacts [ConcreteCategory.congr_hom (w ⟨left⟩) _, ConcreteCategory.congr_hom (w ⟨right⟩) _]

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

Goal state before:
pp: k : ℤ
⊢ k.negOnePow * k.negOnePow = 1

Tactic:
units_mul_self

Goal state after:
k : ℤ
⊢ 1 = 1
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case pos
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : a = 1
⊢ motive (p ^ n * a)

Tactic:
ha1,

Goal state after:
case pos
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : a = 1
⊢ motive (p ^ n * 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ {a ∈ range (p ^ (n + 1)) | (p ^ (n + 1)).Coprime a} = range (p ^ (n + 1)) \ image (fun x ↦ x * p) (range (p ^ n))

Tactic:
by
          rw [sdiff_eq_filter]
          apply filter_congr
          simp only [mem_range, coprime_pow_left_iff n.succ_pos, mem_image, not_exists,
            hp.coprime_iff_not_dvd]
          intro a ha
          constructor
          · intro hap b h; rcases h with ⟨_, rfl⟩
            exact hap (dvd_mul_left _ _)
          · rintro h ⟨b, rfl⟩
            rw [pow_succ'] at ha
            exact h b ⟨lt_of_mul_lt_mul_left ha (zero_le _), mul_comm _ _⟩

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: c d : ℕ
⊢ ∀ᶠ (n : ℕ) in atTop, c ^ n < (n - d)!

Tactic:
rw [eventually_atTop]
  refine ⟨2 * (c ^ 2 + d + 1), ?_⟩
  intro n hn
  obtain ⟨d', rfl⟩ := Nat.exists_eq_add_of_le hn
  obtain (rfl | c0) := c.eq_zero_or_pos
  · simp [Nat.two_mul, ← Nat.add_assoc, Nat.add_right_comm _ 1, Nat.factorial_pos]
  refine (Nat.le_mul_of_pos_right _ (Nat.pow_pos (n := d') c0)).trans_lt ?_
  convert_to! (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!
  · rw [← pow_mul, ← pow_add]
    congr 1
    lia
  · congr 1
    lia
  refine (lt_of_lt_of_le ?_ Nat.factorial_mul_pow_le_factorial).trans_le <|
    (factorial_le (Nat.le_succ _))
  rw [← one_mul (_ ^ _ : ℕ)]
  apply Nat.mul_lt_mul_of_le_of_lt
  · exact Nat.one_le_of_lt (Nat.factorial_pos _)
  · exact Nat.pow_lt_pow_left (Nat.lt_succ_self _) (Nat.succ_ne_zero _)
  · exact (Nat.factorial_pos _)

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: case insert
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
a✝¹ : Set X
s✝ : Set (Set X)
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ih : (∀ t ∈ s✝, IsOpen[inst✝] t) → IsOpen[inst✝] (⋂₀ s✝)
h : ∀ t ∈ insert a✝¹ s✝, IsOpen[inst✝] t
⊢ IsOpen[inst✝] (⋂₀ insert a✝¹ s✝)

Tactic:
simp only [sInter_insert, forall_mem_insert] at h ⊢

Goal state after:
case insert
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
a✝¹ : Set X
s✝ : Set (Set X)
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ih : (∀ t ∈ s✝, IsOpen[inst✝] t) → IsOpen[inst✝] (⋂₀ s✝)
h : IsOpen[inst✝] a✝¹ ∧ ∀ x ∈ s✝, IsOpen[inst✝] x
⊢ IsOpen[inst✝] (a✝¹ ∩ ⋂₀ s✝)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
⊢ b = a + p + (toIcoDiv hp a b - 1) • p

Tactic:
rw [sub_one_zsmul, add_add_add_comm, add_neg_cancel, add_zero]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
x✝ : toIcoMod hp a b = a
h : toIcoMod hp a b = a := x✝
⊢ b = a + toIcoDiv hp a b • p
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
p : X → Prop
⊢ (∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ∃ᶠ (x : X) in 𝓝 x, p x

Tactic:
rw [← not_iff_not]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
p : X → Prop
⊢ (¬∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ¬∃ᶠ (x : X) in 𝓝 x, p x
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Disjoint (interior s) (frontier s)

Tactic:
rw [disjoint_iff_inter_eq_empty, ← closure_sdiff_interior, sdiff_eq,
    ← inter_assoc, inter_comm, ← inter_assoc, compl_inter_self, empty_inter]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h : IsOpen[inst✝] s
⊢ (closure[inst✝] (s ∩ t))ᶜ ⊆ (s ∩ closure[inst✝] t)ᶜ

Tactic:
by
    simpa only [← interior_compl, compl_inter] using IsClosed.interior_union_left h.isClosed_compl

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
⊢ toIcoMod hp a b + ↑(toIcoDiv hp a b) * p = b

Tactic:
by
  simpa using toIcoMod_add_toIcoDiv_zsmul hp a b

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
⊢ IsInducing (g ∘ f) ↔ IsInducing f

Tactic:
refine ⟨fun h ↦ ?_, hg.comp⟩
  rw [isInducing_iff, hg.eq_induced, induced_compose, h.eq_induced]

Goal state after: