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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsDetector G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : ∀ (b : (fun X ↦ X) ((coyoneda.obj (op G)).obj B✝)), ∃! a, (hom ((coyoneda.obj (op G)).map f)) a = b
h : G ⟶ B✝
⊢ ∃! h', h' ≫ f = h

Tactic:
]

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsDetector G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : ∀ (b : (fun X ↦ X) ((coyoneda.obj (op G)).obj B✝)), ∃! a, (hom ((coyoneda.obj (op G)).map f)) a = b
h : G ⟶ B✝
⊢ ∃! h', h' ≫ f = h
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (coyoneda.obj (op G)).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ ∀ (b : (fun X ↦ X) ((coyoneda.obj (op G)).obj Y)), ∃! a, (hom ((coyoneda.obj (op G)).map f)) a = b

Tactic:
]

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (coyoneda.obj (op G)).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ ∀ (b : (fun X ↦ X) ((coyoneda.obj (op G)).obj Y)), ∃! a, (hom ((coyoneda.obj (op G)).map f)) a = b
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCodetector G
A✝ B✝ : Cᵒᵖ
f : A✝ ⟶ B✝
hf : ∀ (b : (fun X ↦ X) ((yoneda.obj G).obj B✝)), ∃! a, (hom ((yoneda.obj G).map f)) a = b
⊢ ∀ (h : unop B✝ ⟶ G), ∃! h', f.unop ≫ h' = h

Tactic:
]

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCodetector G
A✝ B✝ : Cᵒᵖ
f : A✝ ⟶ B✝
hf : ∀ (b : (fun X ↦ X) ((yoneda.obj G).obj B✝)), ∃! a, (hom ((yoneda.obj G).map f)) a = b
⊢ ∀ (h : unop B✝ ⟶ G), ∃! h', f.unop ≫ h' = h
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (yoneda.obj G).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f.op

Tactic:
]

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (yoneda.obj G).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f.op
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (yoneda.obj G).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ ∀ (b : (fun X ↦ X) ((yoneda.obj G).obj (op X))), ∃! a, (hom ((yoneda.obj G).map f.op)) a = b

Tactic:
]

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (yoneda.obj G).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ ∀ (b : (fun X ↦ X) ((yoneda.obj G).obj (op X))), ∃! a, (hom ((yoneda.obj G).map f.op)) a = b
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)
x : F.obj X
u : F.Elements
v : u.fst ⟶ X
h : (ConcreteCategory.hom (F.map v)) u.snd = x
⊢ G.ιColimitType (op u)
      ((ConcreteCategory.hom
          (G.map
            (have this := ⟨v, h⟩;
              this).op))
        (shrinkYonedaObjObjEquiv.symm (𝟙 X))) =
    G.ιColimitType (op u) (shrinkYonedaObjObjEquiv.symm v)

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)
x : F.obj X
u : F.Elements
v : u.fst ⟶ X
h : (ConcreteCategory.hom (F.map v)) u.snd = x
⊢ G.ιColimitType (op u)
      ((ConcreteCategory.hom
          (G.map
            (have this := ⟨v, h⟩;
              this).op))
        (shrinkYonedaObjObjEquiv.symm (𝟙 X))) =
    G.ιColimitType (op u) (shrinkYonedaObjObjEquiv.symm v)
Module: Mathlib.Algebra.Category.Grp.Zero

Goal state before:
pp: case refine_1
G : GrpCat
inst✝ : Subsingleton ↑G
X : GrpCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case refine_1
G : CommGrpCat
inst✝ : Subsingleton ↑G
X : CommGrpCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ 1 = 1

Tactic:
]

Goal state after:
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.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X'✝ X✝ : Type u
Y✝ : AddCommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget AddCommGrpCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ (FreeAbelianGroup.lift ⇑(ConcreteCategory.hom (f✝ ≫ g✝))) x✝ =
    (FreeAbelianGroup.lift (⇑(ConcreteCategory.hom g✝) ∘ ⇑(ConcreteCategory.hom f✝))) x✝

Tactic:
]

Goal state after:
X'✝ X✝ : Type u
Y✝ : AddCommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget AddCommGrpCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ (FreeAbelianGroup.lift ⇑(ConcreteCategory.hom (f✝ ≫ g✝))) x✝ =
    (FreeAbelianGroup.lift (⇑(ConcreteCategory.hom g✝) ∘ ⇑(ConcreteCategory.hom f✝))) x✝
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: case refine_1
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
hx₂ : G.descColimitType c u₂ = x
⊢ G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) =
    G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X))

Tactic:
]

Goal state after:
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.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : Nonempty X
⊢ Mono f

Tactic:
]

Goal state after:
X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : Nonempty X
⊢ Mono f
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
⊢ Function.Bijective ?f ↔ Function.Bijective (fromSigma F c)

pp: case f
C : Type u
F : C → Type v
c : CofanTypes F
⊢ (sigma F).pt → c.pt

pp: case hf
C : Type u
F : C → Type v
c : CofanTypes F
⊢ ∀ (j : Discrete C) (x : (Discrete.functor F).obj j), c.ι j x = ?f ((sigma F).ι j x)

Tactic:
]

Goal state after:
case hf
C : Type u
F : C → Type v
c : CofanTypes F
⊢ ∀ (j : Discrete C) (x : (Discrete.functor F).obj j), c.ι j x = fromSigma F c ((sigma F).ι j 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
⊢ Functor.CoconeTypes.IsColimit c

Tactic:
]

Goal state after:
C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
⊢ Functor.CoconeTypes.IsColimit c
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₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
h : i₁ = i₂
⊢ F i₂ = F i₂

Tactic:
]

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

Goal state before:
pp: C : Type u
F : C → Type v
c : Cofan F
⊢ Function.Bijective (CofanTypes.fromSigma F c.cofanTypes) ↔ Function.Bijective (CofanTypes.fromSigma F c.cofanTypes)

Tactic:
]

Goal state after:
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
hc : IsColimit c
i j : C
x : F i
y : F j
hij : i = j
⊢ F j = F j

Tactic:
]

Goal state after:
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✝¹ = ↾fun x ↦ PEmpty.elim x

Tactic:
by ext x; cases x

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

Goal state before:
pp: case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective
      ⇑(ConcreteCategory.hom
          ((binaryCoproductCocone X Y).ι.app { as := left } ≫
            (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) ∧
    Injective
        ⇑(ConcreteCategory.hom
            ((binaryCoproductCocone X Y).ι.app { as := right } ≫
              (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) ∧
      IsCompl
        (Set.range
          ⇑(ConcreteCategory.hom
              ((binaryCoproductCocone X Y).ι.app { as := left } ≫
                (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))
        (Set.range
          ⇑(ConcreteCategory.hom
              ((binaryCoproductCocone X Y).ι.app { as := right } ≫
                (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))

Tactic:
]

Goal state after:
case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective
      ⇑(ConcreteCategory.hom
          ((binaryCoproductCocone X Y).ι.app { as := left } ≫
            (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) ∧
    Injective
        ⇑(ConcreteCategory.hom
            ((binaryCoproductCocone X Y).ι.app { as := right } ≫
              (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) ∧
      IsCompl
        (Set.range
          ⇑(ConcreteCategory.hom
              ((binaryCoproductCocone X Y).ι.app { as := left } ≫
                (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))
        (Set.range
          ⇑(ConcreteCategory.hom
              ((binaryCoproductCocone X Y).ι.app { as := right } ≫
                (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ ⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) ''
      Set.range ⇑(ConcreteCategory.hom (↾Sum.inl)) =
    (Set.range
        (⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) ∘
          ⇑(ConcreteCategory.hom (↾Sum.inr))))ᶜ

Tactic:
]

Goal state after:
case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ ⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) ''
      Set.range ⇑(ConcreteCategory.hom (↾Sum.inl)) =
    (Set.range
        (⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) ∘
          ⇑(ConcreteCategory.hom (↾Sum.inr))))ᶜ
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ ⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) '' Set.range Sum.inl =
    ⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) '' (Set.range Sum.inr)ᶜ

Tactic:
]

Goal state after:
case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ ⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) '' Set.range Sum.inl =
    ⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) '' (Set.range Sum.inr)ᶜ
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.inl))ᶜ

Tactic:
]

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

Goal state before:
pp: case mpr.refine_3
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))
this✝ :
  ∀ (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)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
y : X
e : (ConcreteCategory.hom c.inl) y = (ConcreteCategory.hom c.inr) x
this : (ConcreteCategory.hom c.inr) x ∈ ⊥
⊢ (ConcreteCategory.hom f)
      ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨(ConcreteCategory.hom c.inr) x, ⋯⟩) =
    (ConcreteCategory.hom g) x

Tactic:
]

Goal state after:
case mpr.refine_3
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))
this✝ :
  ∀ (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)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
y : X
e : (ConcreteCategory.hom c.inl) y = (ConcreteCategory.hom c.inr) x
this : (ConcreteCategory.hom c.inr) x ∈ ⊥
⊢ (ConcreteCategory.hom f)
      ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨(ConcreteCategory.hom c.inr) x, ⋯⟩) =
    (ConcreteCategory.hom g) x
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ Injective ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inl) ∧
    Injective ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inr) ∧
      IsCompl (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inl))
        (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inr))

Tactic:
]

Goal state after:
C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ Injective ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inl) ∧
    Injective ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inr) ∧
      IsCompl (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inl))
        (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inr))
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inr) =
    (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inl))ᶜ

Tactic:
]

Goal state after:
C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inr) =
    (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inl))ᶜ
Module: Mathlib.Algebra.Category.Grp.Injective

Goal state before:
pp: case inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
n : ℤ
hn✝ : n ∈ ℤ ∙ 0
hn : n ∈ ⊥
⊢ 0 n = g ⟨n, hn✝⟩

Tactic:
]

Goal state after:
case inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
n : ℤ
hn✝ : n ∈ ℤ ∙ 0
hn : n ∈ ⊥
⊢ 0 n = g ⟨n, hn✝⟩
Module: Mathlib.Algebra.Category.Grp.Injective

Goal state before:
pp: case inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
hn : 0 ∈ ℤ ∙ 0
⊢ 0 0 = g ⟨0, hn⟩

Tactic:
exact (map_zero g).symm

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

Goal state before:
pp: case inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
n : ℤ
hn : n • m ∈ ℤ ∙ m
⊢ g ⟨n • m, ⋯⟩ = g ⟨n • m, hn⟩

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
n : ℕ
⊢ u ^ n = u ^ n

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
z : ℤ
⊢ u ^ z = u ^ z

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a ↦ a ^ n
n✝ : α
a : A
hn : n✝ ≠ 0
⊢ ⋯.choose ^ n✝ = a

Tactic:
]

Goal state after:
A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a ↦ a ^ n
n✝ : α
a : A
hn : n✝ ≠ 0
⊢ ⋯.choose ^ n✝ = a
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.GroupTheory.Divisible

Goal state before:
pp: 𝕜 : Type ?u.3
inst✝¹ : DivisionRing 𝕜
inst✝ : CharZero 𝕜
n : ℤ
q : 𝕜
hn : n ≠ 0
⊢ q = q

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: case ofNat
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : a✝ ≠ 0
⊢ (match ofNat a✝ with
      | ofNat n => RootableBy.root a n
      | -[n+1] => (RootableBy.root a (n + 1))⁻¹) ^
      ofNat a✝ =
    a

Tactic:
]

Goal state after:
case ofNat
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : a✝ ≠ 0
⊢ (match ofNat a✝ with
      | ofNat n => RootableBy.root a n
      | -[n+1] => (RootableBy.root a (n + 1))⁻¹) ^
      ofNat a✝ =
    a
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
B : Type u_2
α : Type u_3
inst✝⁵ : Zero α
inst✝⁴ : Monoid A
inst✝³ : Monoid B
inst✝² : Pow A α
inst✝¹ : Pow B α
inst✝ : RootableBy A α
f : A → B
hf : Surjective f
hpow : ∀ (a : A) (n : α), f (a ^ n) = f a ^ n
n : α
hn : n ≠ 0
x : B
y : A
hy : f y = x
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.SuccPred

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ b = b

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.SuccPred

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.SuccPred

Goal state before:
pp: a b : ℕ
⊢ ↑a + 1 = ↑b ↔ a + 1 = b

Tactic:
]

Goal state after:
a b : ℕ
⊢ ↑a + 1 = ↑b ↔ a + 1 = b
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ -n.negOnePow = -n.negOnePow

Tactic:
]

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

Goal state before:
pp: k : ℤ
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case mp
n : ℤ
h : n.negOnePow = 1
⊢ ¬Odd n

Tactic:
]

Goal state after:
case mp
n : ℤ
h : n.negOnePow = 1
⊢ ¬Odd n
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case mp
n : ℤ
h : n.negOnePow = -1
⊢ ¬Even n

Tactic:
]

Goal state after:
case mp
n : ℤ
h : n.negOnePow = -1
⊢ ¬Even n
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case mp
n : ℤ
h : 1 = -1
h' : Even n
⊢ False

Tactic:
]

Goal state after:
case mp
n : ℤ
h : 1 = -1
h' : Even n
⊢ False
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ 1 = 1

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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