awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
Goal:
X : TopCat
T : (↑X : Type u_1) → Type u_1
P : LocalPredicate T
x : (↑X : Type u_1)
w :
  ∀ (t : T x),
    ∃ (U : OpenNhds x) (f : (y : ↥(↑U : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1))) (_ :
      P.toPrelocalPredicate (T := T).pred (T := T) f),
      f (Subtype.mk (p := fun (x_2 : (↑X : Type u_1)) ↦ x_2 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) = t
U : OpenNhds x
f : (y : ↥(↑U : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1))
h : P.toPrelocalPredicate (T := T).pred (T := T) f
⊢ ∃ (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes (T := T) P).presheaf.stalk x)),
    Eq (α := (fun (X : Type u_1) ↦ X) (T x))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (stalkToFiber (T := T) P x) :
            (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.stalk x)) → (fun (X : Type u_1) ↦ X) (T x))
          a :
        (fun (X : Type u_1) ↦ X) (T x))
      (f (Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) :
        T (↑(Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) : (↑X : Type u_1)))
have w₁ : (fun (X : Type u_1) ↦ X) ((subsheafToTypes (T := T) P).presheaf.stalk x)
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
Goal:
X : TopCat
T : (↑X : Type u_1) → Type u_1
P : LocalPredicate T
x : (↑X : Type u_1)
w :
  ∀ (t : T x),
    ∃ (U : OpenNhds x) (f : (y : ↥(↑U : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1))) (_ :
      P.toPrelocalPredicate (T := T).pred (T := T) f),
      f (Subtype.mk (p := fun (x_2 : (↑X : Type u_1)) ↦ x_2 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) = t
U : OpenNhds x
f : (y : ↥(↑U : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1))
h : P.toPrelocalPredicate (T := T).pred (T := T) f
w₁ : (fun (X : Type u_1) ↦ X) ((subsheafToTypes (T := T) P).presheaf.stalk x)
⊢ ∃ (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes (T := T) P).presheaf.stalk x)),
    Eq (α := (fun (X : Type u_1) ↦ X) (T x))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (stalkToFiber (T := T) P x) :
            (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.stalk x)) → (fun (X : Type u_1) ↦ X) (T x))
          a :
        (fun (X : Type u_1) ↦ X) (T x))
      (f (Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) :
        T (↑(Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) : (↑X : Type u_1)))
have h₁ : Eq (α := (fun (X : Type u_1) ↦ X) (T x))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (stalkToFiber (T := T) P x) :
        (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.stalk x)) → (fun (X : Type u_1) ↦ X) (T x))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((subsheafToTypes (T := T) P).presheaf.germ (↑U : Opens (↑X : Type u_1)) x sorry) :
          (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.obj (op (↑U : Opens (↑X : Type u_1))))) →
            (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.stalk x))
        (Subtype.mk (p := fun (f : (x_1 : ↥(unop (op (↑U : Opens (↑X : Type u_1))))) → T (↑x_1 : (↑X : Type u_1))) ↦
          P.toPrelocalPredicate (T := T).pred (T := T) f) f h)) :
    (fun (X : Type u_1) ↦ X) (T x))
  (f (Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x sorry) :
    T (↑(Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x sorry) : (↑X : Type u_1)))
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
Goal:
X : TopCat
T : (↑X : Type u_1) → Type u_1
P : LocalPredicate T
x : (↑X : Type u_1)
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T (↑x_1 : (↑X : Type u_1))
hU : P.toPrelocalPredicate (T := T).pred (T := T) fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T (↑x_1 : (↑X : Type u_1))
hV : P.toPrelocalPredicate (T := T).pred (T := T) fV
h :
  Eq (α := T x)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((P.cocone (T := T) x).ι.app U) :
          (a : { f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop U))) → T (↑x_1 : (↑X : Type u_1)) // P.pred f }) →
            (P.cocone x).pt)
        (Subtype.mk (p := fun (f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop U))) → T (↑x_1 : (↑X : Type u_1))) ↦
          P.toPrelocalPredicate (T := T).pred (T := T) f) fU hU) :
      (P.cocone (T := T) x).pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((P.cocone (T := T) x).ι.app V) :
          (a : { f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop V))) → T (↑x_1 : (↑X : Type u_1)) // P.pred f }) →
            (P.cocone x).pt)
        (Subtype.mk (p := fun (f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop V))) → T (↑x_1 : (↑X : Type u_1))) ↦
          P.toPrelocalPredicate (T := T).pred (T := T) f) fV hV) :
      (P.cocone (T := T) x).pt)
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w :
  ∀ (w : ↥(↑W : Opens (↑X : Type u_1))),
    Eq (α :=
      T (↑((iU : (a : ↥(↑W : Opens (↑X : Type u_1))) → ↥(↑(unop U) : Opens (↑X : Type u_1))) w) : (↑X : Type u_1)))
      (fU ((iU : (a : ↥(↑W : Opens (↑X : Type u_1))) → ↥(↑(unop U) : Opens (↑X : Type u_1))) w))
      (fV ((iV : (a : ↥(↑W : Opens (↑X : Type u_1))) → ↥(↑(unop V) : Opens (↑X : Type u_1))) w))
⊢ (↑(unop (op W)) : Opens (↑X : Type u_1)) ⟶ (↑(unop U) : Opens (↑X : Type u_1))
have refine_1 : (W : Opens (↑X : Type u_1)) →
  (m : x ∈ W) →
    (iU : Subtype.mk (p := fun (U : Opens (↑X : Type u_1)) ↦ x ∈ U) W m ⟶ unop U) →
      (iV : Subtype.mk (p := fun (U : Opens (↑X : Type u_1)) ↦ x ∈ U) W m ⟶ unop V) →
        (w :
            ∀ (w : ↥(↑(Subtype.mk (p := fun (U : Opens (↑X : Type u_1)) ↦ x ∈ U) W m) : Opens (↑X : Type u_1))),
              Eq (α :=
                T
                  (↑((iU : (a : ↥(↑⟨W, m⟩ : Opens (↑X : Type u_1))) → ↥(↑(unop U) : Opens (↑X : Type u_1))) w) :
                    (↑X : Type u_1)))
                (fU ((iU : (a : ↥(↑⟨W, m⟩ : Opens (↑X : Type u_1))) → ↥(↑(unop U) : Opens (↑X : Type u_1))) w))
                (fV ((iV : (a : ↥(↑⟨W, m⟩ : Opens (↑X : Type u_1))) → ↥(↑(unop V) : Opens (↑X : Type u_1))) w))) →
          (↑(unop (op (Subtype.mk (p := fun (U : Opens (↑X : Type u_1)) ↦ x ∈ U) W m))) : Opens (↑X : Type u_1)) ⟶
            (↑(unop U) : Opens (↑X : Type u_1))
Tactic: rcases W with ⟨W, m⟩
Cleared hypotheses: W, iU, iV, w
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
T : ℱ ⟶ 𝒢
⊢ IsLocallySurjective (FC := FC) (CC := CC) T ↔
    ∀ (U : Opens (↑X : Type v)) (t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))),
      ∀ x ∈ U,
        ∃ (V : Opens (↑X : Type v)) (x_1 : V ≤ U),
          (∃ (s : CC (ℱ.obj (op V))),
              (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V)))
                  s =
                restrictOpen (FC := FC) (CC := CC) t V x_1) ∧
            x ∈ V
have refine_1 : ∀ (h : IsLocallySurjective (FC := FC) (CC := CC) T) (x : Opens (↑X : Type v))
  (t : ToType (FC := FC) (CC := CC) (𝒢.obj (op x))) (x_1 : (↑X : Type v)) (hx : x_1 ∈ x),
  ∃ (V : Opens (↑X : Type v)) (x_2 : V ≤ x),
    (∃ (s : CC (ℱ.obj (op V))),
        (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s =
          restrictOpen (FC := FC) (CC := CC) t V x_2) ∧
      x_1 ∈ V
Tactic: refine ⟨fun h _ t x hx ↦ ?_, fun h => ⟨fun s x hx ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
T : ℱ ⟶ 𝒢
refine_1 :
  ∀ (h : IsLocallySurjective (FC := FC) (CC := CC) T) (x : Opens (↑X : Type v))
    (t : ToType (FC := FC) (CC := CC) (𝒢.obj (op x))) (x_1 : (↑X : Type v)) (hx : x_1 ∈ x),
    ∃ (V : Opens (↑X : Type v)) (x_2 : V ≤ x),
      (∃ (s : CC (ℱ.obj (op V))),
          (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s =
            restrictOpen (FC := FC) (CC := CC) t V x_2) ∧
        x_1 ∈ V
⊢ IsLocallySurjective (FC := FC) (CC := CC) T ↔
    ∀ (U : Opens (↑X : Type v)) (t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))),
      ∀ x ∈ U,
        ∃ (V : Opens (↑X : Type v)) (x_1 : V ≤ U),
          (∃ (s : CC (ℱ.obj (op V))),
              (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V)))
                  s =
                restrictOpen (FC := FC) (CC := CC) t V x_1) ∧
            x ∈ V
have refine_2 : ∀
  (h :
    ∀ (U : Opens (↑X : Type v)) (t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))),
      ∀ x ∈ U,
        ∃ (V : Opens (↑X : Type v)) (x_1 : V ≤ U),
          (∃ (s : CC (ℱ.obj (op V))),
              (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V)))
                  s =
                restrictOpen (FC := FC) (CC := CC) t V x_1) ∧
            x ∈ V)
  {U : Opens (↑X : Type v)} (s : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))) (x : (↑X : Type v)) (hx : x ∈ U),
  ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T s).arrows f ∧ x ∈ U_1
Tactic: refine ⟨fun h _ t x hx ↦ ?_, fun h => ⟨fun s x hx ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
T : ℱ ⟶ 𝒢
h : IsLocallySurjective (FC := FC) (CC := CC) T
x_1 : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op x_1))
x : (↑X : Type v)
hx : x ∈ x_1
⊢ ∃ (V : Opens (↑X : Type v)) (x_2 : V ≤ x_1),
    (∃ (s : CC (ℱ.obj (op V))),
        (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s =
          restrictOpen (FC := FC) (CC := CC) t V x_2) ∧
      x ∈ V
have refine_1 : ∀ (V : Opens (↑X : Type v)) (i : V ⟶ x_1) (hi : (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows i ∧ x ∈ V),
  ∃ (V : Opens (↑X : Type v)) (x_2 : V ≤ x_1),
    (∃ (s : CC (ℱ.obj (op V))),
        (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s =
          restrictOpen (FC := FC) (CC := CC) t V x_2) ∧
      x ∈ V
Tactic: obtain ⟨V, i, hi⟩ := h.imageSieve_mem t x hx
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
T : ℱ ⟶ 𝒢
h :
  ∀ (U : Opens (↑X : Type v)) (t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))),
    ∀ x ∈ U,
      ∃ (V : Opens (↑X : Type v)) (x_1 : V ≤ U),
        (∃ (s : CC (ℱ.obj (op V))),
            (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V)))
                s =
              restrictOpen (FC := FC) (CC := CC) t V x_1) ∧
          x ∈ V
U : Opens (↑X : Type v)
s : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hx : x ∈ U
⊢ ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T s).arrows f ∧ x ∈ U_1
have refine_2 : ∀ (V : Opens (↑X : Type v)) (Vle : V ≤ U)
  (hV :
    (∃ (s_1 : CC (ℱ.obj (op V))),
        (ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s_1 =
          restrictOpen (FC := FC) (CC := CC) s V Vle) ∧
      x ∈ V),
  ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T s).arrows f ∧ x ∈ U_1
Tactic: obtain ⟨V, Vle, hV⟩ := h _ s x hx
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
⊢ IsLocallySurjective (FC := FC) (CC := CC) T ↔
    ∀ (x : (↑X : Type v)),
      Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
        CC (Functor.obj (stalkFunctor C x) 𝒢))
        (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
          (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
have mp : IsLocallySurjective (FC := FC) (CC := CC) T →
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
mp :
  IsLocallySurjective (FC := FC) (CC := CC) T →
    ∀ (x : (↑X : Type v)),
      Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
        CC (Functor.obj (stalkFunctor C x) 𝒢))
        (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
          (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
⊢ IsLocallySurjective (FC := FC) (CC := CC) T ↔
    ∀ (x : (↑X : Type v)),
      Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
        CC (Functor.obj (stalkFunctor C x) 𝒢))
        (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
          (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
have mpr : (∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))) →
  IsLocallySurjective (FC := FC) (CC := CC) T
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective (FC := FC) (CC := CC) T
x : (↑X : Type v)
g : CC (Functor.obj (stalkFunctor C x) 𝒢)
⊢ ∃ (a : CC (Functor.obj (stalkFunctor C x) ℱ)),
    (ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
          (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
        a =
      g
have mp : ∀ (U : Opens (↑X : Type v)) (hxU : x ∈ U) (t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))),
  ∃ (a : CC (Functor.obj (stalkFunctor C x) ℱ)),
    Eq (α := CC (Functor.obj (stalkFunctor C x) 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
            (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
          a :
        CC (Functor.obj (stalkFunctor C x) 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t :
        CC (𝒢.stalk x))
Tactic: obtain ⟨U, hxU, t, rfl⟩ := 𝒢.exists_germ_eq g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective (FC := FC) (CC := CC) T
x : (↑X : Type v)
U : Opens (↑X : Type v)
hxU : x ∈ U
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
⊢ ∃ (a : CC (Functor.obj (stalkFunctor C x) ℱ)),
    Eq (α := CC (Functor.obj (stalkFunctor C x) 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
            (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
          a :
        CC (Functor.obj (stalkFunctor C x) 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t :
        CC (𝒢.stalk x))
have mp : ∀ (V : Opens (↑X : Type v)) (ι : V ⟶ U) (hxV : x ∈ V) (s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V)))
  (h_eq :
    Eq (α := CC (𝒢.obj (op V)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
        CC (𝒢.obj (op V)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map ι.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op V))) t :
        CC (𝒢.obj (op V)))),
  ∃ (a : CC (Functor.obj (stalkFunctor C x) ℱ)),
    Eq (α := CC (Functor.obj (stalkFunctor C x) 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
            (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
          a :
        CC (Functor.obj (stalkFunctor C x) 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t :
        CC (𝒢.stalk x))
Tactic: rcases hT.imageSieve_mem t x hxU with ⟨V, ι, ⟨s, h_eq⟩, hxV⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective (FC := FC) (CC := CC) T
x : (↑X : Type v)
U : Opens (↑X : Type v)
hxU : x ∈ U
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
V : Opens (↑X : Type v)
ι : V ⟶ U
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
h_eq :
  Eq (α := CC (𝒢.obj (op V)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
      CC (𝒢.obj (op V)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map ι.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op V))) t :
      CC (𝒢.obj (op V)))
⊢ ∃ (a : CC (Functor.obj (stalkFunctor C x) ℱ)),
    Eq (α := CC (Functor.obj (stalkFunctor C x) 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
            (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
          a :
        CC (Functor.obj (stalkFunctor C x) 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t :
        CC (𝒢.stalk x))
have h : Eq (α := CC (Functor.obj (stalkFunctor C x) 𝒢))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.germ V x hxV) : (a : CC (ℱ.obj (op V))) → CC (ℱ.stalk x)) s :
        CC (ℱ.stalk x)) :
    CC (Functor.obj (stalkFunctor C x) 𝒢))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t :
    CC (𝒢.stalk x))
Tactic: use ℱ.germ _ x hxV s
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocallySurjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
⊢ IsLocallySurjective (FC := FC) (CC := CC) T
have mpr : ∀ {U : Opens (↑X : Type v)} (s : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))),
  Presheaf.imageSieve (FA := FC) (CA := CC) T s ∈
    (Opens.grothendieckTopology (↑X : Type v) : (a : Opens (↑X : Type v)) → Set (Sieve a)) U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocallySurjective (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
X : TopCat
ℱ 𝒢 : Presheaf C X
inst_3 : Limits.HasColimits.{v, u} C
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
T : ℱ ⟶ 𝒢
hT :
  ∀ (x : (↑X : Type v)),
    Function.Surjective.{v + 1, v + 1} (α := CC (Functor.obj (stalkFunctor C x) ℱ)) (β :=
      CC (Functor.obj (stalkFunctor C x) 𝒢))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (CategoryTheory.Functor.map (stalkFunctor C x) T)) :
        (a : CC ((stalkFunctor C x).obj ℱ)) → CC ((stalkFunctor C x).obj 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
⊢ ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1
have ht_x : let t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t;
t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
Tactic: set t_x := 𝒢.germ _ x hxU t with ht_x