-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem of_stalk_iso {X Y : SheafedSpace C} (f : X ⟶ Y) (hf : IsOpenEmbedding f.base)
    [H : ∀ x : X.1, IsIso (f.stalkMap x)] : SheafedSpace.IsOpenImmersion f :=
  { base_open := hf
    c_iso := fun U => by
      apply (config := {allowSynthFailures := true})
        TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso
          (show Y.sheaf ⟶ (TopCat.Sheaf.pushforward _ f.base).obj X.sheaf from ⟨f.c⟩)
      rintro ⟨_, y, hy, rfl⟩
      specialize H y
      delta PresheafedSpace.Hom.stalkMap at H
      haveI H' := TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing C
        hf.toIsInducing X.presheaf y
      have := IsIso.comp_isIso' H (@IsIso.inv_isIso _ _ _ _ _ H')
      rwa [Category.assoc, IsIso.hom_inv_id, Category.comp_id] at this }

Proof state:
case inst
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)
H : ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.Hom.stalkMap f x)
U : Opens ↑↑X.toPresheafedSpace
⊢ ∀ (x : ↥(⋯.functor.obj U)),
    IsIso
      ((TopCat.Presheaf.stalkFunctor C ↑x).map
        (let_fun this := { val := f.c };
          this).val)

Tactic:
rintro ⟨_, y, hy, rfl⟩

Result:
case inst.mk.intro.intro
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)
H : ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.Hom.stalkMap f x)
U : Opens ↑↑X.toPresheafedSpace
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑U
⊢ IsIso
    ((TopCat.Presheaf.stalkFunctor C ↑⟨(ConcreteCategory.hom f.base) y, ⋯⟩).map
      (let_fun this := { val := f.c };
        this).val)

Proof state:
case inst.mk.intro.intro
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)
U : Opens ↑↑X.toPresheafedSpace
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑U
H :
  IsIso
    ((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.base) y)).map f.c ≫
      TopCat.Presheaf.stalkPushforward C f.base X.presheaf y)
⊢ IsIso
    ((TopCat.Presheaf.stalkFunctor C ↑⟨(ConcreteCategory.hom f.base) y, ⋯⟩).map
      (let_fun this := { val := f.c };
        this).val)

Tactic:
haveI H' := TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing C
  hf.toIsInducing X.presheaf y

Result:
case inst.mk.intro.intro
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)
U : Opens ↑↑X.toPresheafedSpace
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑U
H :
  IsIso
    ((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.base) y)).map f.c ≫
      TopCat.Presheaf.stalkPushforward C f.base X.presheaf y)
H' : IsIso (TopCat.Presheaf.stalkPushforward C f.base X.presheaf y)
⊢ IsIso
    ((TopCat.Presheaf.stalkFunctor C ↑⟨(ConcreteCategory.hom f.base) y, ⋯⟩).map
      (let_fun this := { val := f.c };
        this).val)

Proof state:
case inst.mk.intro.intro
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)
H : ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.Hom.stalkMap f x)
U : Opens ↑↑X.toPresheafedSpace
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑U
⊢ IsIso
    ((TopCat.Presheaf.stalkFunctor C ↑⟨(ConcreteCategory.hom f.base) y, ⋯⟩).map
      (let_fun this := { val := f.c };
        this).val)

Tactic:
specialize H y

Result:
case inst.mk.intro.intro
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)
U : Opens ↑↑X.toPresheafedSpace
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑U
H : IsIso (PresheafedSpace.Hom.stalkMap f y)
⊢ IsIso
    ((TopCat.Presheaf.stalkFunctor C ↑⟨(ConcreteCategory.hom f.base) y, ⋯⟩).map
      (let_fun this := { val := f.c };
        this).val)

Proof state:
case inst.mk.intro.intro
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)
U : Opens ↑↑X.toPresheafedSpace
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑U
H :
  IsIso
    ((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.base) y)).map f.c ≫
      TopCat.Presheaf.stalkPushforward C f.base X.presheaf y)
H' : IsIso (TopCat.Presheaf.stalkPushforward C f.base X.presheaf y)
⊢ IsIso
    ((TopCat.Presheaf.stalkFunctor C ↑⟨(ConcreteCategory.hom f.base) y, ⋯⟩).map
      (let_fun this := { val := f.c };
        this).val)

Tactic:
have := IsIso.comp_isIso' H (@IsIso.inv_isIso _ _ _ _ _ H')

Result:
case inst.mk.intro.intro
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)
U : Opens ↑↑X.toPresheafedSpace
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑U
H :
  IsIso
    ((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.base) y)).map f.c ≫
      TopCat.Presheaf.stalkPushforward C f.base X.presheaf y)
H' : IsIso (TopCat.Presheaf.stalkPushforward C f.base X.presheaf y)
this :
  IsIso
    (((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.base) y)).map f.c ≫
        TopCat.Presheaf.stalkPushforward C f.base X.presheaf y) ≫
      inv (TopCat.Presheaf.stalkPushforward C f.base X.presheaf y))
⊢ IsIso
    ((TopCat.Presheaf.stalkFunctor C ↑⟨(ConcreteCategory.hom f.base) y, ⋯⟩).map
      (let_fun this := { val := f.c };
        this).val)