mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A B : C
X : Subobject B
f : A ⟶ B
inst✝ : HasImage f
h : A ⟶ underlying.obj X
w : h ≫ X.arrow = f
⊢ ((imageSubobjectIso f).hom ≫ image.lift { I := underlying.obj X, m := X.arrow, m_mono := ⋯, e := h, fac := ⋯ }) ≫
      X.arrow =
    (imageSubobject f).arrow

Tactic:
by rw [assoc, image.lift_fac, imageSubobject_arrow]

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

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Mono f
⊢ { X₁ := 0, X₂ := X✝, X₃ := Y✝, f := 0, g := f, zero := ⋯ }.map L ≅
    { X₁ := L.obj 0, X₂ := L.obj X✝, X₃ := L.obj Y✝, f := 0, g := L.map f, zero := ⋯ }

Tactic:
exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)

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

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
⊢ { X₁ := X✝, X₂ := Y✝, X₃ := 0, f := f, g := 0, zero := ⋯ }.map L ≅
    { X₁ := L.obj X✝, X₂ := L.obj Y✝, X₃ := L.obj 0, f := L.map f, g := 0, zero := ⋯ }

Tactic:
exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)

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

Goal state before:
pp: case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ ((underlyingIso (image.ι (smallCoproductDesc s))).hom ≫
        image.lift
          { I := underlying.obj f, m := f.arrow, m_mono := ⋯, e := Sigma.desc fun b ↦ underlying.map (homOfLE ⋯),
            fac := ⋯ }) ≫
      f.arrow =
    (mk (image.ι (smallCoproductDesc s))).arrow

Tactic:
rw [assoc, image.lift_fac, underlyingIso_hom_comp_eq_mk]

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
X : C
Y : Subobject X
Z : Subobject (underlying.obj Y)
⊢ (underlyingIso (Z.arrow ≫ Y.arrow)).hom ≫ Z.arrow = (↑((fun Z ↦ ⟨mk (Z.arrow ≫ Y.arrow), ⋯⟩) Z)).ofLE Y ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
h : ⟨mk (W.arrow ≫ Y.arrow), ⋯⟩ ≤ ⟨mk (Z.arrow ≫ Y.arrow), ⋯⟩
⊢ ((underlyingIso (W.arrow ≫ Y.arrow)).inv ≫
        (mk (W.arrow ≫ Y.arrow)).ofLE (mk (Z.arrow ≫ Y.arrow)) ⋯ ≫ (underlyingIso (Z.arrow ≫ Y.arrow)).hom) ≫
      Z.arrow =
    W.arrow

Tactic:
by cat_disch

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
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : CostructuredArrow L Y₁
⊢ (E.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right E).map φ ≫ (h Y₂).desc (G.coconeAt Y₂) =
    (E.coconeAt Y₁).ι.app X ≫ (h Y₁).desc (G.coconeAt Y₁) ≫ (StructuredArrow.right G).map φ

Tactic:
rw [(h Y₁).fac_assoc (coconeAt G Y₁) X]

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 : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : CostructuredArrow L Y₁
⊢ (E.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right E).map φ ≫ (h Y₂).desc (G.coconeAt Y₂) =
    (G.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right G).map φ
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.HasLeftKanExtension F
inst✝¹ : HasColimitsOfShape C H
inst✝ : HasColimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ colimit.ι X✝ i ≫ colimMap f ≫ ((L.lan.obj Y✝).colimitIsoOfIsLeftKanExtension (L.lanUnit.app Y✝)).inv =
    colimit.ι X✝ i ≫ ((L.lan.obj X✝).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X✝)).inv ≫ colimMap (L.lan.map f)

Tactic:
ι_colimMap_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
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{v_3, u_3} H
inst✝² : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
inst✝¹ : HasColimitsOfShape C H
inst✝ : HasColimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ f.app i ≫ colimit.ι Y✝ i ≫ ((L.lan.obj Y✝).colimitIsoOfIsLeftKanExtension (L.lanUnit.app Y✝)).inv =
    colimit.ι X✝ i ≫ ((L.lan.obj X✝).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X✝)).inv ≫ colimMap (L.lan.map f)
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A✝ A : Cᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
⊢ ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ} (f : X ⟶ Y),
    ((CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A).obj s).map f ≫
        (OverArrows.costructuredArrowIso s (unop Y)).hom =
      (OverArrows.costructuredArrowIso s (unop X)).hom ≫ (yoneda.obj s).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A✝ A : Cᵒᵖ ⥤ Type v
⊢ ∀ {X Y : CostructuredArrow yoneda A} (f : X ⟶ Y),
    (CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A).map f ≫
        (NatIso.ofComponents (fun x ↦ OverArrows.costructuredArrowIso Y (unop x)) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ OverArrows.costructuredArrowIso X (unop x)) ⋯).hom ≫ yoneda.map f

Tactic:
by cat_disch

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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
G : D ⥤ H
⊢ Function.RightInverse (fun β ↦ F'.liftOfIsRightKanExtension α G β) fun β ↦ L.whiskerLeft β ≫ α

Tactic:
by cat_disch

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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
G : D ⥤ H
⊢ Function.RightInverse (fun β ↦ F'.descOfIsLeftKanExtension α G β) fun β ↦ α ≫ L.whiskerLeft β

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A✝ A : Cᵒᵖ ⥤ Type v
⊢ ∀ {Y Z : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (g : Y ⟶ Z),
    (yonedaCollectionFunctor A).map g ≫ yonedaCollectionPresheafToA Z = yonedaCollectionPresheafToA Y

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
s : (CostructuredArrow yoneda A)ᵒᵖ
x : F.obj s
⊢ yonedaCollectionPresheafMap₁ η ≫ yonedaCollectionPresheafToA G = yonedaCollectionPresheafToA F

Tactic:
by cat_disch

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
G : D ⥤ H
α : L ⋙ G ⟶ F
Y : D
⊢ ∀ ⦃X Y_1 : StructuredArrow Y L⦄ (f : X ⟶ Y_1),
    ((const (StructuredArrow Y L)).obj (G.obj Y)).map f ≫ G.map Y_1.hom ≫ α.app Y_1.right =
      (G.map X.hom ≫ α.app X.right) ≫ (StructuredArrow.proj Y L ⋙ F).map f

Tactic:
by simp [← α.naturality, ← G.map_comp_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ counitForward F (unop s) ((ConcreteCategory.hom (F.map f)) x) = (counitForward F (unop t) x).map₂ f.unop.left ⋯

Tactic:
by
  refine OverArrows.ext <| YonedaCollection.ext (by simp) ?_
  have : (CostructuredArrow.mkPrecomp t.unop.hom f.unop.left).op =
      f ≫ eqToHom (by simp [← CostructuredArrow.eq_mk]) := by
    apply Quiver.Hom.unop_inj
    simp
  have : F.map (CostructuredArrow.mkPrecomp
      (YonedaCollection.fst (counitForward F (unop t) x).val) f.unop.left).op
      (F.map (eqToHom (by simp; rfl)) x) = _ :=
    map_mkPrecomp_eqToHom (h := by simp)
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F✝ : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
⊢ ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ} (f : X ⟶ Y),
    F.map f ≫ (counitAuxAux F (unop Y)).hom =
      (counitAuxAux F (unop X)).hom ≫ (restrictedYonedaObj (yonedaCollectionPresheafToA F)).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A✝ : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A✝)ᵒᵖ ⥤ Type v
X : C
A : Cᵒᵖ ⥤ Type v
⊢ ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (f : X ⟶ Y),
    (𝟭 ((CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v)).map f ≫ (counitAux Y).hom =
      (counitAux X).hom ≫ (costructuredArrowPresheafToOver A ⋙ restrictedYoneda A).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A✝ A : Cᵒᵖ ⥤ Type v
T : Over A
⊢ ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ} (f : X ⟶ Y),
    ((toOver yoneda A).op ⋙ yoneda.obj T).map f ≫
        ((overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv.toIso ≪≫
            (((toOverCompOverEquivPresheafCostructuredArrow A).app (unop Y)).homCongr
                (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj T))).toIso).hom =
      ((overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv.toIso ≪≫
            (((toOverCompOverEquivPresheafCostructuredArrow A).app (unop X)).homCongr
                (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj T))).toIso).hom ≫
        (yoneda.op ⋙ yoneda.obj ((overEquivPresheafCostructuredArrow A).functor.obj T)).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A✝ A : Cᵒᵖ ⥤ Type v
⊢ ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ} (f : X ⟶ Y),
    ((toOver yoneda A).op ⋙ coyoneda).map f ≫
        (NatIso.ofComponents
            (fun Y_1 ↦
              (overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv.toIso ≪≫
                (((toOverCompOverEquivPresheafCostructuredArrow A).app (unop Y)).homCongr
                    (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj Y_1))).toIso)
            ⋯).hom =
      (NatIso.ofComponents
            (fun Y ↦
              (overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv.toIso ≪≫
                (((toOverCompOverEquivPresheafCostructuredArrow A).app (unop X)).homCongr
                    (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj Y))).toIso)
            ⋯).hom ≫
        (yoneda.op ⋙
              coyoneda ⋙
                (Functor.whiskeringLeft (Over A) ((CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) (Type (max u v))).obj
                  (overEquivPresheafCostructuredArrow A).functor).map
          f

Tactic:
by cat_disch

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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
⊢ α ≫
      L.whiskerLeft
        (F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι ≫
          (const D).map (hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι })) =
    α ≫ L.whiskerLeft s.ι

Tactic:
by cat_disch

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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
⊢ L.whiskerLeft
        ((const D).map (hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α }) ≫
          F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π) ≫
      α =
    L.whiskerLeft s.π ≫ α

Tactic:
by cat_disch

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

Goal state before:
pp: case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasLimitsOfShape J C
inst✝ : lim.PreservesEpimorphisms
⊢ lim.PreservesHomology

pp: case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasLimitsOfShape J C
inst✝ : lim.PreservesEpimorphisms
⊢ lim.Additive

Tactic:
· exact preservesHomology_of_preservesEpis_and_kernels _

Goal state after:
case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasLimitsOfShape J C
inst✝ : lim.PreservesEpimorphisms
⊢ lim.Additive
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
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.unop_inj (hP _ _ fun G hG h => Quiver.Hom.op_inj ?_)
    simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ hG _

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

Goal state before:
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.unop_inj (hP _ _ fun G hG h => Quiver.Hom.op_inj ?_)
    simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ hG _

Goal state after:
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 ≫ colimMap S.g)) y = 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range

Tactic:
colimMap_eq,

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 ≫ colim.map S.g)) y = 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case left
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
y : (Discrete.functor F).ColimitType
i : C
x : (Discrete.functor F).obj { as := i }
h :
  (Discrete.functor F).descColimitType c ((Discrete.functor F).ιColimitType { as := i } x) =
    (Discrete.functor F).descColimitType c y
⊢ (Discrete.functor F).ιColimitType { as := i } x = y

Tactic:
obtain ⟨⟨j⟩, y, rfl⟩ := (Discrete.functor F).ιColimitType_jointly_surjective y

Goal state after:
case left
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
i : C
x : (Discrete.functor F).obj { as := i }
j : C
y : (Discrete.functor F).obj { as := j }
h :
  (Discrete.functor F).descColimitType c ((Discrete.functor F).ιColimitType { as := i } x) =
    (Discrete.functor F).descColimitType c ((Discrete.functor F).ιColimitType { as := j } y)
⊢ (Discrete.functor F).ιColimitType { as := i } x = (Discrete.functor F).ιColimitType { as := j } y
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

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

Tactic:
by cat_disch

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

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

Tactic:
by cat_disch

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

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

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul ((z₁ * z₂) • au) = Additive.toMul (z₁ • z₂ • au)

Tactic:
by
    dsimp only [ZMod.smul_units_def, toMul_nsmul]
    rw [← pow_mul, ZMod.val_mul, ← Int.units_pow_eq_pow_mod_two, mul_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : NonAssocRing α
h : Periodic f c
n : ℕ
⊢ f (x - ↑n * c) = f x

Tactic:
by
  simpa only [nsmul_eq_mul] using h.sub_nsmul_eq n

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ r • ↑a = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y

Tactic:
rw [ExtensionOfMaxAdjoin.eqn, smul_add, smul_eq_mul, mul_smul]

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ r • ↑(ExtensionOfMaxAdjoin.fst i a) + r • ExtensionOfMaxAdjoin.snd i a • y =
    ↑(r • ExtensionOfMaxAdjoin.fst i a) + r • ExtensionOfMaxAdjoin.snd i a • y
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case coprime
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a : ℕ
⊢ ∀ (b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          (a ≠ 0 → f a = a.factorization.prod fun p k ↦ f (p ^ k)) →
            (b ≠ 0 → f b = b.factorization.prod fun p k ↦ f (p ^ k)) →
              a * b ≠ 0 → f (a * b) = (a * b).factorization.prod fun p k ↦ f (p ^ k)

Tactic:
b

Goal state after:
case coprime
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
⊢ 1 < a →
    1 < b →
      a.Coprime b →
        (a ≠ 0 → f a = a.factorization.prod fun p k ↦ f (p ^ k)) →
          (b ≠ 0 → f b = b.factorization.prod fun p k ↦ f (p ^ k)) →
            a * b ≠ 0 → f (a * b) = (a * b).factorization.prod fun p k ↦ f (p ^ k)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
⊢ ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)

Tactic:
b

Goal state after:
case mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
b : ℕ
⊢ ¬(b < p ^ n ∧ b * p = a)
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
⊢ Tendsto (fun p ↦ p.1 ×ˢ p.2) atTop atTop

Tactic:
apply Monotone.tendsto_atTop_atTop

Goal state after:
case hf
ι : Type u_1
ι' : Type u_2
⊢ Monotone fun p ↦ p.1 ×ˢ p.2

case h
ι : Type u_1
ι' : Type u_2
⊢ ∀ (b : Finset (ι × ι')), ∃ a, b ⊆ a.1 ×ˢ a.2
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : 0 < p
⊢ φ p = p - 1 ↔ Prime p

Tactic:
refine ⟨fun h => ?_, totient_prime⟩
  replace hp : 1 < p := by
    apply lt_of_le_of_ne
    · rwa [succ_le_iff]
    · rintro rfl
      rw [totient_one, tsub_self] at h
      exact one_ne_zero h
  rw [totient_eq_card_coprime, range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico hp.le,
    Finset.filter_insert, if_neg (not_coprime_of_dvd_of_dvd hp (dvd_refl p) (dvd_zero p)),
    ← Nat.card_Ico 1 p] at h
  refine
    p.prime_of_coprime hp fun n hn hnz => Finset.filter_card_eq h n <| Finset.mem_Ico.mpr ⟨?_, hn⟩
  lia

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: case empty
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
h : ∀ t ∈ ∅, IsOpen[inst✝] t
⊢ IsOpen[inst✝] (⋂₀ ∅)

Tactic:
rw [sInter_empty]

Goal state after:
case empty
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
h : ∀ t ∈ ∅, IsOpen[inst✝] t
⊢ IsOpen[inst✝] univ
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsClosed[inst✝] s₁
h₂ : IsClosed[inst✝] s₂
⊢ IsClosed[inst✝] (s₁ ∩ s₂)

Tactic:
rw [← isOpen_compl_iff] at *

Goal state after:
X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen[inst✝] s₁ᶜ
h₂ : IsOpen[inst✝] s₂ᶜ
⊢ IsOpen[inst✝] (s₁ ∩ s₂)ᶜ
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsClosed[inst✝] s₁
h₂ : IsClosed[inst✝] s₂
⊢ IsClosed[inst✝] (s₁ ∩ s₂)

Tactic:
by
  rw [← isOpen_compl_iff] at *
  rw [compl_inter]
  exact IsOpen.union h₁ h₂

Goal state after: