awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
⊢ ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1
have mpr : ∀ (s_x : CC (Functor.obj (stalkFunctor C x) ℱ))
  (hs_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 𝒢))
        s_x =
      t_x),
  ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1
Tactic: obtain ⟨s_x, hs_x : ((stalkFunctor C x).map T) s_x = t_x⟩ := hT x t_x
-- 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 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
s_x : CC (Functor.obj (stalkFunctor C x) ℱ)
hs_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 𝒢))
      s_x =
    t_x
⊢ ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1
have mpr : ∀ (V : Opens (↑X : Type v)) (hxV : x ∈ V) (s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V)))
  (hs_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)) =
      t_x),
  ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1
Tactic: obtain ⟨V, hxV, s, rfl⟩ := ℱ.exists_germ_eq s_x
Cleared hypotheses: s_x, hs_x
-- 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 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_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)) =
    t_x
⊢ Eq (α := CC (𝒢.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ V x hxV) : (a : CC (𝒢.obj (op V))) → CC (𝒢.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.stalk 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 : CC (𝒢.stalk x) = CC (Functor.obj (stalkFunctor C x) 𝒢) →
  Eq (α := CC (𝒢.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ V x hxV) : (a : CC (𝒢.obj (op V))) → CC (𝒢.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.stalk 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) 𝒢))
Tactic: convert! hs_x using 1
-- 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 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_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)) =
    t_x
e_1 : CC (𝒢.stalk x) = CC (Functor.obj (stalkFunctor C x) 𝒢)
⊢ Eq (α := CC (𝒢.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ V x hxV) : (a : CC (𝒢.obj (op V))) → CC (𝒢.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.stalk 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) 𝒢))
have h : Eq (α := CC (𝒢.stalk 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 V x hxV) : (a : CC (𝒢.obj (op V))) → CC (𝒢.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
        CC (𝒢.obj (op V))) :
    CC (𝒢.stalk x))
Tactic: symm
-- 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
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_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)) =
    t_x
⊢ ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1
have key_W : ∃ (W : Opens (↑X : Type v)) (_ : x ∈ W) (iU : W ⟶ V) (iV : W ⟶ U),
  Eq (α := CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map iU.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map iV.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
      CC (𝒢.obj (op W)))
Tactic: have key_W := 𝒢.germ_eq x hxV hxU (T.app _ s) t <| by
      convert! hs_x using 1
      symm
      convert! stalkFunctor_map_germ_apply _ _ _ _ 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 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_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)) =
    t_x
key_W :
  ∃ (W : Opens (↑X : Type v)) (_ : x ∈ W) (iU : W ⟶ V) (iV : W ⟶ U),
    Eq (α := CC (𝒢.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map iU.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
            CC (𝒢.obj (op V))) :
        CC (𝒢.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map iV.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
        CC (𝒢.obj (op W)))
⊢ ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1
have mpr : ∀ (W : Opens (↑X : Type v)) (hxW : x ∈ W) (hWV : W ⟶ V) (hWU : W ⟶ U)
  (h_eq :
    Eq (α := CC (𝒢.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWV.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
            CC (𝒢.obj (op V))) :
        CC (𝒢.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWU.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
        CC (𝒢.obj (op W)))),
  ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1
Tactic: obtain ⟨W, hxW, hWV, hWU, h_eq⟩ := key_W
Cleared hypotheses: key_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
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
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_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)) =
    t_x
W : Opens (↑X : Type v)
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq :
  Eq (α := CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWV.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWU.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
      CC (𝒢.obj (op W)))
⊢ ∃ (U_1 : Opens (↑X : Type v)) (f : U_1 ⟶ U), (Presheaf.imageSieve (FA := FC) (CA := CC) T t).arrows f ∧ x ∈ U_1
have mpr : Eq (α := CC (𝒢.obj (op W)))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op W)) : (a : CC (ℱ.obj (op W))) → CC (𝒢.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.map hWV.op) : (a : CC (ℱ.obj (op V))) → CC (ℱ.obj (op W))) s :
        CC (ℱ.obj (op W))) :
    CC (𝒢.obj (op W)))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWU.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
    CC (𝒢.obj (op W)))
Tactic: refine ⟨W, hWU, ⟨ℱ.map hWV.op s, ?_⟩, hxW⟩
-- 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 𝒢))
U : Opens (↑X : Type v)
t : ToType (FC := FC) (CC := CC) (𝒢.obj (op U))
x : (↑X : Type v)
hxU : x ∈ U
t_x : CC (𝒢.stalk x) :=
  (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
ht_x : t_x = (ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.germ U x hxU) : (a : CC (𝒢.obj (op U))) → CC (𝒢.stalk x)) t
V : Opens (↑X : Type v)
hxV : x ∈ V
s : ToType (FC := FC) (CC := CC) (ℱ.obj (op V))
hs_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)) =
    t_x
W : Opens (↑X : Type v)
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq :
  Eq (α := CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWV.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
          CC (𝒢.obj (op V))) :
      CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWU.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
      CC (𝒢.obj (op W)))
⊢ Eq (α := CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op W)) : (a : CC (ℱ.obj (op W))) → CC (𝒢.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.map hWV.op) : (a : CC (ℱ.obj (op V))) → CC (ℱ.obj (op W))) s :
          CC (ℱ.obj (op W))) :
      CC (𝒢.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWU.op) : (a : CC (𝒢.obj (op U))) → CC (𝒢.obj (op W))) t :
      CC (𝒢.obj (op W)))
have h : Eq (α := CC (𝒢.obj (op W)))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op W)) : (a : CC (ℱ.obj (op W))) → CC (𝒢.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (ℱ.map hWV.op) : (a : CC (ℱ.obj (op V))) → CC (ℱ.obj (op W))) s :
        CC (ℱ.obj (op W))) :
    CC (𝒢.obj (op W)))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (𝒢.map hWV.op) : (a : CC (𝒢.obj (op V))) → CC (𝒢.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (T.app (op V)) : (a : CC (ℱ.obj (op V))) → CC (𝒢.obj (op V))) s :
        CC (𝒢.obj (op V))) :
    CC (𝒢.obj (op W)))
Tactic: convert! h_eq using 1
-- Lean 4 proof step from Mathlib.Topology.Sheaves.MayerVietoris (goal)
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
⊢ IsLimit sq.pullbackCone
have refine_1 : (s : PullbackCone sq.f₂₄ sq.f₃₄) → s.pt ⟶ sq.X₁
Tactic: refine PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Sheaves.MayerVietoris (goal)
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
refine_1 : (s : PullbackCone sq.f₂₄ sq.f₃₄) → s.pt ⟶ sq.X₁
⊢ IsLimit sq.pullbackCone
have refine_2 : ∀ (s : PullbackCone sq.f₂₄ sq.f₃₄), homOfLE sorry ≫ sq.f₁₂ = s.fst
Tactic: refine PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Sheaves.MayerVietoris (goal)
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
refine_1 : (s : PullbackCone sq.f₂₄ sq.f₃₄) → s.pt ⟶ sq.X₁
refine_2 : ∀ (s : PullbackCone sq.f₂₄ sq.f₃₄), homOfLE ⋯ ≫ sq.f₁₂ = s.fst
⊢ IsLimit sq.pullbackCone
have refine_3 : ∀ (s : PullbackCone sq.f₂₄ sq.f₃₄), homOfLE sorry ≫ sq.f₁₃ = s.snd
Tactic: refine PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Sheaves.MayerVietoris (goal)
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
refine_1 : (s : PullbackCone sq.f₂₄ sq.f₃₄) → s.pt ⟶ sq.X₁
refine_2 : ∀ (s : PullbackCone sq.f₂₄ sq.f₃₄), homOfLE ⋯ ≫ sq.f₁₂ = s.fst
refine_3 : ∀ (s : PullbackCone sq.f₂₄ sq.f₃₄), homOfLE ⋯ ≫ sq.f₁₃ = s.snd
⊢ IsLimit sq.pullbackCone
have refine_4 : ∀ (s : PullbackCone sq.f₂₄ sq.f₃₄) (m : s.pt ⟶ sq.X₁), m ≫ sq.f₁₂ = s.fst → m ≫ sq.f₁₃ = s.snd → m = homOfLE sorry
Tactic: refine PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Sheaves.MayerVietoris (goal)
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s : PullbackCone sq.f₂₄ sq.f₃₄
⊢ s.pt ⟶ sq.X₁
have refine_1 : s.pt ≤ sq.X₁
Tactic: apply homOfLE
-- Lean 4 proof step from Mathlib.Topology.Sheaves.MayerVietoris (goal)
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s : PullbackCone sq.f₂₄ sq.f₃₄
⊢ s.pt ≤ sq.X₁
have refine_1 : s.pt ≤ sq.X₂ ∧ s.pt ≤ sq.X₃
Tactic: rw [h₁, le_inf_iff]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.MayerVietoris (hypothesis)
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ sq.X₄
⊢ ∃ (U : Opens T) (f : U ⟶ sq.X₄), (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U
have hx₁ : x ∈ sq.X₂ ⊔ sq.X₃
Tactic: rw [h₄] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Sheaves.MayerVietoris (goal)
Goal:
T : Type u
inst : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ sq.X₂ ⊔ sq.X₃
⊢ ∃ (U : Opens T) (f : U ⟶ sq.X₄), (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U
have inl : ∀ (hx : x ∈ (↑sq.X₂ : Set T)), ∃ (U : Opens T) (f : U ⟶ sq.X₄), (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U
Tactic: obtain (hx | hx) := hx
Cleared hypotheses: hx