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

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
⊢ (ConcreteCategory.hom ((structureSheafInType R M).obj.map (homOfLE ?m.192).op)) s =
    const (g j • f i) (g i * g j) (basicOpen (g i * g j)) ⋯

pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
⊢ basicOpen (g i * g j) ≤ U

Tactic:
· refine congr((structureSheafInType R M).obj.map (homOfLE ((PrimeSpectrum.basicOpen_mul (g i)
        (g j)).trans_le inf_le_left)).op $(H i)).symm.trans (Subtype.ext <| funext fun a ↦ ?_)
      exact LocalizedModule.mk_eq.mpr ⟨1, by simp [Submonoid.smul_def, ← smul_assoc]⟩

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
⊢ basicOpen (g i * g j) ≤ U
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ IsPullback (f ∣_ U) (f ⁻¹ᵁ U).ι U.ι f

Tactic:
apply IsOpenImmersion.isPullback

Goal state after:
case H
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (f ⁻¹ᵁ U).ι ≫ f = f ∣_ U ≫ U.ι

case H'
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange U.ι = Scheme.Hom.opensRange (f ⁻¹ᵁ U).ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_1
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ V.ι ''ᵁ (Opens.map ((X.homOfLE hV).base ≫ W.ι.base)).obj U = U ⊓ V

Tactic:
← Scheme.Hom.comp_base,

Goal state after:
case refine_1
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ V.ι ''ᵁ (Opens.map (X.homOfLE hV ≫ W.ι).base).obj U = U ⊓ V
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_1.e_a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : ↑U ⊆ ⋃ i ∈ t, ↑(basicOpen (g i))
N : ℕ := (t ×ˢ t).sup fun x ↦ n x.1 x.2 + 1
i j : ↥t
this : n ↑i ↑j + 1 ≤ N
⊢ (g ↑i * g ↑j) ^ (n ↑i ↑j + 1) • g ↑j • f ↑i = (g ↑i * g ↑j) ^ (n ↑i ↑j + 1) • g ↑i • f ↑j

Tactic:
convert! (hn i j).symm using 1 <;> module

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
⊢ X.toΓSpec ≫ (Γ.rightOp ⋙ Spec.toLocallyRingedSpace).map f = (𝟭 LocallyRingedSpace).map f ≫ Y.toΓSpec

Tactic:
apply LocallyRingedSpace.comp_ring_hom_ext

Goal state after:
case w
X Y : LocallyRingedSpace
f : X ⟶ Y
⊢ ((𝟭 LocallyRingedSpace).obj X).toΓSpec.base ≫ (Spec.locallyRingedSpaceMap (Γ.rightOp.map f).unop).base =
    ((𝟭 LocallyRingedSpace).map f ≫ Y.toΓSpec).base

case h
X Y : LocallyRingedSpace
f : X ⟶ Y
⊢ ∀ (r : ↑(unop (Γ.rightOp.obj Y))),
    (Γ.rightOp.map f).unop ≫ ((𝟭 LocallyRingedSpace).obj X).presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom
          (algebraMap (↑(unop (Γ.rightOp.obj Y)))
            ((structureSheafInType ↑(unop (Γ.rightOp.obj Y)) ↑(unop (Γ.rightOp.obj Y))).obj.obj (op (basicOpen r)))) ≫
        ((𝟭 LocallyRingedSpace).map f ≫ Y.toΓSpec).c.app (op (basicOpen r))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
U : Y.Opens
hU : IsAffineOpen U
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hU' : U ≤ Scheme.Hom.opensRange f
⊢ IsAffineOpen (Scheme.Hom.opensRange f ⊓ U)

Tactic:
inf_eq_right.mpr hU'

Goal state after:
X Y : Scheme
U : Y.Opens
hU : IsAffineOpen U
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hU' : U ≤ Scheme.Hom.opensRange f
⊢ IsAffineOpen U
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ''ᵁ PrimeSpectrum.basicOpen f = X.basicOpen f

Tactic:
rw [← hU.fromSpec_preimage_basicOpen]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f = X.basicOpen f
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCat
⊢ identityToΓSpec.app (Spec.toLocallyRingedSpace.obj (op R)) ≫
      Spec.toLocallyRingedSpace.map (SpecΓIdentity.inv.app R).op =
    𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))

Tactic:
apply LocallyRingedSpace.comp_ring_hom_ext

Goal state after:
case w
R : CommRingCat
⊢ ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).toΓSpec.base ≫
      (Spec.locallyRingedSpaceMap (SpecΓIdentity.inv.app R).op.unop).base =
    (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).base

case h
R : CommRingCat
⊢ ∀ (r : ↑(unop (op ((𝟭 CommRingCat).obj R)))),
    (SpecΓIdentity.inv.app R).op.unop ≫
        ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom
          (algebraMap (↑(unop (op ((𝟭 CommRingCat).obj R))))
            ((structureSheafInType ↑(unop (op ((𝟭 CommRingCat).obj R))) ↑(unop (op ((𝟭 CommRingCat).obj R)))).obj.obj
              (op (basicOpen r)))) ≫
        (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).c.app (op (basicOpen r))
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
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs✝ : (isLocallyFraction R M).pred s
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
W : Opens ↑(PrimeSpectrum.Top R)
m : ↑⟨PrimeSpectrum.comap σ p, ⋯⟩ ∈ W
iWU : W ⟶ U
a : M
b : R
h_frac : ∀ (x : ↥W), ∃ (hs : b ∉ (↑x).asIdeal), (fun x ↦ s (iWU x)) x = LocalizedModule.mk a ⟨b, hs⟩
q : ↑(PrimeSpectrum.Top S)
hqW : q ∈ ↑{ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ }
hqV : q ∈ ↑V
hs : b ∉ (↑⟨PrimeSpectrum.comap σ q, hqW⟩).asIdeal
H : (fun x ↦ s (iWU x)) ⟨PrimeSpectrum.comap σ q, hqW⟩ = LocalizedModule.mk a ⟨b, hs⟩
⊢ ∃ (hs : σ b ∉ (↑⟨q, ⋯⟩).asIdeal),
    (fun x ↦ comapFun f U V hUV s (({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ }.infLERight V) x))
        ⟨q, ⋯⟩ =
      LocalizedModule.mk (f a) ⟨σ b, hs⟩

Tactic:
refine ⟨hs, ?_⟩

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
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs✝ : (isLocallyFraction R M).pred s
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
W : Opens ↑(PrimeSpectrum.Top R)
m : ↑⟨PrimeSpectrum.comap σ p, ⋯⟩ ∈ W
iWU : W ⟶ U
a : M
b : R
h_frac : ∀ (x : ↥W), ∃ (hs : b ∉ (↑x).asIdeal), (fun x ↦ s (iWU x)) x = LocalizedModule.mk a ⟨b, hs⟩
q : ↑(PrimeSpectrum.Top S)
hqW : q ∈ ↑{ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ }
hqV : q ∈ ↑V
hs : b ∉ (↑⟨PrimeSpectrum.comap σ q, hqW⟩).asIdeal
H : (fun x ↦ s (iWU x)) ⟨PrimeSpectrum.comap σ q, hqW⟩ = LocalizedModule.mk a ⟨b, hs⟩
⊢ (fun x ↦ comapFun f U V hUV s (({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ }.infLERight V) x))
      ⟨q, ⋯⟩ =
    LocalizedModule.mk (f a) ⟨σ b, hs⟩
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 k : D.J
hik : ¬i = k
⊢ ((if hij : i = i then
        (pullbackSymmetry (D.f' i i) (D.f' i k)).hom ≫
          pullback.map (D.f' i k) (D.f' i i) (D.f' i k) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
      else
        if hik : i = k then
          have this := ⋯;
          pullback.fst (D.f' i i) (D.f' i k) ≫
            eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i k) (D.f' i i))
        else
          if hjk : i = k then
            have this := ⋯;
            pullback.fst (D.f' i i) (D.f' i k) ≫
              eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i k) (D.f' i i))
          else
            pullback.map (D.f' i i) (D.f' i k) (D.f i i hij) (D.f i k hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
              D.t' i i k hij hik hjk ≫
                pullback.map (D.f i k hjk) (D.f i i ⋯) (D.f' i k) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯) ≫
      (if hij : i = k then
          (pullbackSymmetry (D.f' i k) (D.f' i i)).hom ≫
            pullback.map (D.f' i i) (D.f' i k) (D.f' k i) (D.f' k i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
        else
          if hik : i = i then
            have this := ⋯;
            pullback.fst (D.f' i k) (D.f' i i) ≫
              eqToHom ⋯ ≫ D.t i k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k i))
          else
            if hjk : k = i then
              have this := ⋯;
              pullback.fst (D.f' i k) (D.f' i i) ≫
                eqToHom ⋯ ≫ D.t i k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k i))
            else
              pullback.map (D.f' i k) (D.f' i i) (D.f i k hij) (D.f i i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                D.t' i k i hij hik hjk ≫
                  pullback.map (D.f k i hjk) (D.f k i ⋯) (D.f' k i) (D.f' k i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                    ⋯) ≫
        if hij : k = i then
          (pullbackSymmetry (D.f' k i) (D.f' k i)).hom ≫
            pullback.map (D.f' k i) (D.f' k i) (D.f' i i) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
        else
          if hik : k = i then
            have this := ⋯;
            pullback.fst (D.f' k i) (D.f' k i) ≫
              eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i k))
          else
            if hjk : i = i then
              have this := ⋯;
              pullback.fst (D.f' k i) (D.f' k i) ≫
                eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i k))
            else
              pullback.map (D.f' k i) (D.f' k i) (D.f k i hij) (D.f k i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                D.t' k i i hij hik hjk ≫
                  pullback.map (D.f i i hjk) (D.f i k ⋯) (D.f' i i) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                    ⋯) =
    𝟙 (pullback (D.f' i i) (D.f' i k))

Tactic:
simp [hik, Ne.symm hik, fst_eq_snd_of_mono_eq]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
⊢ ∀ (x : ↑(coproductCofan F).pt.toTopCat),
    IsLocalHom
      (CommRingCat.Hom.hom
        (PresheafedSpace.Hom.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom
          x))

Tactic:
by
        intro x
        obtain ⟨i, y, ⟨⟩⟩ := SheafedSpace.colimit_exists_rep (F ⋙ forgetToSheafedSpace) x
        have := PresheafedSpace.stalkMap.comp
          (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom
          (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom y
        simp only [← IsIso.comp_inv_eq,
          ← InducedCategory.comp_hom,
          PresheafedSpace.stalkMap.congr_hom _ _
            (congr_arg (InducedCategory.Hom.hom) (colimit.ι_desc
              (forgetToSheafedSpace.mapCocone s) i))] at this
        rw [← this]
        dsimp
        infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑(hom (X.isoSpec.inv.base ≫ X.toSpecΓ.base)) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus s

Tactic:
← Scheme.Hom.comp_base,

Goal state after:
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑(X.isoSpec.inv ≫ X.toSpecΓ) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus s
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R : CommRingCat
x : PrimeSpectrum ↑R
⊢ CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal)) ≫ (stalkIso R x).inv =
    (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial

Tactic:
ext s : 2

Goal state after:
R : CommRingCat
x : PrimeSpectrum ↑R
s : ↑(CommRingCat.of ↑R)
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal)) ≫ (stalkIso R x).inv)) s =
    (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)) s
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ pullback (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ⟶
    pullback (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))

Tactic:
refine (pullbackRightPullbackFstIso _ _ _).hom ≫ ?_
  refine ?_ ≫ (pullbackSymmetry _ _).hom
  refine ?_ ≫ (pullbackRightPullbackFstIso _ _ _).inv
  refine pullback.map _ _ _ _ (pullbackSymmetry _ _).hom (𝟙 _) (𝟙 _) ?_ ?_
  · simp [pullback.condition]
  · simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h :
  (ConcreteCategory.hom (((gluedCover 𝒰).ι i).base ≫ (fromGlued 𝒰).base)) x =
    (ConcreteCategory.hom (((gluedCover 𝒰).ι j).base ≫ (fromGlued 𝒰).base)) y
⊢ ((gluedCover 𝒰).ι i) x = ((gluedCover 𝒰).ι j) y

Tactic:
← Scheme.Hom.comp_base

Goal state after:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : ((gluedCover 𝒰).ι i ≫ fromGlued 𝒰) x = ((gluedCover 𝒰).ι j ≫ fromGlued 𝒰) y
⊢ ((gluedCover 𝒰).ι i) x = ((gluedCover 𝒰).ι j) y
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ { I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1}, X := fun x ↦ Sum.elim (fun x ↦ X) (fun x ↦ Y) x,
        f := fun x ↦ Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr) x }.presieve₀ ∈
    (Scheme.precoverage IsOpenImmersion).coverings (X ⨿ Y)

Tactic:
rw [Scheme.presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, fun x ↦ x.rec (fun _ ↦ inferInstance) (fun _ ↦ inferInstance)⟩
    use ((coprodMk X Y).symm x).elim (fun _ ↦ Sum.inl .unit) (fun _ ↦ Sum.inr .unit)
    obtain ⟨x, rfl⟩ := (coprodMk X Y).surjective x
    simp only [Sum.elim_inl, Sum.elim_inr, Set.mem_range]
    rw [Homeomorph.symm_apply_apply]
    obtain (x | x) := x
    · simp only [Sum.elim_inl, coprodMk_inl, exists_apply_eq_apply]
    · simp only [Sum.elim_inr, coprodMk_inr, exists_apply_eq_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case a
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ Scheme.Hom.opensRange coprod.inl ≤ coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl

Tactic:
· rintro _ ⟨x, rfl⟩
    exact ⟨f x, by simp [← Scheme.Hom.comp_apply, -Scheme.Hom.comp_base]⟩

Goal state after:
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:
IsOpenImmersion.comp_lift_assoc

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)
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
s : PullbackCone f g
i : 𝒰.I₀
⊢ (gluing 𝒰 f g).ι i ≫ p1 𝒰 f g = pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i

Tactic:
gluing_ι,

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
⊢ Multicoequalizer.π (gluing 𝒰 f g).diagram i ≫ p1 𝒰 f g = pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
      limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (j, k))) =
    𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (j, k)))

Tactic:
rw [← limit.w (componentwiseDiagram 𝖣.diagram.multispan _)
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))),
      ← Category.assoc, Category.id_comp]
    congr 1
    simp_rw [Category.assoc]
    apply π_ιInvApp_π

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: case hP₁
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), SpecializingMap ⇑f

Tactic:
introv
    exact f.isClosedMap.specializingMap

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: M S T : Scheme
inst✝¹ : M.Over S
f : T ⟶ S
inst✝ : MonObj (Over.mk (M ↘ S))
⊢ MonObj (Over.mk (pullback (M ↘ S) f ↘ T))

Tactic:
exact Over.monObjMkPullbackSnd

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: case hP₃
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
x✝ : Continuous[inst✝¹, inst✝] f
hsp :
  ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy : y ∈ closure[inst✝] {f x}
this : ∃ i, y ∈ U i
⊢ y ∈ f '' closure[inst✝¹] {x}

Tactic:
obtain ⟨i, hi⟩ := this

Goal state after:
case hP₃
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
x✝ : Continuous[inst✝¹, inst✝] f
hsp :
  ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy : y ∈ closure[inst✝] {f x}
i : ι
hi : y ∈ U i
⊢ y ∈ f '' closure[inst✝¹] {x}
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
by
  classical
  intro R S T _ _ _ f g hf hg
  rw [locally_iff_finite] at hf hg
  obtain ⟨sf, hsfone, hsf⟩ := hf
  obtain ⟨sg, hsgone, hsg⟩ := hg
  rw [locally_iff_exists hPi]
  refine ⟨sf × sg, fun (a, b) ↦ g a * b, ?_,
      fun (a, b) ↦ Localization.Away ((algebraMap T (Localization.Away b.val)) (g a.val)),
      inferInstance, inferInstance, inferInstance, ?_⟩
  · rw [eq_top_iff, ← hsgone, Ideal.span_le]
    intro t ht
    have : 1 ∈ Ideal.span (Set.range <| fun a : sf ↦ a.val) := by simp [hsfone]
    simp only [Ideal.mem_span_range_iff_exists_fun, SetLike.mem_coe] at this ⊢
    obtain ⟨cf, hcf⟩ := this
    let cg : sg → T := Pi.single ⟨t, ht⟩ 1
    use fun (a, b) ↦ g (cf a) * cg b
    simp [cg, Pi.single_apply, Fintype.sum_prod_type, ← mul_assoc, ← Finset.sum_mul, ← map_mul,
      ← map_sum, hcf] at hcf ⊢
  · intro ⟨a, b⟩
    let g' := (algebraMap T (Localization.Away b.val)).comp g
    let a' := (algebraMap T (Localization.Away b.val)) (g a.val)
    have : (algebraMap T <| Localization.Away a').comp (g.comp f) =
        (Localization.awayMap g' a.val).comp ((algebraMap S (Localization.Away a.val)).comp f) := by
      ext x
      simp only [coe_comp, Function.comp_apply, a']
      change _ = Localization.awayMap g' a.val (algebraMap S _ (f x))
      simp only [Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_eq]
      rfl
    simp only [this, a']
    apply hPc _ _ (hsf a.val a.property)
    apply @hPl _ _ _ _ g' _ _ _ _ _ _ _ _ ?_ (hsg b.val b.property)
    exact IsLocalization.Away.instMapRingHomPowersOfCoe (Localization.Away (g' a.val)) a.val

Goal state after: