mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
t : S
inst✝ : IsLocalization.Away t T
f : R →+* 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)
a : S
ha : a ∈ s
this✝ : Algebra (Localization.Away a) (Localization.Away ((algebraMap S T) a)) :=
  (IsLocalization.Away.map (Localization.Away a) (Localization.Away ((algebraMap S T) a)) (algebraMap S T) a).toAlgebra
this :
  (algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      (algebraMap S (Localization.Away a)) =
    (algebraMap T (Localization.Away ((algebraMap S T) a))).comp (algebraMap S T)
⊢ P (((algebraMap T (Localization.Away ((algebraMap S T) a))).comp (algebraMap S T)).comp f)

Tactic:
← this,

Goal state after:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
t : S
inst✝ : IsLocalization.Away t T
f : R →+* 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)
a : S
ha : a ∈ s
this✝ : Algebra (Localization.Away a) (Localization.Away ((algebraMap S T) a)) :=
  (IsLocalization.Away.map (Localization.Away a) (Localization.Away ((algebraMap S T) a)) (algebraMap S T) a).toAlgebra
this :
  (algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      (algebraMap S (Localization.Away a)) =
    (algebraMap T (Localization.Away ((algebraMap S T) a))).comp (algebraMap S T)
⊢ P
    (((algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
          (algebraMap S (Localization.Away a))).comp
      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
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))
this :
  (pullback.fst (Scheme.Hom.appTop (AffineScheme.ofHom f).hom).op
          (Scheme.Hom.appTop (AffineScheme.ofHom g).hom).op).unop ≫
      (PreservesPullback.iso (AffineScheme.forgetToScheme.op ⋙ Scheme.Γ).rightOp (AffineScheme.ofHom f)
            (AffineScheme.ofHom g)).hom.unop =
    Scheme.Hom.appTop (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)).hom
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)).hom))

Tactic:
← this,

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))
this :
  (pullback.fst (Scheme.Hom.appTop (AffineScheme.ofHom f).hom).op
          (Scheme.Hom.appTop (AffineScheme.ofHom g).hom).op).unop ≫
      (PreservesPullback.iso (AffineScheme.forgetToScheme.op ⋙ Scheme.Γ).rightOp (AffineScheme.ofHom f)
            (AffineScheme.ofHom g)).hom.unop =
    Scheme.Hom.appTop (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)).hom
⊢ P
    (CommRingCat.Hom.hom
      ((pullback.fst (Scheme.Hom.appTop (AffineScheme.ofHom f).hom).op
            (Scheme.Hom.appTop (AffineScheme.ofHom g).hom).op).unop ≫
        (PreservesPullback.iso (AffineScheme.forgetToScheme.op ⋙ Scheme.Γ).rightOp (AffineScheme.ofHom f)
              (AffineScheme.ofHom g)).hom.unop))
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:
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
⊢ IsOpenImmersion iX →
    IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
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
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f ↔
    ∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), P (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))

Tactic:
by
  simp [affineLocally_iff_affineOpens_le, Scheme.affineOpens]

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

Goal state before:
pp: case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯) →
    ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

pp: case mpr
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)) →
    ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯

Tactic:
· intro H U V
    let g : pullback U.1.ι V.1.ι ⟶ X := pullback.fst _ _ ≫ U.1.ι
    have e := g.isOpenEmbedding.isEmbedding.toHomeomorph
    rw [IsOpenImmersion.range_pullback_to_base_of_left, Scheme.Opens.range_ι, Scheme.Opens.range_ι]
      at e
    rw [isCompact_iff_compactSpace]
    exact @Homeomorph.compactSpace _ _ _ _ (H _ _) e

Goal state after:
case mpr
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)) →
    ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
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 = y ^ n.succ * ↑m' ^ (n + 1)
⊢ x = 0

Tactic:
← mul_pow

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.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
hI : I.height = ↑n
⊢ ∃ p, ∃ (_ : p.IsPrime) (_ : I ≤ p), p.height = ↑n

Tactic:
simp only [Ideal.height, ENat.iInf_eq_natCast_iff] at hI
  rcases hI with ⟨⟨p, ⟨⟨⟨hpp, hIp⟩, _⟩, h⟩, -⟩, -⟩
  exact ⟨p, hpp, hIp, h ▸ p.height_eq_primeHeight⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
K : Ideal R
hK : K ∈ S
e : I ≤ K
this : ¬↑r < ↑(r + 1)
⊢ False

Tactic:
norm_cast at this

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
K : Ideal R
hK : K ∈ S
e : I ≤ K
this : ¬r < r + 1
⊢ False
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case inr
X : Scheme
x : ↥X
hx : closure {x} ∈ irreducibleComponents ↥X
inst✝ : IsReduced X
this :
  ∀ (X : Scheme) (x : ↥X),
    closure {x} ∈ irreducibleComponents ↥X → ∀ [IsReduced X], (∃ R, X = Spec R) → IsField ↑(X.presheaf.stalk x)
hX : ¬∃ R, X = Spec R
⊢ IsField ↑(X.presheaf.stalk x)

Tactic:
obtain ⟨i, x, rfl⟩ := X.affineCover.exists_eq x
    have inst : IsReduced (X.affineCover.X i) := isReduced_of_isOpenImmersion (X.affineCover.f i)
    refine (asIso <| (X.affineCover.f i).stalkMap x).commRingCatIsoToRingEquiv.isField
      (this _ x ?_ ⟨_, rfl⟩)
    rw [(X.affineCover.f i).isOpenEmbedding.closure_eq_preimage_closure_image, Set.image_singleton]
    exact preimage_mem_irreducibleComponents hx (X.affineCover.f i).isOpenEmbedding
      ⟨X.affineCover.f i x, subset_closure rfl, _, rfl⟩

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 ((𝒰.f i) x))

Tactic:
rw [← (IsIso.comp_inv_eq _).mpr (Scheme.Hom.stalkMap_comp (𝒰.f i) f x)]

Goal state after:
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))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
⊢ Hom.opensRange (I.glueDataObjMap ⋯) = I.glueDataObjι V ⁻¹ᵁ (↑V).ι ⁻¹ᵁ X.basicOpen f

Tactic:
let := (Ideal.quotientMap _ _ (I.ideal_le_comap_ideal (X.affineBasicOpen_le f))).toAlgebra
  let f' : Γ(X, V) ⧸ I.ideal V := Ideal.Quotient.mk _ f
  have := I.isLocalization_away (X.affineBasicOpen_le f) f rfl
  ext1
  refine (localization_away_comap_range _ f').trans ?_
  rw [← comap_basicOpen, ← V.2.fromSpec_preimage_basicOpen,
    ← Scheme.Hom.comp_preimage, glueDataObjι_ι]
  rfl

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

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

Tactic:
f.naturality,

Goal state after:
case refine_1.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s x : ↑Γ(Y, ↑U)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))
⊢ x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U ≫ X.presheaf.map ((Opens.map f.base).map (homOfLE ⋯).op.unop).op))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
⊢ Y.evaluation ⟨(ConcreteCategory.hom f.base) ↑x, ⋯⟩ ≫ residueFieldMap f ↑x = f.c.app (op V) ≫ X.evaluation x

Tactic:
by
  dsimp only [LocallyRingedSpace.evaluation,
    LocallyRingedSpace.residueFieldMap]
  rw [Category.assoc]
  ext a
  simp only [CommRingCat.comp_apply]
  erw [IsLocalRing.ResidueField.map_residue]
  rw [LocallyRingedSpace.stalkMap_germ_apply]
  rfl

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
⊢ IsAffineHom (f ≫ g)

Tactic:
constructor
  intro U hU
  rw [Scheme.Hom.comp_base, Opens.map_comp_obj]
  apply IsAffineHom.isAffine_preimage
  apply IsAffineHom.isAffine_preimage
  exact hU

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

Goal state before:
pp: X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Tactic:
intro U V

Goal state after:
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
⊢ IsCompact (↑↑U ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case refine_4
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ IsIso (Scheme.Hom.appTop (X.toSpecΓ ∣_ ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩))

Tactic:
· simp only [Opens.map_top, morphismRestrict_app]
    refine IsIso.comp_isIso' ?_ inferInstance
    convert! isIso_ΓSpec_adjunction_unit_app_basicOpen i.1 using 0
    exact congr(IsIso ((ΓSpec.adjunction.unit.app X).app $(by simp)))

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

Goal state before:
pp: case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y),
    (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty f →
      (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty (f ≫ e.hom)

Tactic:
· intro X Y Z e f ⟨hZ, hf⟩
    simpa [AffineTargetMorphismProperty.toProperty, IsAffine.of_isIso e.inv, hP.cancel_left_isIso]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h.fst
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun X ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x).1
h2 : (pullback.snd f g) z = (↑x).2
⊢ (↑((⇑(ConcreteCategory.hom (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom) ∘
            ⇑(ConcreteCategory.hom (pullbackComparison forget f g)))
          z)).1 =
    (↑x).1

Tactic:
simp only [Function.comp_apply, Types.pullbackIsoPullback_hom_fst]
    rwa [← types_comp_apply (g := pullback.fst _ _), pullbackComparison_comp_fst]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
b : ↥(I.glueDataObj ib)
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) a) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) b)
this : ↑((I.glueDataObjι ia) a) = ↑((I.glueDataObjι ib) b)
f : ↑Γ(X, ↑ia)
g : ↑Γ(X, ↑ib)
hfg : X.basicOpen f = X.basicOpen g
H : ↑((I.glueDataObjι ia) a) ∈ X.basicOpen f
⊢ ↑((I.glueDataObjι ib) b) ∈ X.basicOpen g

Tactic:
← this,

Goal state after:
X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
b : ↥(I.glueDataObj ib)
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) a) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) b)
this : ↑((I.glueDataObjι ia) a) = ↑((I.glueDataObjι ib) b)
f : ↑Γ(X, ↑ia)
g : ↑Γ(X, ↑ib)
hfg : X.basicOpen f = X.basicOpen g
H : ↑((I.glueDataObjι ia) a) ∈ X.basicOpen f
⊢ ↑((I.glueDataObjι ia) a) ∈ X.basicOpen g
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 * y ^ n) • x = x' * ↑a

Tactic:
smul_eq_mul,

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)
⊢ ↑(a * y ^ n) * x = x' * ↑a
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case a.inr
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥V
hx : (coprodMk U V) (Sum.inr x) ∈ coprod.desc f g ⁻¹ᵁ W
⊢ (coprodMk U V) (Sum.inr x) ∈ Scheme.Hom.opensRange i

Tactic:
· replace hx : g x ∈ W := by simpa [← Scheme.Hom.comp_apply] using hx
      exact ⟨coprodMk _ _ (.inr ⟨x, hx⟩), by simp [i, ← Scheme.Hom.comp_apply]⟩

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) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := ⋯
x : S
⊢ ↑s ⊆ ↑(adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support))

Tactic:
intro x hx
    apply Algebra.subset_adjoin
    rw [Finset.coe_union, Finset.coe_union]
    exact Or.inl (Or.inr hx)

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

Goal state before:
pp: X : Scheme
I✝ I J : X.IdealSheafData
h : I ≤ J
⊢ ∀ (x y : J.subschemeCover.openCover.I₀),
    pullback.fst (J.subschemeCover.openCover.f x) (J.subschemeCover.openCover.f y) ≫
        glueDataObjHom h x ≫ I.subschemeCover.f x =
      pullback.snd (J.subschemeCover.openCover.f x) (J.subschemeCover.openCover.f y) ≫
        glueDataObjHom h y ≫ I.subschemeCover.f y

Tactic:
intro U V

Goal state after:
X : Scheme
I✝ I J : X.IdealSheafData
h : I ≤ J
U V : J.subschemeCover.openCover.I₀
⊢ pullback.fst (J.subschemeCover.openCover.f U) (J.subschemeCover.openCover.f V) ≫
      glueDataObjHom h U ≫ I.subschemeCover.f U =
    pullback.snd (J.subschemeCover.openCover.f U) (J.subschemeCover.openCover.f V) ≫
      glueDataObjHom h V ≫ I.subschemeCover.f V
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U✝ : ↑Y.affineOpens
U : (Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).I₀
⊢ (ker f).ideal U ≤
    RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso Γ(Y, ↑U)).inv ≫ appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)))

Tactic:
by exact ideal_ker_le_ker_ΓSpecIso_inv_comp f U

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
⊢ ∀ (x y : (Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).I₀),
    pullback.fst ((Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f x)
          ((Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f y) ≫
        liftQuotient (pullback.snd f (↑x).ι ≫ (↑x).toSpecΓ) ((ker f).ideal x) ⋯ ≫ (ker f).subschemeCover.f x =
      pullback.snd ((Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f x)
          ((Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f y) ≫
        liftQuotient (pullback.snd f (↑y).ι ≫ (↑y).toSpecΓ) ((ker f).ideal y) ⋯ ≫ (ker f).subschemeCover.f y

Tactic:
intro U V

Goal state after:
X Y : Scheme
f : X ⟶ Y
U✝ : ↑Y.affineOpens
U V : (Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).I₀
⊢ pullback.fst ((Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f U)
        ((Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f V) ≫
      liftQuotient (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ) ((ker f).ideal U) ⋯ ≫ (ker f).subschemeCover.f U =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f U)
        ((Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f V) ≫
      liftQuotient (pullback.snd f (↑V).ι ≫ (↑V).toSpecΓ) ((ker f).ideal V) ⋯ ≫ (ker f).subschemeCover.f V
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
⊢ IsIso Y.kerAdjunction.rightOp.counit

Tactic:
by
    simp [NatTrans.isIso_iff_isIso_app, CategoryTheory.instIsIsoEqToHom]

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

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ TopologicalSpace.Closeds.closure (⇑f '' ↑Z) ≤ (Hom.ker ((vanishingIdeal Z).subschemeι ≫ f)).support

Tactic:
TopologicalSpace.Closeds.closure_le

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ ⇑f '' ↑Z ⊆ ↑(Hom.ker ((vanishingIdeal Z).subschemeι ≫ f)).support
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: case h₂
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], (algebraMap R T).FinitePresentation → (algebraMap S (S ⊗[R] T)).FinitePresentation

Tactic:
· simp only [finitePresentation_algebraMap]
    intros
    infer_instance

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

Goal state before:
pp: R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Algebra.FinitePresentation R S

Tactic:
exact IsLocalization.Away.finitePresentation r

Goal state after: