mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
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 ι
⊢ (isoImage S hkf hcc fac).hom ≫ image.ι (S.iCycles ≫ S.pOpcycles) = ι ≫ (S.isoOpcyclesOfIsColimit hcc).hom

Tactic:
apply image.isoStrongEpiMono_hom_comp_ι

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
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 ι
⊢ ((S.isoCyclesOfIsLimit hkf).inv ≫ π) ≫ ι ≫ (S.isoOpcyclesOfIsColimit hcc).hom = S.iCycles ≫ S.pOpcycles
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₃ + (h₁₂.h₂ + h₂₃.h₂) ≫ S₂.g + φ₃.τ₃

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

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 φ₂ φ₃
⊢ h₁₂.h₃ + h₁₂.h₂ ≫ S₂.g + (h₂₃.h₃ + h₂₃.h₂ ≫ S₂.g + φ₃.τ₃) = h₁₂.h₃ + h₂₃.h₃ + (h₁₂.h₂ + h₂₃.h₂) ≫ S₂.g + φ₃.τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: case h₃
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 ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (F.map f ≫
        { τ₁ := colimit.ι (F ⋙ π₁) x✝, τ₂ := colimit.ι (F ⋙ π₂) x✝, τ₃ := colimit.ι (F ⋙ π₃) x✝, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₃ =
    ({ τ₁ := colimit.ι (F ⋙ π₁) x✝¹, τ₂ := colimit.ι (F ⋙ π₂) x✝¹, τ₃ := colimit.ι (F ⋙ π₃) x✝¹, comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        ((const J).obj
              { X₁ := colimit (F ⋙ π₁), X₂ := colimit (F ⋙ π₂), X₃ := colimit (F ⋙ π₃),
                f := colimMap (F.whiskerLeft π₁Toπ₂), g := colimMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).map
          f).τ₃

Tactic:
· simp [← colimit.w (F ⋙ π₃) f]

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 : ShortComplex C
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
⊢ ((S.homologyData.right.map F).homologyIso ≪≫ F.mapIso S.homologyData.right.homologyIso.symm).hom =
    ((S.homologyData.left.map F).homologyIso ≪≫ F.mapIso S.homologyData.left.homologyIso.symm).hom

Tactic:
dsimp only [Iso.trans, Iso.symm, Iso.refl, Functor.mapIso, RightHomologyData.homologyIso,
    rightHomologyIso, RightHomologyData.rightHomologyIso, LeftHomologyData.homologyIso,
    leftHomologyIso, LeftHomologyData.leftHomologyIso]

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
inst✝² : S.HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
⊢ (((S.map F).homologyData.iso.hom ≫
          (rightHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ }
              (S.map F).rightHomologyData (S.map F).homologyData.right).inv) ≫
        (rightHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ }
            (S.map F).rightHomologyData (S.homologyData.right.map F)).hom) ≫
      F.map
        ((rightHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.rightHomologyData
              S.homologyData.right).inv ≫
          (rightHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.rightHomologyData
                S.homologyData.right).hom ≫
            S.homologyData.iso.inv) =
    ((leftHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ }
            (S.map F).leftHomologyData (S.map F).homologyData.left).inv ≫
        (leftHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ }
            (S.map F).leftHomologyData (S.homologyData.left.map F)).hom) ≫
      F.map
        ((leftHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.leftHomologyData
              S.homologyData.left).inv ≫
          (leftHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.leftHomologyData
              S.homologyData.left).hom)
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

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

Tactic:
rw [e.hom.comm₂₃]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
h : S₁.ShortExact
this : Epi S₁.g
⊢ Epi (S₁.g ≫ e.hom.τ₃)
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₂₃ := ⋯ }
b : S'' ⟶ S' := { τ₁ := 𝟙 S''.X₁, τ₂ := 𝟙 S''.X₂, τ₃ := h.right.g', comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ S'.Exact

Tactic:
← ShortComplex.exact_iff_of_epi_of_isIso_of_mono a

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₂₃ := ⋯ }
⊢ S.Exact
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
⊢ S.Exact

Tactic:
(HomologyData.ofIsColimitCokernelCofork S hg _
      (CokernelCofork.IsColimit.ofEpiOfIsZero (CokernelCofork.ofπ (0 : S.X₂ ⟶ 0) comp_zero)
        inferInstance (isZero_zero C))).exact_iff

Goal state after:
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
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 : C
Y : D
f : L.obj X ⟶ Y
⊢ iC.map (((adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y) f) =
    iC.map (hiC.preimage (adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y))

Tactic:
simp only [homEquiv_apply, Functor.map_comp, map_restrictFullyFaithful_unit_app,
    Functor.id_obj, assoc, Functor.FullyFaithful.map_preimage]

Goal state after:
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 : C
Y : D
f : L.obj X ⟶ Y
⊢ adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ comm2.hom.app (L.obj X) ≫ iC.map (R.map f) =
    adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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

Tactic:
rw [← φ.comm₁₂, hf₂, comp_zero]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (pullback g).obj (Quotient.mk'' f₁ ⊓ f₂) = (pullback g).obj (Quotient.mk'' f₁) ⊓ (pullback g).obj f₂

Tactic:
inf_def,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (pullback g).obj ((inf.obj (Quotient.mk'' f₁)).obj f₂) = (pullback g).obj (Quotient.mk'' f₁) ⊓ (pullback g).obj f₂
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (pullback g).obj ((inf.obj (Quotient.mk'' f₁)).obj f₂) = (pullback g).obj (Quotient.mk'' f₁) ⊓ (pullback g).obj f₂

Tactic:
inf_def,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (pullback g).obj ((inf.obj (Quotient.mk'' f₁)).obj f₂) =
    (inf.obj ((pullback g).obj (Quotient.mk'' f₁))).obj ((pullback g).obj f₂)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map g).obj (Quotient.mk'' f₁ ⊓ f₂) = (map g).obj (Quotient.mk'' f₁) ⊓ (map g).obj f₂

Tactic:
inf_def,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map g).obj ((inf.obj (Quotient.mk'' f₁)).obj f₂) = (map g).obj (Quotient.mk'' f₁) ⊓ (map g).obj f₂
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map g).obj ((inf.obj (Quotient.mk'' f₁)).obj f₂) = (map g).obj (Quotient.mk'' f₁) ⊓ (map g).obj f₂

Tactic:
inf_def,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map g).obj ((inf.obj (Quotient.mk'' f₁)).obj f₂) = (inf.obj ((map g).obj (Quotient.mk'' f₁))).obj ((map g).obj f₂)
Module: Mathlib.CategoryTheory.Limits.Filtered

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ IsCofiltered C ↔
    ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))

Tactic:
rw [IsCofiltered.iff_cone_nonempty.{v}]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
⊢ (∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) ↔
    ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan Z
c : Cofan fun x ↦ op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
j : α
⊢ ((f'.proj j).op ≫ (opProductIsoCoproduct' hf' hc).hom) ≫ (opProductIsoCoproduct' hf' hc).inv =
    (f'.π.app { as := j }).op

Tactic:
simp only [Category.assoc, Iso.hom_inv_id, Category.comp_id]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan Z
c : Cofan fun x ↦ op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
j : α
⊢ (f'.proj j).op = (f'.π.app { as := j }).op
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
Y : D
h : E.IsPointwiseLeftKanExtensionAt Y
T : H
f g : (StructuredArrow.right E).obj Y ⟶ T
hfg :
  ∀ ⦃X : C⦄ (φ : L.obj X ⟶ Y),
    (StructuredArrow.hom E).app X ≫ (StructuredArrow.right E).map φ ≫ f =
      (StructuredArrow.hom E).app X ≫ (StructuredArrow.right E).map φ ≫ g
j : CostructuredArrow L Y
⊢ (E.coconeAt Y).ι.app j ≫ f = (E.coconeAt Y).ι.app j ≫ g

Tactic:
simpa using hfg j.hom

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.HasPointwiseRightKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (L.map f ≫ 𝟙 (L.obj X₂))) =
    limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f

Tactic:
rw [comp_id]

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.HasPointwiseRightKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (L.map f)) =
    limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f
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
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
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝² : F'.IsLeftKanExtension α
inst✝¹ : HasColimit F
inst✝ : HasColimit F'
i : C
⊢ colimit.ι F i = α.app i ≫ colimit.ι F' (L.obj i) ≫ (F'.colimitIsoOfIsLeftKanExtension α).hom

Tactic:
ι_colimitIsoOfIsLeftKanExtension_hom

Goal state after:
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
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝² : F'.IsLeftKanExtension α
inst✝¹ : HasColimit F
inst✝ : HasColimit F'
i : C
⊢ colimit.ι F i = colimit.ι F i
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
⊢ Function.LeftInverse
    (fun x ↦
      match x with
      | none => Arrow.mk (𝟙 zero)
      | some none => Arrow.mk (𝟙 one)
      | some (some t) => Arrow.mk (line t))
    fun f ↦
    match f.left, f.right, f.hom with
    | zero, .(zero), Hom.id .(zero) => none
    | one, .(one), Hom.id .(one) => some none
    | zero, one, line t => some (some t)

Tactic:
rintro ⟨(_ | _), _, (_ | _)⟩ <;> rfl

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ (((proj S T).mapIso i.unop).op.hom ≫ g.unop.left.op).unop = f.unop.left.op.unop

Tactic:
have := congr_arg Quiver.Hom.unop hi

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
this : (i.hom ≫ g).unop = f.unop
⊢ (((proj S T).mapIso i.unop).op.hom ≫ g.unop.left.op).unop = f.unop.left.op.unop
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : ObjectProperty C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ underlying.obj Q
this : P.Factors (f ≫ Q.arrow)
g : G ⟶ underlying.obj P
hg : g ≫ P.ofLE Q h₁ = f
⊢ g = P.factorThru (f ≫ Q.arrow) this

Tactic:
simp only [← cancel_mono (Subobject.ofLE _ _ h₁), ← cancel_mono Q.arrow, hg, Category.assoc,
      ofLE_arrow, factorThru_arrow]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
⊢ (hom ((φ.app X).app (F.op.obj (op X)))) { down := 𝟙 (unop (F.op.obj (op X))) } =
    uliftYonedaEquiv
      (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj X) ≫
        F.op.whiskerLeft ((compULiftYonedaIsoULiftYonedaCompLan F).inv.app X ≫ φ.app X))

Tactic:
exact _root_.congr_arg _ (compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id F X).symm

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ IsSeparator (G ⨿ H) ↔ (ObjectProperty.pair G H).IsSeparating

Tactic:
refine (isSeparator_iff_of_isColimit_cofan (coprodIsCoprod G H)).trans ?_
  convert! Iff.rfl
  ext X
  simp only [ObjectProperty.pair_iff, ObjectProperty.ofObj_iff]
  constructor
  · rintro (rfl | rfl); exacts [⟨.left, rfl⟩, ⟨.right, rfl⟩]
  · rintro ⟨⟨_ | _⟩, rfl⟩ <;> tauto

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : HasSeparator Cᵒᵖ
⊢ HasCoseparator C

Tactic:
simp_all

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasCoseparator Cᵒᵖ
⊢ HasSeparator C

Tactic:
simp_all

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasDetector Cᵒᵖ
⊢ HasCodetector C

Tactic:
simp_all

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasCodetector Cᵒᵖ
⊢ HasDetector C

Tactic:
simp_all

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
⊢ ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)

Tactic:
rw [eq_compl_iff_isCompl.mpr h₃.symm]

Goal state after:
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
⊢ ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ (Set.range ⇑(ConcreteCategory.hom c.inl))ᶜ
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝ : Add α
h : Periodic f c
g : β → γ
⊢ Periodic (g ∘ f) c

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝ : Add α
h : Periodic f c
g : β → γ
⊢ Periodic (g ∘ f) c

Tactic:
by
  simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
c : α
inst✝¹ : Add α
inst✝ : Mul β
hf : Periodic f c
hg : Periodic g c
⊢ Periodic (f * g) c

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
c : α
inst✝¹ : Add α
inst✝ : Div β
hf : Periodic f c
hg : Periodic g c
⊢ Periodic (f / g) c

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝¹ : Add α
inst✝ : SMul γ β
h : Periodic f c
a : γ
⊢ Periodic (a • f) c

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝³ : Add α
inst✝² : Monoid γ
inst✝¹ : AddGroup β
inst✝ : DistribMulAction γ β
h : Antiperiodic f c
a : γ
⊢ Antiperiodic (a • f) c

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
c : α
inst✝² : Add α
inst✝¹ : Mul β
inst✝ : HasDistribNeg β
hf : Antiperiodic f c
hg : Antiperiodic g c
⊢ Periodic (f * g) c

Tactic:
simp_all

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p 0 = 0

Tactic:
simp [count]

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

Goal state before:
pp: a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * (a2 / b2) * (c1 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)

Tactic:
congr 1
        exact div_mul_div_comm h1 h2

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
g : Filter ι
inst✝¹ : g.IsCountablyGenerated
u : ι → α
f : Filter α
inst✝ : f.IsCountablyGenerated
hx : (map u (comap u f ⊓ g)).NeBot
⊢ ∃ θ, Tendsto θ atTop g ∧ Tendsto (u ∘ θ) atTop f

Tactic:
map_neBot_iff

Goal state after:
α : Type u_1
ι : Type u_3
g : Filter ι
inst✝¹ : g.IsCountablyGenerated
u : ι → α
f : Filter α
inst✝ : f.IsCountablyGenerated
hx : (comap u f ⊓ g).NeBot
⊢ ∃ θ, Tendsto θ atTop g ∧ Tendsto (u ∘ θ) atTop f
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (closure s).Nonempty ↔ s.Nonempty

Tactic:
by
  simp only [nonempty_iff_ne_empty, Ne, closure_empty_iff]

Goal state after: