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

Goal state before:
pp: case w
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α.hom.base = β.hom.base

Tactic:
exact w

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ appLE g U V e₁ ≫ appLE f V W e₂ = appLE (f ≫ g) U W ⋯

Tactic:
dsimp [Hom.appLE]
  rw [Category.assoc, f.naturality_assoc, ← Functor.map_comp]
  rfl

Goal state after:
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:
aesop

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

Goal state before:
pp: P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
⊢ ((∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑f) ∧ ∀ (i : PUnit.{1}), P f) ↔ Function.Surjective ⇑f ∧ P f

Tactic:
aesop

Goal state after:
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 Y : Scheme
𝒰 : Cover (precoverage P) X
f : Y ⟶ X
hf : P f
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑((𝒰.add f).f i)) ∧ ∀ (i : (𝒰.add f).I₀), P ((𝒰.add f).f i)

Tactic:
refine ⟨fun x ↦ ⟨some <| 𝒰.idx x, 𝒰.covers x⟩, ?_⟩

Goal state after:
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 Y : Scheme
𝒰 : Cover (precoverage P) X
f : Y ⟶ X
hf : P f
⊢ ∀ (i : (𝒰.add f).I₀), P ((𝒰.add f).f i)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (eqToHom ⋯ ≫ (Opens.map f.base).map (eqToHom ⋯).op.unop).op

Tactic:
Quiver.Hom.unop_op,

Goal state after:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (eqToHom ⋯ ≫ (Opens.map f.base).map (eqToHom ⋯)).op
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 j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
⊢ (Opens.map (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base).obj
      ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (⋯.functor.obj U)) =
    ⊥

Tactic:
by
  ext x
  apply iff_false_intro
  rintro ⟨y, hy, eq⟩
  replace eq := ConcreteCategory.congr_arg (preservesColimitIso (SheafedSpace.forget C) F ≪≫
    HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫ TopCat.sigmaIsoSigma.{v, v} _).hom eq
  simp_rw [CategoryTheory.Iso.trans_hom, ← TopCat.comp_app, ← PresheafedSpace.comp_base] at eq
  rw [ι_preservesColimitIso_inv] at eq
  change
    ((SheafedSpace.forget C).map (colimit.ι F i) ≫ (preservesColimitIso (forget C) F).hom ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom) y =
      ((SheafedSpace.forget C).map (colimit.ι F j) ≫ (preservesColimitIso (forget C) F).hom ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom) x at eq
  cases i; cases j
  rw [ι_preservesColimitIso_hom_assoc, ι_preservesColimitIso_hom_assoc,
    HasColimit.isoOfNatIso_ι_hom_assoc, HasColimit.isoOfNatIso_ι_hom_assoc,
    TopCat.sigmaIsoSigma_hom_ι, TopCat.sigmaIsoSigma_hom_ι] at eq
  convert! h (congr_arg Discrete.mk (congr_arg Sigma.fst eq))

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
S : (x : ↑X) → Submonoid ↑(F.stalk x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : ↑(F.obj U)
hs : ∀ (i : ↥(unop U)), (CommRingCat.Hom.hom (F.germ (unop U) ↑i ⋯)) s ∈ S ↑i
x : ↥(unop V)
⊢ (ConcreteCategory.hom (F.map i.unop.op ≫ F.germ (unop V) ↑x ⋯)) s ∈ S ↑x

Tactic:
rw [F.germ_res]

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
S : (x : ↑X) → Submonoid ↑(F.stalk x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : ↑(F.obj U)
hs : ∀ (i : ↥(unop U)), (CommRingCat.Hom.hom (F.germ (unop U) ↑i ⋯)) s ∈ S ↑i
x : ↥(unop V)
⊢ (ConcreteCategory.hom (F.germ (unop U) ↑x ⋯)) s ∈ S ↑x
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ U.topIso.hom ≫ (Arrow.mk (Scheme.Hom.appLE f U V e)).hom =
    (Arrow.mk (Scheme.Hom.appTop (Scheme.Hom.resLE f U V e))).hom ≫ V.topIso.hom

Tactic:
simp only [Scheme.Opens.topIso_hom, eqToHom_op, Arrow.mk_hom, Scheme.Hom.map_appLE]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ = Scheme.Hom.appTop (Scheme.Hom.resLE f U V e) ≫ X.presheaf.map (eqToHom ⋯)
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝ : Category.{v_1, u_1} J
F : Discrete J ⥤ Type u_2
⊢ F.IsLocallyDirected

Tactic:
constructor
  rintro ⟨i⟩ ⟨j⟩ ⟨k⟩ ⟨⟨⟨⟩⟩⟩ ⟨⟨⟨⟩⟩⟩
  simpa using fun x ↦ ⟨i, 𝟙 _, 𝟙 _, x, by simp⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case e_a
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
r : R
m : (structureSheafInType R M).obj.obj (op U)
⊢ r • m = (algebraMap R ((structureSheafInType R R).obj.obj (op U))) ((RingHom.id R) r) • m

Tactic:
exact (IsScalarTower.algebraMap_smul Γ(R, U) r m).symm

Goal state after:
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
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
x✝ : ↥(unop (op V))
⊢ ↑((comapₗ f.toSemilinearMap U V hUV).toFun 1) x✝ = ↑1 x✝

Tactic:
dsimp
    simp only [comapₗ_eq_localRingHom, PrimeSpectrum.comap_asIdeal]
    exact (Localization.localRingHom ..).map_one

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
⊢ ∃ i y, (ConcreteCategory.hom (F.map (D.ι i))) y = x

Tactic:
let e := D.gluedIso F

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 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
⊢ (if h : i = k then D.U i else D.V i k h) = if h : j = k then D.U j else D.V j k h

Tactic:
aesop

Goal state after:
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
⊢ (if h : i = j then D.U i else D.V i j h) = if h : j = i then D.U j else D.V j i h

Tactic:
aesop

Goal state after:
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
⊢ D.U i = D.U j

Tactic:
aesop

Goal state after:
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
⊢ D.f' i k ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f' j k

Tactic:
aesop

Goal state after:
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
⊢ D.f' i j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f' j i

Tactic:
aesop

Goal state after:
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
hjk : ¬j = k
this : j ≠ i
⊢ (if h : i = j then D.U i else D.V i j h) = D.V i j hij

Tactic:
aesop

Goal state after:
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
hjk : ¬j = k
this : j ≠ i
⊢ (if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i j h) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i j hij

Tactic:
aesop

Goal state after:
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
hjk : ¬j = k
this : j ≠ i
⊢ (if h : i = k then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i k h) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i k hik

Tactic:
aesop

Goal state after:
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
hjk : ¬j = k
this : j ≠ i
⊢ D.V j k hjk = if h : j = k then D.U j else D.V j k h

Tactic:
aesop

Goal state after:
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
hjk : ¬j = k
this : j ≠ i
⊢ D.V j i ⋯ = if h : j = i then D.U j else D.V j i h

Tactic:
aesop

Goal state after:
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
hjk : ¬j = k
this : j ≠ i
⊢ D.f j k hjk ≫ eqToHom ⋯ = eqToHom ⋯ ≫ if h : j = k then eqToHom ⋯ else eqToHom ⋯ ≫ D.f j k h

Tactic:
aesop

Goal state after:
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
hjk : ¬j = k
this : j ≠ i
⊢ D.f j i ⋯ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ D.f j i h

Tactic:
aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
i : ι
hi : ↑x ∈ ↑(U i)
f : ↑Γ(X, ↑V)
g : ↑Γ(X, ↑(U i))
e : X.basicOpen f = X.basicOpen g
hf : ↑x ∈ X.basicOpen f
⊢ P (X.affineBasicOpen f)

Tactic:
convert! basicOpen _ g (hU i) using 1

Goal state after:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
i : ι
hi : ↑x ∈ ↑(U i)
f : ↑Γ(X, ↑V)
g : ↑Γ(X, ↑(U i))
e : X.basicOpen f = X.basicOpen g
hf : ↑x ∈ X.basicOpen f
⊢ X.affineBasicOpen f = X.affineBasicOpen g
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : IsOpen s
⊢ IsOpen[inst✝] (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s)

Tactic:
(ofOpenSubsets U).isOpen_iff

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
⊢ IsOpen[inst✝] (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case right.left
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
⊢ IsOpen[inst✝]
    (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion'))

Tactic:
rw [← Set.image_preimage_eq_inter_range]
    apply (Opens.isOpenEmbedding (X := TopCat.of α) (U i)).isOpenMap
    convert! hs i using 1
    rw [← ι_fromOpenSubsetsGlue, coe_comp, Set.preimage_comp]
    congr! 1
    exact Set.preimage_image_eq _ (fromOpenSubsetsGlue_injective U)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ (D.ι i) x = (D.ι j) y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩

Tactic:
refine Iff.trans ?_
    (TopCat.GlueData.ι_eq_iff_rel
      D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData
      i j x y)

Goal state after:
D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ (D.ι i) x = (D.ι j) y ↔
    (ConcreteCategory.hom
          (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i))
        x =
      (ConcreteCategory.hom
          (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι j))
        y
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case k
X : Scheme
𝒰 : X.OpenCover
⊢ (b : (MultispanShape.prod (gluedCover 𝒰).J).R) → (gluedCover 𝒰).diagram.right b ⟶ X

Tactic:
exact fun x => 𝒰.f x

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case 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
⊢ (fun x ↦ (ConcreteCategory.hom (D.ι j).base) ((ConcreteCategory.hom (D.f j k).base) x)) ⁻¹' ↑(⋯.functor.obj U) =
    ⇑(ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.left (j, k))).base) ⁻¹' ↑(⋯.functor.obj U)

Tactic:
change (D.f j k ≫ 𝖣.ι j).base ⁻¹' _ = _

Goal state after:
case 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
⊢ ⇑(ConcreteCategory.hom (D.f j k ≫ D.ι j).base) ⁻¹' ↑(⋯.functor.obj U) =
    ⇑(ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.left (j, k))).base) ⁻¹' ↑(⋯.functor.obj U)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inr x)))

