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

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ ↑(⨆ i, Hom.opensRange (𝒰.f i)) = ↑⊤

Tactic:
rw [Opens.coe_iSup]; exact 𝒰.iUnion_range

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

Goal state before:
pp: X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
l : Y ⟶ X
hl : l ≫ f = g
⊢ g = lift f g H' ≫ f

Tactic:
lift_fac

Goal state after:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
l : Y ⟶ X
hl : l ≫ f = g
⊢ g = g
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen f
x✝ : ↥(unop (op U))
⊢ 1 • 1 • (algebraMap R A) f = 1 • ⟨f, ⋯⟩ • 1

Tactic:
by simp [Algebra.smul_def, Submonoid.smul_def]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case mp
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
x : ↥X
⊢ x ∈ ↑(U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W) → x ∈ ↑(V.ι ''ᵁ W ⊓ U)

Tactic:
rintro ⟨⟨y, hyU⟩, hyW, rfl⟩

Goal state after:
case mp
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
y : ↥X
hyU : y ∈ U
hyW : ⟨y, hyU⟩ ∈ ↑(X.homOfLE e ⁻¹ᵁ W)
⊢ (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom U.ι)).hom.base) ⟨y, hyU⟩ ∈ ↑(V.ι ''ᵁ W ⊓ U)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ pullback.fst s v ≫ f = lhs ≫ pullback.fst t v

Tactic:
by simp [lhs]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

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

Tactic:
symm
    apply LocallyRingedSpace.comp_ring_hom_ext
    · ext1 x
      dsimp
      change PrimeSpectrum.comap (f.c.app (op ⊤)).hom (X.toΓSpecFun x) = Y.toΓSpecFun (f.base x)
      dsimp [toΓSpecFun]
      rw [← IsLocalRing.comap_closedPoint (f.stalkMap x).hom, ←
        PrimeSpectrum.comap_comp_apply, ← PrimeSpectrum.comap_comp_apply,
        ← CommRingCat.hom_comp, ← CommRingCat.hom_comp]
      congr 2
      exact (PresheafedSpace.stalkMap_germ f.1 ⊤ x trivial).symm
    · intro r
      rw [LocallyRingedSpace.comp_c_app, ← Category.assoc]
      erw [Y.toΓSpecSheafedSpace_app_spec, f.c.naturality]
      rfl

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
r s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op V))
⊢ ↑((comapₗ f.toSemilinearMap U V hUV).toFun (r * s)) p =
    ↑((comapₗ f.toSemilinearMap U V hUV).toFun r * (comapₗ f.toSemilinearMap U V hUV).toFun s) p

Tactic:
dsimp
    change _ = (comapₗ f.toSemilinearMap U V hUV r).1 p * (comapₗ f.toSemilinearMap U V hUV s).1 p
    simp only [comapₗ_eq_localRingHom, PrimeSpectrum.comap_asIdeal]
    exact (Localization.localRingHom ..).map_mul _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case left
D : GlueData
i : D.toLocallyRingedSpaceGlueData.J
y : ↑(D.toLocallyRingedSpaceGlueData.U i).toTopCat
j : (D.U i).affineCover.I₀
z : ↥((D.U i).affineCover.X j)
hz : ((D.U i).affineCover.f j) z = y
⊢ (ConcreteCategory.hom (D.toLocallyRingedSpaceGlueData.ι i).base) y ∈
    Set.range ⇑(ConcreteCategory.hom (Hom.toLRSHom ((D.U i).affineCover.f j) ≫ D.toLocallyRingedSpaceGlueData.ι i).base)

Tactic:
simp only [LocallyRingedSpace.comp_toHom, PresheafedSpace.comp_base,
      TopCat.hom_comp, ContinuousMap.coe_comp, Set.range_comp]
    exact Set.mem_image_of_mem _ ⟨z, hz⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h₁
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))

Tactic:
apply glued_cover_cocycle_snd

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

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Function.Injective ⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv)

Tactic:
← TopCat.mono_iff_injective

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono (D.gluedIso (forget C)).inv
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ IsIso (coprodSpec R S).base

Tactic:
convert_to IsIso (TopCat.isoOfHomeo (X := Spec (.of <| R × S)) <|
    PrimeSpectrum.primeSpectrumProdHomeo.trans (coprodMk (Spec <| .of R) (Spec <| .of S))).inv

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ (coprodSpec R S).base =
    (TopCat.isoOfHomeo
        (PrimeSpectrum.primeSpectrumProdHomeo.trans (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))))).inv

ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ IsIso
    (TopCat.isoOfHomeo
        (PrimeSpectrum.primeSpectrumProdHomeo.trans (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))))).inv
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case e_a
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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.fst (D.f j k) (D.f j i)).c.app
        (op
          ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
            ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).obj
              ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U))))) ≫
      (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
        (pullback (D.f j k) (D.f j i)).presheaf.map
            ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op ≫
          (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
            invApp (pullback.fst (D.f j k) (D.f j i))
                ((Opens.map (D.t' j k i).base).1
                  ((Opens.map (pullback.fst (D.f k i) (D.f k j)).base).obj
                    ((Opens.map (D.t k i).base).obj ((Opens.map (D.f i k).base).obj U)))) ≫
              (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
                (D.V (j, k)).presheaf.map ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫
                  (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
rw [IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.inv_naturality_assoc,
              IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.app_invApp_assoc]

Goal state after:
case e_a
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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op) ≫
          (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              (D.V (j, k)).presheaf.map ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫
                (D.V (j, k)).presheaf.map (eqToHom ⋯)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case inj
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
x y : ↑↑(D.U i)
h1 : y ∈ U
h2 :
  (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) y =
    (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) x
this : (D.mapGlueData (forget C)).ι i ≫ (D.gluedIso (forget C)).inv = (D.ι i).base
⊢ Function.Injective ⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv)

Tactic:
← TopCat.mono_iff_injective

Goal state after:
case inj
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
x y : ↑↑(D.U i)
h1 : y ∈ U
h2 :
  (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) y =
    (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) x
this : (D.mapGlueData (forget C)).ι i ≫ (D.gluedIso (forget C)).inv = (D.ι i).base
⊢ Mono (D.gluedIso (forget C)).inv
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : IsAffine S
H : Q g
this✝ : Q.IsLocal := ⋯
i : X.affineCover.toPreZeroHypercover.1
e : pullback (pullback.fst f g) (X.affineCover.f i) ≅ pullback (X.affineCover.f i ≫ f) g := ⋯
this : e.hom ≫ pullback.fst (X.affineCover.f i ≫ f) g = Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i
⊢ Q g

Tactic:
exact H

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

Goal state before:
pp: case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.f j i).c.app
      (op
        ((Opens.map
              (colimit.ι D.diagram.multispan
                  (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
          (⋯.functor.obj U))))

Tactic:
erw [D.ι_image_preimage_eq i j U]

Goal state after:
case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.f j i).c.app
      (op ((opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U)))))
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
H : Function.Surjective ⇑f
x : S
s : R
hs : s ∈ ↑M
⊢ ∃ a, (IsLocalization.map S' f ⋯) a = IsLocalization.mk' S' x ⟨f s, ⋯⟩

Tactic:
obtain ⟨y, rfl⟩ := H x

Goal state after:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
H : Function.Surjective ⇑f
s : R
hs : s ∈ ↑M
y : R
⊢ ∃ a, (IsLocalization.map S' f ⋯) a = IsLocalization.mk' S' (f y) ⟨f s, ⋯⟩
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (Localization.awayMap f ↑r) (IsLocalization.mk' (Localization.Away ↑r) b ⟨(fun x ↦ ↑r ^ x) n, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) x
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range

Tactic:
rw [Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_mk', eq_comm,
    IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, Subtype.coe_mk, ← map_mul] at e'

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x ↦ ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range
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
hPb : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
hf : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
⊢ Ideal.map Algebra.TensorProduct.includeRight
      (Ideal.span {g | P ((algebraMap T (Localization.Away g)).comp (algebraMap R T))}) ≤
    Ideal.span {g | P ((algebraMap (S ⊗[R] T) (Localization.Away g)).comp (algebraMap S (S ⊗[R] T)))}

Tactic:
Ideal.map_le_iff_le_comap,

Goal state after:
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
hPb : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
hf : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
⊢ Ideal.span {g | P ((algebraMap T (Localization.Away g)).comp (algebraMap R T))} ≤
    Ideal.comap Algebra.TensorProduct.includeRight
      (Ideal.span {g | P ((algebraMap (S ⊗[R] T) (Localization.Away g)).comp (algebraMap S (S ⊗[R] T)))})
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst f g)))

Tactic:
← PreservesPullback.iso_inv_fst AffineScheme.forgetToScheme (AffineScheme.ofHom f)
      (AffineScheme.ofHom g)

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ P
    (CommRingCat.Hom.hom
      (Scheme.Hom.appTop
        ((PreservesPullback.iso AffineScheme.forgetToScheme (AffineScheme.ofHom f) (AffineScheme.ofHom g)).inv ≫
          AffineScheme.forgetToScheme.map (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)))))
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
⊢ ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))

Tactic:
intro R A B f' g' iX iY iS e₁ e₂ _ _ _

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A B : CommRingCat
f' : Spec A ⟶ Spec R
g' : Spec B ⟶ Spec R
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
e₁ : f' ≫ iS = iX ≫ f
e₂ : g' ≫ iS = iY ≫ g
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
⊢ IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i ∈ s, ↑i
g : ↑s → ↑X.affineOpens := fun V ↦ ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
this : Finite ↑s
⊢ X.basicOpen f = U ⊓ X.basicOpen f

Tactic:
inf_eq_right.mpr (X.basicOpen_le f)

Goal state after:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i ∈ s, ↑i
g : ↑s → ↑X.affineOpens := fun V ↦ ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
this : Finite ↑s
⊢ X.basicOpen f = X.basicOpen f
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
⊢ ∃ r s,
    ∃ (_ : x ∈ X.basicOpen s) (e : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))

Tactic:
have hxa : x ∈ X.basicOpen (f.appLE U₂ V₂ e₂ r') := by
    simpa [Scheme.Hom.appLE, ← Scheme.preimage_basicOpen] using And.intro hx₂ (hBrr' ▸ hBfx)

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hxa : x ∈ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
⊢ ∃ r s,
    ∃ (_ : x ∈ X.basicOpen s) (e : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : CompactSpace ↥Y
⊢ CompactSpace ↥X

Tactic:
by
  constructor
  rw [← Set.preimage_univ (f := f)]
  exact QuasiCompact.isCompact_preimage _ isOpen_univ CompactSpace.isCompact_univ

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
R S : Type u
x✝¹ : CommRing R
x✝ : CommRing S
f : R →+* S
⊢ Q f ↔ Q' f

Tactic:
exact (e' f)

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

Goal state before:
pp: case basicOpen
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H✝ : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
U : ↑X.affineOpens
r : ↑Γ(X, ↑U)
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen r) ⋯))

Tactic:
simp_rw [Scheme.affineBasicOpen_coe,
      ← f.appLE_map (U := ⊤) le_top (homOfLE (X.basicOpen_le r)).op]

Goal state after:
case basicOpen
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H✝ : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
U : ↑X.affineOpens
r : ↑Γ(X, ↑U)
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯ ≫ X.presheaf.map (homOfLE ⋯).op))
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: case zero
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
e : x ^ 0 = 0
⊢ x = 0

Tactic:
simpa using congr_arg (· * x) e

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : 0 = ↑m' * (y ^ n.succ * ↑m' ^ n)
⊢ x = 0

Tactic:
rw [← mul_left_comm, ← pow_succ', ← mul_pow] at hm'

Goal state after:
case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : 0 = (y * ↑m') ^ n.succ
⊢ x = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case hU
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
i : 𝒰.I₀
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((IsOpenImmersion.isoOfRangeEq (𝒰.f i) (↑(S i)).ι ⋯).inv ≫ 𝒰.f i ≫ f)))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(S i) ⋯))

Tactic:
IsOpenImmersion.isoOfRangeEq_inv_fac_assoc,

Goal state after:
case hU
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
i : 𝒰.I₀
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((↑(S i)).ι ≫ f)))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(S i) ⋯))