awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
B : Set (Opens (↑X : Type v))
hB : Opens.IsBasis B
F G : Presheaf C X
α : F ⟶ G
hα :
  ∀ U ∈ B,
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (α.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₁
hU₁ : U₁ ∈ B
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
hU₂ : U₂ ∈ B
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) α) :
          (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) α) :
          (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) (α.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) (α.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))
B : Set (Opens (↑X : Type v))
hB : Opens.IsBasis B
F G : Presheaf C X
α : F ⟶ G
hα :
  ∀ U ∈ B,
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (α.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₁
hU₁ : U₁ ∈ B
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
hU₂ : U₂ ∈ B
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) (α.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) (α.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) (hW : W ∈ B) (iWU₁ : W ≤ U₁) (iWU₂ : W ≤ U₂)
  (heq :
    Eq (α := CC (G.obj (op W)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map (homOfLE iWU₁).op) :
            (a : CC (G.obj (op U₁))) → CC (G.obj (op W)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.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 (homOfLE iWU₂).op) :
            (a : CC (G.obj (op U₂))) → CC (G.obj (op W)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.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, hW, iWU₁, iWU₂, heq⟩ := germ_eq_of_isBasis hB _ _ 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))
B : Set (Opens (↑X : Type v))
hB : Opens.IsBasis B
F G : Presheaf C X
α : F ⟶ G
hα :
  ∀ U ∈ B,
    Function.Injective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (G.obj (op U)))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (α.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₁
hU₁ : U₁ ∈ B
s : ToType (FC := FC) (CC := CC) (F.obj (op U₁))
U₂ : Opens (↑X : Type v)
hxU₂ : x ∈ U₂
hU₂ : U₂ ∈ B
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) (α.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) (α.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
hW : W ∈ B
iWU₁ : W ≤ U₁
iWU₂ : W ≤ U₂
heq :
  Eq (α := CC (G.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map (homOfLE iWU₁).op) :
          (a : CC (G.obj (op U₁))) → CC (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.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 (homOfLE iWU₂).op) :
          (a : CC (G.obj (op U₂))) → CC (G.obj (op W)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (α.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))
have heq₁ : Eq (α := CC (F.obj (op W)))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE 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 (homOfLE iWU₂).op) : (a : CC (F.obj (op U₂))) → CC (F.obj (op W)))
      t :
    CC (F.obj (op W)))
Tactic: simp only [← α.naturality_apply, (hα W hW).eq_iff] at heq
Cleared hypotheses: heq
-- 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))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F : Sheaf C X
U : Opens (↑X : Type v)
s t :
  ToType (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
h :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Eq (α := CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          s :
        CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          t :
        CC (F.presheaf.stalk x))
⊢ s = t
have choose : ∀ (V : (x : ↥U) → Opens (↑X : Type v)) (m : ∀ (x : ↥U), (↑x : (↑X : Type v)) ∈ V x) (i₁ i₂ : (x : ↥U) → V x ⟶ U)
  (heq :
    ∀ (x : ↥U),
      Eq (α := CC (F.presheaf.obj (op (V x))))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₁ x).op) :
              (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
            s :
          CC (F.presheaf.obj (op (V x))))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₂ x).op) :
              (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
            t :
          CC (F.presheaf.obj (op (V x))))),
  s = t
Tactic: choose V m i₁ i₂ heq using fun x : U => F.presheaf.germ_eq x.1 x.2 x.2 s t (h x.1 x.2)
-- 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))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F : Sheaf C X
U : Opens (↑X : Type v)
s t :
  ToType (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
h :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Eq (α := CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          s :
        CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          t :
        CC (F.presheaf.stalk x))
V : (x : ↥U) → Opens (↑X : Type v)
m : ∀ (x : ↥U), (↑x : (↑X : Type v)) ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U),
    Eq (α := CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₁ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          s :
        CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₂ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          t :
        CC (F.presheaf.obj (op (V x))))
⊢ s = t
have hcover : U ≤ iSup V
Tactic: apply F.eq_of_locally_eq' V U i₁
-- 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))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F : Sheaf C X
U : Opens (↑X : Type v)
s t :
  ToType (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
h :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Eq (α := CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          s :
        CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          t :
        CC (F.presheaf.stalk x))
V : (x : ↥U) → Opens (↑X : Type v)
m : ∀ (x : ↥U), (↑x : (↑X : Type v)) ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U),
    Eq (α := CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₁ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          s :
        CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₂ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          t :
        CC (F.presheaf.obj (op (V x))))
hcover : U ≤ iSup V
⊢ s = t
have h₁ : ∀ (i : ↥U),
  Eq (α := CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V i))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (i₁ i).op) :
          (a : CC (F.obj.obj (op U))) → CC (F.obj.obj (op (V i))))
        s :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V i))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (i₁ i).op) :
          (a : CC (F.obj.obj (op U))) → CC (F.obj.obj (op (V i))))
        t :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V i))))
Tactic: apply F.eq_of_locally_eq' V U i₁
-- 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))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F : Sheaf C X
U : Opens (↑X : Type v)
s t :
  ToType (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
h :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Eq (α := CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          s :
        CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          t :
        CC (F.presheaf.stalk x))
V : (x : ↥U) → Opens (↑X : Type v)
m : ∀ (x : ↥U), (↑x : (↑X : Type v)) ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U),
    Eq (α := CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₁ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          s :
        CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₂ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          t :
        CC (F.presheaf.obj (op (V x))))
x : (↑X : Type v)
hxU : x ∈ U
⊢ x ∈ iSup V
have hcover : ∃ (i : ↥U), x ∈ V i
Tactic: simp only [Opens.mem_iSup]
-- 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))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F : Sheaf C X
G : Presheaf C X
f : F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))) ⟶ G
U : Opens (↑X : Type v)
h :
  ∀ x ∈ U,
    Function.Injective.{v + 1, v + 1} (α :=
      CC
        (obj (stalkFunctor C x)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
      (β := CC (obj (stalkFunctor C x) G))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f)) :
        (a : CC ((stalkFunctor C x).obj F.obj)) → CC ((stalkFunctor C x).obj G))
s t : CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
hst :
  Eq (α := CC (G.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U)) : (a : CC (F.obj.obj (op U))) → CC (G.obj (op U))) s :
      CC (G.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U)) : (a : CC (F.obj.obj (op U))) → CC (G.obj (op U))) t :
      CC (G.obj (op U)))
x : (↑X : Type v)
hx : x ∈ U
⊢ 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.obj)) → CC ((stalkFunctor C x).obj G))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
              (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
            s :
          CC (F.presheaf.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.obj)) → CC ((stalkFunctor C x).obj G))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
              (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
            t :
          CC (F.presheaf.stalk x)) :
      CC (obj (stalkFunctor C x) G))
have rw : Eq (α := CC (obj (stalkFunctor C x) G))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.germ U x hx) : (a : CC (G.obj (op U))) → CC (G.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op U)) : (a : CC (F.obj.obj (op U))) → CC (G.obj (op U))) s :
        CC (G.obj (op U))) :
    CC (G.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f) :
        (a : CC ((stalkFunctor C x).obj F.obj)) → CC ((stalkFunctor C x).obj G))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          t :
        CC (F.presheaf.stalk x)) :
    CC (obj (stalkFunctor C x) G))
Tactic: rw [stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply, 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))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
h :
  ∀ x ∈ U,
    Function.Bijective.{v + 1, v + 1} (α :=
      CC
        (obj (stalkFunctor C x)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
      (β :=
      CC
        (obj (stalkFunctor C x)
          (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))))))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (map (stalkFunctor C x) f.hom)) :
        (a : CC ((stalkFunctor C x).obj F.obj)) → CC ((stalkFunctor C x).obj G.obj))
⊢ Function.Surjective.{v + 1, v + 1} (α :=
    CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))) (β :=
    CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U)))
    (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op U))) :
      (a : CC (F.obj.obj (op U))) → CC (G.obj.obj (op U)))
have refine : ∀ (t : CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U)))
  (x : (↑X : Type v)) (hx : x ∈ U),
  ∃ (V : Opens (↑X : Type v)) (_ : x ∈ V) (iVU : V ⟶ U) (s :
    ToType (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op V))),
    Eq (α := CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op V)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op V)) :
            (a : CC (F.obj.obj (op V))) → CC (G.obj.obj (op V)))
          s :
        CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op V)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map iVU.op) :
            (a : CC (G.obj.obj (op U))) → CC (G.obj.obj (op V)))
          t :
        CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op V)))
Tactic: refine app_surjective_of_injective_of_locally_surjective f U (And.left <| h · ·) fun t x hx => ?_
-- 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))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F G : Sheaf C X
f : F ⟶ G
U : Opens (↑X : Type v)
inst_7 :
  ∀ (x : ↥U),
    IsIso (X :=
      obj (stalkFunctor C (↑x : (↑X : Type v)))
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v)))))
      (map (stalkFunctor C (↑x : (↑X : Type v))) f.hom)
⊢ IsIso (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
    (f.hom.app (op U))
have suffices : IsIso (X :=
  obj (forget C (FC := FC) (CC := CC))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U)))
  (map (forget C (FC := FC) (CC := CC)) (f.hom.app (op U)))
Tactic: suffices IsIso ((forget C).map (f.1.app (op U))) by
    exact isIso_of_reflects_iso (f.1.app (op U)) (forget C)