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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(f ⁻¹ᵁ U)
U' : Set ↥Y
hU' : IsOpen U'
e : ⇑f ⁻¹' U' = V.carrier
⊢ ↑(f ⁻¹ᵁ ({ carrier := U', is_open' := hU' } ⊓ U)) = ↑V

Tactic:
by

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

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
h : I ≤ J
U : ↑X.affineOpens
⊢ glueDataObjHom h U ≫ I.glueDataObjι U = J.glueDataObjι U

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(f ⁻¹ᵁ U)
⊢ ∃ U' ≤ U, f ⁻¹ᵁ U' = V

Tactic:
by

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ glueDataObjHom ⋯ U = 𝟙 (I.glueDataObj U)

Tactic:
by

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

Goal state before:
pp: X : Scheme
I J K : X.IdealSheafData
hIJ : I ≤ J
hJK : J ≤ K
U : ↑X.affineOpens
⊢ glueDataObjHom hJK U ≫ glueDataObjHom hIJ U = glueDataObjHom ⋯ U

Tactic:
by

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:
by

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

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
h : I ≤ J
x✝ : J.subschemeCover.openCover.I₀
⊢ J.subschemeCover.openCover.f x✝ ≫ inclusion h ≫ I.subschemeι = J.subschemeCover.openCover.f x✝ ≫ J.subschemeι

Tactic:
by

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 := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
x✝ : Set S
⊢ (∃ n, ↑r ^ n • x ∈ adjoin R x✝) ↔ ∃ m, ↑m • x ∈ adjoin R x✝

Tactic:
by

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

Goal state before:
pp: case neg
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
y : ↥Y
hy : y ∉ Set.range ⇑f
⊢ ∃ U, y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hyU, hU'⟩ :=
      Y.isBasis_affineOpens.exists_subset_of_mem_open hy hf₂.isOpen_compl
    rw [Set.subset_compl_iff_disjoint_right, ← Set.preimage_eq_empty_iff] at hU'
    refine ⟨U, hyU, hU, ?_⟩
    convert isAffineOpen_bot _
    exact Opens.ext hU'

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
⊢ IsAffineHom f

Tactic:
by

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x✝ : I.subschemeCover.openCover.I₀
⊢ I.subschemeCover.openCover.f x✝ ≫ inclusion ⋯ = I.subschemeCover.openCover.f x✝ ≫ 𝟙 I.subscheme

Tactic:
by

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

Goal state before:
pp: X : Scheme
I J K : X.IdealSheafData
h₁ : I ≤ J
h₂ : J ≤ K
x✝ : K.subschemeCover.openCover.I₀
⊢ K.subschemeCover.openCover.f x✝ ≫ inclusion h₂ ≫ inclusion h₁ = K.subschemeCover.openCover.f x✝ ≫ inclusion ⋯

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
⊢ pullback.fst f (↑U).ι ''ᵁ ⊤ = f ⁻¹ᵁ ↑U

Tactic:
by

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

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
h :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
U : Y.Opens
hU : IsAffineOpen U
⊢ ↑⟨f ⁻¹ᵁ U, ⋯⟩ ≤ f ⁻¹ᵁ ↑⟨U, hU⟩

Tactic:
by

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
⊢ Set.range ⇑(V.ι ≫ g) ⊆ Set.range ⇑W.ι

Tactic:
by

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

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) f ↔
    IsAffineHom f ∧ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
by

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

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) =
    @IsAffineHom ⊓ affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q

Tactic:
by

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

Goal state before:
pp: Q W : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQW : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → W f
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) ≤
    targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ W)

Tactic:
intro X Y f h U
  exact ⟨(h U).1, hQW (h U).2⟩

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

Goal state before:
pp: Q W : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQW : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → W f
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) ≤
    targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ W)

Tactic:
by

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) ⋯
⊢ f' ≫ W.ι = U.ι ≫ f

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(pullback f (↑U).ι, ⊤) :=
  Functor.mapIso X.presheaf (eqToIso ⋯).op ≪≫ Hom.appIso (pullback.fst f (↑U).ι) ⊤
⊢ Hom.app f ↑U ≫ e.hom = (ΓSpecIso Γ(Y, ↑U)).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)

Tactic:
by

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) ⋯
⊢ q ≫ W.ι = V.ι ≫ g

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
⊢ (Hom.ker f).ideal U ≤
    RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso Γ(Y, ↑U)).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)))

Tactic:
by

Goal state after:
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
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
⊢ P (f ≫ g)

Tactic:
by

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

Goal state after:
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
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQ : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen (𝟙 X ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app (𝟙 X) U))

Tactic:
exact ⟨hU, hQ _⟩

Goal state after:
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
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQ : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
⊢ P (𝟙 X)

Tactic:
by

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
⊢ IsCompact (↑(pullback.fst f g ⁻¹ᵁ U) ⊓ ↑(pullback.snd f g ⁻¹ᵁ V))

Tactic:
by

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:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ toImageAux f ≫ imageι f = f

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ toImage f ≫ imageι f = f

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ DenseRange ⇑(Hom.toImage f)

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ QuasiCompact (Hom.toImage f ≫ Hom.imageι f)

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
⊢ ⊥.subschemeι ≫ Hom.toImage (𝟙 X) ≫ IdealSheafData.inclusion ⋯ = 𝟙 ⊥.subscheme

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
⊢ (Hom.toImage (𝟙 X) ≫ IdealSheafData.inclusion ⋯) ≫ ⊥.subschemeι = 𝟙 X

Tactic:
by

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
h : IsIso I.subschemeι
⊢ I = ⊥

Tactic:
by

Goal state after:
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
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) ↔
    ∀ {X Y : Scheme} (f : X ⟶ Y),
      P f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
⊢ IsIso (f ∣_ U) ↔ IsIso (Scheme.Hom.app f U)

Tactic:
by

Goal state after:
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
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
⊢ P ≤ @IsAffineHom

Tactic:
by

Goal state after:
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 P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ P = @IsAffineHom ⊓ P'

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
⊢ app (toImage f) (imageι f ⁻¹ᵁ ↑U) =
    ((ker f).subschemeObjIso U).hom ≫
      CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f ↑U)) ⋯)

Tactic:
by

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

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ RingHom.ker (CommRingCat.Hom.hom (app f ↑U)) ≤ (ker f).ideal U

Tactic:
by

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

Goal state before:
pp: Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hP' : HasAffineProperty P' (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q')
hQQ' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → Q' f
⊢ P ≤ P'

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ Function.Injective ⇑(ConcreteCategory.hom (app (toImage f) (imageι f ⁻¹ᵁ ↑U)))

Tactic:
by

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 = ⊤
h : ∀ x ∈ s, FiniteType R (Localization.Away x)
⊢ FiniteType R S

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁] [IsOpenImmersion f₂],
    IsAffine (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
this✝ : IsAffine ↑U
this : IsAffine ↑V
g : pullback U.ι V.ι ⟶ X := pullback.fst U.ι V.ι ≫ U.ι
⊢ X.homOfLE ⋯ ≫ V.ι = X.homOfLE ⋯ ≫ U.ι

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
x : ↥(image f)
⊢ Function.Injective ⇑(ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor CommRingCat x).map (toImage f).c))

Tactic:
by

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

Goal state before:
pp: X Y✝ : Scheme
f : X ⟶ Y✝
U : ↑Y✝.affineOpens
Y : Scheme
I : Y.IdealSheafData
⊢ (𝟭 Y.IdealSheafData).obj I = ((subschemeFunctor Y).rightOp ⋙ Y.kerFunctor).obj I

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁] [IsOpenImmersion f₂],
    IsAffine (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
this✝ : IsAffine ↑U
this : IsAffine ↑V
g : pullback U.ι V.ι ⟶ X := pullback.fst U.ι V.ι ≫ U.ι
⊢ V.ι ⁻¹ᵁ Scheme.Hom.opensRange U.ι = Scheme.Hom.opensRange (X.homOfLE ⋯)

Tactic:
by

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:
by

Goal state after:
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
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this✝ : IsAffineHom f
this : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
⊢ f ⁻¹ᵁ W = Limits.coprod.inl ⁻¹ᵁ Limits.coprod.desc f g ⁻¹ᵁ W

Tactic:
by

Goal state after:
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
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this✝ : IsAffineHom f
this : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
⊢ g ⁻¹ᵁ W = Limits.coprod.inr ⁻¹ᵁ Limits.coprod.desc f g ⁻¹ᵁ W

Tactic:
by

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

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

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

Goal state before:
pp: X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
⊢ IsAffineOpen (Scheme.Hom.opensRange (pullback.fst f₁ f₂ ≫ f₁))

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ AffineTargetMorphismProperty.diagonal (fun X x x_1 x_2 ↦ IsAffine X) f ↔
    ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)

Tactic:
by

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

Goal state before:
pp: ⊢ StableUnderComposition @Finite

Tactic:
by

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

Goal state before:
pp: ⊢ RespectsIso @Finite

Tactic:
by

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

Goal state before:
pp: ⊢ IsStableUnderBaseChange @Finite

Tactic:
by

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

Goal state before:
pp: R S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
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'
hf : f.Finite
this✝³ : Algebra R S := f.toAlgebra
this✝² : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝¹ : Algebra R' S' := f'.toAlgebra
this✝ : IsScalarTower R R' S'
this : IsScalarTower R S S'
⊢ IsLocalization (Algebra.algebraMapSubmonoid S M) S'

Tactic:
by

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

Goal state before:
pp: ⊢ LocalizationPreserves @Finite

Tactic:
by

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 R
hs✝ : Ideal.span s✝ = ⊤
s : Finset R
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away ↑i) (Localization.Away ↑i ⊗[R] S)
f : R →+* S := algebraMap R S
this : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away ↑r ⊗[R] S)
s₂ : ∀ (r : ↥s), adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
t✝ : Set S
r : ↑↑s
⊢ (algebraMap S (Localization.Away ↑r ⊗[R] S)) x ∈ adjoin (Localization.Away ↑r) ↑(s₁ r)

Tactic:
by

Goal state after: