awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type u
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_6_to_1 :
  ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    LightCondensed.IsDiscrete M
h :
  ∀ (S : LightProfinite.{u}),
    Nonempty.{u + 2}
      (IsColimit
        ((obj (LightCondensed.forget R) M).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
          (coconeRightOpOfCone S.asLimitCone)))
S : LightProfinite
this : ReflectsFilteredColimitsOfSize.{0, 0, u, u, u + 1, u + 1}
  (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
    ModuleCat.carrier)) :=
  ⋯
⊢ Nonempty
    (IsColimit
      (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))

Tactic:
exact ⟨isColimitOfReflects (forget (ModuleCat R)) (h S).some⟩
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type u
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_6_to_1 :
  ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    LightCondensed.IsDiscrete M
⊢ ∀ (a : LightCondensed.IsDiscrete M) (S : LightProfinite.{u}),
    Nonempty
      (IsColimit
        (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))

Tactic:
tfae_have 1 → 6 := by
    intro h S
    rw [isDiscrete_iff_isDiscrete_forget, ((LightCondSet.isDiscrete_tfae _).out 0 5 :)] at h
    letI : ReflectsFilteredColimitsOfSize.{0, 0} (forget (ModuleCat R)) :=
      reflectsFilteredColimitsOfSize_shrink.{0, u, 0, u} _
    exact ⟨isColimitOfReflects (forget (ModuleCat R)) (h S).some⟩
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type u
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_6_to_1 :
  ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    LightCondensed.IsDiscrete M
tfae_1_to_6 :
  ∀ (a : LightCondensed.IsDiscrete M) (S : LightProfinite.{u}),
    Nonempty
      (IsColimit
        (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))
⊢ [LightCondensed.IsDiscrete M,
      IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
        (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M),
      essImage (LightCondensed.discrete (ModuleCat R)) M, essImage (functor R) M,
      IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M),
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
f : LocallyConstant (↑(c.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) X
refine_1 :
  ∀ (j : I)
    (h :
      ∃ (g :
        LocallyConstant
          (↑(((F ⋙ toProfinite).obj j).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
            Type u)
          X),
        f = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) g),
    ∃ (i : Iᵒᵖ) (xi : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i)),
      f =
        (ConcreteCategory.hom (FC := TypeCat.Fun) (((locallyConstantPresheaf X).mapCocone c.op).ι.app i) :
            (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i)) →
              (fun (X : Type (u + 1)) ↦ X) (((const Iᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj i))
          xi
⊢ ∃ (i : Iᵒᵖ) (xi : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i)),
    f =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (((locallyConstantPresheaf X).mapCocone c.op).ι.app i) :
          (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i)) →
            (fun (X : Type (u + 1)) ↦ X) (((const Iᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj i))
        xi

Tactic:
obtain ⟨j, h⟩ := Profinite.exists_locallyConstant.{_, u} c hc f
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
f : LocallyConstant (↑(c.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) X
j : I
h :
  ∃ (g :
    LocallyConstant
      (↑(((F ⋙ toProfinite).obj j).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
      X),
    f = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) g
⊢ ∃ (i : Iᵒᵖ) (xi : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i)),
    f =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (((locallyConstantPresheaf X).mapCocone c.op).ι.app i) :
          (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i)) →
            (fun (X : Type (u + 1)) ↦ X) (((const Iᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj i))
        xi

Tactic:
⟨⟨j⟩, h⟩

Premises used: Opposite.op, Exists.intro
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
f : LocallyConstant (↑(c.pt.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) X
j : I
h :
  ∃ (g :
    LocallyConstant
      (↑(((F ⋙ toProfinite).obj j).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
      X),
    f = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) g
⊢ ∃ (i : Iᵒᵖ) (xi : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i)),
    f =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (((locallyConstantPresheaf X).mapCocone c.op).ι.app i) :
          (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i)) →
            (fun (X : Type (u + 1)) ↦ X) (((const Iᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj i))
        xi

Tactic:
exact ⟨⟨j⟩, h⟩
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
i j : I
fi :
  LocallyConstant
    (↑(((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    X
fj :
  LocallyConstant
    (↑(((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : I
ki : k ⟶ i
kj : k ⟶ j
h_1 : True
⊢ ∃ (k : Iᵒᵖ) (f : Opposite.op i ⟶ k) (g : Opposite.op j ⟶ k),
    Eq (α := (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map f) :
            (a :
                (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
              (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          fi :
        (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map g) :
            (a :
                (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))) →
              (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          fj :
        (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))

Tactic:
⟨⟨k⟩, ki.op, kj.op, ?_⟩

Premises used: Quiver.Hom.op, Opposite.op, Exists.intro
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
i j : I
fi :
  LocallyConstant
    (↑(((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    X
fj :
  LocallyConstant
    (↑(((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : I
ki : k ⟶ i
kj : k ⟶ j
h_1 : True
refine_2 :
  Eq (α := (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op k)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map ki.op) :
          (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
            (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op k)))
        fi :
      (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op k)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map kj.op) :
          (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))) →
            (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op k)))
        fj :
      (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op k)))
⊢ ∃ (k : Iᵒᵖ) (f : Opposite.op i ⟶ k) (g : Opposite.op j ⟶ k),
    Eq (α := (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map f) :
            (a :
                (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
              (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          fi :
        (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map g) :
            (a :
                (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))) →
              (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          fj :
        (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))

Tactic:
refine ⟨⟨k⟩, ki.op, kj.op, ?_⟩
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
i j : I
fi :
  LocallyConstant
    (↑(((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    X
fj :
  LocallyConstant
    (↑(((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : I
ki : k ⟶ i
kj : k ⟶ j
h_1 : True
x_1 :
  (↑((toProfinite.obj (F.obj k)).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
x :
  (↑((obj (obj (const I) c.pt) k).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
hx :
  (ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (c.π.app k) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              (((const I).obj c.pt).obj k)) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
            ((F ⋙ toProfinite).obj k))
      x =
    x_1
⊢ Eq (α := X)
    ((LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi :
          (a : (↑(((const I).obj c.pt).obj i).toTop : Type u)) → X)
        x :
      X)
    ((LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj :
          (a : (↑(((const I).obj c.pt).obj i).toTop : Type u)) → X)
        x :
      X)

Tactic:
have h := LocallyConstant.congr_fun h x
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
s : Cocone ((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X)
i : I
f :
  LocallyConstant
    (↑((toProfinite.obj (F.obj i)).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    X
change :
  Eq (α := (fun (X : Type (u + 1)) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i) ≫
              (isColimitLocallyConstantPresheaf c X hc).desc s) :
          (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
            (fun (X : Type (u + 1)) ↦ X) s.pt)
        f :
      (fun (X : Type (u + 1)) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app (Opposite.op i)) :
          (a : LocallyConstant (↑(toProfinite.obj (F.obj i)).toTop : Type u) X) → s.pt)
        f :
      s.pt)
⊢ Eq (α := s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((isColimitLocallyConstantPresheaf c X hc).desc s) :
          (a : LocallyConstant (↑c.pt.toTop : Type u) X) → s.pt)
        (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) f) :
      s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app (Opposite.op i)) :
          (a : LocallyConstant (↑(toProfinite.obj (F.obj i)).toTop : Type u) X) → s.pt)
        f :
      s.pt)

Tactic:
change ((((locallyConstantPresheaf X).mapCocone c.op).ι.app ⟨i⟩) ≫
    (isColimitLocallyConstantPresheaf c X hc).desc s) _ = _

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.ConcreteCategory.hom, Condensed.locallyConstantPresheaf, Condensed.isColimitLocallyConstantPresheaf, CategoryTheory.Limits.Cocone.ι, Opposite.op, CategoryTheory.Limits.IsColimit.desc, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Cone.op, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
s : Cocone ((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X)
i : I
f :
  LocallyConstant
    (↑((toProfinite.obj (F.obj i)).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    X
rw :
  Eq (α := (fun (X : Type (u + 1)) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app (Opposite.op i)) :
          (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
            (fun (X : Type (u + 1)) ↦ X) s.pt)
        f :
      (fun (X : Type (u + 1)) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app (Opposite.op i)) :
          (a : LocallyConstant (↑(toProfinite.obj (F.obj i)).toTop : Type u) X) → s.pt)
        f :
      s.pt)
⊢ Eq (α := (fun (X : Type (u + 1)) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i) ≫
              (isColimitLocallyConstantPresheaf c X hc).desc s) :
          (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
            (fun (X : Type (u + 1)) ↦ X) s.pt)
        f :
      (fun (X : Type (u + 1)) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app (Opposite.op i)) :
          (a : LocallyConstant (↑(toProfinite.obj (F.obj i)).toTop : Type u) X) → s.pt)
        f :
      s.pt)

Tactic:
rw [(isColimitLocallyConstantPresheaf c X hc).fac]

Premises used: CategoryTheory.Limits.IsColimit.fac, Condensed.isColimitLocallyConstantPresheaf
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
s : Cocone ((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X)
i : I
f :
  LocallyConstant
    (↑((toProfinite.obj (F.obj i)).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    X
⊢ Eq (α := (fun (X : Type (u + 1)) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app (Opposite.op i)) :
          (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
            (fun (X : Type (u + 1)) ↦ X) s.pt)
        f :
      (fun (X : Type (u + 1)) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app (Opposite.op i)) :
          (a : LocallyConstant (↑(toProfinite.obj (F.obj i)).toTop : Type u) X) → s.pt)
        f :
      s.pt)

Tactic:
rfl
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
X : Type (u + 1)
S : Profinite
s : Cocone (S.diagram.op ⋙ locallyConstantPresheaf X)
i : DiscreteQuotient (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
f :
  LocallyConstant
    (↑((S.diagram.obj i).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) X
⊢ Eq (α := s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((isColimitLocallyConstantPresheafDiagram X S).desc s) :
          (a : LocallyConstant (↑S.asLimitCone.pt.toTop : Type u) X) → s.pt)
        (LocallyConstant.comap (TopCat.Hom.hom (S.asLimitCone.π.app i).hom) f) :
      s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app (Opposite.op i)) :
          (a : LocallyConstant (↑(toProfinite.obj (S.fintypeDiagram.obj i)).toTop : Type u) X) → s.pt)
        f :
      s.pt)

Tactic:
isColimitLocallyConstantPresheaf_desc_apply S.asLimitCone X S.asLimit s i f

Premises used: Profinite.asLimit, Profinite.asLimitCone, Condensed.isColimitLocallyConstantPresheaf_desc_apply
-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
simp :
  Eq (α :=
    (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ F)).obj S ⟶
      (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G)).obj S)
    (colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F)
        (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
          (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
          (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S) :
      colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) ⟶
        (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
            (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
            (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S).pt)
    (colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.hom))
⊢ (lanPresheafExt i).hom.app S = colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.hom)

Tactic:
simp only [lanPresheaf, lanPresheafExt,
    leftKanExtensionUniqueOfIso_hom, pointwiseLeftKanExtension_desc_app]

Premises used: Condensed.lanPresheaf, CategoryTheory.Functor.leftKanExtensionUniqueOfIso_hom, CategoryTheory.Functor.pointwiseLeftKanExtension_desc_app, Condensed.lanPresheafExt