Tactic:
have := Scheme.Hom.stalkMap_comp coprod.inr (coprodSpec R S) x
    rw [← IsIso.comp_inv_eq,
      Scheme.Hom.stalkMap_congr_hom _ (Spec.map _) (coprodSpec_inr R S)] at this
    rw [coprodMk_inr, ← this]
    let := (RingHom.snd R S).toAlgebra
    have : IsOpenImmersion (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) :=
      IsOpenImmersion.of_isLocalization (0, 1)
    infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case pos
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := (Pi.evalRingHom R i).toAlgebra
j : ι
h : j = i
⊢ (Function.update 0 i 1 * Function.update 0 i 1) j = Function.update 0 i 1 j

Tactic:
aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case neg
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := (Pi.evalRingHom R i).toAlgebra
j : ι
h : ¬j = i
⊢ (Function.update 0 i 1 * Function.update 0 i 1) j = Function.update 0 i 1 j

Tactic:
aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case pos
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := (Pi.evalRingHom R i).toAlgebra
x y : (a : ι) → R a
e : (algebraMap ((a : ι) → R a) (R i)) x = (algebraMap ((a : ι) → R a) (R i)) y
j : ι
h : j = i
⊢ (Function.update 0 i 1 * x) j = (Function.update 0 i 1 * y) j

