awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso
Goal:
C : Type (u + 1)
inst : Category.{v_1, u + 1} C
FC : C → C → Type u
CC : C → Type u
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u, v_1, u + 1, u} C FC (CC := CC)
D : Type (u + 1)
inst_3 : Category.{v_2, u + 1} D
FD : D → D → Type u
CD : D → Type u
inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory.{u, v_2, u + 1, u} D FD (CC := CD)
inst_6 : HasForget₂.{u, v_1, u + 1, u, v_2, u + 1, u} C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)
inst_7 : Functor.ReflectsIsomorphisms.{v_1, u + 1, u, u + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
i :
  IsIso.{v_2, u + 1} (X :=
    Functor.obj.{v_1, v_2, u + 1, u + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X)
    (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f)
⊢ IsIso (X :=
    Functor.obj.{v_2, u, u + 1, u + 1} (forget D (FC := FD) (CC := CD))
      (Functor.obj.{v_1, v_2, u + 1, u + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X))
    (Functor.map (forget D (FC := FD) (CC := CD))
      (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f))

Tactic:
haveI i' : IsIso ((forget D).map ((forget₂ C D).map f)) := Functor.map_isIso (forget D) _
-- Module: Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso
Goal:
C : Type (u + 1)
inst : Category.{v_1, u + 1} C
FC : C → C → Type u
CC : C → Type u
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u, v_1, u + 1, u} C FC (CC := CC)
D : Type (u + 1)
inst_3 : Category.{v_2, u + 1} D
FD : D → D → Type u
CD : D → Type u
inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory.{u, v_2, u + 1, u} D FD (CC := CD)
inst_6 : HasForget₂.{u, v_1, u + 1, u, v_2, u + 1, u} C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)
inst_7 : Functor.ReflectsIsomorphisms.{v_1, u + 1, u, u + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
i :
  IsIso.{v_2, u + 1} (X :=
    Functor.obj.{v_1, v_2, u + 1, u + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X)
    (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f)
i' :
  IsIso (X :=
    Functor.obj.{v_2, u, u + 1, u + 1} (forget D (FC := FD) (CC := CD))
      (Functor.obj.{v_1, v_2, u + 1, u + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X))
    (Functor.map (forget D (FC := FD) (CC := CD))
      (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f))
rwa rwa₁ rwa₂ rwa₃ :
  IsIso (X :=
    Functor.obj.{v_1, u, u + 1, u + 1}
      (Functor.comp.{v_1, v_2, u, u + 1, u + 1, u + 1} (@HasForget₂.forget₂ _ _ FC CC _ inst_2 _ _ FD CD _ inst_5 _)
        (forget D (FC := FD) (CC := CD)))
      X)
    (Functor.map
      (Functor.comp.{v_1, v_2, u, u + 1, u + 1, u + 1} (@HasForget₂.forget₂ _ _ FC CC _ inst_2 _ _ FD CD _ inst_5 _)
        (forget D (FC := FD) (CC := CD)))
      f)
⊢ IsIso (X := Functor.obj.{v_1, u, u + 1, u + 1} (forget C (FC := FC) (CC := CC)) X)
    (Functor.map (forget C (FC := FC) (CC := CC)) f)

Tactic:
rwa [← @HasForget₂.forget_comp C _ _ _ _ _ D _ _ _ _ _]

Premises used: CategoryTheory.HasForget₂.forget_comp
-- Module: Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso
Goal:
C : Type (u + 1)
inst : Category.{v_1, u + 1} C
FC : C → C → Type u
CC : C → Type u
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u, v_1, u + 1, u} C FC (CC := CC)
D : Type (u + 1)
inst_3 : Category.{v_2, u + 1} D
FD : D → D → Type u
CD : D → Type u
inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory.{u, v_2, u + 1, u} D FD (CC := CD)
inst_6 : HasForget₂.{u, v_1, u + 1, u, v_2, u + 1, u} C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)
inst_7 : Functor.ReflectsIsomorphisms.{v_1, u + 1, u, u + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
i :
  IsIso.{v_2, u + 1} (X :=
    Functor.obj.{v_1, v_2, u + 1, u + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X)
    (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f)
i' :
  IsIso (X :=
    Functor.obj.{v_2, u, u + 1, u + 1} (forget D (FC := FD) (CC := CD))
      (Functor.obj.{v_1, v_2, u + 1, u + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X))
    (Functor.map (forget D (FC := FD) (CC := CD))
      (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f))
⊢ IsIso (X := Functor.obj.{v_1, u, u + 1, u + 1} (forget C (FC := FC) (CC := CC)) X)
    (Functor.map (forget C (FC := FC) (CC := CC)) f)

Tactic:
haveI : IsIso ((forget C).map f) := by
        rwa [← @HasForget₂.forget_comp C _ _ _ _ _ D _ _ _ _ _]
-- Module: Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso
Goal:
C : Type (u + 1)
inst : Category.{v_1, u + 1} C
FC : C → C → Type u
CC : C → Type u
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u, v_1, u + 1, u} C FC (CC := CC)
D : Type (u + 1)
inst_3 : Category.{v_2, u + 1} D
FD : D → D → Type u
CD : D → Type u
inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory.{u, v_2, u + 1, u} D FD (CC := CD)
inst_6 : HasForget₂.{u, v_1, u + 1, u, v_2, u + 1, u} C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)
inst_7 : Functor.ReflectsIsomorphisms.{v_1, u + 1, u, u + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
i :
  IsIso.{v_2, u + 1} (X :=
    Functor.obj.{v_1, v_2, u + 1, u + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X)
    (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f)
i' :
  IsIso (X :=
    Functor.obj.{v_2, u, u + 1, u + 1} (forget D (FC := FD) (CC := CD))
      (Functor.obj.{v_1, v_2, u + 1, u + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X))
    (Functor.map (forget D (FC := FD) (CC := CD))
      (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f))
this :
  IsIso (X := Functor.obj.{v_1, u, u + 1, u + 1} (forget C (FC := FC) (CC := CC)) X)
    (Functor.map (forget C (FC := FC) (CC := CC)) f)
⊢ IsIso f

Tactic:
apply isIso_of_reflects_iso f (forget C)

Premises used: CategoryTheory.isIso_of_reflects_iso, CategoryTheory.forget
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Representable
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
CD : D → Type u_3
FD : D → D → Type u_4
inst_2 : (X Y : D) → FunLike.{u_4 + 1, u_3 + 1, u_3 + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{u_3, v_2, u_2, u_4} D FD (CC := CD)
Y : C
α : (F ⋙ forget D (FC := FD) (CC := CD)).RepresentableBy Y
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
⊢ Eq.{u_3 + 1} (α := ToType.{u_3, v_2, u_2, u_4} (FC := FD) (CC := CD) (F.obj (op X)))
    (((α.homEquiv' (CD := CD) (FD := FD) :
            Equiv.{v_1 + 1, u_3 + 1} (X ⟶ Y) (ToType.{u_3, v_2, u_2, u_4} (FC := FD) (CC := CD) (F.obj (op X)))) :
          (a : X ⟶ Y) → ToType (F.obj (op X)))
        (f ≫ g) :
      ToType.{u_3, v_2, u_2, u_4} (FC := FD) (CC := CD) (F.obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map f.op) : (a : CD (F.obj (op X'))) → CD (F.obj (op X)))
        (((α.homEquiv' (CD := CD) (FD := FD) :
                Equiv.{v_1 + 1, u_3 + 1} (X' ⟶ Y) (ToType.{u_3, v_2, u_2, u_4} (FC := FD) (CC := CD) (F.obj (op X')))) :
              (a : X' ⟶ Y) → ToType (F.obj (op X')))
            g :
          ToType.{u_3, v_2, u_2, u_4} (FC := FD) (CC := CD) (F.obj (op X'))) :
      CD (F.obj (op X)))

Tactic:
α.homEquiv_comp _ _

Premises used: CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Conj
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : End X
⊢ (α.conj : (a : End X) → End Y) f = α.inv ≫ f ≫ α.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Conj
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f g : End X
⊢ Eq (α := End Y) ((α.conj : (a : End X) → End Y) (f ≫ g) : End Y)
    (CategoryStruct.comp (Y := Y) ((α.conj : (a : End X) → End Y) f) ((α.conj : (a : End X) → End Y) g) : Y ⟶ Y)

Tactic:
map_mul α.conj g f

Premises used: CategoryTheory.Iso.conj, map_mul
-- Module: Mathlib.CategoryTheory.Conj
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ Eq (α := End Y) ((α.conj : (a : End X) → End Y) (𝟙 X) : End Y) (𝟙 Y : Y ⟶ Y)

Tactic:
map_one α.conj

Premises used: CategoryTheory.Iso.conj, map_one
-- Module: Mathlib.CategoryTheory.Conj
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : End X
rw : inv (refl X) ≫ f ≫ hom (refl X) = f
rw₁ : 𝟙 X ≫ f ≫ hom (refl X) = f
rw₂ : 𝟙 X ≫ f ≫ 𝟙 X = f
rw₃ : f ≫ 𝟙 X = f
rw₄ rw₅ : f = f
⊢ (conj (refl X) : (a : End X) → End X) f = f

Tactic:
rw [conj_apply, Iso.refl_inv, Iso.refl_hom, Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Iso.refl_inv, CategoryTheory.Iso.refl_hom, CategoryTheory.Iso.conj_apply, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Conj
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
Z : C
β : Y ≅ Z
f : End X
⊢ Eq (α := End Z) (((α ≪≫ β).conj : (a : End X) → End Z) f : End Z)
    ((β.conj : (a : End Y) → End Z) ((α.conj : (a : End X) → End Y) f : End Y) : End Z)

Tactic:
homCongr_trans α α β β f

Premises used: CategoryTheory.Iso.homCongr_trans, CategoryTheory.End
-- Module: Mathlib.CategoryTheory.Conj
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : End X
rw : ((α ≪≫ α.symm).conj : (a : End X) → End X) f = f
rw₁ : (conj (refl X) : (a : End X) → End X) f = f
rw₂ rw₃ : f = f
⊢ (α.symm.conj : (a : End Y) → End X) ((α.conj : (a : End X) → End Y) f : End Y) = f

Tactic:
rw [← trans_conj, α.self_symm_id, refl_conj]

Premises used: CategoryTheory.Iso.refl_conj, CategoryTheory.Iso.self_symm_id, CategoryTheory.Iso.trans_conj
-- Module: Mathlib.CategoryTheory.Conj
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : End Y
⊢ (α.conj : (a : End X) → End Y) ((α.symm.conj : (a : End Y) → End X) f : End X) = f

Tactic:
α.symm.symm_self_conj f

Premises used: CategoryTheory.Iso.symm_self_conj, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Conj
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : End X
n : ℕ
⊢ (α.conj : (a : End X) → End Y) (f ^ n) = HPow.hPow (α := End Y) ((α.conj : (a : End X) → End Y) f : End Y) n

Tactic:
α.conj.toMonoidHom.map_pow f n

Premises used: CategoryTheory.Iso.conj, MulEquiv.toMonoidHom, MonoidHom.map_pow
-- Module: Mathlib.CategoryTheory.Conj
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Aut X
⊢ Eq (α := Y ⟶ Y) (hom ((α.conjAut : (a : Aut X) → Aut Y) f) : Y ⟶ Y) ((α.conj : (a : End X) → End Y) f.hom : End Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Conj
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
Z : C
β : Y ≅ Z
f : Aut X
⊢ Eq (α := Aut Z) (((α ≪≫ β).conjAut : (a : Aut X) → Aut Z) f : Aut Z)
    ((β.conjAut : (a : Aut Y) → Aut Z) ((α.conjAut : (a : Aut X) → Aut Y) f : Aut Y) : Aut Z)

Tactic:
simp only [conjAut_apply, Iso.trans_symm, Iso.trans_assoc]

Premises used: CategoryTheory.Iso.conjAut_apply, CategoryTheory.Iso.trans_assoc, CategoryTheory.Iso.trans_symm
-- Module: Mathlib.CategoryTheory.Conj
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f g : Aut X
⊢ (α.conjAut : (a : Aut X) → Aut Y) (f * g) =
    HMul.hMul (α := Aut Y) (β := Aut Y) ((α.conjAut : (a : Aut X) → Aut Y) f : Aut Y)
      ((α.conjAut : (a : Aut X) → Aut Y) g : Aut Y)

Tactic:
map_mul α.conjAut f g

Premises used: CategoryTheory.Iso.conjAut, map_mul
-- Module: Mathlib.CategoryTheory.Conj
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f g : Aut X
⊢ Eq (α := Aut Y) ((α.conjAut : (a : Aut X) → Aut Y) (f ≪≫ g) : Aut Y)
    (trans (Y := Y) ((α.conjAut : (a : Aut X) → Aut Y) f) ((α.conjAut : (a : Aut X) → Aut Y) g) : Y ≅ Y)

Tactic:
conjAut_mul α g f

Premises used: CategoryTheory.Iso.conjAut_mul
-- Module: Mathlib.CategoryTheory.Conj
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Aut X
n : ℕ
⊢ (α.conjAut : (a : Aut X) → Aut Y) (f ^ n) = HPow.hPow (α := Aut Y) ((α.conjAut : (a : Aut X) → Aut Y) f : Aut Y) n

Tactic:
map_pow α.conjAut f n

Premises used: CategoryTheory.Iso.conjAut, map_pow
-- Module: Mathlib.CategoryTheory.Conj
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Aut X
n : ℤ
⊢ (α.conjAut : (a : Aut X) → Aut Y) (f ^ n) = HPow.hPow (α := Aut Y) ((α.conjAut : (a : Aut X) → Aut Y) f : Aut Y) n

Tactic:
map_zpow α.conjAut f n

Premises used: CategoryTheory.Iso.conjAut, map_zpow
-- Module: Mathlib.CategoryTheory.Conj
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
X Y : C
α : X ≅ Y
f : End X
⊢ Eq (α := F.obj Y ⟶ F.obj Y) (F.map ((α.conj : (a : End X) → End Y) f))
    (((F.mapIso α).conj : (a : End (F.obj X)) → End (F.obj Y)) (F.map f))

Tactic:
map_homCongr F α α f

Premises used: CategoryTheory.Functor.map_homCongr
-- Module: Mathlib.CategoryTheory.Conj
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
X Y : C
α : X ≅ Y
f : Aut X
w :
  Eq (α := F.obj Y ⟶ F.obj Y) (Iso.hom (F.mapIso ((α.conjAut : (a : Aut X) → Aut Y) f)))
    (Iso.hom (((F.mapIso α).conjAut : (a : Aut (F.obj X)) → Aut (F.obj Y)) (F.mapIso f)))
⊢ Eq (α := F.obj Y ≅ F.obj Y) (F.mapIso ((α.conjAut : (a : Aut X) → Aut Y) f))
    (((F.mapIso α).conjAut : (a : Aut (F.obj X)) → Aut (F.obj Y)) (F.mapIso f))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Conj
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
X Y : C
α : X ≅ Y
f : Aut X
⊢ Eq (α := F.obj Y ⟶ F.obj Y) (Iso.hom (F.mapIso ((α.conjAut : (a : Aut X) → Aut Y) f)))
    (Iso.hom (((F.mapIso α).conjAut : (a : Aut (F.obj X)) → Aut (F.obj Y)) (F.mapIso f)))

Tactic:
simp only [mapIso_hom, Iso.conjAut_hom, F.map_conj]

Premises used: CategoryTheory.Functor.map_conj, CategoryTheory.Iso.conjAut_hom, CategoryTheory.Functor.mapIso_hom
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
F : Functor.{v₁, v₂, u₁, u₂} J K
j : J
⊢ F.mapConnectedComponents ⟦j⟧ = ⟦F.obj j⟧

Tactic:
rfl

Premises used: CategoryTheory.Functor.mapConnectedComponents, rfl
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J_1 : Type u₁
inst : Category.{v₁, u₁} J_1
J : Type u_2
inst_1 : Category.{v_1, u_2} J
X : Type u_1
f : ConnectedComponents.{v_1, u_2} J → X
x : ConnectedComponents.{v_1, u_2} J
obtain : ∀ (x_1 : J) (h : ⟦x_1⟧ = x), liftFunctor J (functorToDiscrete X f) x = f x
⊢ liftFunctor J (functorToDiscrete X f) x = f x

Tactic:
obtain ⟨x, h⟩ := Quotient.exists_rep x

Premises used: Quotient.exists_rep
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J_1 : Type u₁
inst : Category.{v₁, u₁} J_1
J : Type u_2
inst_1 : Category.{v_1, u_2} J
X : Type u_1
f : ConnectedComponents.{v_1, u_2} J → X
x_1 : ConnectedComponents.{v_1, u_2} J
x : J
h : ⟦x⟧ = x_1
rw : liftFunctor J (functorToDiscrete X f) ⟦x⟧ = f ⟦x⟧
⊢ liftFunctor J (functorToDiscrete X f) x_1 = f x_1

Tactic:
rw [← h]
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J_1 : Type u₁
inst : Category.{v₁, u₁} J_1
J : Type u_2
inst_1 : Category.{v_1, u_2} J
X : Type u_1
f : ConnectedComponents.{v_1, u_2} J → X
x_1 : ConnectedComponents.{v_1, u_2} J
x : J
h : ⟦x⟧ = x_1
⊢ liftFunctor J (functorToDiscrete X f) ⟦x⟧ = f ⟦x⟧

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j : ConnectedComponents.{v₁, u₁} J
h : ∀ (a : J), Nonempty.{u₁ + 1} (ConnectedComponents.Component.{v₁, u₁} (Quotient.mk'' a))
⊢ Nonempty.{u₁ + 1} j.Component

Tactic:
induction j using Quotient.inductionOn'
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
a : J
⊢ Nonempty.{u₁ + 1} (ConnectedComponents.Component.{v₁, u₁} (Quotient.mk'' a))

Tactic:
⟨⟨_, rfl⟩⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, Nonempty.intro, rfl
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
a : J
⊢ Nonempty.{u₁ + 1} (ConnectedComponents.Component.{v₁, u₁} (Quotient.mk'' a))

Tactic:
exact ⟨⟨_, rfl⟩⟩
-- Module: Mathlib.CategoryTheory.ConnectedComponents
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j : ConnectedComponents.{v₁, u₁} J
h : ∀ (j₁ j₂ : j.Component), ∃ (l : List j.Component), List.IsChain Zag.{v₁, u₁} (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
⊢ IsConnected.{v₁, u₁} j.Component

Tactic:
apply isConnected_of_zigzag

Premises used: CategoryTheory.isConnected_of_zigzag
-- 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₁
⊢ Zigzag.{v₁, u₁} j₁ j₂

Tactic:
have h₁₂ : Zigzag j₁ j₂ := Quotient.exact' hj₁
-- 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₂
h :
  ∀ (l : List J) (hl₁ : List.IsChain Zag.{v₁, u₁} (j₁ :: l)) (hl₂ : (j₁ :: l).getLast ⋯ = j₂),
    ∃ (l : List (ConnectedComponents.Component.{v₁, u₁} (Quotient.mk'' j₂))),
      List.IsChain Zag.{v₁, u₁}
          (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ :: l) ∧
        (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ ::
                l).getLast
            ⋯ =
          ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₂ ⋯
⊢ ∃ (l : List (ConnectedComponents.Component.{v₁, u₁} (Quotient.mk'' j₂))),
    List.IsChain Zag.{v₁, u₁}
        (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ :: l) ∧
      (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ ::
              l).getLast
          ⋯ =
        ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₂ ⋯

Tactic:
rcases List.exists_isChain_cons_of_relationReflTransGen h₁₂ with ⟨l, hl₁, hl₂⟩

Premises used: List.exists_isChain_cons_of_relationReflTransGen
-- 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 ⋯
i : J
hi : i ∈ l
apply : ∀ ⦃x y : J⦄, Zag.{v₁, u₁} x y → (fun (t : J) ↦ Zigzag.{v₁, u₁} t j₂) y → (fun (t : J) ↦ Zigzag.{v₁, u₁} t j₂) x
apply₁ : Zigzag.{v₁, u₁} j₂ j₂
⊢ Zigzag.{v₁, u₁} i j₂

Tactic:
apply hl₁.backwards_cons_induction (fun t => Zigzag t j₂) _ hl₂ _ _ _ (List.mem_of_mem_tail hi)

Premises used: CategoryTheory.Zigzag, List.mem_of_mem_tail, List.IsChain.backwards_cons_induction
-- 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 ⋯
i : J
hi : i ∈ l
j k : J
⊢ Zag.{v₁, u₁} j k → (fun (t : J) ↦ Zigzag.{v₁, u₁} t j₂) k → (fun (t : J) ↦ Zigzag.{v₁, u₁} t j₂) j

Tactic:
apply Relation.ReflTransGen.head

Premises used: Relation.ReflTransGen.head
-- 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 ⋯
i : J
hi : i ∈ l
⊢ Zigzag.{v₁, u₁} j₂ j₂

Tactic:
apply Relation.ReflTransGen.refl

Premises used: Relation.ReflTransGen.refl
-- 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 ⋯
⊢ ∀ a ∈ l, Zigzag.{v₁, u₁} a j₂

Tactic:
have hf : ∀ a : J, a ∈ l → Zigzag a j₂ := by
    intro i hi
    apply hl₁.backwards_cons_induction (fun t => Zigzag t j₂) _ hl₂ _ _ _ (List.mem_of_mem_tail hi)
    · intro j k
      apply Relation.ReflTransGen.head
    · apply Relation.ReflTransGen.refl
-- 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₂
⊢ (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).getLast
      ⋯ =
    ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₂ ⋯

Tactic:
grind
-- 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 :
  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)
⊢ ∃ (l : List (ConnectedComponents.Component.{v₁, u₁} (Quotient.mk'' j₂))),
    List.IsChain Zag.{v₁, u₁}
        (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ :: l) ∧
      (ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₁ hj₁ ::
              l).getLast
          ⋯ =
        ObjectProperty.FullSubcategory.mk (P := ConnectedComponents.objectProperty (Quotient.mk'' j₂)) j₂ ⋯

Tactic:
refine ⟨l.pmap f hf, ?_, by grind⟩