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

Goal state before:
pp: case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : ↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f)),
    X.basicOpen s = ⊥ →
      ∀ (x : ↥X) (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
        (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx)) s = 0
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) (f x) ⋯)) s = 0

Tactic:
have := isReduced_of_isOpenImmersion f

Goal state after:
case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : ↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f)),
    X.basicOpen s = ⊥ →
      ∀ (x : ↥X) (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
        (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx)) s = 0
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) (f x) ⋯)) s = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : ↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f)),
    X.basicOpen s = ⊥ →
      ∀ (x : ↥X) (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
        (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx)) s = 0
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
⊢ f ⁻¹ᵁ ⊥ = ⊥

Tactic:
ext1

Goal state after:
case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : ↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f)),
    X.basicOpen s = ⊥ →
      ∀ (x : ↥X) (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
        (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx)) s = 0
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
⊢ ↑(f ⁻¹ᵁ ⊥) = ↑⊥
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
x : ↥X
⊢ x ∈ ⊥ ↔ x ∈ ⋂ U, X.zeroLocus ↑(⊤ U)

Tactic:
simpa using X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

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

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
⊢ (∃ a, f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U) ↔ (∃ a, f ^ a * x ∈ I.ideal U) ∧ ∃ a, f ^ a * x ∈ J.ideal U

Tactic:
refine ⟨fun ⟨n, h₁, h₂⟩ ↦ ⟨⟨n, h₁⟩, ⟨n, h₂⟩⟩, ?_⟩

Goal state after:
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
⊢ ((∃ a, f ^ a * x ∈ I.ideal U) ∧ ∃ a, f ^ a * x ∈ J.ideal U) → ∃ a, f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U
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
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
hXY : ∃ R S, Y = Spec R ∧ X = Spec S
⊢ P f

Tactic:
obtain ⟨R, S, rfl, rfl⟩ := hXY

Goal state after:
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 : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine (Spec R)
hX : IsAffine (Spec S)
f : Spec S ⟶ Spec R
H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ P f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
this✝ : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f)) :=
  (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯).toAlgebra
f' : ↑Γ(X, ↑V) ⧸ I.ideal V := (Ideal.Quotient.mk (I.ideal V)) f
this :
  IsLocalization.Away ((Ideal.Quotient.mk (I.ideal V)) f)
    (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f))
⊢ Hom.opensRange (I.glueDataObjMap ⋯) = I.glueDataObjι V ⁻¹ᵁ (↑V).ι ⁻¹ᵁ X.basicOpen f

Tactic:
ext1

Goal state after:
X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
this✝ : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f)) := ⋯
f' : ↑Γ(X, ↑V) ⧸ I.ideal V := ⋯
this :
  IsLocalization.Away ((Ideal.Quotient.mk (I.ideal V)) f)
    (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f))
⊢ ↑(Hom.opensRange (I.glueDataObjMap ⋯)) = ↑(I.glueDataObjι V ⁻¹ᵁ (↑V).ι ⁻¹ᵁ X.basicOpen f)
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
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
hXY : ∃ R S, Y = Spec R ∧ X = Spec S
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
obtain ⟨R, S, rfl, rfl⟩ := hXY

Goal state after:
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
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
R S : CommRingCat
hY : IsAffine (Spec R)
x : ↥(Spec S)
hX : IsAffine (Spec S)
f : Spec S ⟶ Spec R
hf : P f
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case mpr
X : Scheme
x y : ↥X
⊢ y ∈ {y | y ⤳ x} → y ∈ Set.range ⇑(X.fromSpecStalk x)

Tactic:
· rintro (hy : y ⤳ x)
    have := fromSpecStalk_closedPoint (x := y)
    rw [← SpecMap_stalkSpecializes_fromSpecStalk hy] at this
    exact ⟨_, this⟩

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

Goal state before:
pp: X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
r : ↑Γ(X, ⊤)
U : X.Opens
hU : IsAffineOpen U
⊢ (X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U = U ⊓ X.basicOpen r

Tactic:
ext1

Goal state after:
X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
r : ↑Γ(X, ⊤)
U : X.Opens
hU : IsAffineOpen U
⊢ ↑((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U) = ↑(U ⊓ X.basicOpen r)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
        (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯ ≫
      pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
        (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)) =
    pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
        (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
      I.glueDataT i j

Tactic:
by
    apply pullback.hom_ext
    · rw [← cancel_mono (glueDataObjι _ _)]
      simp
    · rw [← cancel_mono (Scheme.Opens.ι _)]
      simp [pullback.condition_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mp.right
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
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✝ : Mono i₃
t : ↥(pullback f g)
⊢ (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) t ∈ ⇑(pullback.snd f' g') ⁻¹' Set.range ⇑i₂

Tactic:
use pullback.snd f g t

Goal state after:
case h
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
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✝ : Mono i₃
t : ↥(pullback f g)
⊢ i₂ ((pullback.snd f g) t) = (pullback.snd f' g') ((pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) t)
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
hmem : ∀ (W : ↑X.affineOpens) (hW : W = X.affineBasicOpen g), b ∈ Set.range ⇑(I.glueDataObjMap ⋯)
⊢ (I.glueData.ι ia) a = (I.glueData.ι ib) b

Tactic:
obtain ⟨a, rfl⟩ := (I.opensRange_glueDataObjMap f).ge H

Goal state after:
X : Scheme
I : X.IdealSheafData
ia ib : I.glueData.J
b : ↥(I.glueDataObj ib)
f : ↑Γ(X, ↑ia)
g : ↑Γ(X, ↑ib)
hfg : X.basicOpen f = X.basicOpen g
hmem : ∀ (W : ↑X.affineOpens) (hW : W = X.affineBasicOpen g), b ∈ Set.range ⇑(I.glueDataObjMap ⋯)
a : ↥(I.glueDataObj (X.affineBasicOpen f))
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) ((I.glueDataObjMap ⋯) a)) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) b)
this : ↑((I.glueDataObjι ia) ((I.glueDataObjMap ⋯) a)) = ↑((I.glueDataObjι ib) b)
H : ↑((I.glueDataObjι ia) ((I.glueDataObjMap ⋯) a)) ∈ X.basicOpen f
⊢ (I.glueData.ι ia) ((I.glueDataObjMap ⋯) a) = (I.glueData.ι ib) b
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
ia ib : I.glueData.J
b : ↥(I.glueDataObj ib)
f : ↑Γ(X, ↑ia)
g : ↑Γ(X, ↑ib)
hfg : X.basicOpen f = X.basicOpen g
hmem : ∀ (W : ↑X.affineOpens) (hW : W = X.affineBasicOpen g), b ∈ Set.range ⇑(I.glueDataObjMap ⋯)
a : ↥(I.glueDataObj (X.affineBasicOpen f))
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) ((I.glueDataObjMap ⋯) a)) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) b)
this : ↑((I.glueDataObjι ia) ((I.glueDataObjMap ⋯) a)) = ↑((I.glueDataObjι ib) b)
H : ↑((I.glueDataObjι ia) ((I.glueDataObjMap ⋯) a)) ∈ X.basicOpen f
⊢ (I.glueData.ι ia) ((I.glueDataObjMap ⋯) a) = (I.glueData.ι ib) b

Tactic:
obtain ⟨b, rfl⟩ := hmem (X.affineBasicOpen f) (Subtype.ext hfg)

Goal state after:
X : Scheme
I : X.IdealSheafData
ia ib : I.glueData.J
f : ↑Γ(X, ↑ia)
g : ↑Γ(X, ↑ib)
hfg : X.basicOpen f = X.basicOpen g
a : ↥(I.glueDataObj (X.affineBasicOpen f))
H : ↑((I.glueDataObjι ia) ((I.glueDataObjMap ⋯) a)) ∈ X.basicOpen f
b : ↥(I.glueDataObj (X.affineBasicOpen f))
hmem : ∀ (W : ↑X.affineOpens) (hW : W = X.affineBasicOpen g), (I.glueDataObjMap ⋯) b ∈ Set.range ⇑(I.glueDataObjMap ⋯)
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) ((I.glueDataObjMap ⋯) a)) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) ((I.glueDataObjMap ⋯) b))
this : ↑((I.glueDataObjι ia) ((I.glueDataObjMap ⋯) a)) = ↑((I.glueDataObjι ib) ((I.glueDataObjMap ⋯) b))
⊢ (I.glueData.ι ia) ((I.glueDataObjMap ⋯) a) = (I.glueData.ι ib) ((I.glueDataObjMap ⋯) b)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Hom.opensRange (I.glueData.ι U ≫ I.subschemeIso.inv) = I.subschemeι ⁻¹ᵁ ↑U

Tactic:
ext1

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ↑(Hom.opensRange (I.glueData.ι U ≫ I.subschemeIso.inv)) = ↑(I.subschemeι ⁻¹ᵁ ↑U)
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))

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
⊢ ∀ (i : ↑↑s), l i ∈ adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

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
⊢ ∀ (r : ↑↑s), ∃ n, ↑r ^ n • x ∈ 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:
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
⊢ ∀ (i : ↑↑s), l i ∈ adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

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
⊢ ∀ (r : ↑↑s), ∃ n, ↑r ^ n • x ∈ adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
f : R ⟶ S
⊢ P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)

Tactic:
have := RingHom.toMorphismProperty_respectsIso_iff.mp hQi
  rw [HasAffineProperty.iff_of_isAffine (P := P), affineAnd, and_iff_right]
  exacts [MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty Q)
    (arrowIsoΓSpecOfIsAffine f).symm, inferInstance]

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

Goal state before:
pp: X Y✝ : Scheme
f : X ⟶ Y✝
U : ↑Y✝.affineOpens
Y : Scheme
x✝² x✝¹ : (Over Y)ᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).map x✝ ≫
        (Over.homMk (Hom.toImage (Opposite.unop x✝¹).hom) ⋯).op).unop =
    ((Over.homMk (Hom.toImage (Opposite.unop x✝²).hom) ⋯).op ≫ (𝟭 (Over Y)ᵒᵖ).map x✝).unop

Tactic:
ext1

Goal state after:
X Y✝ : Scheme
f : X ⟶ Y✝
U : ↑Y✝.affineOpens
Y : Scheme
x✝² x✝¹ : (Over Y)ᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ Over.Hom.left
      ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).map x✝ ≫
          (Over.homMk (Hom.toImage (Opposite.unop x✝¹).hom) ⋯).op).unop =
    Over.Hom.left ((Over.homMk (Hom.toImage (Opposite.unop x✝²).hom) ⋯).op ≫ (𝟭 (Over Y)ᵒᵖ).map x✝).unop
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y✝ : Scheme
f : X ⟶ Y✝
U : ↑Y✝.affineOpens
Y : Scheme
I : Y.IdealSheafData
⊢ ((subschemeFunctor Y).rightOp.map ({ app := fun I ↦ eqToHom ⋯, naturality := ⋯ }.app I) ≫
        { app := fun f ↦ (Over.homMk (Hom.toImage (Opposite.unop f).hom) ⋯).op, naturality := ⋯ }.app
          ((subschemeFunctor Y).rightOp.obj I)).unop =
    (𝟙 ((subschemeFunctor Y).rightOp.obj I)).unop

Tactic:
ext1

Goal state after:
X Y✝ : Scheme
f : X ⟶ Y✝
U : ↑Y✝.affineOpens
Y : Scheme
I : Y.IdealSheafData
⊢ Over.Hom.left
      ((subschemeFunctor Y).rightOp.map ({ app := fun I ↦ eqToHom ⋯, naturality := ⋯ }.app I) ≫
          { app := fun f ↦ (Over.homMk (Hom.toImage (Opposite.unop f).hom) ⋯).op, naturality := ⋯ }.app
            ((subschemeFunctor Y).rightOp.obj I)).unop =
    Over.Hom.left (𝟙 ((subschemeFunctor Y).rightOp.obj I)).unop
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V₁ : X.Opens
hV₁ : V₁ ≤ f ⁻¹ᵁ U
V₂ : X.Opens
hV₂ : V₂ ≤ f ⁻¹ᵁ U
⊢ IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (f ⁻¹ᵁ U ⊓ (V₁ ⊓ V₂)) ↔
    IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)

Tactic:
inf_eq_right.mpr (inf_le_left.trans hV₁)

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V₁ : X.Opens
hV₁ : V₁ ≤ f ⁻¹ᵁ U
V₂ : X.Opens
hV₂ : V₂ ≤ f ⁻¹ᵁ U
⊢ IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂) ↔
    IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ (I.comap f).support = I.support.preimage ⋯

Tactic:
ext1

Goal state after:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ ↑(I.comap f).support = ↑(I.support.preimage ⋯)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst✝ : IsClosedImmersion i
⊢ Hom.ker (pullback.fst f i) = (Hom.ker i).comap f

Tactic:
by
  delta IdealSheafData.comap
  rw [← Hom.ker_comp_of_isIso (pullback.map f i f i.imageι (𝟙 _) (i.toImage) (𝟙 _)
    (by simp) (by simp)), pullback.lift_fst, Category.comp_id]

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

Goal state before:
pp: X : Scheme
X✝ Y✝ Z✝ : X.IdealSheafData
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (MorphismProperty.Over.homMk (Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op.unop =
    ((MorphismProperty.Over.homMk (Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op ≫
        (MorphismProperty.Over.homMk (Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op).unop

Tactic:
ext1

Goal state after:
X : Scheme
X✝ Y✝ Z✝ : X.IdealSheafData
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (MorphismProperty.Over.homMk (Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op.unop.left =
    ((MorphismProperty.Over.homMk (Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op ≫
          (MorphismProperty.Over.homMk (Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op).unop.left
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X✝ : Scheme
X Y : (MorphismProperty.Over @IsClosedImmersion ⊤ X✝)ᵒᵖ
f : X ⟶ Y
⊢ ((𝟭 (MorphismProperty.Over @IsClosedImmersion ⊤ X✝)ᵒᵖ).map f ≫
        (MorphismProperty.Over.isoMk (asIso (Scheme.Hom.toImage (unop Y).hom)).symm ⋯).op.hom).unop =
    ((MorphismProperty.Over.isoMk (asIso (Scheme.Hom.toImage (unop X).hom)).symm ⋯).op.hom ≫
        (((MorphismProperty.Over.forget @IsClosedImmersion ⊤ X✝).op ⋙ X✝.kerFunctor) ⋙
              { obj := fun I ↦ op (MorphismProperty.Over.mk ⊤ I.subschemeι ⋯),
                map := fun {I J} h ↦ (MorphismProperty.Over.homMk (Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op,
                map_id := ⋯, map_comp := ⋯ }).map
          f).unop

Tactic:
ext1

Goal state after:
X✝ : Scheme
X Y : (MorphismProperty.Over @IsClosedImmersion ⊤ X✝)ᵒᵖ
f : X ⟶ Y
⊢ ((𝟭 (MorphismProperty.Over @IsClosedImmersion ⊤ X✝)ᵒᵖ).map f ≫
          (MorphismProperty.Over.isoMk (asIso (Scheme.Hom.toImage (unop Y).hom)).symm ⋯).op.hom).unop.left =
    ((MorphismProperty.Over.isoMk (asIso (Scheme.Hom.toImage (unop X).hom)).symm ⋯).op.hom ≫
          (((MorphismProperty.Over.forget @IsClosedImmersion ⊤ X✝).op ⋙ X✝.kerFunctor) ⋙
                { obj := fun I ↦ op (MorphismProperty.Over.mk ⊤ I.subschemeι ⋯),
                  map := fun {I J} h ↦ (MorphismProperty.Over.homMk (Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op,
                  map_id := ⋯, map_comp := ⋯ }).map
            f).unop.left
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ (I.map f).support = TopologicalSpace.Closeds.closure (⇑f '' ↑I.support)

Tactic:
ext1

Goal state after:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ ↑(I.map f).support = ↑(TopologicalSpace.Closeds.closure (⇑f '' ↑I.support))
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
H : IsConstructible s
⊢ ∃ S, S.toSet = s

Tactic:
induction s, H using IsConstructible.induction_of_isTopologicalBasis
      _ (isTopologicalBasis_basic_opens (R := R)) with

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

Goal state before:
pp: case e'_3
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z
S : Scheme
X Y : Over S
inst✝ : IsSeparated Y.hom
f g : X ⟶ Y
e_1✝ : (Over.forget S).obj Y = Y.left
⊢ (Over.forget S).map (prod.lift (𝟙 Y) (𝟙 Y)) ≫ (Y.prodLeftIsoPullback Y).hom = pullback.diagonal Y.hom

Tactic:
ext1

Goal state after:
case e'_3.h₀
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z
S : Scheme
X Y : Over S
inst✝ : IsSeparated Y.hom
f g : X ⟶ Y
e_1✝ : (Over.forget S).obj Y = Y.left
⊢ ((Over.forget S).map (prod.lift (𝟙 Y) (𝟙 Y)) ≫ (Y.prodLeftIsoPullback Y).hom) ≫ pullback.fst Y.hom Y.hom =
    pullback.diagonal Y.hom ≫ pullback.fst Y.hom Y.hom

case h₁
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z
S : Scheme
X Y : Over S
inst✝ : IsSeparated Y.hom
f g : X ⟶ Y
e_1✝ : (Over.forget S).obj Y = Y.left
⊢ ((Over.forget S).map (prod.lift (𝟙 Y) (𝟙 Y)) ≫ (Y.prodLeftIsoPullback Y).hom) ≫ pullback.snd Y.hom Y.hom =
    pullback.diagonal Y.hom ≫ pullback.snd Y.hom Y.hom
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this : IsSeparated Y'.hom
⊢ ι' ≫ f' = ι' ≫ g'

Tactic:
ext1

Goal state after:
W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := ⋯
Y' : Over Z := ⋯
U' : Over Z := ⋯
f' : X' ⟶ Y' := ⋯
g' : X' ⟶ Y' := ⋯
ι' : U' ⟶ X' := ⋯
this : IsSeparated Y'.hom
⊢ Over.Hom.left (ι' ≫ f') = Over.Hom.left (ι' ≫ g')
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr.hS'
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hCNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
fS : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
i : 𝒰.I₀
⊢ IsNoetherianRing ↑Γ(X, ↑(fS i))

Tactic:
apply isNoetherianRing_of_ringEquiv (R := Γ(𝒰.X i, ⊤))

Goal state after:
case mpr.hS'
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hCNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
fS : 𝒰.I₀ → ↑X.affineOpens := ⋯
i : 𝒰.I₀
⊢ ↑Γ(𝒰.X i, ⊤) ≃+* ↑Γ(X, ↑(fS i))