Tactic:
aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case neg
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := (Pi.evalRingHom R i).toAlgebra
x y : (a : ι) → R a
e : (algebraMap ((a : ι) → R a) (R i)) x = (algebraMap ((a : ι) → R a) (R i)) y
j : ι
h : ¬j = i
⊢ (Function.update 0 i 1 * x) j = (Function.update 0 i 1 * y) j

Tactic:
aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
X : Scheme
s : Set σ
hs : s.Finite
U : σ → X.Opens
hU : ∀ i ∈ s, IsAffineOpen (U i)
hU' : s.Pairwise (Disjoint on U)
this : Finite ↑s
i j : ↑s
e : i ≠ j
⊢ ↑i ≠ ↑j

Tactic:
aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
H : Disjoint U V
⊢ U ⊔ V = ⨆ i, Sum.elim (fun x ↦ U) (fun x ↦ V) i

Tactic:
aesop

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✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i :
  { I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
      f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.I₀
⊢ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (pullbackSymmetry (𝒰.f i ≫ f) g).hom ≫
      (pullbackLeftPullbackSndIso g f (𝒰.f i)).inv ≫
        pullback.fst (pullback.snd g f) (𝒰.f i) ≫ (pullbackSymmetry g f).hom

Tactic:
aesop

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

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
f' : Z ⟶ Y
g' : Z ⟶ X
h : IsPullback g' f' f g
hg : P g
⊢ P (h.isoPullback.inv ≫ g')

Tactic:
h.isoPullback_inv_fst

Goal state after:
P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
f' : Z ⟶ Y
g' : Z ⟶ X
h : IsPullback g' f' f g
hg : P g
⊢ P (pullback.fst f g)
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✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullback f g).OpenCover

Tactic:
apply
    (openCoverOfBase' 𝒰 f g).copy 𝒰.I₀
      (fun i =>
        pullback (pullback.snd _ _ : pullback f (𝒰.f i) ⟶ _)
          (pullback.snd _ _ : pullback g (𝒰.f i) ⟶ _))
      (fun i =>
        pullback.map _ _ _ _ (pullback.fst _ _) (pullback.fst _ _) (𝒰.f i)
          pullback.condition.symm pullback.condition.symm)
      ((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit).symm) fun _ => Iso.refl _

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✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
⊢ ∀ (i : 𝒰.I₀),
    pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i)) (pullback.fst g (𝒰.f i))
        (𝒰.f i) ⋯ ⋯ =
      (Iso.refl (pullback (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)))).hom ≫
        (openCoverOfBase' 𝒰 f g).f
          (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i)
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : DenseRange ⇑(f ≫ g)
⊢ DenseRange ⇑g

Tactic:
denseRange_iff_closure_range,

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : closure (Set.range ⇑(f ≫ g)) = Set.univ
⊢ closure (Set.range ⇑g) = Set.univ
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f ↔
    Ideal.span {g | P ((algebraMap S (Localization.Away g)).comp f)} = ⊤

Tactic:
by
  refine ⟨fun ⟨s, hs, h⟩ ↦ ?_, fun h ↦ ⟨_, h, fun g hg ↦ hg⟩⟩
  rw [eq_top_iff, ← hs, Ideal.span_le]
  intro g hg
  exact Ideal.subset_span (h _ hg)

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
this :
  IsPullback (pullback.fst (𝒰.f i.1) (𝒰.f i.2) ≫ 𝒰.f i.1) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f) (pullback.diagonal f)
    (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯)
⊢ Q (pullback.snd (pullback.diagonal f) (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯))

Tactic:
rw [← Q.cancel_left_of_respectsIso this.isoPullback.hom, IsPullback.isoPullback_hom_snd]

Goal state after:
Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
this :
  IsPullback (pullback.fst (𝒰.f i.1) (𝒰.f i.2) ≫ 𝒰.f i.1) (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f) (pullback.diagonal f)
    (pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯)
⊢ Q (pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f)