awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (goal)
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
Y : C
U : Opens (↑X : Type u)
h : p₀ ∈ U
⊢ Eq (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (CategoryStruct.comp (Y := if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C)
        (Presheaf.germ (skyscraperPresheaf p₀ Y) U p₀ ⋯ ≫ eqToHom ⋯)
        (eqToHom ⋯ ≫
          CategoryStruct.comp (Y := Y)
            (Iso.hom
                (colimit.isoColimitCocone
                  { cocone := skyscraperPresheafCoconeOfSpecializes p₀ Y ⋯,
                    isColimit := skyscraperPresheafCoconeIsColimitOfSpecializes p₀ Y ⋯ }) :
              Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ ⟶ Y)
            (eqToHom ⋯)) :
      (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U) :
      Functor.obj (skyscraperPresheaf p₀ Y) (op U) ⟶ Functor.obj (skyscraperPresheaf p₀ Y) (op U))
have pos : Eq.{u + 1} (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
  (𝟙 (if p₀ ∈ U then Y else terminal.{u, v} C)) (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U))
Tactic: simp [Presheaf.germ]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (goal)
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
inst_3 : HasColimits.{u, v} C
Y : C
U : Opens (↑X : Type u)
h : p₀ ∉ U
⊢ Eq.{u + 1} (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
    (IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C) ⋯)
        (if p₀ ∈ U then Y else terminal.{u, v} C) ≫
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{u, v} C = x) ↦ IsTerminal.{u, v} x) terminalIsTerminal
          (if p₀ ∈ U then Y else terminal.{u, v} C) ⋯)
        (if p₀ ∈ U then Presheaf.stalk (skyscraperPresheaf p₀ Y) p₀ else terminal.{u, v} C))
    (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U))
have neg : Eq.{u + 1} (α := (if p₀ ∈ U then Y else terminal.{u, v} C) ⟶ if p₀ ∈ U then Y else terminal.{u, v} C)
  (𝟙 (if p₀ ∈ U then Y else terminal.{u, v} C)) (NatTrans.app (𝟙 (skyscraperPresheaf p₀ Y)) (op U))
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (goal)
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
U : (Opens (↑X : Type u))ᵒᵖ
h : p₀ ∉ unop U
⊢ IsTerminal.{u, v}
    (Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) (skyscraperSheaf p₀ A))
      U)
have dsimp : IsTerminal.{u, v} (if p₀ ∈ unop U then A else terminal.{u, v} C)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Skyscraper (goal)
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
U : (Opens (↑X : Type u))ᵒᵖ
h : p₀ ∉ unop U
⊢ IsTerminal.{u, v} (if p₀ ∈ unop U then A else terminal.{u, v} C)
have rw : IsTerminal.{u, v} (terminal.{u, v} C)
Tactic: rw [if_neg 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 u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
F : Presheaf C X
U V : Opens (↑X : Type v)
i : U ⟶ V
x : (↑X : Type v)
hx : x ∈ U
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
s : CC (F.obj (op V))
⊢ Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map i.op) : (a : CC (F.obj (op V))) → CC (F.obj (op U))) s :
          CC (F.obj (op U))) :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x ⋯) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
      CC (F.stalk x))
have rw : Eq (α := CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map i.op ≫ F.germ U x hx) : (a : CC (F.obj (op V))) → CC (F.stalk x))
      s :
    CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x sorry) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
    CC (F.stalk x))
Tactic: rw [← ConcreteCategory.comp_apply, germ_res]
-- 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 u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
F : Presheaf C X
U V : Opens (↑X : Type v)
i : U ⟶ V
x : (↑X : Type v)
hx : x ∈ U
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
s : CC (F.obj (op V))
rw :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map i.op ≫ F.germ U x hx) :
          (a : CC (F.obj (op V))) → CC (F.stalk x))
        s :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x ⋯) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
      CC (F.stalk x))
⊢ Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map i.op) : (a : CC (F.obj (op V))) → CC (F.obj (op U))) s :
          CC (F.obj (op U))) :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x ⋯) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
      CC (F.stalk x))
have rw₁ : Eq (α := CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x sorry) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
    CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x sorry) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
    CC (F.stalk x))
Tactic: rw [← ConcreteCategory.comp_apply, germ_res]
-- 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 u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
F : Presheaf C X
U V : Opens (↑X : Type v)
i : op V ⟶ op U
x : (↑X : Type v)
hx : x ∈ U
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
s : CC (F.obj (op V))
⊢ Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map i) : (a : CC (F.obj (op V))) → CC (F.obj (op U))) s :
          CC (F.obj (op U))) :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x ⋯) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
      CC (F.stalk x))
have rw : Eq (α := CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map i ≫ F.germ U x hx) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
    CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x sorry) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
    CC (F.stalk x))
Tactic: rw [← ConcreteCategory.comp_apply, germ_res']
-- 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 u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
F : Presheaf C X
U V : Opens (↑X : Type v)
i : op V ⟶ op U
x : (↑X : Type v)
hx : x ∈ U
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
s : CC (F.obj (op V))
rw :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map i ≫ F.germ U x hx) : (a : CC (F.obj (op V))) → CC (F.stalk x))
        s :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x ⋯) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
      CC (F.stalk x))
⊢ Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map i) : (a : CC (F.obj (op V))) → CC (F.obj (op U))) s :
          CC (F.obj (op U))) :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x ⋯) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
      CC (F.stalk x))
have rw₁ : Eq (α := CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x sorry) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
    CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x sorry) : (a : CC (F.obj (op V))) → CC (F.stalk x)) s :
    CC (F.stalk x))
Tactic: rw [← ConcreteCategory.comp_apply, germ_res']
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
F : Presheaf C X
x : (↑X : Type v)
Y : C
f₁ f₂ : F.stalk x ⟶ Y
ih : ∀ (U : Opens (↑X : Type v)) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂
U : OpenNhds x
⊢ Eq (α :=
    (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F).obj (op U) ⟶ Y)
    (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
        (op U) ≫
      f₁)
    (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
        (op U) ≫
      f₂)
have op : ∀ (U : Opens (↑X : Type v)) (hxU : x ∈ U),
  Eq (α :=
    (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F).obj
        (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U hxU)) ⟶
      Y)
    (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
        (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U hxU)) ≫
      f₁)
    (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
        (op (Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U hxU)) ≫
      f₂)
Tactic: obtain ⟨U, hxU⟩ := U
Cleared hypotheses: U
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
F : Presheaf C X
x : (↑X : Type v)
Y : C
f₁ f₂ : F.stalk x ⟶ Y
ih : ∀ (U : Opens (↑X : Type v)) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂
U : (OpenNhds x)ᵒᵖ
⊢ colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F) U ≫ f₁ =
    colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F) U ≫ f₂
have op : ∀ (U : OpenNhds x),
  Eq (α :=
    (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F).obj (op U) ⟶ Y)
    (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
        (op U) ≫
      f₁)
    (colimit.ι (obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
        (op U) ≫
      f₂)
Tactic: induction U with | op U => obtain ⟨U, hxU⟩ := U; exact ih U hxU
Cleared hypotheses: U
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
F G : Presheaf C X
U : Opens (↑X : Type v)
x : (↑X : Type v)
hx : x ∈ U
f : F ⟶ G
s : CC (F.obj (op 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)) → CC ((stalkFunctor C x).obj G))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (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) (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 (op U))) → CC (G.obj (op U))) s :
          CC (G.obj (op U))) :
      CC (G.stalk x))
have rw : 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 hx) : (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 (F.stalk x)) → CC (G.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x)) s :
        CC (F.stalk x)) :
    CC (G.stalk x))
Tactic: rw [← ConcreteCategory.comp_apply, ← stalkFunctor_map_germ, ConcreteCategory.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C X
x : (↑X : Type v)
⊢ (obj (pushforward C f) F).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x) ⟶
    F.stalk x
have refine : (obj (pushforward C f) F).stalk
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
        (a : (↑X : Type v)) → (↑Y : Type v))
      x) ⟶
  colimit
    ((OpenNhds.map f x).op ⋙
      obj (obj (whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (OpenNhds.inclusion x).op) F)
Tactic: refine ?_ ≫ colimit.pre _ (OpenNhds.map f x).op
-- 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
ℱ : Presheaf C X
x : (↑X : Type v)
⊢ Eq (α :=
    (obj (pushforward C (𝟙 X)) ℱ).stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (𝟙 X) :
            (a : (↑X : Type v)) → (↑X : Type v))
          x) ⟶
      ℱ.stalk x)
    (stalkPushforward C (𝟙 X) ℱ x) (map (stalkFunctor C x) (Pushforward.id ℱ).hom)
have ih : ∀ (U : Opens (↑X : Type v))
  (hxU :
    Membership.mem (α := (↑X : Type v)) U
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (𝟙 X) :
            (a : (↑X : Type v)) → (↑X : Type v))
          x :
        (↑X : Type v))),
  Eq (α := (obj (pushforward C (𝟙 X)) ℱ).obj (op U) ⟶ ℱ.stalk x)
    ((obj (pushforward C (𝟙 X)) ℱ).germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (𝟙 X) :
            (a : (↑X : Type v)) → (↑X : Type v))
          x)
        hxU ≫
      stalkPushforward C (𝟙 X) ℱ x)
    ((obj (pushforward C (𝟙 X)) ℱ).germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (𝟙 X) :
            (a : (↑X : Type v)) → (↑X : Type v))
          x)
        hxU ≫
      map (stalkFunctor C x) (Pushforward.id ℱ).hom)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X : Type v)
⊢ Eq (α :=
    (obj (pushforward C (f ≫ g)) ℱ).stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              (f ≫ g) :
            (a : (↑X : Type v)) → (↑Z : Type v))
          x) ⟶
      ℱ.stalk x)
    (stalkPushforward C (f ≫ g) ℱ x)
    (stalkPushforward C g (obj (pushforward C f) ℱ)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
            (a : (↑X : Type v)) → (↑Y : Type v))
          x) ≫
      stalkPushforward C f ℱ x)
have ih : ∀ (U : Opens (↑Z : Type v))
  (hxU :
    Membership.mem (α := (↑Z : Type v)) U
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (f ≫ g) :
            (a : (↑X : Type v)) → (↑Z : Type v))
          x :
        (↑Z : Type v))),
  Eq (α := (obj (pushforward C (f ≫ g)) ℱ).obj (op U) ⟶ ℱ.stalk x)
    ((obj (pushforward C (f ≫ g)) ℱ).germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              (f ≫ g) :
            (a : (↑X : Type v)) → (↑Z : Type v))
          x)
        hxU ≫
      stalkPushforward C (f ≫ g) ℱ x)
    ((obj (pushforward C (f ≫ g)) ℱ).germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              (f ≫ g) :
            (a : (↑X : Type v)) → (↑Z : Type v))
          x)
        hxU ≫
      stalkPushforward C g (obj (pushforward C f) ℱ)
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
              (a : (↑X : Type v)) → (↑Y : Type v))
            x) ≫
        stalkPushforward C f ℱ x)
Tactic: ext
-- 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 Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
F : Presheaf C X
x : (↑X : Type v)
⊢ IsIso (X :=
    (obj (pushforward C f) F).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x))
    (stalkPushforward C f F x)
have this : (OpenNhds.map f x).Initial
Tactic: haveI := Functor.initial_of_adjunction (hf.adjunctionNhds x)
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
F : Presheaf C X
x : (↑X : Type v)
this : (OpenNhds.map f x).Initial
⊢ IsIso (X :=
    (obj (pushforward C f) F).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x))
    (stalkPushforward C f F x)
have h : (obj (pushforward C f) F).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x) =
    colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F) →
  F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F) →
    Eq (α :=
      (obj (pushforward C f) F).stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
              (a : (↑X : Type v)) → (↑Y : Type v))
            x) ⟶
        F.stalk x)
      (stalkPushforward C f F x) (Iso.hom (Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)))
Tactic: convert!
    (Functor.Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).isIso_hom
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
F : Presheaf C X
x : (↑X : Type v)
this : (OpenNhds.map f x).Initial
e_3 :
  (obj (pushforward C f) F).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
          (a : (↑X : Type v)) → (↑Y : Type v))
        x) =
    colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F)
e_4 : F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F)
⊢ Eq (α :=
    (obj (pushforward C f) F).stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
            (a : (↑X : Type v)) → (↑Y : Type v))
          x) ⟶
      F.stalk x)
    (stalkPushforward C f F x) (Iso.hom (Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)))
have h : ∀ (U : Opens (↑Y : Type v))
  (hU :
    Membership.mem (α := (↑Y : Type v)) U
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
            (a : (↑X : Type v)) → (↑Y : Type v))
          x :
        (↑Y : Type v))),
  Eq (α := (obj (pushforward C f) F).obj (op U) ⟶ F.stalk x) (F.germ ((Opens.map f).obj U) x hU)
    (CategoryStruct.comp (Y :=
      (obj (pushforward C f) F).stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
            (a : (↑X : Type v)) → (↑Y : Type v))
          x))
      ((obj (pushforward C f) F).germ U
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f :
            (a : (↑X : Type v)) → (↑Y : Type v))
          x)
        hU)
      (Iso.hom (Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F))))
Tactic: refine stalk_hom_ext _ fun U hU ↦ (stalkPushforward_germ _ f F _ x hU).trans ?_