mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x✝² : YonedaCollection F Z
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₂ F (f ≫ g) x✝²).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom (((map₂ F f ∘ map₂ F g) x✝²).fst.app x✝¹)).toFun x✝

pp: case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x✝ : YonedaCollection F Z
⊢ (ConcreteCategory.hom (F.map (eqToHom ⋯))) ((map₂ F f ∘ map₂ F g) x✝).snd = (map₂ F (f ≫ g) x✝).snd

Tactic:
;

Goal state after:
case h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x✝² : YonedaCollection F Z
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₂ F (f ≫ g) x✝²).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom (((map₂ F f ∘ map₂ F g) x✝²).fst.app x✝¹)).toFun x✝

case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x✝ : YonedaCollection F Z
⊢ (ConcreteCategory.hom (F.map (eqToHom ⋯))) ((map₂ F f ∘ map₂ F g) x✝).snd = (map₂ F (f ≫ g) x✝).snd
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h
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
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₂ G f (map₁ η p)).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom ((map₁ η (map₂ F f p)).fst.app x✝¹)).toFun x✝

pp: case h'
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
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ (ConcreteCategory.hom (G.map (eqToHom ⋯))) (map₁ η (map₂ F f p)).snd = (map₂ G f (map₁ η p)).snd

Tactic:
;

Goal state after:
case h
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
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₂ G f (map₁ η p)).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom ((map₁ η (map₂ F f p)).fst.app x✝¹)).toFun x✝

case h'
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
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ (ConcreteCategory.hom (G.map (eqToHom ⋯))) (map₁ η (map₂ F f p)).snd = (map₂ G f (map₁ η p)).snd
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
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
⊢ t = op (CostructuredArrow.mk (unop t).hom)

Tactic:
;

Goal state after:
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
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
⊢ t = op (CostructuredArrow.mk (unop t).hom)
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
w✝¹ : C
h : P w✝¹
w✝ : S ⟶ T.obj w✝¹
⊢ P (mk w✝).right

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
w✝¹ : C
h : P w✝¹
w✝ : S ⟶ T.obj w✝¹
⊢ P (mk w✝).right
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

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
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
w✝¹ : C
h : P w✝¹
w✝ : S.obj w✝¹ ⟶ T
⊢ P (mk w✝).left

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
w✝¹ : C
h : P w✝¹
w✝ : S.obj w✝¹ ⟶ T
⊢ P (mk w✝).left
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 : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ (q ≫ T.map (Subobject.underlyingIso (Hom.right f)).hom) ≫ T.map (Hom.right f) = P.hom ≫ T.map (Hom.right f)

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ (q ≫ T.map (Subobject.underlyingIso (Hom.right f)).hom) ≫ T.map (Hom.right f) = P.hom ≫ T.map (Hom.right f)
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case refine_2
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
h :
  { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk f) ≤
    { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk g)
⊢ (homMk (Subobject.ofMkLEMk (MonoOver.mk f).arrow.unop.left.op (MonoOver.mk g).arrow.unop.left.op h).unop ⋯).op ≫ g = f

pp: case refine_3
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
h : Subobject.mk f ≤ Subobject.mk g
⊢ { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk f) ≤
    { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk g)

Tactic:
· apply Quiver.Hom.unop_inj
      ext
      exact unop_left_comp_ofMkLEMk_unop _

Goal state after:
case refine_3
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
h : Subobject.mk f ≤ Subobject.mk g
⊢ { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk f) ≤
    { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk g)
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
X✝ : K
⊢ Mono ((whiskerRight f H).app X✝)

Tactic:
;

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✝² : HasPullbacks C
inst✝¹ : Mono f
H : C ⥤ D
inst✝ : H.PreservesMonomorphisms
X✝ : K
⊢ Mono ((whiskerRight f H).app X✝)
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
X✝ : K
⊢ Mono (H.map (f.app X✝))

Tactic:
;

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✝² : HasPullbacks C
inst✝¹ : Mono f
H : C ⥤ D
inst✝ : H.PreservesMonomorphisms
X✝ : K
⊢ Mono (H.map (f.app X✝))
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
F : C ⥤ D
inst✝ : F.PreservesMonomorphisms
X✝ Y✝ : K ⥤ C
f : X✝ ⟶ Y✝
x✝ : Mono f
⊢ Mono (whiskerRight f F)

Tactic:
;

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✝¹ : HasPullbacks C
F : C ⥤ D
inst✝ : F.PreservesMonomorphisms
X✝ Y✝ : K ⥤ C
f : X✝ ⟶ Y✝
x✝ : Mono f
⊢ Mono (whiskerRight f F)
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
X✝ : K
⊢ Epi ((whiskerRight f H).app X✝)

Tactic:
;

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
X✝ : K
⊢ Epi ((whiskerRight f H).app X✝)
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
X✝ : K
⊢ Epi (H.map (f.app X✝))

Tactic:
;

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
X✝ : K
⊢ Epi (H.map (f.app X✝))
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
x✝⁵ : (coyoneda.obj (op G)).Faithful
x✝⁴ x✝³ : C
x✝² x✝¹ : x✝⁴ ⟶ x✝³
hfg : ∀ (h : G ⟶ x✝⁴), h ≫ x✝² = h ≫ x✝¹
x✝ : (coyoneda.obj (op G)).obj x✝⁴
⊢ (hom ((coyoneda.obj (op G)).map x✝²)).toFun x✝ = (hom ((coyoneda.obj (op G)).map x✝¹)).toFun x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
x✝⁵ : (coyoneda.obj (op G)).Faithful
x✝⁴ x✝³ : C
x✝² x✝¹ : x✝⁴ ⟶ x✝³
hfg : ∀ (h : G ⟶ x✝⁴), h ≫ x✝² = h ≫ x✝¹
x✝ : (coyoneda.obj (op G)).obj x✝⁴
⊢ (hom ((coyoneda.obj (op G)).map x✝²)).toFun x✝ = (hom ((coyoneda.obj (op G)).map x✝¹)).toFun x✝
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
x✝⁵ : (yoneda.obj G).Faithful
x✝⁴ x✝³ : C
x✝² x✝¹ : x✝⁴ ⟶ x✝³
hfg : ∀ (h : x✝³ ⟶ G), x✝² ≫ h = x✝¹ ≫ h
x✝ : (yoneda.obj G).obj (op x✝³)
⊢ (hom ((yoneda.obj G).map x✝².op)).toFun x✝ = (hom ((yoneda.obj G).map x✝¹.op)).toFun x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
x✝⁵ : (yoneda.obj G).Faithful
x✝⁴ x✝³ : C
x✝² x✝¹ : x✝⁴ ⟶ x✝³
hfg : ∀ (h : x✝³ ⟶ G), x✝² ≫ h = x✝¹ ≫ h
x✝ : (yoneda.obj G).obj (op x✝³)
⊢ (hom ((yoneda.obj G).map x✝².op)).toFun x✝ = (hom ((yoneda.obj G).map x✝¹.op)).toFun x✝
Module: Mathlib.CategoryTheory.Generator.Basic

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

pp: case e'_2.mp.inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ ∃ i, WalkingPair.rec G H i = H

Tactic:
;

Goal state after:
case e'_2.mp.inl
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ ∃ i, WalkingPair.rec G H i = G

case e'_2.mp.inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ ∃ i, WalkingPair.rec G H i = H
Module: Mathlib.CategoryTheory.Generator.Basic

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

pp: case e'_2.mp.inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ ∃ i, WalkingPair.rec G H i = H

Tactic:
;

Goal state after:
case e'_2.mp.inl
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ ∃ i, WalkingPair.rec G H i = G

case e'_2.mp.inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ ∃ i, WalkingPair.rec G H i = H
Module: Mathlib.Algebra.Category.Grp.AB

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

Tactic:
;

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

Goal state before:
pp: case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
A B : AddCommGrpCat
f g : A ⟶ B
h :
  ∀ (h : AddCommGrpCat.of (ULift.{u, 0} ℤ) ⟶ A) (x : ℤ),
    (AddCommGrpCat.Hom.hom f) ((AddCommGrpCat.Hom.hom h) { down := x }) =
      (AddCommGrpCat.Hom.hom g) ((AddCommGrpCat.Hom.hom h) { down := x })
x : ↑A
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) x

Tactic:
;

Goal state after:
case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
A B : AddCommGrpCat
f g : A ⟶ B
h :
  ∀ (h : AddCommGrpCat.of (ULift.{u, 0} ℤ) ⟶ A) (x : ℤ),
    (AddCommGrpCat.Hom.hom f) ((AddCommGrpCat.Hom.hom h) { down := x }) =
      (AddCommGrpCat.Hom.hom g) ((AddCommGrpCat.Hom.hom h) { down := x })
x : ↑A
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) x
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
A B : AddCommGrpCat
f g : A ⟶ B
x : ↑A
h :
  (AddCommGrpCat.Hom.hom f)
      ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun y ↦ y • x) ⋯))) { down := 1 }) =
    (AddCommGrpCat.Hom.hom g)
      ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun y ↦ y • x) ⋯))) { down := 1 })
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) x

Tactic:
;

Goal state after:
case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
A B : AddCommGrpCat
f g : A ⟶ B
x : ↑A
h :
  (AddCommGrpCat.Hom.hom f)
      ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun y ↦ y • x) ⋯))) { down := 1 }) =
    (AddCommGrpCat.Hom.hom g)
      ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun y ↦ y • x) ⋯))) { down := 1 })
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) x
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
this :
  ∀ (u : G.ColimitType) (x : F.obj X),
    G.descColimitType c u = x → G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u
u₁ u₂ : ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).ColimitType
hu :
  ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₁ =
    ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₂
x : c.pt
hx₁ : G.descColimitType c u₁ = x
⊢ G.descColimitType c u₂ = G.descColimitType c u₁

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
this :
  ∀ (u : G.ColimitType) (x : F.obj X),
    G.descColimitType c u = x → G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u
u₁ u₂ : ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).ColimitType
hu :
  ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₁ =
    ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₂
x : c.pt
hx₁ : G.descColimitType c u₁ = x
⊢ G.descColimitType c u₂ = G.descColimitType c u₁
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
x✝² : C
x✝¹ x✝ : F x✝²
h : ((sigma F).inj x✝² x✝¹).fst = ((sigma F).inj x✝² x✝).fst ∧ ((sigma F).inj x✝² x✝¹).snd ≍ ((sigma F).inj x✝² x✝).snd
⊢ x✝¹ = x✝

Tactic:
;

Goal state after:
C : Type u
F : C → Type v
x✝² : C
x✝¹ x✝ : F x✝²
h : ((sigma F).inj x✝² x✝¹).fst = ((sigma F).inj x✝² x✝).fst ∧ ((sigma F).inj x✝² x✝¹).snd ≍ ((sigma F).inj x✝² x✝).snd
⊢ x✝¹ = x✝
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i₁ : C
y₂ : F i₁
x✝ : ∃ (h : i₁ = i₁), y₂ = cast ⋯ y₂
⊢ c.inj i₁ y₂ = c.inj i₁ y₂

Tactic:
;

Goal state after:
C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i₁ : C
y₂ : F i₁
x✝ : ∃ (h : i₁ = i₁), y₂ = cast ⋯ y₂
⊢ c.inj i₁ y₂ = c.inj i₁ y₂
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
x✝² : Cocone (Functor.empty (Type u))
x✝¹ :
  { pt := PEmpty.{u + 1},
        ι := ((Functor.const (Discrete PEmpty.{?u.24 + 1})).obj PEmpty.{u + 1}).uniqueFromEmpty.inv }.pt ⟶
    x✝².pt
x✝ :
  ∀ (j : Discrete PEmpty.{?u.24 + 1}),
    { pt := PEmpty.{u + 1},
                ι := ((Functor.const (Discrete PEmpty.{?u.24 + 1})).obj PEmpty.{u + 1}).uniqueFromEmpty.inv }.ι.app
          j ≫
        x✝¹ =
      x✝².ι.app j
x :
  { pt := PEmpty.{u + 1},
      ι := ((Functor.const (Discrete PEmpty.{?u.24 + 1})).obj PEmpty.{u + 1}).uniqueFromEmpty.inv }.pt
⊢ (ConcreteCategory.hom x✝¹).toFun x = (ConcreteCategory.hom (↾fun x ↦ PEmpty.elim x)).toFun x

Tactic:
;

Goal state after:
C : Type u
F : C → Type v
x✝² : Cocone (Functor.empty (Type u))
x✝¹ :
  { pt := PEmpty.{u + 1},
        ι := ((Functor.const (Discrete PEmpty.{?u.24 + 1})).obj PEmpty.{u + 1}).uniqueFromEmpty.inv }.pt ⟶
    x✝².pt
x✝ :
  ∀ (j : Discrete PEmpty.{?u.24 + 1}),
    { pt := PEmpty.{u + 1},
                ι := ((Functor.const (Discrete PEmpty.{?u.24 + 1})).obj PEmpty.{u + 1}).uniqueFromEmpty.inv }.ι.app
          j ≫
        x✝¹ =
      x✝².ι.app j
x :
  { pt := PEmpty.{u + 1},
      ι := ((Functor.const (Discrete PEmpty.{?u.24 + 1})).obj PEmpty.{u + 1}).uniqueFromEmpty.inv }.pt
⊢ (ConcreteCategory.hom x✝¹).toFun x = (ConcreteCategory.hom (↾fun x ↦ PEmpty.elim x)).toFun x
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X✝ : CommGrpCat
Y✝ : CommMonCat
f✝ : (forget₂ CommGrpCat CommMonCat).obj X✝ ⟶ Y✝
⊢ { toFun := fun f ↦ ofHom (CommMonCat.Hom.hom f).toHomUnits,
        invFun := fun f ↦ CommMonCat.ofHom ((Units.coeHom ↑Y✝).comp (Hom.hom f)), left_inv := ⋯, right_inv := ⋯ }
      f✝ =
    { app := fun X ↦ ofHom toUnits.toMonoidHom, naturality := ⋯ }.app X✝ ≫ CommMonCat.units.map f✝

Tactic:
;

Goal state after:
X✝ : CommGrpCat
Y✝ : CommMonCat
f✝ : (forget₂ CommGrpCat CommMonCat).obj X✝ ⟶ Y✝
⊢ { toFun := fun f ↦ ofHom (CommMonCat.Hom.hom f).toHomUnits,
        invFun := fun f ↦ CommMonCat.ofHom ((Units.coeHom ↑Y✝).comp (Hom.hom f)), left_inv := ⋯, right_inv := ⋯ }
      f✝ =
    { app := fun X ↦ ofHom toUnits.toMonoidHom, naturality := ⋯ }.app X✝ ≫ CommMonCat.units.map f✝
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X✝ : CommGrpCat
Y✝ : CommMonCat
g✝ : X✝ ⟶ CommMonCat.units.obj Y✝
⊢ { toFun := fun f ↦ ofHom (CommMonCat.Hom.hom f).toHomUnits,
          invFun := fun f ↦ CommMonCat.ofHom ((Units.coeHom ↑Y✝).comp (Hom.hom f)), left_inv := ⋯, right_inv := ⋯ }.symm
      g✝ =
    (forget₂ CommGrpCat CommMonCat).map g✝ ≫
      { app := fun X ↦ CommMonCat.ofHom (Units.coeHom ↑X), naturality := ⋯ }.app Y✝

Tactic:
;

Goal state after:
X✝ : CommGrpCat
Y✝ : CommMonCat
g✝ : X✝ ⟶ CommMonCat.units.obj Y✝
⊢ { toFun := fun f ↦ ofHom (CommMonCat.Hom.hom f).toHomUnits,
          invFun := fun f ↦ CommMonCat.ofHom ((Units.coeHom ↑Y✝).comp (Hom.hom f)), left_inv := ⋯, right_inv := ⋯ }.symm
      g✝ =
    (forget₂ CommGrpCat CommMonCat).map g✝ ≫
      { app := fun X ↦ CommMonCat.ofHom (Units.coeHom ↑X), naturality := ⋯ }.app Y✝
Module: Mathlib.Algebra.Category.ModuleCat.Injective

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R M
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.of R M
f : X✝ ⟶ Y✝
m : Mono f
l : ↑Y✝ →ₗ[R] M
h : ∀ (x : ↑X✝), l ((ModuleCat.Hom.hom f) x) = (ModuleCat.Hom.hom g) x
x : ↑X✝
⊢ (ModuleCat.Hom.hom (f ≫ ModuleCat.ofHom l)) x = (ModuleCat.Hom.hom g) x

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R M
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.of R M
f : X✝ ⟶ Y✝
m : Mono f
l : ↑Y✝ →ₗ[R] M
h : ∀ (x : ↑X✝), l ((ModuleCat.Hom.hom f) x) = (ModuleCat.Hom.hom g) x
x : ↑X✝
⊢ (ModuleCat.Hom.hom (f ≫ ModuleCat.ofHom l)) x = (ModuleCat.Hom.hom g) x
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
a : A
n : ℤ
hn : ¬n = 0
⊢ a ∈ ⊤

Tactic:
;

Goal state after:
A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
a : A
n : ℤ
hn : ¬n = 0
⊢ a ∈ ⊤
Module: Mathlib.Data.Int.SuccPred

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ Order.succ^[(b - a).toNat] a = b

Tactic:
rw [succ_iterate, toNat_sub_of_le h, ← add_sub_assoc, add_sub_cancel_left]

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

Goal state before:
pp: case pos
n₁ n₂ : ℤ
h₂ : Even n₂
⊢ n₁.negOnePow = 1 ↔ Even (n₁ - n₂)

Tactic:
Int.even_sub,

Goal state after:
case pos
n₁ n₂ : ℤ
h₂ : Even n₂
⊢ n₁.negOnePow = 1 ↔ (Even n₁ ↔ Even n₂)
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case neg
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ n₁.negOnePow = -1 ↔ Even (n₁ - n₂)

Tactic:
Int.even_sub,

Goal state after:
case neg
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ n₁.negOnePow = -1 ↔ (Even n₁ ↔ Even n₂)