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 : 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 : (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
have revert : ∀
  (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: revert s e
Cleared hypotheses: s, e
-- 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)
V : Opens (↑X : Type v)
hV : x ∈ V
⊢ ∃ U ≤ 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 rcases : ∀ (U : Opens (↑X : Type v)) (hxU : x ∈ U) (s : ToType (FC := FC) (CC := CC) (F.obj (op U))),
  ∃ U_1 ≤ V,
    ∃ (m : x ∈ U_1) (s_1 : ToType (FC := FC) (CC := CC) (F.obj (op U_1))),
      Eq (α := CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U_1 x m) : (a : CC (F.obj (op U_1))) → CC (F.stalk x))
            s_1 :
          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)) s :
          CC (F.stalk x))
Tactic: rcases F.exists_germ_eq t with ⟨U, hxU, s, rfl⟩
Cleared hypotheses: t
-- 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)
V : Opens (↑X : Type v)
hV : x ∈ V
U : Opens (↑X : Type v)
hxU : x ∈ U
s : ToType (FC := FC) (CC := CC) (F.obj (op U))
⊢ ∃ U_1 ≤ V,
    ∃ (m : x ∈ U_1) (s_1 : ToType (FC := FC) (CC := CC) (F.obj (op U_1))),
      Eq (α := CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U_1 x m) : (a : CC (F.obj (op U_1))) → CC (F.stalk x))
            s_1 :
          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)) s :
          CC (F.stalk x))
have refine : Eq (α := CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ (U ⊓ V) x sorry) : (a : CC (F.obj (op (U ⊓ V)))) → CC (F.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (Quiver.Hom.op (homOfLE sorry))) :
            (a : CC (F.obj (op U))) → CC (F.obj (op (U ⊓ V))))
          s :
        CC (F.obj (op (U ⊓ V)))) :
    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)) s :
    CC (F.stalk x))
Tactic: refine ⟨U ⊓ V, inf_le_right, by simp [*], F.map (homOfLE inf_le_left).op s, ?_⟩
-- 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
U V : Opens (↑X : Type v)
x : (↑X : Type v)
mU : x ∈ U
mV : x ∈ V
s : ToType (FC := FC) (CC := CC) (F.obj (op U))
t : ToType (FC := FC) (CC := CC) (F.obj (op V))
h :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x mU) : (a : CC (F.obj (op U))) → CC (F.stalk x)) s :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x mV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) t :
      CC (F.stalk x))
⊢ ∃ (W : Opens (↑X : Type v)) (_ : x ∈ W) (iU : W ⟶ U) (iV : W ⟶ V),
    Eq (α := CC (F.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W))) s :
        CC (F.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) t :
        CC (F.obj (op W)))
have obtain : ∀ (W : (OpenNhds x)ᵒᵖ) (iU : op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U mU) ⟶ W)
  (iV : op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) V mV) ⟶ W)
  (e :
    Eq (α := CC (((OpenNhds.inclusion x).op ⋙ F).obj W))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (((OpenNhds.inclusion x).op ⋙ F).map iU) :
            (a : CC (((OpenNhds.inclusion x).op ⋙ F).obj (op ⟨U, mU⟩))) → CC (((OpenNhds.inclusion x).op ⋙ F).obj W))
          s :
        CC (((OpenNhds.inclusion x).op ⋙ F).obj W))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (((OpenNhds.inclusion x).op ⋙ F).map iV) :
            (a : CC (((OpenNhds.inclusion x).op ⋙ F).obj (op ⟨V, mV⟩))) → CC (((OpenNhds.inclusion x).op ⋙ F).obj W))
          t :
        CC (((OpenNhds.inclusion x).op ⋙ F).obj W))),
  ∃ (W : Opens (↑X : Type v)) (_ : x ∈ W) (iU : W ⟶ U) (iV : W ⟶ V),
    Eq (α := CC (F.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W))) s :
        CC (F.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) t :
        CC (F.obj (op W)))
Tactic: obtain ⟨W, iU, iV, e⟩ := (colimit.isColimit ((OpenNhds.inclusion x).op ⋙ F)).eq_iff.mp h
-- 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 G : Presheaf C X
f : F ⟶ G
h :
  ∀ (U : Opens (↑X : Type v)),
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U))) : (a : CC (F.obj (op U))) → CC (G.obj (op U)))
x : (↑X : Type v)
s t : CC (obj (stalkFunctor C x) F)
hst :
  Eq (α := CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f) :
          (a : CC ((stalkFunctor C x).obj F)) → CC ((stalkFunctor C x).obj G))
        s :
      CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f) :
          (a : CC ((stalkFunctor C x).obj F)) → CC ((stalkFunctor C x).obj G))
        t :
      CC (obj (stalkFunctor C x) G))
⊢ s = t
have rcases : ∀ (U₁ : Opens (↑X : Type v)) (hxU₁ : x ∈ U₁) (s : ToType (FC := FC) (CC := CC) (F.obj (op U₁)))
  (hst :
    Eq (α := CC (obj (stalkFunctor C x) G))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f) :
            (a : CC ((stalkFunctor C x).obj F)) → CC ((stalkFunctor C x).obj G))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x))
              s :
            CC (F.stalk x)) :
        CC (obj (stalkFunctor C x) G))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f) :
            (a : CC ((stalkFunctor C x).obj F)) → CC ((stalkFunctor C x).obj G))
          t :
        CC (obj (stalkFunctor C x) G))),
  (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x)) s = t
Tactic: rcases exists_germ_eq F s with ⟨U₁, hxU₁, s, rfl⟩
Cleared hypotheses: s, hst
-- 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 G : Presheaf C X
f : F ⟶ G
h :
  ∀ (U : Opens (↑X : Type v)),
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U))) : (a : CC (F.obj (op U))) → CC (G.obj (op U)))
x : (↑X : Type v)
t : CC (obj (stalkFunctor C x) F)
U₁ : Opens (↑X : Type v)
hxU₁ : x ∈ U₁
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
hst :
  Eq (α := CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f) :
          (a : CC ((stalkFunctor C x).obj F)) → CC ((stalkFunctor C x).obj G))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x)) s :
          CC (F.stalk x)) :
      CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f) :
          (a : CC ((stalkFunctor C x).obj F)) → CC ((stalkFunctor C x).obj G))
        t :
      CC (obj (stalkFunctor C x) G))
⊢ (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x)) s = t
have rcases : ∀ (U₂ : Opens (↑X : Type v)) (hxU₂ : x ∈ U₂) (t : ToType (FC := FC) (CC := CC) (F.obj (op U₂)))
  (hst :
    Eq (α := CC (obj (stalkFunctor C x) G))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f) :
            (a : CC ((stalkFunctor C x).obj F)) → CC ((stalkFunctor C x).obj G))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x))
              s :
            CC (F.stalk x)) :
        CC (obj (stalkFunctor C x) G))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f) :
            (a : CC ((stalkFunctor C x).obj F)) → CC ((stalkFunctor C x).obj G))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₂ x hxU₂) : (a : CC (F.obj (op U₂))) → CC (F.stalk x))
              t :
            CC (F.stalk x)) :
        CC (obj (stalkFunctor C x) G))),
  Eq (α := CC (obj (stalkFunctor C x) F))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x)) s :
      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)) t :
      CC (F.stalk x))
Tactic: rcases exists_germ_eq F t with ⟨U₂, hxU₂, t, rfl⟩
Cleared hypotheses: t, hst
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (hypothesis)
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 G : Presheaf C X
f : F ⟶ G
h :
  ∀ (U : Opens (↑X : Type v)),
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U))) : (a : CC (F.obj (op U))) → CC (G.obj (op U)))
x : (↑X : Type v)
U₁ : Opens (↑X : Type v)
hxU₁ : x ∈ U₁
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
t : ToType (FC := FC) (CC := CC) (F.obj (op U₂))
hst :
  Eq (α := CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f) :
          (a : CC ((stalkFunctor C x).obj F)) → CC ((stalkFunctor C x).obj G))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x)) s :
          CC (F.stalk x)) :
      CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f) :
          (a : CC ((stalkFunctor C x).obj F)) → CC ((stalkFunctor C x).obj G))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₂ x hxU₂) : (a : CC (F.obj (op U₂))) → CC (F.stalk x)) t :
          CC (F.stalk x)) :
      CC (obj (stalkFunctor C x) G))
⊢ Eq (α := CC (obj (stalkFunctor C x) F))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x)) s :
      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)) t :
      CC (F.stalk x))
have hst₁ : Eq (α := CC (obj (stalkFunctor C x) G))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U₁ x hxU₁) : (a : CC (G.obj (op U₁))) → CC (G.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U₁)) : (a : CC (F.obj (op U₁))) → CC (G.obj (op U₁))) s :
        CC (G.obj (op U₁))) :
    CC (G.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U₂ x hxU₂) : (a : CC (G.obj (op U₂))) → CC (G.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U₂)) : (a : CC (F.obj (op U₂))) → CC (G.obj (op U₂))) t :
        CC (G.obj (op U₂))) :
    CC (G.stalk x))
Tactic: rw [stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply] at hst
Cleared hypotheses: hst
-- 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 G : Presheaf C X
f : F ⟶ G
h :
  ∀ (U : Opens (↑X : Type v)),
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U))) : (a : CC (F.obj (op U))) → CC (G.obj (op U)))
x : (↑X : Type v)
U₁ : Opens (↑X : Type v)
hxU₁ : x ∈ U₁
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
t : ToType (FC := FC) (CC := CC) (F.obj (op U₂))
hst :
  Eq (α := CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U₁ x hxU₁) : (a : CC (G.obj (op U₁))) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U₁)) : (a : CC (F.obj (op U₁))) → CC (G.obj (op U₁)))
            s :
          CC (G.obj (op U₁))) :
      CC (G.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U₂ x hxU₂) : (a : CC (G.obj (op U₂))) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U₂)) : (a : CC (F.obj (op U₂))) → CC (G.obj (op U₂)))
            t :
          CC (G.obj (op U₂))) :
      CC (G.stalk x))
⊢ Eq (α := CC (obj (stalkFunctor C x) F))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x)) s :
      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)) t :
      CC (F.stalk x))
have obtain : ∀ (W : Opens (↑X : Type v)) (hxW : x ∈ W) (iWU₁ : W ⟶ U₁) (iWU₂ : W ⟶ U₂)
  (heq :
    Eq (α := CC (G.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map iWU₁.op) : (a : CC (G.obj (op U₁))) → CC (G.obj (op W)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U₁)) : (a : CC (F.obj (op U₁))) → CC (G.obj (op U₁)))
              s :
            CC (G.obj (op U₁))) :
        CC (G.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map iWU₂.op) : (a : CC (G.obj (op U₂))) → CC (G.obj (op W)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U₂)) : (a : CC (F.obj (op U₂))) → CC (G.obj (op U₂)))
              t :
            CC (G.obj (op U₂))) :
        CC (G.obj (op W)))),
  Eq (α := CC (obj (stalkFunctor C x) F))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x)) s :
      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)) t :
      CC (F.stalk x))
Tactic: obtain ⟨W, hxW, iWU₁, iWU₂, heq⟩ := G.germ_eq x hxU₁ hxU₂ _ _ hst
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (hypothesis)
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 G : Presheaf C X
f : F ⟶ G
h :
  ∀ (U : Opens (↑X : Type v)),
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U))) : (a : CC (F.obj (op U))) → CC (G.obj (op U)))
x : (↑X : Type v)
U₁ : Opens (↑X : Type v)
hxU₁ : x ∈ U₁
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
t : ToType (FC := FC) (CC := CC) (F.obj (op U₂))
hst :
  Eq (α := CC (obj (stalkFunctor C x) G))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U₁ x hxU₁) : (a : CC (G.obj (op U₁))) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U₁)) : (a : CC (F.obj (op U₁))) → CC (G.obj (op U₁)))
            s :
          CC (G.obj (op U₁))) :
      CC (G.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U₂ x hxU₂) : (a : CC (G.obj (op U₂))) → CC (G.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U₂)) : (a : CC (F.obj (op U₂))) → CC (G.obj (op U₂)))
            t :
          CC (G.obj (op U₂))) :
      CC (G.stalk x))
W : Opens (↑X : Type v)
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  Eq (α := CC (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op W)) : (a : CC (F.obj (op W))) → CC (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU₁.op) : (a : CC (F.obj (op U₁))) → CC (F.obj (op W))) s :
          CC (F.obj (op W))) :
      CC (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op W)) : (a : CC (F.obj (op W))) → CC (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU₂.op) : (a : CC (F.obj (op U₂))) → CC (F.obj (op W))) t :
          CC (F.obj (op W))) :
      CC (G.obj (op W)))
⊢ Eq (α := CC (obj (stalkFunctor C x) F))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U₁ x hxU₁) : (a : CC (F.obj (op U₁))) → CC (F.stalk x)) s :
      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)) t :
      CC (F.stalk x))
have heq₁ : 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))) s :
    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))) t :
    CC (F.obj (op W)))
Tactic: replace heq := h W heq
Cleared hypotheses: heq