awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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)
⊢ [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
have tfae_6_to_1 : ∀
  (a :
    ∀ (S : LightProfinite.{u}),
      Nonempty
        (IsColimit
          (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
            (coconeRightOpOfCone S.asLimitCone)))),
  LightCondensed.IsDiscrete M
Tactic: tfae_have 6 → 1 := by
    intro h
    rw [isDiscrete_iff_isDiscrete_forget, ((LightCondSet.isDiscrete_tfae _).out 0 5 :)]
    intro S
    letI : PreservesFilteredColimitsOfSize.{0, 0} (forget (ModuleCat R)) :=
      preservesFilteredColimitsOfSize_shrink.{0, u, 0, u} _
    exact ⟨isColimitOfPreserves (forget (ModuleCat R)) (h S).some⟩
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (goal)
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 : LightCondensed.IsDiscrete M
S : LightProfinite
⊢ Nonempty
    (IsColimit
      (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))
have rw : ∀
  (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.{u}),
  Nonempty
    (IsColimit
      (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))
Tactic: rw [isDiscrete_iff_isDiscrete_forget, ((LightCondSet.isDiscrete_tfae _).out 0 5 :)] at h
Cleared hypotheses: h, S
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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
⊢ [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
have tfae_1_to_6 : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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)
⊢ IsColimit ((locallyConstantPresheaf X).mapCocone c.op)
have refine_1 : ∀ (x : ((locallyConstantPresheaf X).mapCocone c.op).pt),
  ∃ (i : Iᵒᵖ) (xi : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i)),
    x =
      (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: refine Types.FilteredColimit.isColimitOf _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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)
refine_1 :
  ∀ (x : ((locallyConstantPresheaf X).mapCocone c.op).pt),
    ∃ (i : Iᵒᵖ) (xi : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i)),
      x =
        (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
⊢ IsColimit ((locallyConstantPresheaf X).mapCocone c.op)
have refine_2 : ∀ (i j : Iᵒᵖ) (xi : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i))
  (xj : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj j)),
  Eq (α := (fun (X : Type (u + 1)) ↦ X) (obj (obj (const Iᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) i))
      ((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 :
        (fun (X : Type (u + 1)) ↦ X) (obj (obj (const Iᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (((locallyConstantPresheaf X).mapCocone c.op).ι.app j) :
            (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj j)) →
              (fun (X : Type (u + 1)) ↦ X) (((const Iᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj j))
          xj :
        (fun (X : Type (u + 1)) ↦ X) (obj (obj (const Iᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) j)) →
    ∃ (k : Iᵒᵖ) (f : i ⟶ k) (g : 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 i)) →
                (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
            xi :
          (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 j)) →
                (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
            xj :
          (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
Tactic: refine Types.FilteredColimit.isColimitOf _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨j, h⟩ := Profinite.exists_locallyConstant.{_, u} c hc f
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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ᵒᵖ) (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))
have refine_2 : ∀ (k : I) (ki : k ⟶ i) (kj : k ⟶ j),
  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: obtain ⟨k, ki, kj, _⟩ := IsCofilteredOrEmpty.cone_objs i j
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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))
have 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)))
Tactic: refine ⟨⟨k⟩, ki.op, kj.op, ?_⟩
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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 (α := 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)
have 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)
Tactic: change ((((locallyConstantPresheaf X).mapCocone c.op).ι.app ⟨i⟩) ≫
    (isColimitLocallyConstantPresheaf c X hc).desc s) _ = _
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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)
            (((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)
have 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)
Tactic: rw [(isColimitLocallyConstantPresheaf c X hc).fac]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ (lanPresheafExt i).hom.app S = colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.hom)
have 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))
Tactic: simp only [lanPresheaf, lanPresheafExt,
    leftKanExtensionUniqueOfIso_hom, pointwiseLeftKanExtension_desc_app]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ 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))
have w : ∀ (j : CostructuredArrow toProfinite.op S),
  Eq (α :=
    (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F).obj j ⟶
      (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
          (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
          (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S).pt)
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F))
      (colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) j)
      (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)))
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F))
      (colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) j)
      (colimMap ((CostructuredArrow.proj toProfinite.op S).whiskerLeft i.hom)))
Tactic: apply colimit.hom_ext