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

Goal state before:
pp: X Y S X' Y' S' : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝² : IsOpenImmersion i₁
inst✝¹ : IsOpenImmersion i₂
inst✝ : Mono i₃
⊢ IsOpenImmersion
    ((pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv ≫
      pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) ≫
        pullback.fst (pullback.snd f' g') i₂)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ (Hom.hom (𝟙 (of S))) x = (Hom.hom (ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R))) x

Tactic:
change x = Algebra.TensorProduct.lmul' R (S := S) (x ⊗ₜ[R] 1)

Goal state after:
case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ x = (lmul' R) (x ⊗ₜ[R] 1)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Spec.map (𝟙 (of S)) = Spec.map (ofHom ↑includeRight ≫ ofHom ↑(lmul' R))

Tactic:
· congr 1; ext x; change x = Algebra.TensorProduct.lmul' R (S := S) (1 ⊗ₜ[R] x); simp

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

Goal state before:
pp: case convert_1
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ IsAffine (pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))

Tactic:
infer_instance

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

Goal state before:
pp: case convert_2
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ IsOpenImmersion
    (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g) g
      ⋯ ⋯)

Tactic:
infer_instance

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := isLocal_affineProperty P
hf : Q.diagonal (pullback.snd f (𝟙 Y))
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) (pullback f (𝟙 Y)) :=
  Scheme.Cover.pushforwardIso X.affineCover (inv (pullback.fst f (𝟙 Y)))
i : 𝒰.I₀
⊢ IsAffine (X.affineCover.X i)

Tactic:
infer_instance

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
i : 𝒱.I₀
⊢ IsAffine (pullback (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
intro R S T _ _ _ _ r _ f ⟨s, hsone, hs⟩

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwaySource 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
r : R
inst✝ : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap T (Localization.Away t)).comp f)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp (algebraMap R S))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₁ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f → ∀ (U : Opens X), P f → P (f ∘ Subtype.val)
hP₂ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f → ∀ {ι : Type u} (U : ι → Opens X), IsOpenCover U → (∀ (i : ι), P (f ∘ Subtype.val)) → P f
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) ((U i).ι ≫ f)) →
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f

Tactic:
· introv hU hf
    exact hP₂ f f.continuous _ hU hf

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
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'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
Mₐ : (a : ↑s) → Submonoid (Localization.Away ↑a) :=
  fun a ↦ Submonoid.map (algebraMap S (Localization.Away ↑a)) (Submonoid.map f M)
Sₐ : ↑s → Type u := fun a ↦ Localization (Mₐ a)
hM : ∀ (a : ↑s), Submonoid.map ((algebraMap S (Localization.Away ↑a)).comp f) M = Mₐ a
a : ↑s
⊢ IsLocalization (Mₐ a) (Sₐ a)

Tactic:
infer_instance

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

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),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X Y Z : Scheme
f✝ f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : QuasiSeparated f
⊢ QuasiSeparated (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparated (terminal.from Y)
inst✝ : QuasiSeparated f
⊢ QuasiSeparated (f ≫ terminal.from Y)

Tactic:
infer_instance

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
⊢ Finite Y.affineCover.finiteSubcover.I₀

Tactic:
infer_instance

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this✝ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
this : Finite 𝒰.I₀
i : 𝒰.I₀
⊢ CompactSpace ↥(pullback f (Y.affineCover.f (Scheme.Cover.idx Y.affineCover ↑i) ≫ g))

Tactic:
infer_instance

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
i : 𝒰.I₀
⊢ IsAffine ((pullback g (Z.affineCover.f i.fst)).affineCover.X i.snd)

Tactic:
infer_instance

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

Goal state before:
pp: X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (⇑f '' Z)
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X),
    IsClosed Z → StableUnderSpecialization (⇑f '' Z) → (∃ R, X = Spec R) → IsClosed (⇑f '' Z)
hX : ¬∃ R, X = Spec R
R : CommRingCat
g : Spec R ⟶ X
hg : Function.Surjective ⇑g
⊢ CompactSpace ↥(Spec R)

Tactic:
infer_instance

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
heq : Q = Q'
⊢ HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q

Tactic:
infer_instance

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

Goal state before:
pp: 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' : y * ↑m' = 0
⊢ ↑m' * y = y * ↑m'

Tactic:
mul_comm

Goal state after:
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' : y * ↑m' = 0
⊢ y * ↑m' = y * ↑m'
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ↑(⨆ I, ⨆ (_ : I.IsPrime), I.height) = ringKrullDim R

Tactic:
rw [← sup_height_eq_ringKrullDim, WithBot.coe_inj]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ⨆ I, ⨆ (_ : I.IsPrime), I.height = ⨆ I, ⨆ (_ : I ≠ ⊤), I.height
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
R : CommRingCat
H : _root_.IsReduced ↑R
x : ↥(Spec R)
⊢ _root_.IsReduced (Localization.AtPrime x.asIdeal)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case inl
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
h : U.carrier = ∅
this✝ : U = ⊥
this : Subsingleton ↑Γ(X, U)
⊢ _root_.IsReduced ↑Γ(X, U)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case inr
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
h : U.carrier.Nonempty
this : Nonempty ↥↑U
⊢ _root_.IsReduced ↑Γ(X, U)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case nonempty
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
⊢ autoParam (Nonempty ↥X) IsIntegral.nonempty._autoParam

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case nonempty
X Y : Scheme
f : X ⟶ Y
inst✝² : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↥X
⊢ autoParam (Nonempty ↥X) IsIntegral.nonempty._autoParam

Tactic:
infer_instance

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

Goal state before:
pp: case inst
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
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q

Tactic:
infer_instance

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

Goal state before:
pp: case mpr
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
⊢ (∃ e, IsIdempotentElem e ∧ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}) → IsOpenImmersion (Spec.map f)

Tactic:
rintro ⟨e, he, he'⟩
    let := f.hom.toAlgebra
    have : IsLocalization.Away (1 - e) S :=
      IsLocalization.away_of_isIdempotentElem he.one_sub (by simpa using! he') hf
    exact IsOpenImmersion.of_isLocalization (1 - e)

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

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
i : 𝒰.I₀
x : ↥(𝒰.X i)
⊢ IsIso (Scheme.Hom.stalkMap (𝒰.f i ≫ f) x ≫ inv (Scheme.Hom.stalkMap (𝒰.f i) x))

Tactic:
infer_instance

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

Goal state before:
pp: X : Scheme
I✝ : X.IdealSheafData
I : Ideal ↑Γ(X, ⊤)
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) I) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) I

Tactic:
Ideal.map_map,

Goal state after:
X : Scheme
I✝ : X.IdealSheafData
I : Ideal ↑Γ(X, ⊤)
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map
      ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).comp (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)))
      I =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) I
Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
h : IsIso (Spec.map f)
⊢ IsIso (Scheme.Hom.appTop (Spec.map f))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    (IsAffineOpen.isoSpec ⋯).inv ≫ X.homOfLE h

Tactic:
rw [Iso.eq_inv_comp, IsAffineOpen.isoSpec_hom, CommRingCat.ofHom_hom]

Goal state after:
case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ (↑U).toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE h).op) ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
x : ↑Γ(Y, Y.basicOpen s)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
⊢ x ∈ Ideal.map (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)) (RingHom.ker (CommRingCat.Hom.hom (f.app ↑U)))

Tactic:
obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers s) x

Goal state after:
case a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
⊢ IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n, ⋯⟩ ∈
    Ideal.map (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)) (RingHom.ker (CommRingCat.Hom.hom (f.app ↑U)))
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R S : CommRingCat
inst✝ : IsLocalRing ↑S
φ : R ⟶ S
⊢ φ ≫
      (ΓSpecIso S).inv ≫
        (Spec S).presheaf.germ (Spec.map φ ⁻¹ᵁ ⊤) (closedPoint ↑S) trivial ≫ (stalkClosedPointIso S).hom =
    φ

Tactic:
simp_rw [Opens.map_top]

Goal state after:
R S : CommRingCat
inst✝ : IsLocalRing ↑S
φ : R ⟶ S
⊢ φ ≫ (ΓSpecIso S).inv ≫ (Spec S).presheaf.germ ⊤ (closedPoint ↑S) trivial ≫ (stalkClosedPointIso S).hom = φ
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X✝¹ : Scheme
U : X✝¹.Opens
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
x : ↥X
⊢ IsPreimmersion (Spec.map (X.residue x))

Tactic:
infer_instance

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

Goal state before:
pp: X✝¹ Y✝ Z : Scheme
f✝ : X✝¹ ⟶ Y✝
g✝ : Y✝ ⟶ Z
this : ∀ (P : MorphismProperty Scheme) {Q : outParam AffineTargetMorphismProperty} [self : HasAffineProperty P Q],
  Q.IsLocal :=
  HasAffineProperty.isLocal_affineProperty
X✝ Y S : Scheme
X : IsAffine S
hX : IsAffine X✝
f : X✝ ⟶ S
g : Y ⟶ S
H : IsAffine Y
⊢ IsAffine (pullback f g)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.RingHom.EssFiniteType

Goal state before:
pp: R S T : Type u_4
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : Algebra.EssFiniteType R T
⊢ Algebra.EssFiniteType S (TensorProduct R S T)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ Function.Injective ⇑I.gluedTo

Tactic:
by
  intro a b e
  obtain ⟨ia, a : I.glueDataObj ia, rfl⟩ :=
    I.glueData.toGlueData.ι_jointly_surjective forget a
  obtain ⟨ib, b : I.glueDataObj ib, rfl⟩ :=
    I.glueData.toGlueData.ι_jointly_surjective forget b
  change I.glueData.ι ia a = I.glueData.ι ib b
  have : (I.glueDataObjι ia a).1 = (I.glueDataObjι ib b).1 := by
    have : (I.glueData.ι ia ≫ I.gluedTo) a = (I.glueData.ι ib ≫ I.gluedTo) b := e
    rwa [ι_gluedTo, ι_gluedTo] at this
  obtain ⟨f, g, hfg, H⟩ := exists_basicOpen_le_affine_inter ia.2 ib.2
    (I.glueDataObjι ia a).1
      ⟨(I.glueDataObjι ia a).2, this ▸ (I.glueDataObjι ib b).2⟩
  have hmem (W) (hW : W = X.affineBasicOpen g) :
      b ∈ Set.range (I.glueDataObjMap (hW.trans_le (X.affineBasicOpen_le g))) := by
    subst hW
    refine (I.opensRange_glueDataObjMap g).ge ?_
    change (I.glueDataObjι ib b).1 ∈ X.basicOpen g
    rwa [← this, ← hfg]
  obtain ⟨a, rfl⟩ := (I.opensRange_glueDataObjMap f).ge H
  obtain ⟨b, rfl⟩ := hmem (X.affineBasicOpen f) (Subtype.ext hfg)
  simp only [glueData_U, ← Scheme.Hom.comp_apply, glueDataObjMap_glueDataObjι] at this ⊢
  simp only [Scheme.affineBasicOpen_coe, Scheme.Hom.comp_base, TopCat.comp_app,
    Scheme.homOfLE_apply, SetLike.coe_eq_coe] at this
  obtain rfl := (I.glueDataObjι (X.affineBasicOpen f)).isEmbedding.injective this
  simp only [glueDataObjMap_ι]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Set.range ⇑(I.glueData.ι U) = ↑(I.gluedTo ⁻¹ᵁ ↑U)

Tactic:
simp only [TopologicalSpace.Opens.map_coe]
  apply I.gluedTo_injective.image_injective
  rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ι_gluedTo,
    range_glueDataObjι_ι, Set.image_preimage_eq_inter_range, range_gluedTo,
    ← coe_support_inter, Set.inter_comm]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
S' : Type u_4
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)
n : ℕ
hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ ↑A.toSubsemiring
hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)
a : ↥M
ha₂ : ↑a * x' = ↑a * (↑y ^ n * x)
⊢ ↑a * x' = x' * ↑a

Tactic:
mul_comm

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
S' : Type u_4
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)
n : ℕ
hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ ↑A.toSubsemiring
hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)
a : ↥M
ha₂ : ↑a * x' = ↑a * (↑y ^ n * x)
⊢ x' * ↑a = x' * ↑a
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ IsPreimmersion (I.glueDataObjι U)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ IsPreimmersion (I.subschemeIso.hom ≫ I.gluedTo)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ QuasiCompact (I.subschemeIso.hom ≫ I.gluedTo)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
⊢ 1 ∈ Ideal.span ↑s

Tactic:
rw [hs]; trivial

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact ↑V
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
this✝¹ : IsAffine ↑U
this✝ : IsAffine ↑W
this : CompactSpace ↥↑V
f' : ↑U ⟶ ↑W := Scheme.Hom.resLE f W U hUW
q : ↑V ⟶ ↑W := IsOpenImmersion.lift W.ι (V.ι ≫ g) ⋯
⊢ IsCompact (↑(pullback.fst f g ⁻¹ᵁ U) ⊓ ↑(pullback.snd f g ⁻¹ᵁ V))

Tactic:
let p : pullback f' q ⟶ pullback f g :=
    pullback.map _ _ _ _ U.ι (Scheme.Opens.ι _) W.ι (by simp [f']) (by simp [q])

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact ↑V
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
this✝¹ : IsAffine ↑U
this✝ : IsAffine ↑W
this : CompactSpace ↥↑V
f' : ↑U ⟶ ↑W := Scheme.Hom.resLE f W U hUW
q : ↑V ⟶ ↑W := IsOpenImmersion.lift W.ι (V.ι ≫ g) ⋯
p : pullback f' q ⟶ pullback f g := pullback.map f' q f g U.ι V.ι W.ι ⋯ ⋯
⊢ IsCompact (↑(pullback.fst f g ⁻¹ᵁ U) ⊓ ↑(pullback.snd f g ⁻¹ᵁ V))