awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty.{v₁, u₁} (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag.{v₁, u₁} j₁ j₂
l : List J
hl₁ : List.IsChain Zag.{v₁, u₁} (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag.{v₁, u₁} x j₂ → ConnectedComponents.Component.{v₁, u₁} (ConnectedComponents.mk j₂) :=
  fun (x : J) (h : Zigzag.{v₁, u₁} x j₂) ↦
    ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (ConnectedComponents.mk j₂)) x ⋯
hf : ∀ a ∈ l, Zigzag.{v₁, u₁} a j₂
⊢ List.IsChain Zag.{v₁, u₁}
    (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ ::
      List.pmap (P := fun (a : J) ↦ Zigzag.{v₁, u₁} a j₂) f l hf)

Tactic:
@List.isChain_cons_pmap_of_isChain_cons _ _ Zag _ _ f
    (fun x y _ _ h => ?_) _ _ h₁₂ hl₁ _

Premises used: List.isChain_cons_pmap_of_isChain_cons
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty.{v₁, u₁} (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag.{v₁, u₁} j₁ j₂
l : List J
hl₁ : List.IsChain Zag.{v₁, u₁} (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag.{v₁, u₁} x j₂ → ConnectedComponents.Component.{v₁, u₁} (ConnectedComponents.mk j₂) :=
  fun (x : J) (h : Zigzag.{v₁, u₁} x j₂) ↦
    ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (ConnectedComponents.mk j₂)) x ⋯
hf : ∀ a ∈ l, Zigzag.{v₁, u₁} a j₂
h :
  ∀ (x y : J) (x_1 : Zigzag.{v₁, u₁} x j₂) (x_2 : Zigzag.{v₁, u₁} y j₂) (h : Zag.{v₁, u₁} x y),
    Zag.{v₁, u₁} (f x x_1) (f y x_2)
⊢ List.IsChain Zag.{v₁, u₁}
    (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ ::
      List.pmap (P := fun (a : J) ↦ Zigzag.{v₁, u₁} a j₂) f l hf)

Tactic:
refine @List.isChain_cons_pmap_of_isChain_cons _ _ Zag _ _ f
    (fun x y _ _ h => ?_) _ _ h₁₂ hl₁ _

Premises used: List.isChain_cons_pmap_of_isChain_cons
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty.{v₁, u₁} (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag.{v₁, u₁} j₁ j₂
l : List J
hl₁ : List.IsChain Zag.{v₁, u₁} (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag.{v₁, u₁} x j₂ → ConnectedComponents.Component.{v₁, u₁} (ConnectedComponents.mk j₂) :=
  fun (x : J) (h : Zigzag.{v₁, u₁} x j₂) ↦
    ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (ConnectedComponents.mk j₂)) x ⋯
hf : ∀ a ∈ l, Zigzag.{v₁, u₁} a j₂
x y : J
h_1 : Zigzag.{v₁, u₁} x j₂
h_2 : Zigzag.{v₁, u₁} y j₂
h : Zag.{v₁, u₁} x y
⊢ Zag.{v₁, u₁} (f x h_1) (f y h_2)

Tactic:
zag_of_zag_obj (ConnectedComponents.ι _) h

Premises used: CategoryTheory.zag_of_zag_obj, CategoryTheory.ConnectedComponents.ι
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty.{v₁, u₁} (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag.{v₁, u₁} j₁ j₂
l : List J
hl₁ : List.IsChain Zag.{v₁, u₁} (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag.{v₁, u₁} x j₂ → ConnectedComponents.Component.{v₁, u₁} (ConnectedComponents.mk j₂) :=
  fun (x : J) (h : Zigzag.{v₁, u₁} x j₂) ↦
    ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (ConnectedComponents.mk j₂)) x ⋯
hf : ∀ a ∈ l, Zigzag.{v₁, u₁} a j₂
x y : J
h_1 : Zigzag.{v₁, u₁} x j₂
h_2 : Zigzag.{v₁, u₁} y j₂
h : Zag.{v₁, u₁} x y
⊢ Zag.{v₁, u₁} (f x h_1) (f y h_2)

Tactic:
exact zag_of_zag_obj (ConnectedComponents.ι _) h
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j : ConnectedComponents.{v₁, u₁} J
⊢ inclusion j ⋙ decomposedTo J = j.ι

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.comp, CategoryTheory.Sigma.descMap, CategoryTheory.inducedFunctor, CategoryTheory.InducedCategory, rfl
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j' : ConnectedComponents.{v₁, u₁} J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents.{v₁, u₁} J
Y : J
hY : k'.objectProperty Y
f : X ⟶ Y
rw : (Zigzag.setoid J : J → J → Prop) X Y
⊢ j' = k'

Tactic:
rw [← hX, ← hY, Quotient.eq'']

Premises used: Quotient.eq''
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j' : ConnectedComponents.{v₁, u₁} J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents.{v₁, u₁} J
Y : J
hY : k'.objectProperty Y
f : X ⟶ Y
⊢ (Zigzag.setoid J : J → J → Prop) X Y

Tactic:
Relation.ReflTransGen.single (Or.inl ⟨f⟩)

Premises used: CategoryTheory.Zigzag, Nonempty.intro, Relation.ReflTransGen.single, Or.inl
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j' : ConnectedComponents.{v₁, u₁} J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents.{v₁, u₁} J
Y : J
hY : k'.objectProperty Y
f : X ⟶ Y
⊢ (Zigzag.setoid J : J → J → Prop) X Y

Tactic:
exact Relation.ReflTransGen.single (Or.inl ⟨f⟩)

Premises used: Relation.ReflTransGen.single, Or.inl
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j' : ConnectedComponents.{v₁, u₁} J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents.{v₁, u₁} J
Y : J
hY : k'.objectProperty Y
f : X ⟶ Y
⊢ j' = k'

Tactic:
have : j' = k' := by
      rw [← hX, ← hY, Quotient.eq'']
      exact Relation.ReflTransGen.single (Or.inl ⟨f⟩)
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j' : ConnectedComponents.{v₁, u₁} J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents.{v₁, u₁} J
Y : J
hY : k'.objectProperty Y
f : X ⟶ Y
this : j' = k'
subst :
  ∀ (hY : j'.objectProperty Y),
    ∃ (a :
      Quiver.Hom (V := Decomposed.{v₁, u₁} J)
        (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) j'
          (ObjectProperty.FullSubcategory.mk (P := j'.objectProperty) X hX))
        (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) j'
          (ObjectProperty.FullSubcategory.mk (P := j'.objectProperty) Y hY))),
      Functor.map (decomposedTo J) a = f
⊢ ∃ (a :
    Quiver.Hom (V := Decomposed.{v₁, u₁} J)
      (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) j'
        (ObjectProperty.FullSubcategory.mk (P := j'.objectProperty) X hX))
      (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) k'
        (ObjectProperty.FullSubcategory.mk (P := k'.objectProperty) Y hY))),
    Functor.map (decomposedTo J) a = f

Tactic:
subst this
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j' : ConnectedComponents.{v₁, u₁} J
X : J
hX : j'.objectProperty X
Y : J
f : X ⟶ Y
hY : j'.objectProperty Y
⊢ ∃ (a :
    Quiver.Hom (V := Decomposed.{v₁, u₁} J)
      (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) j'
        (ObjectProperty.FullSubcategory.mk (P := j'.objectProperty) X hX))
      (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) j'
        (ObjectProperty.FullSubcategory.mk (P := j'.objectProperty) Y hY))),
    Functor.map (decomposedTo J) a = f

Tactic:
⟨Sigma.SigmaHom.mk (ObjectProperty.homMk f), rfl⟩

Premises used: CategoryTheory.Sigma.SigmaHom.mk, CategoryTheory.ObjectProperty.homMk, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j' : ConnectedComponents.{v₁, u₁} J
X : J
hX : j'.objectProperty X
Y : J
f : X ⟶ Y
hY : j'.objectProperty Y
⊢ ∃ (a :
    Quiver.Hom (V := Decomposed.{v₁, u₁} J)
      (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) j'
        (ObjectProperty.FullSubcategory.mk (P := j'.objectProperty) X hX))
      (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) j'
        (ObjectProperty.FullSubcategory.mk (P := j'.objectProperty) Y hY))),
    Functor.map (decomposedTo J) a = f

Tactic:
exact ⟨Sigma.SigmaHom.mk (ObjectProperty.homMk f), rfl⟩
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j k : J
hY : ConnectedComponents.objectProperty.{v₁, u₁} (Quotient.mk'' j) k
f :
  ObjectProperty.FullSubcategory.obj (P := ConnectedComponents.objectProperty (Quotient.mk'' j))
      (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j)) j ⋯) ⟶
    (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j)) k hY).obj (P :=
      ConnectedComponents.objectProperty (Quotient.mk'' j))
⊢ Eq (α :=
    Quiver.Hom (V := Decomposed.{v₁, u₁} J)
      (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) (Quotient.mk'' j)
        (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j)) j ⋯))
      (Sigma.mk (β := fun (j : ConnectedComponents.{v₁, u₁} J) ↦ j.Component) (Quotient.mk'' j)
        (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j)) k hY)))
    (Sigma.SigmaHom.mk (C := ConnectedComponents.Component) { hom := f })
    (Sigma.SigmaHom.mk (C := ConnectedComponents.Component)
      { hom := Functor.map (decomposedTo J) (Sigma.SigmaHom.mk (C := ConnectedComponents.Component) { hom := f }) })

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.CopyDiscardCategory.Deterministic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : CopyDiscardCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : Deterministic f
⊢ Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ) (Δ ≫ (f ⊗ₘ f))

Tactic:
IsComonHom.hom_comul f

Premises used: CategoryTheory.IsComonHom.hom_comul
-- Module: Mathlib.CategoryTheory.CopyDiscardCategory.Deterministic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : CopyDiscardCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : Deterministic f
⊢ Eq (α := X ⟶ tensorUnit.{v, u} C (𝒞 := inst)) (f ≫ ε) ε

Tactic:
IsComonHom.hom_counit f

Premises used: CategoryTheory.IsComonHom.hom_counit
-- Module: Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : BraidedCategory.{v_1, u_1} C
inst_3 : P.IsStableUnderBraiding
c : WideSubcategory P
inst_4 : ComonObj (c.obj (_P := P))
inst_5 : IsCommComonObj.{v_1, u_1} (c.obj (_P := P))
inst_6 : P.IsStableUnderComonoid (c.obj (_P := P))
h :
  Eq (α :=
    c.obj (_P := P) ⟶ (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := WideSubcategory.category P) c c).obj (_P := P))
    (InducedWideCategory.Hom.hom (P := P) (Δ ≫ Iso.hom (β_ c c))) (InducedWideCategory.Hom.hom (P := P) Δ)
⊢ Eq (α := c ⟶ MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := WideSubcategory.category P) c c) (Δ ≫ Iso.hom (β_ c c))
    Δ

Tactic:
ext
-- Module: Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : BraidedCategory.{v_1, u_1} C
inst_3 : P.IsStableUnderBraiding
c : WideSubcategory P
inst_4 : ComonObj (c.obj (_P := P))
inst_5 : IsCommComonObj.{v_1, u_1} (c.obj (_P := P))
inst_6 : P.IsStableUnderComonoid (c.obj (_P := P))
⊢ Eq (α :=
    c.obj (_P := P) ⟶ (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := WideSubcategory.category P) c c).obj (_P := P))
    (InducedWideCategory.Hom.hom (P := P) (Δ ≫ Iso.hom (β_ c c))) (InducedWideCategory.Hom.hom (P := P) Δ)

Tactic:
IsCommComonObj.comul_comm _

Premises used: CategoryTheory.IsCommComonObj.comul_comm
-- Module: Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : BraidedCategory.{v_1, u_1} C
inst_3 : P.IsStableUnderBraiding
c : WideSubcategory P
inst_4 : ComonObj (c.obj (_P := P))
inst_5 : IsCommComonObj.{v_1, u_1} (c.obj (_P := P))
inst_6 : P.IsStableUnderComonoid (c.obj (_P := P))
⊢ Eq (α :=
    c.obj (_P := P) ⟶ (MonoidalCategoryStruct.tensorObj.{v_1, u_1} (𝒞 := WideSubcategory.category P) c c).obj (_P := P))
    (InducedWideCategory.Hom.hom (P := P) (Δ ≫ Iso.hom (β_ c c))) (InducedWideCategory.Hom.hom (P := P) Δ)

Tactic:
exact IsCommComonObj.comul_comm _

Premises used: CategoryTheory.IsCommComonObj.comul_comm
-- Module: Mathlib.CategoryTheory.Core
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
x y z : Core C
f : x ⟶ y
g : y ⟶ z
⊢ (f ≫ g).iso = f.iso ≪≫ g.iso

Tactic:
rfl

Premises used: CategoryTheory.Iso.trans, rfl
-- Module: Mathlib.CategoryTheory.Core
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Core C
f g : X ⟶ Y
h : f.iso.hom = g.iso.hom
iso : f.iso = g.iso
⊢ f = g

Tactic:
apply CoreHom.ext

Premises used: CategoryTheory.CoreHom.ext
-- Module: Mathlib.CategoryTheory.Core
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Core C
f g : X ⟶ Y
h : f.iso.hom = g.iso.hom
⊢ f.iso = g.iso

Tactic:
Iso.ext h

Premises used: CategoryTheory.Iso.ext
-- Module: Mathlib.CategoryTheory.Core
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Core C
f g : X ⟶ Y
h : f.iso.hom = g.iso.hom
⊢ f.iso = g.iso

Tactic:
exact Iso.ext h

Premises used: CategoryTheory.Iso.ext
-- Module: Mathlib.CategoryTheory.Core
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (X : Core C), (F.core ⋙ Core.inclusion D).obj X = (Core.inclusion C ⋙ F).obj X
⊢ ∀ (X : Core C), (F.core ⋙ Core.inclusion D).obj X = (Core.inclusion C ⋙ F).obj X

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Core
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
β : G ≅ H
⊢ (α ≪≫ β).core = α.core ≪≫ β.core

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Iso.core, CategoryTheory.Iso.trans, CategoryTheory.Iso.app, rfl, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Core
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ core (refl F) = refl F.core

Tactic:
rfl

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Iso.core, CategoryTheory.NatTrans.id, CategoryTheory.Iso.app, rfl, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Core
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Type u₂
inst_1 : Groupoid.{v₂, u₂} G
G' : Type u₃
inst_2 : Groupoid.{v₃, u₃} G'
H : Functor.{v₂, v₁, u₂, u₁} G C
F : Functor.{v₃, v₂, u₃, u₂} G' G
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : ∀ (X : G'), (functorToCore (F ⋙ H)).obj X = (F ⋙ functorToCore H).obj X
⊢ ∀ (X : G'), (functorToCore (F ⋙ H)).obj X = (F ⋙ functorToCore H).obj X

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Core
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Type u₂
inst_1 : Groupoid.{v₂, u₂} G
C' : Type u₄
inst_2 : Category.{v₄, u₄} C'
H : Functor.{v₂, v₁, u₂, u₁} G C
F : Functor.{v₁, v₄, u₁, u₄} C C'
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : ∀ (X : G), (functorToCore (H ⋙ F)).obj X = (functorToCore H ⋙ F.core).obj X
⊢ ∀ (X : G), (functorToCore (H ⋙ F)).obj X = (functorToCore H ⋙ F.core).obj X

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Core
Goal:
G : Type u₂
inst : Groupoid.{v₂, u₂} G
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (X : Core G), obj.{v₂, v₂, u₂, u₂} (inclusion G ⋙ functorToCore (𝟭 G)) X = obj.{v₂, v₂, u₂, u₂} (𝟭 (Core G)) X
⊢ ∀ (X : Core G), obj.{v₂, v₂, u₂, u₂} (inclusion G ⋙ functorToCore (𝟭 G)) X = obj.{v₂, v₂, u₂, u₂} (𝟭 (Core G)) X

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Core
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (X : Core C), obj.{v₁, v₁, u₁, u₁} (functorToCore (inclusion C)) X = obj.{v₁, v₁, u₁, u₁} (𝟭 (Core C)) X
⊢ ∀ (X : Core C), obj.{v₁, v₁, u₁, u₁} (functorToCore (inclusion C)) X = obj.{v₁, v₁, u₁, u₁} (𝟭 (Core C)) X

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Core
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst_1 : EquivFunctor m
α : Core (Type u₁)
h :
  ∀ (x : { of := m α.of }.of),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            { iso := (EquivFunctor.mapEquiv m (CoreHom.iso (𝟙 α)).toEquiv).toIso :
                  CoreHom { of := m α.of : Core (Type u₂) } { of := m α.of : Core (Type u₂) } }.iso.hom).toFun
        x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (CoreHom.iso (𝟙 { of := m α.of : Core (Type u₂) })).hom).toFun x
⊢ { iso := (EquivFunctor.mapEquiv m (CoreHom.iso (𝟙 α)).toEquiv).toIso :
      CoreHom { of := m α.of : Core (Type u₂) } { of := m α.of : Core (Type u₂) } } =
    𝟙 { of := m α.of }

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Core
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst_1 : EquivFunctor m
α : Core (Type u₁)
x : { of := m α.of }.of
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          { iso := (EquivFunctor.mapEquiv m (CoreHom.iso (𝟙 α)).toEquiv).toIso :
                CoreHom { of := m α.of : Core (Type u₂) } { of := m α.of : Core (Type u₂) } }.iso.hom).toFun
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (CoreHom.iso (𝟙 { of := m α.of : Core (Type u₂) })).hom).toFun x

Tactic:
congr_fun (EquivFunctor.map_refl' _) x

Premises used: CategoryTheory.Iso.toEquiv, EquivFunctor.map_refl', congr_fun, Equiv.refl
-- Module: Mathlib.CategoryTheory.Core
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst_1 : EquivFunctor m
α : Core (Type u₁)
x : { of := m α.of }.of
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          { iso := (EquivFunctor.mapEquiv m (CoreHom.iso (𝟙 α)).toEquiv).toIso :
                CoreHom { of := m α.of : Core (Type u₂) } { of := m α.of : Core (Type u₂) } }.iso.hom).toFun
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (CoreHom.iso (𝟙 { of := m α.of : Core (Type u₂) })).hom).toFun x

Tactic:
exact congr_fun (EquivFunctor.map_refl' _) x

Premises used: EquivFunctor.map_refl', congr_fun
-- Module: Mathlib.CategoryTheory.Core
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst_1 : EquivFunctor m
X Y Z : Core (Type u₁)
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (x : { of := m X.of }.of),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            { iso := (EquivFunctor.mapEquiv m (f ≫ g).iso.toEquiv).toIso :
                  CoreHom { of := m X.of : Core (Type u₂) } { of := m Z.of : Core (Type u₂) } }.iso.hom).toFun
        x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
            (CoreHom.iso
              ({ iso := (EquivFunctor.mapEquiv m f.iso.toEquiv).toIso :
                  CoreHom { of := m X.of : Core (Type u₂) } { of := m Y.of : Core (Type u₂) } } ≫
                { iso := (EquivFunctor.mapEquiv m g.iso.toEquiv).toIso :
                  CoreHom { of := m Y.of : Core (Type u₂) } { of := m Z.of : Core (Type u₂) } }))))
        x
⊢ { iso := (EquivFunctor.mapEquiv m (f ≫ g).iso.toEquiv).toIso :
      CoreHom { of := m X.of : Core (Type u₂) } { of := m Z.of : Core (Type u₂) } } =
    { iso := (EquivFunctor.mapEquiv m f.iso.toEquiv).toIso :
        CoreHom { of := m X.of : Core (Type u₂) } { of := m Y.of : Core (Type u₂) } } ≫
      { iso := (EquivFunctor.mapEquiv m g.iso.toEquiv).toIso }

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Core
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst_1 : EquivFunctor m
X Y Z : Core (Type u₁)
f : X ⟶ Y
g : Y ⟶ Z
x : { of := m X.of }.of
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          { iso := (EquivFunctor.mapEquiv m (f ≫ g).iso.toEquiv).toIso :
                CoreHom { of := m X.of : Core (Type u₂) } { of := m Z.of : Core (Type u₂) } }.iso.hom).toFun
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
          (CoreHom.iso
            ({ iso := (EquivFunctor.mapEquiv m f.iso.toEquiv).toIso :
                CoreHom { of := m X.of : Core (Type u₂) } { of := m Y.of : Core (Type u₂) } } ≫
              { iso := (EquivFunctor.mapEquiv m g.iso.toEquiv).toIso :
                CoreHom { of := m Y.of : Core (Type u₂) } { of := m Z.of : Core (Type u₂) } }))))
      x

Tactic:
simp [Equiv.toIso, EquivFunctor.map_trans']

Premises used: EquivFunctor.map_trans', Equiv.toIso
-- Module: Mathlib.CategoryTheory.Countable
Goal:
α : Type u_1
inst : Countable α
⊢ Countable.{u_1 + 1} (Discrete α)

Tactic:
Countable.of_equiv α discreteEquiv.symm

Premises used: Countable.of_equiv, Equiv.symm, CategoryTheory.discreteEquiv
-- Module: Mathlib.CategoryTheory.Countable
Goal:
J : Type u
inst : Countable J
inst_1 : Category.{v_1, u} J
inst_2 : Quiver.IsThin.{u, v_1} J
⊢ CountableCategory.{v_1, u} J

Tactic:
CountableCategory.mk inferInstance (fun _ _ ↦ ⟨fun _ ↦ 0, fun _ _ _ ↦ Subsingleton.elim _ _⟩)

Premises used: inferInstance, CategoryTheory.CountableCategory.mk, Countable.mk, Exists.intro, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Countable
Goal:
α : Type u
inst : Category.{v, u} α
inst_1 : CountableCategory.{v, u} α
⊢ Countable (ObjAsType.{v, u} α)

Tactic:
Countable.of_equiv α (equivShrink.{0} α)

Premises used: Countable.of_equiv, equivShrink
-- Module: Mathlib.CategoryTheory.Countable
Goal:
α : Type u
inst : Category.{v, u} α
inst_1 : CountableCategory.{v, u} α
i j : ObjAsType.{v, u} α
⊢ Countable.{v + 1} (i ⟶ j)

Tactic:
Countable.of_equiv _ InducedCategory.homEquiv.symm

Premises used: Countable.of_equiv, CategoryTheory.InducedCategory.homEquiv, Equiv.symm
-- Module: Mathlib.CategoryTheory.Countable
Goal:
α : Type u
inst : Category.{v, u} α
inst_1 : CountableCategory.{v, u} α
⊢ Countable (HomAsType.{v, u} α)

Tactic:
Countable.of_equiv α (equivShrink.{0} α)

Premises used: Countable.of_equiv, equivShrink
-- Module: Mathlib.CategoryTheory.Countable
Goal:
α : Type u
inst : Category.{v, u} α
inst_1 : CountableCategory.{v, u} α
i j : HomAsType.{v, u} α
⊢ Countable (i ⟶ j)

Tactic:
Countable.of_equiv ((ShrinkHoms.equivalence _).inverse.obj i ⟶
    (ShrinkHoms.equivalence _).inverse.obj j)
    (Functor.FullyFaithful.ofFullyFaithful _).homEquiv.symm

Premises used: Countable.of_equiv, Quiver.Hom, CategoryTheory.Functor.FullyFaithful.homEquiv, CategoryTheory.ShrinkHoms.equivalence, Equiv.symm, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Dialectica.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y Z : Dial.{v, u} C
F : X.Hom Y
G : Y.Hom Z
⊢ LE.le (α := Subobject.{v, u} (Limits.prod.{v, u} X.src Z.tgt))
    (Functor.obj (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)) X.rel)
    (Functor.obj (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))) Z.rel)

Tactic:
le_trans ?_ <| ((Subobject.pullback (π(π₁, prod.map F.f (𝟙 _) ≫ G.F))).monotone F.le).trans <|
    le_trans ?_ <| ((Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).monotone G.le).trans ?_

Premises used: CategoryTheory.Dial.Hom.F, CategoryTheory.Limits.prod.fst, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.monotone, CategoryTheory.Dial.Hom.le, CategoryTheory.Subobject.pullback, CategoryTheory.CategoryStruct.comp, LE.le.trans, CategoryTheory.Dial.tgt, CategoryTheory.Limits.prod.lift, CategoryTheory.Dial.Hom.f, CategoryTheory.Limits.prod.map, le_trans