awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
h :
  { f := p.f, comm := ⋯ : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.Hom P } ≫ { f := p.f, comm := ⋯ } =
      𝟙 { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C } ∧
    { f := p.f, comm := ⋯ : P.Hom { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C } } ≫
        { f := p.f, comm := ⋯ } =
      p
⊢ ∃ (e : P ⟶ { X := P.X, p := p.f, idem := hp }),
    { f := p.f, comm := ⋯ : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.Hom P } ≫ e =
        𝟙 { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C } ∧
      e ≫ { f := p.f, comm := ⋯ : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.Hom P } = p

Tactic:
use ⟨p.f, by rw [hp, p_comp p]⟩
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ { f := p.f, comm := ⋯ : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.Hom P } ≫ { f := p.f, comm := ⋯ } =
      𝟙 { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C } ∧
    { f := p.f, comm := ⋯ : P.Hom { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C } } ≫
        { f := p.f, comm := ⋯ } =
      p

Tactic:
simp [hp]
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : IsIdempotentComplete.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
rcases : ∀ (Y : C) (i : Y ⟶ P.X) (e : P.X ⟶ Y) (h₁ : i ≫ e = 𝟙 Y) (h₂ : e ≫ i = P.p), Functor.essImage (toKaroubi C) P
⊢ Functor.essImage (toKaroubi C) P

Tactic:
rcases IsIdempotentComplete.idempotents_split P.X P.p P.idem with ⟨Y, i, e, ⟨h₁, h₂⟩⟩

Premises used: CategoryTheory.Idempotents.Karoubi.p, CategoryTheory.Idempotents.Karoubi.X, CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.IsIdempotentComplete.idempotents_split
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : IsIdempotentComplete.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
h : Nonempty.{v_1 + 1} (Functor.obj (toKaroubi C) Y ≅ P)
⊢ Functor.essImage (toKaroubi C) P

Tactic:
use Y
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : IsIdempotentComplete.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ p (Functor.obj (toKaroubi C) Y) ≫ i ≫ P.p = i

Tactic:
simp [← Category.assoc, h₁, ← h₂]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : IsIdempotentComplete.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ P.p ≫ e ≫ p (Functor.obj (toKaroubi C) Y) = e

Tactic:
simp [Category.assoc, h₁, ← h₂]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : IsIdempotentComplete.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ Nonempty.{v_1 + 1} (Functor.obj (toKaroubi C) Y ≅ P)

Tactic:
exact
      Nonempty.intro
        { hom := ⟨i, by simp [← Category.assoc, h₁, ← h₂]⟩
          inv := ⟨e, by simp [Category.assoc, h₁, ← h₂]⟩ }

Premises used: Nonempty.intro
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
⊢ Functor.Additive (D := Karoubi.{v_1, u_1} C) (Equivalence.functor (toKaroubiEquivalence C))

Tactic:
inferInstanceAs <| (toKaroubi C).Additive

Premises used: _private.0.CategoryTheory.Idempotents.toKaroubiEquivalence_functor_additive._proof_1
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
rw : P.p ≫ P.p ≫ 𝟙 P.X = P.p
rw₁ : P.p ≫ P.p = P.p
rw₂ rw₃ : P.p = P.p
⊢ P.p ≫ P.p ≫ p { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } = P.p

Tactic:
rw [coe_p, comp_id, P.idem]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Idempotents.Karoubi.coe_p, CategoryTheory.Idempotents.Karoubi.idem
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
rw : 𝟙 P.X ≫ P.p ≫ P.p = P.p
rw₁ : P.p ≫ P.p = P.p
rw₂ rw₃ : P.p = P.p
⊢ p { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } ≫ P.p ≫ P.p = P.p

Tactic:
rw [coe_p, id_comp, P.idem]

Premises used: CategoryTheory.Idempotents.Karoubi.coe_p, CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
h : Hom.f (𝟙 P) = (P.decompId_i ≫ P.decompId_p).f
⊢ 𝟙 P = P.decompId_i ≫ P.decompId_p

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
⊢ Hom.f (𝟙 P) = (P.decompId_i ≫ P.decompId_p).f

Tactic:
simp only [comp_f, id_f, P.idem, decompId_i, decompId_p]

Premises used: CategoryTheory.Idempotents.Karoubi.decompId_p, CategoryTheory.Idempotents.Karoubi.id_f, CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.Idempotents.Karoubi.decompId_i
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
h : Hom.f (Functor.map (toKaroubi C) P.p) = (P.decompId_p ≫ P.decompId_i).f
⊢ Functor.map (toKaroubi C) P.p = P.decompId_p ≫ P.decompId_i

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
⊢ Hom.f (Functor.map (toKaroubi C) P.p) = (P.decompId_p ≫ P.decompId_i).f

Tactic:
simp only [comp_f, decompId_p_f, decompId_i_f, P.idem, toKaroubi_map_f]

Premises used: CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Idempotents.toKaroubi_map_f, CategoryTheory.Idempotents.Karoubi.decompId_i_f, CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.Idempotents.Karoubi.decompId_p_f
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom (V := Karoubi.{v_1, u_1} C) (Functor.obj (toKaroubi C) X)
      { X := Karoubi.X.{v_1, u_1} (Functor.obj (toKaroubi C) X),
        p := 𝟙 (Karoubi.X.{v_1, u_1} (Functor.obj (toKaroubi C) X)), idem := ⋯ })
    (decompId_i (Functor.obj (toKaroubi C) X)) (𝟙 (Functor.obj (toKaroubi C) X))

Tactic:
rfl

Premises used: rfl, CategoryTheory.Idempotents.Karoubi.decompId_i
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom (V := Karoubi.{v_1, u_1} C)
      { X := Karoubi.X.{v_1, u_1} (Functor.obj (toKaroubi C) X),
        p := 𝟙 (Karoubi.X.{v_1, u_1} (Functor.obj (toKaroubi C) X)), idem := ⋯ }
      (Functor.obj (toKaroubi C) X))
    (decompId_p (Functor.obj (toKaroubi C) X))
    (𝟙
      { X := Karoubi.X.{v_1, u_1} (Functor.obj (toKaroubi C) X),
        p := 𝟙 (Karoubi.X.{v_1, u_1} (Functor.obj (toKaroubi C) X)), idem := ⋯ })

Tactic:
rfl

Premises used: CategoryTheory.Idempotents.Karoubi.decompId_p, rfl
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
⊢ p { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } ≫
      f.f ≫ p { X := Q.X, p := 𝟙 Q.X, idem := ⋯ : Karoubi.{v_1, u_1} C } =
    f.f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
⊢ Quiver.Hom (V := Karoubi.{v_1, u_1} C) { X := P.X, p := 𝟙 P.X, idem := ⋯ } { X := Q.X, p := 𝟙 Q.X, idem := ⋯ }

Tactic:
exact Hom.mk f.f (by simp)

Premises used: CategoryTheory.Idempotents.Karoubi.Hom.f, CategoryTheory.Idempotents.Karoubi.Hom.mk
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
⊢ f ≫ Q.decompId_i = P.decompId_i ≫ { f := f.f, comm := ⋯ }

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
⊢ P.decompId_p ≫ f =
    { f := f.f, comm := ⋯ :
        Hom { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C }
          { X := Q.X, p := 𝟙 Q.X, idem := ⋯ : Karoubi.{v_1, u_1} C } } ≫
      Q.decompId_p

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
n : ℤ
f : P ⟶ Q
⊢ (n • f).f = n • f.f

Tactic:
map_zsmul (inclusionHom P Q) n f

Premises used: CategoryTheory.Idempotents.Karoubi.inclusionHom, map_zsmul
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Karoubi.{v_1, u_1} C
⊢ X.p ≫ X.p ≫ p (Functor.obj (toKaroubi C) X.X) = X.p

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Karoubi.{v_1, u_1} C
⊢ p (Functor.obj (toKaroubi C) X.X) ≫ X.p ≫ X.p = X.p

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : Epi f
Z : Karoubi.{v_1, u_1} C
g h : Functor.obj (toKaroubi C) Y ⟶ Z
eq : Functor.map (toKaroubi C) f ≫ g = Functor.map (toKaroubi C) f ≫ h
h₁ : g.f = h.f
⊢ g = h

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : Epi f
Z : Karoubi.{v_1, u_1} C
g h : Functor.obj (toKaroubi C) Y ⟶ Z
eq : Functor.map (toKaroubi C) f ≫ g = Functor.map (toKaroubi C) f ≫ h
h₁ : f ≫ g.f = f ≫ h.f
⊢ g.f = h.f

Tactic:
rw [← cancel_epi f]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : Epi f
Z : Karoubi.{v_1, u_1} C
g h : Functor.obj (toKaroubi C) Y ⟶ Z
eq : Functor.map (toKaroubi C) f ≫ g = Functor.map (toKaroubi C) f ≫ h
⊢ f ≫ g.f = f ≫ h.f

Tactic:
simpa using eq
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : Mono f
Z : Karoubi.{v_1, u_1} C
g h : Z ⟶ Functor.obj (toKaroubi C) X
eq : g ≫ Functor.map (toKaroubi C) f = h ≫ Functor.map (toKaroubi C) f
h₁ : g.f = h.f
⊢ g = h

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : Mono f
Z : Karoubi.{v_1, u_1} C
g h : Z ⟶ Functor.obj (toKaroubi C) X
eq : g ≫ Functor.map (toKaroubi C) f = h ≫ Functor.map (toKaroubi C) f
h₁ : g.f ≫ f = h.f ≫ f
⊢ g.f = h.f

Tactic:
rw [← cancel_mono f]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : Mono f
Z : Karoubi.{v_1, u_1} C
g h : Z ⟶ Functor.obj (toKaroubi C) X
eq : g ≫ Functor.map (toKaroubi C) f = h ≫ Functor.map (toKaroubi C) f
⊢ g.f ≫ f = h.f ≫ f

Tactic:
simpa using eq
-- Module: Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi (Karoubi.{v_1, u_1} C)
⊢ P.p.f ≫ P.p.f = P.p.f

Tactic:
simpa only [hom_ext_iff, comp_f] using P.idem

Premises used: CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi (Karoubi.{v_1, u_1} C)
f : P ⟶ Q
⊢ P.p.f ≫ f.f.f = f.f.f ≫ Q.p.f

Tactic:
simpa only [hom_ext_iff, comp_f] using p_comm f

Premises used: CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Idempotents.Karoubi.hom_ext_iff, CategoryTheory.Idempotents.Karoubi.p_comm
-- Module: Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi (Karoubi.{v_1, u_1} C)
⊢ P.p.f ≫ P.p.f = P.p.f

Tactic:
simpa only [hom_ext_iff] using P.idem

Premises used: CategoryTheory.Idempotents.Karoubi.idem, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : Karoubi (Karoubi.{v_1, u_1} C)
f : X ⟶ Y
⊢ { X := X.X.X, p := X.p.f, idem := ⋯ : Karoubi.{v_1, u_1} C }.p ≫
      f.f.f ≫ { X := Y.X.X, p := Y.p.f, idem := ⋯ : Karoubi.{v_1, u_1} C }.p =
    f.f.f

Tactic:
simpa only [hom_ext_iff] using f.comm

Premises used: CategoryTheory.Idempotents.Karoubi.Hom.comm, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (X : Karoubi.{v_1, u_1} C),
    Functor.obj (𝟭 (Karoubi.{v_1, u_1} C)) X = Functor.obj (toKaroubi (Karoubi.{v_1, u_1} C) ⋙ inverse C) X
⊢ ∀ (X : Karoubi.{v_1, u_1} C),
    Functor.obj (𝟭 (Karoubi.{v_1, u_1} C)) X = Functor.obj (toKaroubi (Karoubi.{v_1, u_1} C) ⋙ inverse C) X

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ ∀ (X Y : Karoubi.{v_1, u_1} C) (f : X ⟶ Y),
    Functor.map (𝟭 (Karoubi.{v_1, u_1} C)) f =
      eqToHom ⋯ ≫ Functor.map (toKaroubi (Karoubi.{v_1, u_1} C) ⋙ inverse C) f ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.SimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : IsIdempotentComplete.{v_1, u_1} C
⊢ IsIdempotentComplete (SimplicialObject.{v_1, u_1} C)

Tactic:
Idempotents.functor_category_isIdempotentComplete _ _

Premises used: CategoryTheory.Idempotents.functor_category_isIdempotentComplete
-- Module: Mathlib.CategoryTheory.Idempotents.SimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : IsIdempotentComplete.{v_1, u_1} C
⊢ IsIdempotentComplete (CosimplicialObject.{v_1, u_1} C)

Tactic:
Idempotents.functor_category_isIdempotentComplete _ _

Premises used: CategoryTheory.CosimplicialObject, CategoryTheory.Idempotents.functor_category_isIdempotentComplete
-- Module: Mathlib.CategoryTheory.InducedCategory
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v, u₂} D
F : C → D
X Y : InducedCategory D F
f g : X ⟶ Y
h : f.hom = g.hom
⊢ f = g

Tactic:
Hom.ext h

Premises used: CategoryTheory.InducedCategory.Hom.ext
-- Module: Mathlib.CategoryTheory.InducedCategory
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v, u₂} D
F : C → D
⊢ Functor.Full.{v, v, u₁, u₂} (inducedFunctor F)

Tactic:
(fullyFaithfulInducedFunctor F).full

