mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ : LocallyRingedSpace
U : TopCat
X : LocallyRingedSpace
f : U ⟶ X.toTopCat
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ ∀ (x : ↑↑(X.restrict h).toPresheafedSpace), IsLocalRing ↑((X.restrict h).presheaf.stalk x)

Tactic:
intro x

Goal state after:
X✝ : LocallyRingedSpace
U : TopCat
X : LocallyRingedSpace
f : U ⟶ X.toTopCat
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑↑(X.restrict h).toPresheafedSpace
⊢ IsLocalRing ↑((X.restrict h).presheaf.stalk x)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
⊢ U ≤ X.basicOpen f

Tactic:
intro x

Goal state after:
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
x : ↑↑X.toPresheafedSpace
⊢ x ∈ U → x ∈ X.basicOpen f
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : Type ?u.10
inst✝ : TopologicalSpace T
U : Opens ↑X
f : ↥U → T
w : ∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (X.continuousPrelocal T).pred fun x ↦ f (i x)
⊢ ∀ (x : ↥U), ContinuousAt f x

Tactic:
intro x

Goal state after:
X : TopCat
T✝ : ↑X → Type u_1
T : Type ?u.10
inst✝ : TopologicalSpace T
U : Opens ↑X
f : ↥U → T
w : ∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (X.continuousPrelocal T).pred fun x ↦ f (i x)
x : ↥U
⊢ ContinuousAt f x
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)

Tactic:
intro x

Goal state after:
case refine_1
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
x : ↥U✝
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_2
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, Q.pred fun x ↦ f (i x)

Tactic:
intro x

Goal state after:
case refine_2
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
x : ↥U✝
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, Q.pred fun x ↦ f (i x)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_2
P : PrelocalPredicate T
op : {x : ↑X} → T x → T x
hop : ∀ {U : Opens ↑X} {a : (x : ↥U) → T ↑x}, P.pred a → ∀ (p : ↥U), ∃ W i, ↑p ∈ W ∧ P.pred fun x ↦ op (a (i x))
U : Opens ↑X
a : (x : ↥U) → T ↑x
ha : P.sheafify.pred a
⊢ P.sheafify.pred fun x ↦ op (a x)

Tactic:
intro x

Goal state after:
X : TopCat
T : ↑X → Type u_2
P : PrelocalPredicate T
op : {x : ↑X} → T x → T x
hop : ∀ {U : Opens ↑X} {a : (x : ↥U) → T ↑x}, P.pred a → ∀ (p : ↥U), ∃ W i, ↑p ∈ W ∧ P.pred fun x ↦ op (a (i x))
U : Opens ↑X
a : (x : ↥U) → T ↑x
ha : P.sheafify.pred a
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ (fun x ↦ op (a x)) (i x)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T₁ : ↑X → Type u_2
T₂ : ↑X → Type u_3
T₃ : ↑X → Type u_4
P₁ : PrelocalPredicate T₁
P₂ : PrelocalPredicate T₂
P₃ : PrelocalPredicate T₃
op : {x : ↑X} → T₁ x → T₂ x → T₃ x
hop :
  ∀ {U V : Opens ↑X} {a : (x : ↥U) → T₁ ↑x} {b : (x : ↥V) → T₂ ↑x},
    P₁.pred a → P₂.pred b → ∀ (p : ↥(U ⊓ V)), ∃ W ia ib, ↑p ∈ W ∧ P₃.pred fun x ↦ op (a (ia x)) (b (ib x))
U : Opens ↑X
a : (x : ↥U) → T₁ ↑x
b : (x : ↥U) → T₂ ↑x
ha : P₁.sheafify.pred a
hb : P₂.sheafify.pred b
⊢ P₃.sheafify.pred fun x ↦ op (a x) (b x)

Tactic:
intro x

Goal state after:
X : TopCat
T₁ : ↑X → Type u_2
T₂ : ↑X → Type u_3
T₃ : ↑X → Type u_4
P₁ : PrelocalPredicate T₁
P₂ : PrelocalPredicate T₂
P₃ : PrelocalPredicate T₃
op : {x : ↑X} → T₁ x → T₂ x → T₃ x
hop :
  ∀ {U V : Opens ↑X} {a : (x : ↥U) → T₁ ↑x} {b : (x : ↥V) → T₂ ↑x},
    P₁.pred a → P₂.pred b → ∀ (p : ↥(U ⊓ V)), ∃ W ia ib, ↑p ∈ W ∧ P₃.pred fun x ↦ op (a (ia x)) (b (ib x))
U : Opens ↑X
a : (x : ↥U) → T₁ ↑x
b : (x : ↥U) → T₂ ↑x
ha : P₁.sheafify.pred a
hb : P₂.sheafify.pred b
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P₃.pred fun x ↦ (fun x ↦ op (a x) (b x)) (i x)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
e : U = V
⊢ app f U = Y.presheaf.map (eqToHom ⋯).op ≫ app f V ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
by
  aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
⊢ X.basicOpen (f + g) ≤ X.basicOpen f ⊔ X.basicOpen g

Tactic:
intro x

Goal state after:
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↥X
⊢ x ∈ X.basicOpen (f + g) → x ∈ X.basicOpen f ⊔ X.basicOpen g
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ Codisjoint (X.zeroLocus s) ↑U

Tactic:
have (x : X) : ∀ f ∈ s, x ∈ X.basicOpen f → x ∈ U := fun _ _ h ↦ X.basicOpen_le _ h

Goal state after:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
this : ∀ (x : ↥X), ∀ f ∈ s, x ∈ X.basicOpen f → x ∈ U
⊢ Codisjoint (X.zeroLocus s) ↑U
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : (Opens ↑↑Y)ᵒᵖ
⊢ IsIso (f.c.app U)

Tactic:
have : U = op (opensFunctor f |>.obj ((Opens.map f.base).obj (unop U))) := by
      induction U with | op U => ?_
      cases U
      dsimp only [Functor.op, Opens.map]
      congr
      exact (Set.image_preimage_eq _ ((TopCat.epi_iff_surjective _).mp h')).symm

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : (Opens ↑↑Y)ᵒᵖ
this : U = op ((opensFunctor f).obj ((Opens.map f.base).obj (unop U)))
⊢ IsIso (f.c.app U)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₁
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀ x ∈ p.asIdeal.primeCompl,
    IsUnit
      ((algebraMap ↑R
          ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                  (structureSheaf ↑S).obj).stalk
              p))
        x)

Tactic:
intro x

Goal state after:
case h₁
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑R
⊢ x ∈ p.asIdeal.primeCompl →
    IsUnit
      ((algebraMap ↑R
          ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                  (structureSheaf ↑S).obj).stalk
              p))
        x)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀ (x : ↑S), (toPushforwardStalkAlgHom R S p) x = 0 → ∃ m, m • x = 0

Tactic:
intro x

Goal state after:
case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
⊢ (toPushforwardStalkAlgHom R S p) x = 0 → ∃ m, m • x = 0
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x y : ↥X
h : x = y
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f y = stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯

Tactic:
rw [stalkSpecializes_stalkMap]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : LocallyRingedSpace
h : ∀ (x : ↑X.toTopCat), ∃ R f, x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ IsOpenImmersion f
⊢ ∀ (x : ↑X.toTopCat), ∃ U R, Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))

Tactic:
intro x

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : LocallyRingedSpace
h : ∀ (x : ↑X.toTopCat), ∃ R f, x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ IsOpenImmersion f
x : ↑X.toTopCat
⊢ ∃ U R, Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hf : ∀ (x : S), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (f i))
hg : ∀ (i : ι) (x : X i), ∃ i_1, x ∈ Set.range ⇑(ConcreteCategory.hom (g i i_1))
⊢ ∀ (x : S), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (g i.fst i.snd ≫ f i.fst))

Tactic:
intro x

Goal state after:
ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hf : ∀ (x : S), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (f i))
hg : ∀ (i : ι) (x : X i), ∃ i_1, x ∈ Set.range ⇑(ConcreteCategory.hom (g i i_1))
x : S
⊢ ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (g i.fst i.snd ≫ f i.fst))
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
i : X → E.I₀
y : (x : X) → (fun X ↦ X) (E.X (i x))
hy : ∀ (x : X), (ConcreteCategory.hom (E.f (i x))) (y x) = x
⊢ ∀ (x : (fun X ↦ X) X), ∃ i_1, x ∈ Set.range ⇑(ConcreteCategory.hom ((E.restrictIndex i).f i_1))

Tactic:
intro x

Goal state after:
X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
i : X → E.I₀
y : (x : X) → (fun X ↦ X) (E.X (i x))
hy : ∀ (x : X), (ConcreteCategory.hom (E.f (i x))) (y x) = x
x : X
⊢ ∃ i_1, x ∈ Set.range ⇑(ConcreteCategory.hom ((E.restrictIndex i).f i_1))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : CommRingCat
f : ↑R
hf✝ :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (LocallyRingedSpace.Hom.toShHom
              (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f)))))).hom.base)
⊢ ∀ (x : ↥(Spec (CommRingCat.of (Localization.Away f)))),
    IsIso
      (PresheafedSpace.Hom.stalkMap
        (LocallyRingedSpace.Hom.toShHom
            (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f)))))).hom
        x)

Tactic:
intro x

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
R : CommRingCat
f : ↑R
hf✝ :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (LocallyRingedSpace.Hom.toShHom
              (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f)))))).hom.base)
x : ↥(Spec (CommRingCat.of (Localization.Away f)))
⊢ IsIso
    (PresheafedSpace.Hom.stalkMap
      (LocallyRingedSpace.Hom.toShHom
          (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f)))))).hom
      x)
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.map F (Presieve.ofArrows X f) ∈ Types.jointlySurjectivePrecoverage.coverings (F.obj S)
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.map F (Presieve.ofArrows P p₁) ∈ Types.jointlySurjectivePrecoverage.coverings (F.obj Y)

Tactic:
Presieve.map_ofArrows,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf :
  (Presieve.ofArrows (fun i ↦ F.obj (X i)) fun i ↦ F.map (f i)) ∈ Types.jointlySurjectivePrecoverage.coverings (F.obj S)
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ (Presieve.ofArrows (fun i ↦ F.obj (P i)) fun i ↦ F.map (p₁ i)) ∈
    Types.jointlySurjectivePrecoverage.coverings (F.obj Y)
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ ∀ (x : (fun X ↦ X) (F.obj Y)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (p₁ i)))

Tactic:
intro x

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : F.obj Y
⊢ ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (p₁ i)))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈
      Set.range
        ⇑(ConcreteCategory.hom
            ((Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))).base ≫
              { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }.base)) ∧
    Set.range
        ⇑(ConcreteCategory.hom
            ((Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))).base ≫
              { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }.base)) ⊆
      ↑U

Tactic:
TopCat.coe_comp,

Goal state after:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈
      Set.range
        (⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } ∘
          ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))))) ∧
    Set.range
        (⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } ∘
          ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))))) ⊆
      ↑U
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ ∀ (x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat),
    ∃ R f_1, x ∈ Set.range ⇑(ConcreteCategory.hom f_1.base) ∧ LocallyRingedSpace.IsOpenImmersion f_1

Tactic:
intro x

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat
⊢ ∃ R f_1, x ∈ Set.range ⇑(ConcreteCategory.hom f_1.base) ∧ LocallyRingedSpace.IsOpenImmersion f_1
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range
      ⇑(ConcreteCategory.hom
          ((PreservesPullback.iso Scheme.forgetToTop f g).hom ≫
            pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))) =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

Tactic:
TopCat.coe_comp,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range
      (⇑(ConcreteCategory.hom (pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))) ∘
        ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop f g).hom)) =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this : IsIso (pullback.snd f.base g.base)
⊢ IsIso
    ((limit.isoLimitCone { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }).hom ≫
        { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }.cone.π.app
          WalkingCospan.right).base

Tactic:
change IsIso (_ ≫ pullback.snd _ _)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this : IsIso (pullback.snd f.base g.base)
⊢ IsIso
    ((limit.isoLimitCone { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }).hom.base ≫
      pullback.snd f.base g.base)
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
inst✝ : JointlySurjective K
X : Scheme
𝒰 : Cover K X
⊢ ∀ (x : ↥X), x ∈ ⋃ i, Set.range ⇑(𝒰.f i)

Tactic:
intro x

Goal state after:
K : Precoverage Scheme
inst✝ : JointlySurjective K
X : Scheme
𝒰 : Cover K X
x : ↥X
⊢ x ∈ ⋃ i, Set.range ⇑(𝒰.f i)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range
      ⇑(ConcreteCategory.hom
          ((PreservesPullback.iso Scheme.forgetToTop g f).hom ≫
            pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

Tactic:
TopCat.coe_comp,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range
      (⇑(ConcreteCategory.hom (pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) ∘
        ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop g f).hom)) =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(ConcreteCategory.hom ((pullback.snd f g).base ≫ g.base)) = Set.range ⇑f ∩ Set.range ⇑g

Tactic:
TopCat.coe_comp,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range (⇑g ∘ ⇑(pullback.snd f g)) = Set.range ⇑f ∩ Set.range ⇑g
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(ConcreteCategory.hom ((pullback.fst g f).base ≫ g.base)) = Set.range ⇑g ∩ Set.range ⇑f

Tactic:
TopCat.coe_comp,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range (⇑g ∘ ⇑(pullback.fst g f)) = Set.range ⇑g ∩ Set.range ⇑f
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X✝ Y Z : Scheme
𝒰✝ : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
X : Scheme
𝒰 : X.OpenCover
H : CompactSpace ↥X
this : ∃ t, ⋃ x ∈ t, Set.range ⇑(𝒰.f (Cover.idx 𝒰 x)) = ⊤
t : Finset ↥X := this.choose
⊢ ∀ (x : ↥X), ∃ y, x ∈ Set.range ⇑(𝒰.f (Cover.idx 𝒰 ↑y))

Tactic:
intro x

Goal state after:
X✝ Y Z : Scheme
𝒰✝ : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
X : Scheme
𝒰 : X.OpenCover
H : CompactSpace ↥X
this : ∃ t, ⋃ x ∈ t, Set.range ⇑(𝒰.f (Cover.idx 𝒰 x)) = ⊤
t : Finset ↥X := this.choose
x : ↥X
⊢ ∃ y, x ∈ Set.range ⇑(𝒰.f (Cover.idx 𝒰 ↑y))
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case hcover
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) g
⊢ U ≤ ⨆ i, Hom.opensRange (𝒰.f (Cover.idx 𝒰 i)) ⊓ U

Tactic:
intro x

Goal state after:
case hcover
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) g
x : ↥X
⊢ x ∈ U → x ∈ ⨆ i, Hom.opensRange (𝒰.f (Cover.idx 𝒰 i)) ⊓ U
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case prop
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ∀ (x : ↑↑(Y.restrict ⋯).toPresheafedSpace),
    IsLocalHom
      (CommRingCat.Hom.hom
        (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x))

Tactic:
intro x

Goal state after:
case prop
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
x : ↑↑(Y.restrict ⋯).toPresheafedSpace
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x))
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) g
⊢ ∀ (i : ↥X),
    (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) f =
      (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) g

Tactic:
intro x

Goal state after:
case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) g
x : ↥X
⊢ (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) f = (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) g
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
⊢ ∀ (x : ↑↑s.pt.toPresheafedSpace),
    IsLocalHom
      (CommRingCat.Hom.hom
        (PresheafedSpace.Hom.stalkMap
          (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
            (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))
          x))

Tactic:
intro x

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
x : ↑↑s.pt.toPresheafedSpace
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))
        x))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso (pullback.snd f g)

Tactic:
by
  apply +allowSynthFailures Functor.ReflectsIsomorphisms.reflects
    (F := LocallyRingedSpace.forgetToSheafedSpace)
  apply +allowSynthFailures Functor.ReflectsIsomorphisms.reflects
    (F := SheafedSpace.forgetToPresheafedSpace)
  erw [← PreservesPullback.iso_hom_snd
      (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g]
  -- Porting note: was `inferInstance`
  exact IsIso.comp_isIso' inferInstance <|
    PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset _ _ H'

Goal state after: