awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C Y
x : (↑X : Type v)
V : Opens (↑X : Type v)
hV : x ∈ V
V_1 : Opens (↑Y : Type v)
hV_1 : unop (op V) ≤ (Opens.map f).obj V_1
ih :
  NatTrans.app (NatTrans.app (Adjunction.unit (pullbackPushforwardAdjunction C f)) F) (op V_1) ≫
      (obj (pullback C f) F).map (homOfLE hV_1).op ≫ germToPullbackStalk C f F V x hV ≫ stalkPullbackHom C f F x =
    NatTrans.app (NatTrans.app (Adjunction.unit (pullbackPushforwardAdjunction C f)) F) (op V_1) ≫
      (obj (pullback C f) F).map (homOfLE hV_1).op ≫
        (obj (pullback C f) F).germ V x hV ≫ 𝟙 ((obj (pullback C f) F).stalk x)
⊢ NatTrans.app (NatTrans.app (Adjunction.unit (pullbackPushforwardAdjunction C f)) F) (op V_1) ≫
      (obj (pullback C f) F).map (homOfLE hV_1).op ≫
        (obj (pullback C f) F).germ V x hV ≫ stalkPullbackInv C f F x ≫ stalkPullbackHom C f F x =
    NatTrans.app (NatTrans.app (Adjunction.unit (pullbackPushforwardAdjunction C f)) F) (op V_1) ≫
      (obj (pullback C f) F).map (homOfLE hV_1).op ≫
        (obj (pullback C f) F).germ V x hV ≫ 𝟙 ((obj (pullback C f) F).stalk x)
have ih₁ : NatTrans.app (NatTrans.app (Adjunction.unit (pullbackPushforwardAdjunction C f)) F) (op V_1) ≫
    (obj (pullback C f) F).map (homOfLE hV_1).op ≫ germToPullbackStalk C f F V x hV ≫ stalkPullbackHom C f F x =
  NatTrans.app (NatTrans.app (Adjunction.unit (pullbackPushforwardAdjunction C f)) F) (op V_1) ≫
    (obj (pullback C f) F).map (homOfLE hV_1).op ≫ (obj (pullback C f) F).germ V x hV
Tactic: rw [germ_stalkPullbackInv_assoc, Category.comp_id, germToPullbackStalk_stalkPullbackHom]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C Y
x : (↑X : Type v)
V : Opens (↑X : Type v)
hV : x ∈ V
V_1 : Opens (↑Y : Type v)
hV_1 : unop (op V) ≤ (Opens.map f).obj V_1
ih :
  NatTrans.app (NatTrans.app (Adjunction.unit (pullbackPushforwardAdjunction C f)) F) (op V_1) ≫
      (obj (pullback C f) F).map (homOfLE hV_1).op ≫ germToPullbackStalk C f F V x hV ≫ stalkPullbackHom C f F x =
    NatTrans.app (NatTrans.app (Adjunction.unit (pullbackPushforwardAdjunction C f)) F) (op V_1) ≫
      (obj (pullback C f) F).map (homOfLE hV_1).op ≫
        (obj (pullback C f) F).germ V x hV ≫ 𝟙 ((obj (pullback C f) F).stalk x)
ih₁ :
  NatTrans.app (NatTrans.app (Adjunction.unit (pullbackPushforwardAdjunction C f)) F) (op V_1) ≫
      (obj (pullback C f) F).map (homOfLE hV_1).op ≫ germToPullbackStalk C f F V x hV ≫ stalkPullbackHom C f F x =
    NatTrans.app (NatTrans.app (Adjunction.unit (pullbackPushforwardAdjunction C f)) F) (op V_1) ≫
      (obj (pullback C f) F).map (homOfLE hV_1).op ≫ (obj (pullback C f) F).germ V x hV
⊢ NatTrans.app (NatTrans.app (Adjunction.unit (pullbackPushforwardAdjunction C f)) F) (op V_1) ≫
      (obj (pullback C f) F).map (homOfLE hV_1).op ≫
        (obj (pullback C f) F).germ V x hV ≫ stalkPullbackInv C f F x ≫ stalkPullbackHom C f F x =
    NatTrans.app (NatTrans.app (Adjunction.unit (pullbackPushforwardAdjunction C f)) F) (op V_1) ≫
      (obj (pullback C f) F).map (homOfLE hV_1).op ≫
        (obj (pullback C f) F).germ V x hV ≫ 𝟙 ((obj (pullback C f) F).stalk x)
have ih₂ : Eq (α := F.obj (op V_1) ⟶ (obj (pullback C f) F).stalk x)
  (NatTrans.app (NatTrans.app (Adjunction.unit (pullbackPushforwardAdjunction C f)) F) (op V_1) ≫
    (obj (pullback C f) F).map (homOfLE hV_1).op ≫ (obj (pullback C f) F).germ V x hV)
  (NatTrans.app (NatTrans.app (Adjunction.unit (pullbackPushforwardAdjunction C f)) F) (op V_1) ≫
    (obj (pullback C f) F).map (homOfLE hV_1).op ≫ (obj (pullback C f) F).germ V x hV)
Tactic: rw [germ_stalkPullbackInv_assoc, Category.comp_id, germToPullbackStalk_stalkPullbackHom]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : (↑X : Type v)
h : x ⤳ y
⊢ F.stalk y ⟶ F.stalk x
have refine_1 : (U : (OpenNhds y)ᵒᵖ) →
  (obj (obj (whiskeringLeft (OpenNhds y)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion y).op) F).obj U ⟶
    obj (obj (Functor.const (OpenNhds y)ᵒᵖ) ((stalkFunctor C x : Presheaf C X ⥤ C).1 F)) U
Tactic: refine colimit.desc _ ⟨_, fun U => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : (↑X : Type v)
h : x ⤳ y
refine_1 :
  (U : (OpenNhds y)ᵒᵖ) →
    (obj (obj (whiskeringLeft (OpenNhds y)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion y).op) F).obj U ⟶
      obj (obj (Functor.const (OpenNhds y)ᵒᵖ) ((stalkFunctor C x : Presheaf C X ⥤ C).1 F)) U
⊢ F.stalk y ⟶ F.stalk x
have refine_2 : ∀ ⦃X_1 Y : (OpenNhds y)ᵒᵖ⦄ (f : X_1 ⟶ Y),
  Eq (α :=
    (obj (obj (whiskeringLeft (OpenNhds y)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion y).op) F).obj X_1 ⟶
      obj (obj (Functor.const (OpenNhds y)ᵒᵖ) ((stalkFunctor C x : Presheaf C X ⥤ C).1 F)) Y)
    ((obj (obj (whiskeringLeft (OpenNhds y)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion y).op) F).map f ≫
      (fun (U : (OpenNhds y)ᵒᵖ) ↦
          (colimit.ι ((OpenNhds.inclusion x).op ⋙ F)
              (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) (↑(unop U) : Opens (↑X : Type v)) sorry)) :
            ((OpenNhds.inclusion x).op ⋙ F).obj
                (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) (↑(unop U) : Opens (↑X : Type v)) sorry)) ⟶
              colimit ((OpenNhds.inclusion x).op ⋙ F)))
        Y)
    ((fun (U : (OpenNhds y)ᵒᵖ) ↦
          (colimit.ι ((OpenNhds.inclusion x).op ⋙ F)
              (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) (↑(unop U) : Opens (↑X : Type v)) sorry)) :
            ((OpenNhds.inclusion x).op ⋙ F).obj
                (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) (↑(unop U) : Opens (↑X : Type v)) sorry)) ⟶
              colimit ((OpenNhds.inclusion x).op ⋙ F)))
        X_1 ≫
      map (obj (Functor.const (OpenNhds y)ᵒᵖ) ((stalkFunctor C x : Presheaf C X ⥤ C).1 F)) f)
Tactic: refine colimit.desc _ ⟨_, fun U => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : (↑X : Type v)
h : x ⤳ y
U V : (OpenNhds y)ᵒᵖ
i : U ⟶ V
⊢ Eq (α :=
    (obj (obj (whiskeringLeft (OpenNhds y)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion y).op) F).obj U ⟶
      obj (obj (Functor.const (OpenNhds y)ᵒᵖ) ((stalkFunctor C x : Presheaf C X ⥤ C).1 F)) V)
    ((obj (obj (whiskeringLeft (OpenNhds y)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion y).op) F).map i ≫
      (fun (U : (OpenNhds y)ᵒᵖ) ↦
          (colimit.ι ((OpenNhds.inclusion x).op ⋙ F)
              (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) (↑(unop U) : Opens (↑X : Type v)) ⋯)) :
            ((OpenNhds.inclusion x).op ⋙ F).obj
                (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) (↑(unop U) : Opens (↑X : Type v)) ⋯)) ⟶
              colimit ((OpenNhds.inclusion x).op ⋙ F)))
        V)
    ((fun (U : (OpenNhds y)ᵒᵖ) ↦
          (colimit.ι ((OpenNhds.inclusion x).op ⋙ F)
              (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) (↑(unop U) : Opens (↑X : Type v)) ⋯)) :
            ((OpenNhds.inclusion x).op ⋙ F).obj
                (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) (↑(unop U) : Opens (↑X : Type v)) ⋯)) ⟶
              colimit ((OpenNhds.inclusion x).op ⋙ F)))
        U ≫
      map (obj (Functor.const (OpenNhds y)ᵒᵖ) ((stalkFunctor C x : Presheaf C X ⥤ C).1 F)) i)
have refine_2 : Eq (α := F.obj (op ((OpenNhds.inclusion y).obj (unop U))) ⟶ F.stalk x)
  (F.map ((OpenNhds.inclusion y).map i.unop).op ≫
    colimit.ι ((OpenNhds.inclusion x).op ⋙ F)
      (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) (↑(unop V) : Opens (↑X : Type v)) sorry)))
  (colimit.ι ((OpenNhds.inclusion x).op ⋙ F)
      (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) (↑(unop U) : Opens (↑X : Type v)) sorry)) ≫
    𝟙 (F.stalk x))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : (↑X : Type v)
h : x ⤳ y
U V : (OpenNhds y)ᵒᵖ
i : U ⟶ V
⊢ Eq (α := F.obj (op ((OpenNhds.inclusion y).obj (unop U))) ⟶ F.stalk x)
    (F.map ((OpenNhds.inclusion y).map i.unop).op ≫
      colimit.ι ((OpenNhds.inclusion x).op ⋙ F)
        (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) (↑(unop V) : Opens (↑X : Type v)) ⋯)))
    (colimit.ι ((OpenNhds.inclusion x).op ⋙ F)
        (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) (↑(unop U) : Opens (↑X : Type v)) ⋯)) ≫
      𝟙 (F.stalk x))
have refine_2 : Eq (α := F.obj (op ((OpenNhds.inclusion y).obj (unop U))) ⟶ F.stalk x)
  (F.map ((OpenNhds.inclusion y).map i.unop).op ≫
    colimit.ι ((OpenNhds.inclusion x).op ⋙ F)
      (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) (↑(unop V) : Opens (↑X : Type v)) sorry)))
  (colimit.ι ((OpenNhds.inclusion x).op ⋙ F)
    (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) (↑(unop U) : Opens (↑X : Type v)) sorry)))
Tactic: rw [Category.comp_id]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
F : Presheaf C X
x : (↑X : Type v)
⊢ F.stalkSpecializes ⋯ = 𝟙 (F.stalk x)
have ih : ∀ (U : Opens (↑X : Type v)) (hxU : x ∈ U), F.germ U x hxU ≫ F.stalkSpecializes sorry = F.germ U x hxU ≫ 𝟙 (F.stalk x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
F : Presheaf C X
x y z : (↑X : Type v)
h : x ⤳ y
h' : y ⤳ z
⊢ Eq (α := F.stalk z ⟶ F.stalk x) (F.stalkSpecializes h' ≫ F.stalkSpecializes h) (F.stalkSpecializes ⋯)
have ih : ∀ (U : Opens (↑X : Type v)) (hxU : z ∈ U),
  Eq (α := F.obj (op U) ⟶ F.stalk x) (F.germ U z hxU ≫ F.stalkSpecializes h' ≫ F.stalkSpecializes h)
    (F.germ U z hxU ≫ F.stalkSpecializes sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
F G : Presheaf C X
f : F ⟶ G
x y : (↑X : Type v)
h : x ⤳ y
⊢ Eq (α := F.stalk y ⟶ obj (stalkFunctor C x) G) (F.stalkSpecializes h ≫ map (stalkFunctor C x) f)
    (map (stalkFunctor C y) f ≫ G.stalkSpecializes h)
have ih : ∀ (U : Opens (↑X : Type v)) (hxU : y ∈ U),
  Eq (α := F.obj (op U) ⟶ obj (stalkFunctor C x) G) (F.germ U y hxU ≫ F.stalkSpecializes h ≫ map (stalkFunctor C x) f)
    (F.germ U y hxU ≫ map (stalkFunctor C y) f ≫ G.stalkSpecializes h)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C X
x y : (↑X : Type v)
h : x ⤳ y
⊢ Eq (α := (obj (pushforward C f) F).stalk ((Hom.hom f : (a : (↑X : Type v)) → (↑Y : Type v)) y) ⟶ F.stalk x)
    ((obj (pushforward C f) F).stalkSpecializes ⋯ ≫ stalkPushforward C f F x)
    (stalkPushforward C f F y ≫ F.stalkSpecializes h)
have ih : ∀ (U : Opens (↑Y : Type v))
  (hxU : Membership.mem (α := (↑Y : Type v)) U ((Hom.hom f : (a : (↑X : Type v)) → (↑Y : Type v)) y : (↑Y : Type v))),
  Eq (α := (obj (pushforward C f) F).obj (op U) ⟶ F.stalk x)
    ((obj (pushforward C f) F).germ U ((Hom.hom f : (a : (↑X : Type v)) → (↑Y : Type v)) y) hxU ≫
      (obj (pushforward C f) F).stalkSpecializes sorry ≫ stalkPushforward C f F x)
    ((obj (pushforward C f) F).germ U ((Hom.hom f : (a : (↑X : Type v)) → (↑Y : Type v)) y) hxU ≫
      stalkPushforward C f F y ≫ F.stalkSpecializes h)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
F : Presheaf C X
U V : Opens (↑X : Type v)
x : (↑X : Type v)
hxU : x ∈ U
hxV : x ∈ V
W : Opens (↑X : Type v)
hxW : x ∈ W
iWU : W ⟶ U
iWV : W ⟶ V
sU : ToType (FC := FC) (CC := CC) (F.obj (op U))
sV : ToType (FC := FC) (CC := CC) (F.obj (op V))
ih :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W))) sU :
      CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) sV :
      CC (F.obj (op W)))
⊢ Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hxU) : (a : CC (F.obj (op U))) → CC (F.stalk x)) sU :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x hxV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) sV :
      CC (F.stalk x))
have rw : Eq (α := CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op ≫ F.germ W x hxW) :
        (a : CC (F.obj (op U))) → CC (F.stalk x))
      sU :
    CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x hxV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) sV :
    CC (F.stalk x))
Tactic: rw [← F.germ_res iWU x hxW, ← F.germ_res iWV x hxW, ConcreteCategory.comp_apply,
    ConcreteCategory.comp_apply, ih]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
F : Presheaf C X
U V : Opens (↑X : Type v)
x : (↑X : Type v)
hxU : x ∈ U
hxV : x ∈ V
W : Opens (↑X : Type v)
hxW : x ∈ W
iWU : W ⟶ U
iWV : W ⟶ V
sU : ToType (FC := FC) (CC := CC) (F.obj (op U))
sV : ToType (FC := FC) (CC := CC) (F.obj (op V))
ih :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W))) sU :
      CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) sV :
      CC (F.obj (op W)))
rw :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op ≫ F.germ W x hxW) :
          (a : CC (F.obj (op U))) → CC (F.stalk x))
        sU :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x hxV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) sV :
      CC (F.stalk x))
⊢ Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hxU) : (a : CC (F.obj (op U))) → CC (F.stalk x)) sU :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x hxV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) sV :
      CC (F.stalk x))
have rw₁ : Eq (α := CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op ≫ F.germ W x hxW) :
        (a : CC (F.obj (op U))) → CC (F.stalk x))
      sU :
    CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op ≫ F.germ W x hxW) :
        (a : CC (F.obj (op V))) → CC (F.stalk x))
      sV :
    CC (F.stalk x))
Tactic: rw [← F.germ_res iWU x hxW, ← F.germ_res iWV x hxW, ConcreteCategory.comp_apply,
    ConcreteCategory.comp_apply, ih]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
F : Presheaf C X
U V : Opens (↑X : Type v)
x : (↑X : Type v)
hxU : x ∈ U
hxV : x ∈ V
W : Opens (↑X : Type v)
hxW : x ∈ W
iWU : W ⟶ U
iWV : W ⟶ V
sU : ToType (FC := FC) (CC := CC) (F.obj (op U))
sV : ToType (FC := FC) (CC := CC) (F.obj (op V))
ih :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W))) sU :
      CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) sV :
      CC (F.obj (op W)))
rw :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op ≫ F.germ W x hxW) :
          (a : CC (F.obj (op U))) → CC (F.stalk x))
        sU :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x hxV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) sV :
      CC (F.stalk x))
rw₁ :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op ≫ F.germ W x hxW) :
          (a : CC (F.obj (op U))) → CC (F.stalk x))
        sU :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op ≫ F.germ W x hxW) :
          (a : CC (F.obj (op V))) → CC (F.stalk x))
        sV :
      CC (F.stalk x))
⊢ Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hxU) : (a : CC (F.obj (op U))) → CC (F.stalk x)) sU :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x hxV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) sV :
      CC (F.stalk x))
have rw₂ : Eq (α := CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ W x hxW) : (a : CC (F.obj (op W))) → CC (F.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W))) sU :
        CC (F.obj (op W))) :
    CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op ≫ F.germ W x hxW) :
        (a : CC (F.obj (op V))) → CC (F.stalk x))
      sV :
    CC (F.stalk x))
Tactic: rw [← F.germ_res iWU x hxW, ← F.germ_res iWV x hxW, ConcreteCategory.comp_apply,
    ConcreteCategory.comp_apply, ih]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
F : Presheaf C X
U V : Opens (↑X : Type v)
x : (↑X : Type v)
hxU : x ∈ U
hxV : x ∈ V
W : Opens (↑X : Type v)
hxW : x ∈ W
iWU : W ⟶ U
iWV : W ⟶ V
sU : ToType (FC := FC) (CC := CC) (F.obj (op U))
sV : ToType (FC := FC) (CC := CC) (F.obj (op V))
ih :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W))) sU :
      CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) sV :
      CC (F.obj (op W)))
rw :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op ≫ F.germ W x hxW) :
          (a : CC (F.obj (op U))) → CC (F.stalk x))
        sU :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x hxV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) sV :
      CC (F.stalk x))
rw₁ :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op ≫ F.germ W x hxW) :
          (a : CC (F.obj (op U))) → CC (F.stalk x))
        sU :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op ≫ F.germ W x hxW) :
          (a : CC (F.obj (op V))) → CC (F.stalk x))
        sV :
      CC (F.stalk x))
rw₂ :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ W x hxW) : (a : CC (F.obj (op W))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W))) sU :
          CC (F.obj (op W))) :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op ≫ F.germ W x hxW) :
          (a : CC (F.obj (op V))) → CC (F.stalk x))
        sV :
      CC (F.stalk x))
⊢ Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hxU) : (a : CC (F.obj (op U))) → CC (F.stalk x)) sU :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x hxV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) sV :
      CC (F.stalk x))
have rw₃ : Eq (α := CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ W x hxW) : (a : CC (F.obj (op W))) → CC (F.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W))) sU :
        CC (F.obj (op W))) :
    CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ W x hxW) : (a : CC (F.obj (op W))) → CC (F.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) sV :
        CC (F.obj (op W))) :
    CC (F.stalk x))
Tactic: rw [← F.germ_res iWU x hxW, ← F.germ_res iWV x hxW, ConcreteCategory.comp_apply,
    ConcreteCategory.comp_apply, ih]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
F : Presheaf C X
x : (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (F.stalk x)
⊢ ∃ (U : Opens (↑X : Type v)) (m : x ∈ U) (s : ToType (FC := FC) (CC := CC) (F.obj (op U))),
    (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x m) : (a : CC (F.obj (op U))) → CC (F.stalk x)) s = t
have obtain : ∀ (U : (OpenNhds x)ᵒᵖ)
  (s :
    (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F ⋙
          forget C (FC := FC) (CC := CC)).obj
      U)
  (e :
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (Cocone.ι
                (mapCocone (forget C (FC := FC) (CC := CC))
                  (colimit.cocone
                    (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F))))
              U) :
          (a :
              (fun (X : Type v) ↦ X)
                ((((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙
                      forget C).obj
                  U)) →
            (fun (X : Type v) ↦ X)
              (((Functor.const (OpenNhds x)ᵒᵖ).obj
                    ((forget C).mapCocone
                        (colimit.cocone
                          (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj
                            F))).pt).obj
                U))
        s =
      t),
  ∃ (U : Opens (↑X : Type v)) (m : x ∈ U) (s : ToType (FC := FC) (CC := CC) (F.obj (op U))),
    (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x m) : (a : CC (F.obj (op U))) → CC (F.stalk x)) s = t
Tactic: obtain ⟨U, s, e⟩ :=
    Types.jointly_surjective.{v, v} _ (isColimitOfPreserves (forget C) (colimit.isColimit _)) t