Premises used: CategoryTheory.fullyFaithfulInducedFunctor, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.CategoryTheory.InducedCategory
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v, u₂} D
F : C → D
⊢ Functor.Faithful.{v, v, u₁, u₂} (inducedFunctor F)

Tactic:
(fullyFaithfulInducedFunctor F).faithful

Premises used: CategoryTheory.fullyFaithfulInducedFunctor, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
inst_2 : IsPreconnected.{v₁, u₁} J
α : Type u₂
F : Functor.{v₁, u₂, u₁, u₂} J (Discrete α)
j : J
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    Eq (α :=
      obj.{v₁, u₂, u₁, u₂}
          (obj (const J) ((IsPreconnected.IsoConstantAux.liftToDiscrete F).obj j) ⋙ Discrete.functor F.obj) X ⟶
        obj.{v₁, u₂, u₁, u₂} (obj (const J) (F.obj j)) Y)
      (map (obj (const J) ((IsPreconnected.IsoConstantAux.liftToDiscrete F).obj j) ⋙ Discrete.functor F.obj) f ≫
        Iso.hom
          ((fun (x : J) ↦
              (eqToIso ⋯ :
                obj.{v₁, u₂, u₁, u₂}
                    (obj (const J) ((IsPreconnected.IsoConstantAux.liftToDiscrete F).obj j) ⋙ Discrete.functor F.obj)
                    x ≅
                  obj.{v₁, u₂, u₁, u₂} (obj (const J) (F.obj j)) x))
            Y))
      (Iso.hom
          ((fun (x : J) ↦
              (eqToIso ⋯ :
                obj.{v₁, u₂, u₁, u₂}
                    (obj (const J) ((IsPreconnected.IsoConstantAux.liftToDiscrete F).obj j) ⋙ Discrete.functor F.obj)
                    x ≅
                  obj.{v₁, u₂, u₁, u₂} (obj (const J) (F.obj j)) x))
            X) ≫
        map (obj (const J) (F.obj j)) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
α : Type u₂
F : Functor.{v₁, u₂, u₁, u₂} J (Discrete α)
j j' : J
as : (F.obj j).as = (F.obj j').as
⊢ F.obj j = F.obj j'

Tactic:
ext
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
α : Type u₂
F : Functor.{v₁, u₂, u₁, u₂} J (Discrete α)
j j' : J
⊢ (F.obj j).as = (F.obj j').as

Tactic:
((isoConstant F j').hom.app j).down.1

Premises used: CategoryTheory.isoConstant, PLift.down, CategoryTheory.Iso.hom, ULift.down, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
α : Type u₂
F : Functor.{v₁, u₂, u₁, u₂} J (Discrete α)
j j' : J
⊢ (F.obj j).as = (F.obj j').as

Tactic:
exact ((isoConstant F j').hom.app j).down.1

Premises used: CategoryTheory.isoConstant, PLift.down, CategoryTheory.Iso.hom, ULift.down, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
inst_2 : IsPreconnected.{v₁, u₁} J
inst_3 : IsPreconnected.{v₂, u₂} K
⊢ IsPreconnected (J × K)

Tactic:
.of_any_functor_const_on_obj (fun {a} F ⟨j, k⟩ ⟨j', k'⟩ => ?_)

Premises used: Prod.mk, CategoryTheory.IsPreconnected.of_any_functor_const_on_obj, _private.0.CategoryTheory.IsPreconnected.prod.match_1, Eq, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
inst_2 : IsPreconnected.{v₁, u₁} J
inst_3 : IsPreconnected.{v₂, u₂} K
refine :
  ∀ {a : Type (max u₁ u₂)} (F : J × K ⥤ Discrete a) (x x : J × K) (j : J) (k : K) (j' : J) (k' : K),
    F.obj (j, k) = F.obj (j', k')
⊢ IsPreconnected (J × K)

Tactic:
refine .of_any_functor_const_on_obj (fun {a} F ⟨j, k⟩ ⟨j', k'⟩ => ?_)
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
inst_2 : IsPreconnected.{v₁, u₁} J
inst_3 : IsPreconnected.{v₂, u₂} K
a : Type (max u₁ u₂)
F : J × K ⥤ Discrete a
x x_1 : J × K
j : J
k : K
j' : J
k' : K
⊢ F.obj (j, k) = F.obj (j', k')

Tactic:
(any_functor_const_on_obj (Prod.sectL J k ⋙ F) j j').trans
    (any_functor_const_on_obj (Prod.sectR j' K ⋙ F) k k')

Premises used: CategoryTheory.Functor.comp, CategoryTheory.any_functor_const_on_obj, CategoryTheory.Prod.sectR, CategoryTheory.Prod.sectL, Eq.trans
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
inst_2 : IsPreconnected.{v₁, u₁} J
inst_3 : IsPreconnected.{v₂, u₂} K
a : Type (max u₁ u₂)
F : J × K ⥤ Discrete a
x x_1 : J × K
j : J
k : K
j' : J
k' : K
⊢ F.obj (j, k) = F.obj (j', k')

Tactic:
exact (any_functor_const_on_obj (Prod.sectL J k ⋙ F) j j').trans
    (any_functor_const_on_obj (Prod.sectR j' K ⋙ F) k k')

Premises used: CategoryTheory.Functor.comp, CategoryTheory.any_functor_const_on_obj, CategoryTheory.Prod.sectR, CategoryTheory.Prod.sectL, Eq.trans
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : Nonempty J
h : ∀ {α : Type u₁} (F : Functor.{v₁, u₁, u₁, u₁} J (Discrete α)) (j j' : J), F.obj j = F.obj j'
⊢ IsConnected.{v₁, u₁} J

Tactic:
{ IsPreconnected.of_any_functor_const_on_obj h with }

Premises used: CategoryTheory.IsConnected.mk, CategoryTheory.IsPreconnected.of_any_functor_const_on_obj
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' X Y : J
f : X ⟶ Y
as : ((Discrete.mk ∘ F) X).as = ((Discrete.mk ∘ F) Y).as
⊢ (Discrete.mk ∘ F) X = (Discrete.mk ∘ F) Y

Tactic:
ext
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' X Y : J
f : X ⟶ Y
⊢ ((Discrete.mk ∘ F) X).as = ((Discrete.mk ∘ F) Y).as

Tactic:
h _ _ f
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' X Y : J
f : X ⟶ Y
⊢ ((Discrete.mk ∘ F) X).as = ((Discrete.mk ∘ F) Y).as

Tactic:
exact h _ _ f
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' : J
⊢ F j = F j'

Tactic:
simpa using
    any_functor_const_on_obj
      { obj := Discrete.mk ∘ F
        map := fun f => eqToHom (by ext; exact h _ _ f) }
      j j'

Premises used: CategoryTheory.eqToHom, CategoryTheory.Functor.mk, Function.comp, CategoryTheory.any_functor_const_on_obj, CategoryTheory.Discrete.mk
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsConnected.{v₁, u₁} J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∃ (a : α), ∀ (j : J), F j = a

Tactic:
⟨F (Classical.arbitrary _), fun _ ↦ constant_of_preserves_morphisms _ h _ _⟩

Premises used: CategoryTheory.constant_of_preserves_morphisms, Exists.intro, Classical.arbitrary
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
α : Type u₁
F : Functor.{v₁, u₁, u₁, u₁} J (Discrete α)
j₁ j₂ : J
f : j₁ ⟶ j₂
as : (F.obj j₁).as = (F.obj j₂).as
⊢ F.obj j₁ = F.obj j₂

Tactic:
ext
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
α : Type u₁
F : Functor.{v₁, u₁, u₁, u₁} J (Discrete α)
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ (F.obj j₁).as = (F.obj j₂).as

Tactic:
Discrete.eq_of_hom (F.map f)

Premises used: CategoryTheory.Functor.map, CategoryTheory.Discrete.eq_of_hom
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
α : Type u₁
F : Functor.{v₁, u₁, u₁, u₁} J (Discrete α)
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ (F.obj j₁).as = (F.obj j₂).as

Tactic:
exact Discrete.eq_of_hom (F.map f)

Premises used: CategoryTheory.Functor.map, CategoryTheory.Discrete.eq_of_hom
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : Nonempty J
h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
⊢ IsConnected.{v₁, u₁} J

Tactic:
{ IsPreconnected.of_constant_of_preserves_morphisms h with }

Premises used: CategoryTheory.IsPreconnected.of_constant_of_preserves_morphisms, CategoryTheory.IsConnected.mk
-- Module: Mathlib.CategoryTheory.IsConnected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
aux : ∀ (j₁ j₂ : J) (f : j₁ ⟶ j₂), { down := j₁ ∈ p : ULift.{u₁, 0} Prop } = { down := j₂ ∈ p } := ⋯
⊢ (j ∈ p) = (j₀ ∈ p)

Tactic:
injection constant_of_preserves_morphisms (fun k => ULift.up.{u₁} (k ∈ p)) aux j j₀ with i