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

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 ↦ IsAffine X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯) →
    ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)

pp: case mpr
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (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 ↦ IsAffine X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯

Tactic:
·

Goal state after:
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 ↦ IsAffine X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯) →
    ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: case refine_3
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
⊢ (algebraMap S (Localization.Away ↑r)) x ∈ adjoin R ↑(t r)

Tactic:
·

Goal state after:
case refine_3
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
⊢ (algebraMap S (Localization.Away ↑r)) x ∈ adjoin R ↑(t r)
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: case h
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 := ⋯
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 := ⋯
⊢ adjoin R ↑(s.attach.biUnion sf) = ⊤

Tactic:
convert! (Algebra.adjoin_attach_biUnion (R := R) sf).trans _

Goal state after:
case h.convert_2
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, adjoin R ↑(sf x) = ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case mpr
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (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 ↦ IsAffine X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯

Tactic:
·

Goal state after:
case mpr
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (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 ↦ IsAffine X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
Module: Mathlib.RingTheory.RingHom.FiniteType

Goal state before:
pp: ⊢ RespectsIso @FiniteType

Tactic:
refine finiteType_stableUnderComposition.respectsIso (fun {R S} _ _ e ↦ ?_)
  algebraize [e.toRingHom]
  apply Algebra.FiniteType.equiv (inferInstanceAs <| Algebra.FiniteType R R) <|
    .ofRingEquiv (congrFun rfl)

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

Goal state before:
pp: case h₁
⊢ RespectsIso @FiniteType

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

Tactic:
·

Goal state after:
case h₁
⊢ RespectsIso @FiniteType
Module: Mathlib.RingTheory.RingHom.FiniteType

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

Tactic:
·

Goal state after:
case h₂
⊢ ∀ ⦃R S T : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], (algebraMap R T).FiniteType → (algebraMap S (S ⊗[R] T)).FiniteType
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace ↥Y], (∃ S, Y = Spec S) → JacobsonSpace ↥X
hY : ¬∃ S, Y = Spec S
⊢ JacobsonSpace ↥X

pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥Y
hY : ∃ S, Y = Spec S
⊢ JacobsonSpace ↥X

Tactic:
·

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace ↥Y], (∃ S, Y = Spec S) → JacobsonSpace ↥X
hY : ¬∃ S, Y = Spec S
⊢ JacobsonSpace ↥X
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝³ : LocallyOfFiniteType f
inst✝² : JacobsonSpace ↥Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace ↥Y], (∃ S, Y = Spec S) → JacobsonSpace ↥X
hY : ¬∃ S, Y = Spec S
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
inst✝¹ : LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)
inst✝ : JacobsonSpace ↥Y
inst : JacobsonSpace ↥(Y.affineCover.X i)
e : ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i) ≃ₜ
  ↑(Set.range ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i)) :=
  ⋯.toHomeomorph
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i))

Tactic:
have := this (Y.affineCover.pullbackHom f i) ⟨_, rfl⟩

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝³ : LocallyOfFiniteType f
inst✝² : JacobsonSpace ↥Y
this✝ : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace ↥Y], (∃ S, Y = Spec S) → JacobsonSpace ↥X
hY : ¬∃ S, Y = Spec S
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
inst✝¹ : LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)
inst✝ : JacobsonSpace ↥Y
inst : JacobsonSpace ↥(Y.affineCover.X i)
e : ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i) ≃ₜ
  ↑(Set.range ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i)) :=
  ⋯.toHomeomorph
this : JacobsonSpace ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i))
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
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
e : Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) ≅ Γ(U, f ⁻¹ᵁ W) ⨯ Γ(V, g ⁻¹ᵁ W) :=
  Scheme.coprodPresheafObjIso (Limits.coprod.desc f g ⁻¹ᵁ W) ≪≫
    Limits.prod.mapIso (Functor.mapIso U.presheaf (eqToIso ⋯).op) (Functor.mapIso V.presheaf (eqToIso ⋯).op)
this :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S × T),
    Q ((RingHom.fst S T).comp f) → Q ((RingHom.snd S T).comp f) → Q f
⊢ Q
    ((RingHom.snd ↑Γ(U, f ⁻¹ᵁ W) ↑Γ(V, g ⁻¹ᵁ W)).comp
      (CommRingCat.Hom.hom
        ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
          ((Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W))).conePointUniqueUpToIso
              (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))).hom)))

Tactic:
·

Goal state after:
case refine_2
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
e : Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) ≅ Γ(U, f ⁻¹ᵁ W) ⨯ Γ(V, g ⁻¹ᵁ W) :=
  Scheme.coprodPresheafObjIso (Limits.coprod.desc f g ⁻¹ᵁ W) ≪≫
    Limits.prod.mapIso (Functor.mapIso U.presheaf (eqToIso ⋯).op) (Functor.mapIso V.presheaf (eqToIso ⋯).op)
this :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S × T),
    Q ((RingHom.fst S T).comp f) → Q ((RingHom.snd S T).comp f) → Q f
⊢ Q
    ((RingHom.snd ↑Γ(U, f ⁻¹ᵁ W) ↑Γ(V, g ⁻¹ᵁ W)).comp
      (CommRingCat.Hom.hom
        ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
          ((Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W))).conePointUniqueUpToIso
              (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))).hom)))
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥(Spec R)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace ↥(Spec R)],
    (∃ S, X = Spec S) → JacobsonSpace ↥X
hX : ¬∃ S, X = Spec S
⊢ JacobsonSpace ↥X

pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥(Spec R)
hX : ∃ S, X = Spec S
⊢ JacobsonSpace ↥X

Tactic:
·

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥(Spec R)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace ↥(Spec R)],
    (∃ S, X = Spec S) → JacobsonSpace ↥X
hX : ¬∃ S, X = Spec S
⊢ JacobsonSpace ↥X
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case refine_1
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} F.essImage

pp: case refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
⊢ ∀ (Y : CommRingCatᵒᵖ), ObjectProperty.EssentiallySmall.{u, u, u + 1} fun x ↦ Nonempty (F.obj x ≅ Y)

Tactic:
·

Goal state after:
case refine_1
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} F.essImage
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case refine_1.refine_1
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat := fun S ↦ ∃ R ∈ Set.range fun U ↦ Γ(X, U), ∃ f, (CommRingCat.Hom.hom f).FiniteType
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
S : P.CostructuredArrow ⊤ Scheme.Spec X
f : ↥(Spec (unop (F.obj S))) → ↑(unop (F.obj S))
hqf : ∀ (q : ↥(Spec (unop (F.obj S)))), q ∈ PrimeSpectrum.basicOpen (f q)
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ ⨆ i, PrimeSpectrum.basicOpen (f i) = ⊤

pp: case refine_1.refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat := fun S ↦ ∃ R ∈ Set.range fun U ↦ Γ(X, U), ∃ f, (CommRingCat.Hom.hom f).FiniteType
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
S : P.CostructuredArrow ⊤ Scheme.Spec X
f : ↥(Spec (unop (F.obj S))) → ↑(unop (F.obj S))
hqf : ∀ (q : ↥(Spec (unop (F.obj S)))), q ∈ PrimeSpectrum.basicOpen (f q)
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ ∀ (i : ↥(Spec (unop (F.obj S)))), Q'.isoClosure (CommRingCat.of (Localization.Away (f i)))

Tactic:
·

Goal state after:
case refine_1.refine_1
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat := fun S ↦ ∃ R ∈ Set.range fun U ↦ Γ(X, U), ∃ f, (CommRingCat.Hom.hom f).FiniteType
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
S : P.CostructuredArrow ⊤ Scheme.Spec X
f : ↥(Spec (unop (F.obj S))) → ↑(unop (F.obj S))
hqf : ∀ (q : ↥(Spec (unop (F.obj S)))), q ∈ PrimeSpectrum.basicOpen (f q)
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ ⨆ i, PrimeSpectrum.basicOpen (f i) = ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case refine_1.refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat := fun S ↦ ∃ R ∈ Set.range fun U ↦ Γ(X, U), ∃ f, (CommRingCat.Hom.hom f).FiniteType
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
S : P.CostructuredArrow ⊤ Scheme.Spec X
f : ↥(Spec (unop (F.obj S))) → ↑(unop (F.obj S))
hqf : ∀ (q : ↥(Spec (unop (F.obj S)))), q ∈ PrimeSpectrum.basicOpen (f q)
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ ∀ (i : ↥(Spec (unop (F.obj S)))), Q'.isoClosure (CommRingCat.of (Localization.Away (f i)))

Tactic:
·

Goal state after:
case refine_1.refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat := fun S ↦ ∃ R ∈ Set.range fun U ↦ Γ(X, U), ∃ f, (CommRingCat.Hom.hom f).FiniteType
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
S : P.CostructuredArrow ⊤ Scheme.Spec X
f : ↥(Spec (unop (F.obj S))) → ↑(unop (F.obj S))
hqf : ∀ (q : ↥(Spec (unop (F.obj S)))), q ∈ PrimeSpectrum.basicOpen (f q)
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ ∀ (i : ↥(Spec (unop (F.obj S)))), Q'.isoClosure (CommRingCat.of (Localization.Away (f i)))
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
⊢ ∀ (Y : CommRingCatᵒᵖ), ObjectProperty.EssentiallySmall.{u, u, u + 1} fun x ↦ Nonempty (F.obj x ≅ Y)

Tactic:
·

Goal state after:
case refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
⊢ ∀ (Y : CommRingCatᵒᵖ), ObjectProperty.EssentiallySmall.{u, u, u + 1} fun x ↦ Nonempty (F.obj x ≅ Y)
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case refine_2.refine_1
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
R : CommRingCatᵒᵖ
S : P.CostructuredArrow ⊤ Scheme.Spec X
x✝ : (fun x ↦ Nonempty (F.obj x ≅ R)) S
e : F.obj S ≅ R
⊢ Scheme.Spec.map e.hom ≫
      (MorphismProperty.CostructuredArrow.mk ⊤ ↑⟨Spec.map e.inv.unop ≫ S.hom, ?refine_2.refine_2⟩ ⋯).hom =
    S.hom

pp: case refine_2.refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
R : CommRingCatᵒᵖ
S : P.CostructuredArrow ⊤ Scheme.Spec X
x✝ : (fun x ↦ Nonempty (F.obj x ≅ R)) S
e : F.obj S ≅ R
⊢ P (Spec.map e.inv.unop ≫ S.hom)

Tactic:
·

Goal state after:
case refine_2.refine_1
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
R : CommRingCatᵒᵖ
S : P.CostructuredArrow ⊤ Scheme.Spec X
x✝ : (fun x ↦ Nonempty (F.obj x ≅ R)) S
e : F.obj S ≅ R
⊢ Scheme.Spec.map e.hom ≫
      (MorphismProperty.CostructuredArrow.mk ⊤ ↑⟨Spec.map e.inv.unop ≫ S.hom, ?refine_2.refine_2⟩ ⋯).hom =
    S.hom
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case refine_2.refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
R : CommRingCatᵒᵖ
S : P.CostructuredArrow ⊤ Scheme.Spec X
x✝ : (fun x ↦ Nonempty (F.obj x ≅ R)) S
e : F.obj S ≅ R
⊢ P (Spec.map e.inv.unop ≫ S.hom)

Tactic:
·

Goal state after:
case refine_2.refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
R : CommRingCatᵒᵖ
S : P.CostructuredArrow ⊤ Scheme.Spec X
x✝ : (fun x ↦ Nonempty (F.obj x ≅ R)) S
e : F.obj S ≅ R
⊢ P (Spec.map e.inv.unop ≫ S.hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this✝ : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph ⇑(Scheme.Hom.toImage f)
⊢ (MorphismProperty.isomorphisms TopCat).inverseImage Scheme.forgetToTop (Scheme.Hom.toImage f)

pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this✝ : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph ⇑(Scheme.Hom.toImage f)
⊢ stalkwise (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Bijective ⇑f) (Scheme.Hom.toImage f)

Tactic:
·

Goal state after:
case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this✝ : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph ⇑(Scheme.Hom.toImage f)
⊢ (MorphismProperty.isomorphisms TopCat).inverseImage Scheme.forgetToTop (Scheme.Hom.toImage f)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this✝ : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph ⇑(Scheme.Hom.toImage f)
⊢ stalkwise (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Bijective ⇑f) (Scheme.Hom.toImage f)

Tactic:
·

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this✝ : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph ⇑(Scheme.Hom.toImage f)
⊢ stalkwise (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Bijective ⇑f) (Scheme.Hom.toImage f)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: case mp
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
⊢ J ≤ I.map f → J.comap f ≤ I

pp: case mpr
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
⊢ J.comap f ≤ I → J ≤ I.map f

Tactic:
·

Goal state after:
case mp
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
⊢ J ≤ I.map f → J.comap f ≤ I
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: case mpr
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
⊢ J.comap f ≤ I → J ≤ I.map f

Tactic:
·

Goal state after:
case mpr
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
⊢ J.comap f ≤ I → J ≤ I.map f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: case a
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ I.map (f ≫ g) ≤ (I.map f).map g

pp: case a
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ (I.map f).map g ≤ I.map (f ≫ g)

Tactic:
·

Goal state after:
case a
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ I.map (f ≫ g) ≤ (I.map f).map g
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: case a
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ (I.map f).map g ≤ I.map (f ≫ g)

Tactic:
·

Goal state after:
case a
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ (I.map f).map g ≤ I.map (f ≫ g)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ (vanishingIdeal Z).map f ≤ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' ↑Z))

pp: case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' ↑Z)) ≤ (vanishingIdeal Z).map f

Tactic:
·

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ (vanishingIdeal Z).map f ≤ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' ↑Z))