mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Scheme

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

Tactic:
cases f; cases g; congr 1
  apply LocallyRingedSpace.Hom.ext'
  ext : 1
  · exact h_base
  · exact TopCat.Presheaf.ext (fun U ↦ by simpa using! h_app U)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
inst✝ : IsIso f
⊢ map (inv f) = inv (map f)

Tactic:
change Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)

Goal state after:
R S : CommRingCat
f : R ⟶ S
inst✝ : IsIso f
⊢ Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case refine_1
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ x ∉ X.basicOpen 0

Tactic:
simp only [Scheme.basicOpen_zero]; exact not_false

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Scheme.Spec.map (𝟙 Γ(X, U)).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))

Tactic:
op_id,

Goal state after:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Scheme.Spec.map (𝟙 (op Γ(X, U))) = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ ↑(f ⁻¹ᵁ f ''ᵁ U) = ↑U

Tactic:
simp [Set.preimage_image_eq _ f.isOpenEmbedding.injective]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P✝ Q P : MorphismProperty C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ P.precoverage.coverings X
⊢ ∃ T ∈ P.precoverage.coverings Y, T.FactorsThruAlong S f

Tactic:
by
    have : S.HasPullbacks f := ⟨fun {W} h hh ↦ P.hasPullback _ (hS hh)⟩
    refine ⟨S.pullbackArrows f, ?_, .pullbackArrows f S⟩
    intro Z g ⟨W, a, h⟩
    have := S.hasPullback f h
    exact P.pullback_snd _ _ (hS h)

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
this :
  IsUnit
    ((algebraMap ((structureSheafInType R R).obj.obj (op (basicOpen f)))
        (Module.End ((structureSheafInType R R).obj.obj (op (basicOpen f)))
          ((structureSheafInType R M).obj.obj (op (basicOpen f)))))
      ((algebraMap R ((structureSheafInType R R).obj.obj (op (basicOpen f)))) f))
⊢ IsUnit ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) f)

Tactic:
Module.End.isUnit_iff

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
this :
  Function.Bijective
    ⇑((algebraMap ((structureSheafInType R R).obj.obj (op (basicOpen f)))
          (Module.End ((structureSheafInType R R).obj.obj (op (basicOpen f)))
            ((structureSheafInType R M).obj.obj (op (basicOpen f)))))
        ((algebraMap R ((structureSheafInType R R).obj.obj (op (basicOpen f)))) f))
⊢ Function.Bijective ⇑((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) f)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
⊢ (fun x ↦ V.ι ''ᵁ x) (Hom.opensRange (X.homOfLE e)) = (fun x ↦ V.ι ''ᵁ x) (V.ι ⁻¹ᵁ U)

Tactic:
simp [← Hom.opensRange_comp, Hom.image_preimage_eq_opensRange_inf, e]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ (X.isoOfEq ⋯).hom = (Iso.refl ↑U).hom

Tactic:
rw [← cancel_mono U.ι, Scheme.isoOfEq_hom_ι, Iso.refl_hom, Category.id_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ⋂ i ∈ s, (zeroLocus {i})ᶜᶜ

Tactic:
compl_compl

Goal state after:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ⋂ i ∈ s, zeroLocus {i}
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
this :
  IsUnit
    ((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
        (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
      ((ConcreteCategory.hom (toStalk R x)) f))
⊢ IsUnit ((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f)

Tactic:
Module.End.isUnit_iff

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
this :
  Function.Bijective
    ⇑((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))
⊢ Function.Bijective ⇑((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ↑((structurePresheafInModuleCat R M).obj (op U))
g : R
hxg : x ∈ basicOpen g
igU : basicOpen g ≤ U
f : M
hs : const f g (basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map igU.hom.op)) s
⊢ (ModuleCat.Hom.hom
        ((structurePresheafInModuleCat R M).germ U x hxU ≫ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x))
      s =
    (ModuleCat.Hom.hom
        ((structurePresheafInModuleCat R M).germ U x hxU ≫ 𝟙 ((structurePresheafInModuleCat R M).stalk x)))
      s

Tactic:
rw [germ_stalkToLocalizationₗ_assoc, Category.comp_id, ← germ_res_apply _ igU.hom _ hxg]

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ↑((structurePresheafInModuleCat R M).obj (op U))
g : R
hxg : x ∈ basicOpen g
igU : basicOpen g ≤ U
f : M
hs : const f g (basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map igU.hom.op)) s
⊢ (ModuleCat.Hom.hom (openToLocalizationₗ R M U x hxU ≫ localizationtoStalkₗ R M x)) s =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen g) x hxg))
      ((ConcreteCategory.hom ((structurePresheafInModuleCat R M).map igU.hom.op)) s)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen ((X.basicOpen r).ι ⁻¹ᵁ U)

Tactic:
by
  apply (X.basicOpen r).ι.isAffineOpen_iff_of_isOpenImmersion.mp
  rw [Scheme.Hom.image_preimage_eq_opensRange_inf, Scheme.Opens.opensRange_ι, inf_comm,
    ← Scheme.basicOpen_res _ _ (homOfLE le_top).op]
  exact hU.basicOpen _

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) :=
  isLocalization_basicOpen hV ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
⊢ (CommRingCat.Hom.hom
          (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r))
            ⋯)).comp
      (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)) =
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom
            (IsLocalization.map
              (↑(X.presheaf.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)))))
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) ⋯))).comp
      (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r))

Tactic:
CommRingCat.hom_ofHom,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) :=
  isLocalization_basicOpen hV ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
⊢ (CommRingCat.Hom.hom
          (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r))
            ⋯)).comp
      (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)) =
    (IsLocalization.map (↑(X.presheaf.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)))))
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) ⋯).comp
      (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r))).comp (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)) =
    (CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op)).comp
      ((CommRingCat.Hom.hom
            (CommRingCat.ofHom
              (IsLocalization.map (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
                (CommRingCat.Hom.hom (Scheme.Hom.app f U)) ⋯))).comp
        (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)))

Tactic:
CommRingCat.hom_ofHom,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r))).comp (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)) =
    (CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op)).comp
      ((IsLocalization.map (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
            (CommRingCat.Hom.hom (Scheme.Hom.app f U)) ⋯).comp
        (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)))
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
this✝² : Module R N := Module.compHom N σ
this✝¹ : Algebra R S := σ.toAlgebra
this✝ : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
x : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this : IsUnit ((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N))) ↑⟨σ ↑x, ⋯⟩)
⊢ IsUnit ((algebraMap R (Module.End R (LocalizedModule y.asIdeal.primeCompl N))) ↑x)

Tactic:
Module.End.isUnit_iff

Goal state after:
R M A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
this✝² : Module R N := Module.compHom N σ
this✝¹ : Algebra R S := σ.toAlgebra
this✝ : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
x : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this : Function.Bijective ⇑((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N))) ↑⟨σ ↑x, ⋯⟩)
⊢ Function.Bijective ⇑((algebraMap R (Module.End R (LocalizedModule y.asIdeal.primeCompl N))) ↑x)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ (comapFun f y) ((LocalizedModule.mkLinearMap (Ideal.comap σ y.asIdeal).primeCompl M) a) =
    σ ↑b • LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩

Tactic:
dsimp [comapFun, Localizations]

Goal state after:
R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ (IsLocalizedModule.lift (Ideal.comap σ y.asIdeal).primeCompl
        (LocalizedModule.mkLinearMap (Ideal.comap σ y.asIdeal).primeCompl M)
        (↑R (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ∘ₗ { toAddHom := f.toAddHom, map_smul' := ⋯ }) ⋯)
      (LocalizedModule.mk a 1) =
    σ ↑b • LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (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
this✝ : (x : ↥(Spec Γ(X, U))) → Algebra ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec x)) :=
  fun x ↦ X.presheaf.algebra_section_stalk ((Scheme.Hom.toLRSHom hU.isoSpec.inv).base.hom' x)
this :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := hP }))) P
P : Ideal ↑Γ(X, U)
hP : P.IsMaximal
⊢ (Algebra.linearMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ }))) s ∈
    Submodule.localized₀ P.primeCompl
      (Algebra.linearMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ }))) I

Tactic:
Ideal.localized₀_eq_restrictScalars_map

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (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
this✝ : (x : ↥(Spec Γ(X, U))) → Algebra ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec x)) :=
  fun x ↦ X.presheaf.algebra_section_stalk ((Scheme.Hom.toLRSHom hU.isoSpec.inv).base.hom' x)
this :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := hP }))) P
P : Ideal ↑Γ(X, U)
hP : P.IsMaximal
⊢ (Algebra.linearMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ }))) s ∈
    Submodule.restrictScalars (↑Γ(X, U))
      (Ideal.map (algebraMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ }))) I)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
⊢ ∀ {x y : (i : D.J) × ↑(D.U i)}, D.Rel x y → D.Rel y x

Tactic:
rintro a b ⟨x, e₁, e₂⟩
    exact ⟨D.t _ _ x, e₂, by rw [← e₁, D.t_inv_apply]⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
U✝ : X.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X, U✝)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
⊢ Arrow.mk (Scheme.Hom.stalkMap f x) ≅
    Arrow.mk
      (CommRingCat.ofHom
        (Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯))

Tactic:
by
  let := Y.presheaf.algebra_section_stalk ⟨f x, hVU hx⟩
  have := hU.isLocalization_stalk ⟨f x, hVU hx⟩
  let := X.presheaf.algebra_section_stalk ⟨x, hx⟩
  have := hV.isLocalization_stalk ⟨x, hx⟩
  refine Arrow.isoMk' _ _ ?_ ?_ ?_
  · exact ((IsLocalization.algEquiv (hU.primeIdealOf ⟨f x, hVU hx⟩).asIdeal.primeCompl
      (Y.presheaf.stalk (f x))
      (Localization.AtPrime (hU.primeIdealOf ⟨f x, hVU hx⟩).asIdeal)).toCommRingCatIso:)
  · exact ((IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl
      (X.presheaf.stalk x)
      (Localization.AtPrime (hV.primeIdealOf ⟨x, hx⟩).asIdeal)).toCommRingCatIso:)
  · rw [← Iso.comp_inv_eq]
    ext1
    apply IsLocalization.ringHom_ext
      (hU.primeIdealOf ⟨f x, hVU hx⟩).asIdeal.primeCompl
    ext a
    dsimp [← AlgEquiv.symm_toRingEquiv]
    simp only [IsLocalization.map_eq, RingHom.id_apply, Localization.localRingHom_to_map,
      RingHomCompTriple.comp_apply]
    simp only [RingHom.algebraMap_toAlgebra, Scheme.Hom.germ_stalkMap_apply, Scheme.Hom.appLE,
      homOfLE_leOfHom, CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply,
      X.presheaf.germ_res_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this : HasPullback (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
⊢ v 𝒰 f g i j ⟶ v 𝒰 f g j i

Tactic:
have : HasPullback (pullback.snd _ _ ≫ 𝒰.f j ≫ f) g :=
    hasPullback_assoc_symm (𝒰.f i) (𝒰.f j) (𝒰.f j ≫ f) g

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this✝ : HasPullback (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ v 𝒰 f g i j ⟶ v 𝒰 f g j i
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case hf
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥X
⊢ Topology.IsOpenEmbedding ⇑f

pp: case inst
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥X
⊢ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
· exact .of_isEmpty (X := X) _

Goal state after:
case inst
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥X
⊢ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝² : Category.{v, w} J
F : J ⥤ Scheme
inst✝¹ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝ : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst
hlk : l ⟶ k₂.fst
z : (F ⋙ forget).obj l
hy₁ : (F.map k₁.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hli)) z) = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
hy₂ : (F.map k₂.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hlk)) z) = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι := ⋯
this : IsOpenImmersion α
⊢ (pullback.fst (V F i j).ι (V F i k).ι) (α z) = (pullback.fst (V F i j).ι (V F i k).ι) x

Tactic:
apply (V F i j).ι.isOpenEmbedding.injective

Goal state after:
J : Type w
inst✝² : Category.{v, w} J
F : J ⥤ Scheme
inst✝¹ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝ : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst
hlk : l ⟶ k₂.fst
z : (F ⋙ forget).obj l
hy₁ : (F.map k₁.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hli)) z) = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
hy₂ : (F.map k₂.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hlk)) z) = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι := ⋯
this : IsOpenImmersion α
⊢ (V F i j).ι ((pullback.fst (V F i j).ι (V F i k).ι) (α z)) = (V F i j).ι ((pullback.fst (V F i j).ι (V F i k).ι) x)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
this : IsOpenImmersion (Sigma.desc f)
x : ↥S
hx : x ∈ ⊤
⊢ x ∈ ⨆ i, Scheme.Hom.opensRange (f i)

Tactic:
hcov

Goal state after:
σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
this : IsOpenImmersion (Sigma.desc f)
x : ↥S
hx : x ∈ ⊤
⊢ x ∈ ⊤
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [limit.lift_π_assoc, cospan_left, PullbackCone.mk_π_app]

Goal state after:
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)