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

Goal state before:
pp: case refine_1
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
j : Jᵒᵖ
⊢ ((Functor.const Jᵒᵖ).obj (s.pt.presheaf.obj U)).obj j ⟶
    ((pushforwardDiagramToColimit F).leftOp ⋙
          (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
            ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).op.obj U)).obj
      j

Tactic:
refine (s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ?_)

Goal state after:
case refine_1
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
j : Jᵒᵖ
⊢ (Opens.map (s.ι.app (unop j)).base).op.obj U =
    (Opens.map (colimit.ι (F ⋙ forget C) (unop j))).op.obj
      ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).op.obj U)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case succ
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : 0 < n + Nat.succ 0 → X.basicOpen (f ^ (n + Nat.succ 0)) = X.basicOpen f
h : 0 < n + 1 + Nat.succ 0
⊢ X.basicOpen (f ^ (n + 1 + Nat.succ 0)) = X.basicOpen f

Tactic:
pow_add

Goal state after:
case succ
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : 0 < n + Nat.succ 0 → X.basicOpen (f ^ (n + Nat.succ 0)) = X.basicOpen f
h : 0 < n + 1 + Nat.succ 0
⊢ X.basicOpen (f ^ (n + 1) * f ^ Nat.succ 0) = X.basicOpen f
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:
by
  intro x
  rcases ha x with ⟨Va, ma, ia, ha⟩
  rcases hb x with ⟨Vb, mb, ib, hb⟩
  rcases hop ha hb ⟨x, ma, mb⟩ with ⟨W, sa, sb, hx, hw⟩
  exact ⟨W, hx, sa ≫ ia, hw⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
e : f = g
U : Y.Opens
⊢ f ⁻¹ᵁ U = g ⁻¹ᵁ U

Tactic:
subst e

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ⁻¹ᵁ U = f ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.Scheme

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

Tactic:
subst e

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ app f U = app f U ≫ X.presheaf.map (eqToHom ⋯).op
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X = Y
U : Y.Opens
⊢ Γ(Y, U) = Γ(X, eqToHom e ⁻¹ᵁ U)

Tactic:
subst e

Goal state after:
X : Scheme
U : X.Opens
⊢ Γ(X, U) = Γ(X, eqToHom ⋯ ⁻¹ᵁ U)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X = Y
U : Y.Opens
⊢ app (eqToHom e) U = eqToHom ⋯

Tactic:
subst e

Goal state after:
X : Scheme
U : X.Opens
⊢ app (eqToHom ⋯) U = eqToHom ⋯
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R S : CommRingCat
e : R = S
⊢ map (eqToHom e) = eqToHom ⋯

Tactic:
subst e

Goal state after:
R : CommRingCat
⊢ map (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑R
x : ↥(Spec R)
⊢ IsUnit
      ((ConcreteCategory.hom ((Spec R).presheaf.germ ⊤ x _root_.trivial))
        ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f)) ↔
    x ∈ PrimeSpectrum.basicOpen f

Tactic:
suffices IsUnit (algebraMap _ ((structurePresheafInCommRingCat ↑R).stalk x) f) ↔
    f ∉ PrimeSpectrum.asIdeal x by exact this

Goal state after:
R : CommRingCat
f : ↑R
x : ↥(Spec R)
⊢ IsUnit ((algebraMap ↑R ↑((structurePresheafInCommRingCat ↑R).stalk x)) f) ↔ f ∉ x.asIdeal
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsOpenImmersion g
⊢ g ''ᵁ ⊤ = opensRange g

Tactic:
image_top_eq_opensRange

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsOpenImmersion g
⊢ opensRange g = opensRange g
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U V : X.Opens
hUV : (fun x ↦ f ''ᵁ x) U = (fun x ↦ f ''ᵁ x) V
⊢ U = V

Tactic:
simpa using congrArg (f ⁻¹ᵁ ·) hUV

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ IsLocalizedModule p.asIdeal.primeCompl (toPushforwardStalkAlgHom R S p).toLinearMap

Tactic:
by
  apply IsLocalizedModule.mkOfAlgebra
  · intro x hx; rw [algebraMap_pushforward_stalk, toPushforwardStalk_comp]
    change IsUnit ((TopCat.Presheaf.stalkFunctor CommRingCat p).map
      (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap ↑R ↑S))).hom.c _)
    exact (IsLocalization.map_units ((structureSheaf R).presheaf.stalk p) ⟨x, hx⟩).map _
  · apply isLocalizedModule_toPushforwardStalkAlgHom_aux
  · intro x hx
    rw [toPushforwardStalkAlgHom_apply,
      ← (toPushforwardStalk (CommRingCat.ofHom (algebraMap ↑R ↑S)) p).hom.map_zero,
      toPushforwardStalk] at hx
    rw [CommRingCat.comp_apply, map_zero] at hx
    obtain ⟨U, hpU, i₁, i₂, e⟩ := TopCat.Presheaf.germ_eq (C := CommRingCat) _ _ _ _ _ _ hx
    obtain ⟨_, ⟨r, rfl⟩, hpr, hrU⟩ :=
      PrimeSpectrum.isTopologicalBasis_basic_opens.exists_subset_of_mem_open (show p ∈ U.1 from hpU)
        U.2
    apply_fun (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).map
        (homOfLE hrU).op at e
    have : algebraMap S ((structureSheaf S).presheaf.obj _) x = 0 := e
    have :=
      (@IsLocalization.mk'_one _ _ _ _ _ _
            (StructureSheaf.IsLocalization.to_basicOpen S <| algebraMap R S r) x).trans
        this
    obtain ⟨⟨_, n, rfl⟩, e⟩ := (IsLocalization.mk'_eq_zero_iff _ _).mp this
    refine ⟨⟨r, hpr⟩ ^ n, ?_⟩
    rw [Submonoid.smul_def, Algebra.smul_def, SubmonoidClass.coe_pow, map_pow]
    exact e

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ appIso (𝟙 X) U = Functor.mapIso X.presheaf (eqToIso ⋯).op

Tactic:
ext; simp [appIso_hom]

Goal state after:
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 : F.obj Y
⊢ ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (p₁ i)))

Tactic:
obtain ⟨i, hi⟩ := hf (F.map g 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 : ι
hi : (ConcreteCategory.hom (F.map g)) x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
⊢ ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (p₁ i)))
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
⊢ Scheme

Tactic:
apply LocallyRingedSpace.IsOpenImmersion.scheme (toLocallyRingedSpace _ f)

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 ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion g
inst✝ : IsOpenImmersion (f ≫ g)
x : ↥X
⊢ IsIso (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)

Tactic:
rw [← Scheme.Hom.stalkMap_comp]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion g
inst✝ : IsOpenImmersion (f ≫ g)
x : ↥X
⊢ IsIso (Scheme.Hom.stalkMap (f ≫ g) x)
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover P X
⊢ { I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.presieve₀ ∈ (precoverage P).coverings X

Tactic:
by
    rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, 𝒰.map_prop⟩
    obtain ⟨y, hy⟩ := 𝒰.covers x
    use 𝒰.idx x, y

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i : Discrete ι
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (colimit.ι (F ⋙ forget C) i ≫ (preservesColimitIso (forget C) F).inv))

Tactic:
have : _ = _ ≫ colimit.ι (Discrete.functor ((F ⋙ SheafedSpace.forget C).obj ∘ Discrete.mk)) i :=
    HasColimit.isoOfNatIso_ι_hom Discrete.natIsoFunctor i

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i : Discrete ι
this :
  colimit.ι (F ⋙ forget C) i ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom =
    Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (colimit.ι (F ⋙ forget C) i ≫ (preservesColimitIso (forget C) F).inv))
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = 0
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) 0

Tactic:
rw [map_zero]; exact h i

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h_nhds
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
⊢ ∃ v ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}, a ∈ v ∧ v ⊆ U

Tactic:
have hxU' : x ∈ U' := by rw [← e] at haU; exact haU

Goal state after:
case h_nhds
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
⊢ ∃ v ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}, a ∈ v ∧ v ⊆ U
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ (Hom.appIso (X.ofRestrict ⋯) ⊤).inv = X.presheaf.map (𝟙 (op (⋯.functor.obj ⊤)))

Tactic:
exact (PresheafedSpace.IsOpenImmersion.ofRestrict_invApp _ _ _).trans
    (CategoryTheory.Functor.map_id _ _).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case h.h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : (toBasicOpenₗ R M f) (LocalizedModule.mk a b) = (toBasicOpenₗ R M f) (LocalizedModule.mk c d)
⊢ LocalizedModule.mk a b = LocalizedModule.mk c d

Tactic:
suffices f ∈ ((⊥ : Submodule R M).colon {d • a - b • c}).radical by
    rw [LocalizedModule.mk_eq]
    obtain ⟨n, hn⟩ := this
    exact ⟨⟨f ^ n, n, rfl⟩, by simpa [sub_eq_zero, smul_sub] using! Submodule.mem_colon.mp hn _ rfl⟩
  simp only [toBasicOpenₗ_mk] at h_eq
  rw [← PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.mem_vanishingIdeal]
  intro p hfp
  contrapose hfp
  obtain ⟨u, hu⟩ := LocalizedModule.mk_eq.mp congr(($h_eq).1 ⟨p, hfp⟩)
  rw [PrimeSpectrum.mem_zeroLocus, Set.not_subset]
  exact ⟨u.1, by simpa [sub_eq_zero, smul_sub], u.2⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
⊢ Set.range ⇑((V.ι ⁻¹ᵁ U).ι ≫ V.ι) = Set.range ⇑U.ι

Tactic:
rw [Scheme.Hom.comp_base, TopCat.coe_comp, Scheme.Opens.range_ι, Set.range_comp, ← this]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
⊢ ⇑V.ι '' Set.range ⇑(V.ι ⁻¹ᵁ V.ι ''ᵁ V.ι ⁻¹ᵁ U).ι = ↑(V.ι ''ᵁ V.ι ⁻¹ᵁ U)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
e : U = V
⊢ Arrow.mk (f ∣_ U) = Arrow.mk (f ∣_ V)

Tactic:
subst e

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Arrow.mk (f ∣_ U) = Arrow.mk (f ∣_ U)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x : ↑X.toTopCat
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x))

Tactic:
let p : PrimeSpectrum (Γ.obj (op X)) := X.toΓSpecFun x

Goal state after:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: this : HasColimitsOfSize.{u, u, u, u + 1} AffineSchemeᵒᵖ
⊢ HasLimits AffineScheme

Tactic:
have : HasLimits AffineScheme.{u}ᵒᵖᵒᵖ := Limits.hasLimits_op_of_hasColimits

Goal state after:
this✝ : HasColimitsOfSize.{u, u, u, u + 1} AffineSchemeᵒᵖ
this : HasLimits AffineSchemeᵒᵖᵒᵖ
⊢ HasLimits AffineScheme
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
inst✝ : IsAffine X
f : X ⟶ Y
H : IsOpenImmersion f
⊢ IsAffineOpen (Scheme.Hom.opensRange f)

Tactic:
refine .of_isIso (IsOpenImmersion.isoOfRangeEq f (Y.ofRestrict _) ?_).inv

Goal state after:
X Y : Scheme
inst✝ : IsAffine X
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Set.range ⇑f = Set.range ⇑(Y.ofRestrict ⋯)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
⊢ IsAffineOpen ⊤

Tactic:
convert! isAffineOpen_opensRange (𝟙 X)

Goal state after:
X : Scheme
inst✝ : IsAffine X
⊢ ⊤ = Scheme.Hom.opensRange (𝟙 X)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_2.refine_2
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ g ∣_ UX ≫ resLE iX US UX hUSX = resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯ ≫ f ∣_ US

Tactic:
simp [← cancel_mono US.ι, H.w]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.Hom.app hU.fromSpec U)) f) =
    (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f)

Tactic:
hU.fromSpec_app_self

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen
      ((ConcreteCategory.hom ((Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op)) f) =
    (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen (Scheme.Hom.opensRange (X.basicOpen r).ι ⊓ U)

Tactic:
Scheme.Opens.opensRange_ι,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen (X.basicOpen r ⊓ U)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).obj.obj (op (PrimeSpectrum.basicOpen f)))
e_2✝ : CommRing.toCommSemiring ≍ CommRing.toCommSemiring
r✝ : ↑Γ(X, U)
⊢ CommRingCat.Hom.hom
      (Scheme.Hom.app hU.fromSpec U ≫
        (Spec Γ(X, U)).presheaf.map ((Opens.map hU.fromSpec.base).map (homOfLE ⋯).op.unop).op ≫
          (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) =
    algebraMap ↑Γ(X, U) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)

Tactic:
hU.fromSpec_app_self

Goal state after:
case e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).obj.obj (op (PrimeSpectrum.basicOpen f)))
e_2✝ : CommRing.toCommSemiring ≍ CommRing.toCommSemiring
r✝ : ↑Γ(X, U)
⊢ CommRingCat.Hom.hom
      (((Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) ≫
        (Spec Γ(X, U)).presheaf.map ((Opens.map hU.fromSpec.base).map (homOfLE ⋯).op.unop).op ≫
          (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) =
    algebraMap ↑Γ(X, U) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
V : X.Opens
i : V ⟶ U
e : V = X.basicOpen f
⊢ IsLocalization.Away f ↑Γ(X, V)

Tactic:
subst e

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
i : X.basicOpen f ⟶ U
⊢ IsLocalization.Away f ↑Γ(X, X.basicOpen f)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
⊢ s ∈ I ↔
    ∀ (x : ↥X) (h : x ∈ U),
      (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I

Tactic:
by
  refine ⟨fun hs x hxU ↦ Ideal.mem_map_of_mem _ hs, fun H ↦ ?_⟩
  let (x : _) : Algebra Γ(X, U) (X.presheaf.stalk (hU.fromSpec x)) :=
    TopCat.Presheaf.algebra_section_stalk X.presheaf _
  have (P : Ideal Γ(X, U)) [hP : P.IsPrime] : IsLocalization.AtPrime _ P :=
      hU.isLocalization_stalk' ⟨P, hP⟩ (hU.isoSpec.inv _).2
  refine Submodule.mem_of_localization_maximal
      (fun P hP ↦ X.presheaf.stalk (hU.fromSpec ⟨P, hP.isPrime⟩))
      (fun P hP ↦ Algebra.linearMap _ _) _ _ ?_
  intro P hP
  rw [Ideal.localized₀_eq_restrictScalars_map]
  exact H _ _

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v, u₁} C
D : GlueData C
inst✝² : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst✝¹ : PreservesColimit D.diagram.multispan F
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F
⊢ ∃ i y, (ConcreteCategory.hom (F.map (D.ι i))) y = x

Tactic:
obtain ⟨i, y, eq⟩ := (D.mapGlueData F).types_ι_jointly_surjective (e.hom x)

Goal state after:
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : GlueData C
inst✝² : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst✝¹ : PreservesColimit D.diagram.multispan F
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F
i : (D.mapGlueData F).J
y : (D.mapGlueData F).U i
eq : (ConcreteCategory.hom ((D.mapGlueData F).ι i)) y = (ConcreteCategory.hom e.hom) x
⊢ ∃ i y, (ConcreteCategory.hom (F.map (D.ι i))) y = x
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
X Y Z : C
f : X ⟶ Y
e : Z = X
⊢ eqToHom e ≫ f ≍ f

Tactic:
subst e

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
Y Z : C
f : Z ⟶ Y
⊢ eqToHom ⋯ ≫ f ≍ f
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↥X
hx : x ∈ U
⊢ x ∈ ⨆ i ∈ s, X.basicOpen i

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open hx U.2

Goal state after:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ x ∈ ⨆ i ∈ s, X.basicOpen i
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
j : (ofOpenSubsets U).J
y : ↑(of α)
hy : y ∈ U j
e : (ConcreteCategory.hom (U i).inclusion') ⟨x, hx⟩ = (ConcreteCategory.hom (U j).inclusion') ⟨y, hy⟩
⊢ (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩ = (ConcreteCategory.hom ((ofOpenSubsets U).ι j)) ⟨y, hy⟩

Tactic:
subst e

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
j : (ofOpenSubsets U).J
hy : (ConcreteCategory.hom (U i).inclusion') ⟨x, hx⟩ ∈ U j
⊢ (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩ =
    (ConcreteCategory.hom ((ofOpenSubsets U).ι j)) ⟨(ConcreteCategory.hom (U i).inclusion') ⟨x, hx⟩, hy⟩
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
⊢ x✝ ∈ ⋃ i, ↑(U i) → x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
rintro ⟨_, ⟨i, rfl⟩, hx⟩
    rename_i x
    exact ⟨(ofOpenSubsets U).toGlueData.ι i ⟨x, hx⟩, ι_fromOpenSubsetsGlue_apply _ _ _⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
x : (MultispanShape.prod (ulift 𝒰).gluedCover.J).R
⊢ Multicoequalizer.π (ulift 𝒰).gluedCover.diagram x ≫
      Multicoequalizer.desc (ulift 𝒰).gluedCover.diagram X (fun x ↦ (ulift 𝒰).f x) ⋯ ≫ f₁ =
    Multicoequalizer.π (ulift 𝒰).gluedCover.diagram x ≫
      Multicoequalizer.desc (ulift 𝒰).gluedCover.diagram X (fun x ↦ (ulift 𝒰).f x) ⋯ ≫ f₂

Tactic:
Multicoequalizer.π_desc_assoc,

Goal state after:
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
x : (MultispanShape.prod (ulift 𝒰).gluedCover.J).R
⊢ (ulift 𝒰).f x ≫ f₁ =
    Multicoequalizer.π (ulift 𝒰).gluedCover.diagram x ≫
      Multicoequalizer.desc (ulift 𝒰).gluedCover.diagram X (fun x ↦ (ulift 𝒰).f x) ⋯ ≫ f₂
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ t' 𝒰 f g i j k ≫
      t' 𝒰 f g j k i ≫
        t' 𝒰 f g k i j ≫
          pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)

Tactic:
cocycle_snd_snd 𝒰 f g i j k

Goal state after: