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

Goal state before:
pp: case hs
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : 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
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hf : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
hs :
  Ideal.span (⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) '' ↑s) =
    Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ⊤
⊢ Ideal.span (⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) '' ↑s) = ⊤

Tactic:
Ideal.map_top

Goal state after:
case hs
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : 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
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hf : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
hs : Ideal.span (⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) '' ↑s) = ⊤
⊢ Ideal.span (⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) '' ↑s) = ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case of_basicOpenCover
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS' : ∀ (r : ↥S), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)
hS :
  Ideal.span (⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) '' ↑S) =
    Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ⊤
⊢ IsAffine X

Tactic:
Ideal.map_top

Goal state after:
case of_basicOpenCover
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS' : ∀ (r : ↥S), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)
hS : Ideal.span (⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) '' ↑S) = ⊤
⊢ IsAffine X
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
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) f ↔
    IsAffineHom f ∧ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
targetAffineLocally_affineAnd_iff' hQ.respectsIso

Goal state after:
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
⊢ (IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    IsAffineHom f ∧ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
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
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away ↑r ⊗[R] S)) ((algebraMap R S) ↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ * x) ∈ adjoin R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ↑⟨(fun x ↦ ↑r ^ x) n₂, ⋯⟩ • ↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ • x ∈
    adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, adjoin R ↑(sf x))

Tactic:
smul_smul,

Goal state after:
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
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away ↑r ⊗[R] S)) ((algebraMap R S) ↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ * x) ∈ adjoin R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  (↑⟨(fun x ↦ ↑r ^ x) n₂, ⋯⟩ * ↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩) • x ∈
    adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, adjoin R ↑(sf x))
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : ↥s), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ↑⟨(fun x ↦ ↑r ^ x) n₂, ⋯⟩ • ↑⟨↑r ^ n₁, ⋯⟩ • x ∈
    Submodule.span R
      ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)

Tactic:
smul_smul,

Goal state after:
R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : ↥s), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  (↑⟨(fun x ↦ ↑r ^ x) n₂, ⋯⟩ * ↑⟨↑r ^ n₁, ⋯⟩) • x ∈
    Submodule.span R
      ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
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:
· have : (Limits.coprod.desc f g).app W ≫ e.hom ≫ Limits.prod.snd = g.app W := by
      simp [e, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_comp_appLE]
    convert! (hg W hW).2
    exact congr(($this).1)

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

Goal state before:
pp: X Y Z : Scheme
I : Z.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
e : pullback f (I.comap g).subschemeι ≅ pullback (f ≫ g) I.subschemeι :=
  asIso (pullback.map f (I.comap g).subschemeι f (pullback.fst g I.subschemeι) (𝟙 X) (I.comapIso g).hom (𝟙 Y) ⋯ ⋯) ≪≫
    pullbackRightPullbackFstIso g I.subschemeι f
⊢ I.comap (f ≫ g) = (I.comap g).comap f

Tactic:
rw [comap, comap, ← Scheme.Hom.ker_comp_of_isIso e.hom]

Goal state after:
X Y Z : Scheme
I : Z.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
e : pullback f (I.comap g).subschemeι ≅ pullback (f ≫ g) I.subschemeι :=
  asIso (pullback.map f (I.comap g).subschemeι f (pullback.fst g I.subschemeι) (𝟙 X) (I.comapIso g).hom (𝟙 Y) ⋯ ⋯) ≪≫
    pullbackRightPullbackFstIso g I.subschemeι f
⊢ Hom.ker (e.hom ≫ pullback.fst (f ≫ g) I.subschemeι) = Hom.ker (pullback.fst f (I.comap g).subschemeι)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: ⊢ MorphismProperty.RespectsIso @IsClosedImmersion

Tactic:
apply MorphismProperty.RespectsIso.mk <;> intro X Y Z e f hf

Goal state after:
case hprecomp
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
hf : IsClosedImmersion f
⊢ IsClosedImmersion (e.hom ≫ f)

case hpostcomp
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
hf : IsClosedImmersion f
⊢ IsClosedImmersion (f ≫ e.hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X✝ : Scheme
X Y : (MorphismProperty.Over @IsClosedImmersion ⊤ X✝)ᵒᵖ
f : X ⟶ Y
⊢ inv (Scheme.Hom.toImage (unop Y).hom) ≫ (MorphismProperty.Comma.Hom.hom f.unop).left =
    Scheme.IdealSheafData.inclusion ⋯ ≫ inv (Scheme.Hom.toImage (unop X).hom)

Tactic:
rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq,
        ← cancel_mono (Scheme.IdealSheafData.subschemeι _)]

Goal state after:
X✝ : Scheme
X Y : (MorphismProperty.Over @IsClosedImmersion ⊤ X✝)ᵒᵖ
f : X ⟶ Y
⊢ ((MorphismProperty.Comma.Hom.hom f.unop).left ≫ Scheme.Hom.toImage (unop X).hom) ≫
      (Scheme.Hom.ker (Over.hom (unop X).toComma)).subschemeι =
    (Scheme.Hom.toImage (unop Y).hom ≫ Scheme.IdealSheafData.inclusion ⋯) ≫
      (Scheme.Hom.ker (Over.hom (unop X).toComma)).subschemeι
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ ∀ {f' : Y' ⟶ Y} {g' : Y' ⟶ X}, IsPullback f' g' g f → IsImmersion g → IsImmersion g'

Tactic:
f'

Goal state after:
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
⊢ ∀ {g' : Y' ⟶ X}, IsPullback f' g' g f → IsImmersion g → IsImmersion g'
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
s : ConstructibleSetData R
⊢ (map f s).toSet = comap f ⁻¹' s.toSet

Tactic:
unfold toSet map

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
s : ConstructibleSetData R
⊢ ⋃ C ∈ image (BasicConstructibleSetData.map f) s, C.toSet = comap f ⁻¹' ⋃ C ∈ s, C.toSet
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
inst✝ : P.IsClosedUnderIsomorphisms
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : TopologicalSpace.IsOpenCover U
H : ∀ (i : ι), IsIntegral ↑(U i) → Subsingleton ↥↑(U i) → P ↑(f ⁻¹ᵁ U i)
x✝¹ : IsIntegral Y
x✝ : Subsingleton ↥Y
y : ↥Y
i : ι
hy : y ∈ U i
heq : U i = ⊤
e : ↑(U i) ≅ Y := Y.isoOfEq heq ≪≫ Y.topIso
⊢ f ⁻¹ᵁ U i = ⊤

Tactic:
by simp [heq]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
⊢ ∀ (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → topologically (@IsOpenMap) f'

Tactic:
f'

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
⊢ IsPullback f' i₁ i₂ f → topologically (@IsOpenMap) f'
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField ↑K
inst✝¹ : IsIntegral (Spec K)
inst✝ : Subsingleton ↥(Spec K)
φ : K ⟶ S
T : Scheme
g : T ⟶ Spec K
x✝ : HasPullback g (Spec.map φ)
this :
  ∀ {T : Scheme} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)),
    (∃ R, T = Spec R) → topologically (@IsOpenMap) (pullback.fst g (Spec.map φ))
hT : ¬∃ R, T = Spec R
i : T.affineCover.toPreZeroHypercover.1
⊢ topologically (@IsOpenMap) (Scheme.Cover.pullbackHom T.affineCover (pullback.fst g (Spec.map φ)) i)

Tactic:
refine (MorphismProperty.cancel_left_of_respectsIso _
      ((pullbackRightPullbackFstIso ..).inv ≫ (pullbackSymmetry ..).hom) _).mp ?_

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField ↑K
inst✝¹ : IsIntegral (Spec K)
inst✝ : Subsingleton ↥(Spec K)
φ : K ⟶ S
T : Scheme
g : T ⟶ Spec K
x✝ : HasPullback g (Spec.map φ)
this :
  ∀ {T : Scheme} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)),
    (∃ R, T = Spec R) → topologically (@IsOpenMap) (pullback.fst g (Spec.map φ))
hT : ¬∃ R, T = Spec R
i : T.affineCover.toPreZeroHypercover.1
⊢ topologically (@IsOpenMap)
    (((pullbackRightPullbackFstIso g (Spec.map φ) (T.affineCover.f i)).inv ≫
        (pullbackSymmetry (T.affineCover.f i) (pullback.fst g (Spec.map φ))).hom) ≫
      Scheme.Cover.pullbackHom T.affineCover (pullback.fst g (Spec.map φ)) i)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
⊢ ∀ (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → topologically (@IsClosedMap) f'

Tactic:
f'

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
⊢ IsPullback f' i₁ i₂ f → topologically (@IsClosedMap) f'
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : Surjective f
X' Y' : Scheme
i₁ : X' ⟶ Y
i₂ : Y' ⟶ Z
⊢ ∀ (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ g → topologically (@IsClosedMap) f'

Tactic:
f'

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : Surjective f
X' Y' : Scheme
i₁ : X' ⟶ Y
i₂ : Y' ⟶ Z
f' : X' ⟶ Y'
⊢ IsPullback f' i₁ i₂ g → topologically (@IsClosedMap) f'
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X : Scheme} (R : CommRingCat) {f : X ⟶ Spec R},
    UniversallyClosed f → IsAffineHom f → (∃ S, X = Spec S) → IsIntegralHom f
hX : ¬∃ S, X = Spec S
inst : IsAffine X
⊢ IsIntegralHom (X.isoSpec.inv ≫ f)

Tactic:
exact this _ inferInstance inferInstance ⟨_, rfl⟩

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

Goal state before:
pp: X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : ↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K))
htU' : t ∈ basicOpen g
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K := (aeval fun i ↦ if i ∈ σ then MvPolynomial.X i else 0).toRingHom
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : t' ∈ basicOpen g
z : ↥(pullback f q)
hzr : (pullback.snd f q) z = t'
hx : ∀ i ∈ σ, (pullback.fst f q) z ∉ (U i).carrier
this : ∀ (i : 𝒰.I₀), t ∈ (Opens.comap { toFun := comap φ, continuous_toFun := ⋯ }) (Ti i) → p z ∉ U i
⊢ z ∈ Z

Tactic:
by simpa [Z, p, fT, hzr]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : UniversallyClosed f
⊢ IsProperMap ⇑f

Tactic:
by
  rw [isProperMap_iff_isClosedMap_and_compact_fibers]
  refine ⟨f.continuous, f.isClosedMap, fun y ↦ ?_⟩
  have := compactSpace_of_universallyClosed (pullback.snd f (Y.fromSpecResidueField y))
  rw [← Scheme.range_fromSpecResidueField, ← Scheme.Pullback.range_fst]
  exact isCompact_range (Scheme.Hom.continuous _)

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsDominant f
⊢ Set.range ⇑f = closure (Set.range ⇑f)

Tactic:
f.isClosedMap.isClosed_range.closure_eq

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsDominant f
⊢ Set.range ⇑f = Set.range ⇑f
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
refine (isIso_pushoutSection_iff ..).mpr (IsPullback.of_map_of_faithful Scheme.Spec ?_).unop
  have : IsAffine _ := hUS
  have : IsAffine _ := hUT
  have : IsAffine _ := hUX
  have hUY' : IsAffineOpen UY :=
    .of_isIso (Scheme.Hom.isPullback_resLE H hUST hUSX hUY).isoPullback.hom
  exact .of_iso (Scheme.Hom.isPullback_resLE H hUST hUSX hUY).flip hUY'.isoSpec hUT.isoSpec
    hUX.isoSpec hUS.isoSpec (by simp) (by simp) (by simp) (by simp)

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

Goal state before:
pp: case hUU'
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
hUST : UT ≤ f ⁻¹ᵁ US
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := ⋯
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
i : ι
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(X, iSup VX) := ⋯
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) := ⋯
⊢ VX i ≤ iSup VX

Tactic:
exact le_iSup _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
i : ↑Γ(Spec (CommRingCat.of (MvPolynomial n ↑R)), ⊤)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop (SpecIso n R).hom)) i =
    (CommRingCat.Hom.hom
        ((Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).hom ≫
          CommRingCat.ofHom
            (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
              (coord (Spec R)))))
      i

Tactic:
simp [SpecIso]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
inst✝ : Finite n
this : IsIso (terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))
⊢ LocallyOfFinitePresentation (Spec.map (CommRingCat.ofHom C))

Tactic:
HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation),

Goal state after:
n : Type u
S : Scheme
inst✝ : Finite n
this : IsIso (terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom C)).FinitePresentation
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
W : Set X
inst✝ : Zero Y
f : X → Y
h : LocallyFiniteSupport f
hW : IsCompact W
this : {i | ({↑i} ∩ W).Nonempty}.Finite
lem : ∀ {α : Type u_1} (s t : Set α), Subtype.val '' {i | ({↑i} ∩ t).Nonempty} = t ∩ s
⊢ (W ∩ support f).Finite

Tactic:
rw [← lem f.support W]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
W : Set X
inst✝ : Zero Y
f : X → Y
h : LocallyFiniteSupport f
hW : IsCompact W
this : {i | ({↑i} ∩ W).Nonempty}.Finite
lem : ∀ {α : Type u_1} (s t : Set α), Subtype.val '' {i | ({↑i} ∩ t).Nonempty} = t ∩ s
⊢ (Subtype.val '' {i | ({↑i} ∩ W).Nonempty}).Finite
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeSup Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
⊢ (t₁ ∩ t₂ ∩ Function.support fun z ↦ D₁ z ⊔ D₂ z).Finite

Tactic:
apply Set.Finite.subset (s := (t₁ ∩ D₁.support) ∪ (t₂ ∩ D₂.support)) (ht₁.2.union ht₂.2)

Goal state after:
case right
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeSup Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
⊢ (t₁ ∩ t₂ ∩ Function.support fun z ↦ D₁ z ⊔ D₂ z) ⊆ t₁ ∩ D₁.support ∪ t₂ ∩ D₂.support
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeInf Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
⊢ (t₁ ∩ t₂ ∩ Function.support fun z ↦ D₁ z ⊓ D₂ z).Finite

Tactic:
apply Set.Finite.subset (s := (t₁ ∩ D₁.support) ∪ (t₂ ∩ D₂.support)) (ht₁.2.union ht₂.2)

Goal state after:
case right
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeInf Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
⊢ (t₁ ∩ t₂ ∩ Function.support fun z ↦ D₁ z ⊓ D₂ z) ⊆ t₁ ∩ D₁.support ∪ t₂ ∩ D₂.support
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
⊢ ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))),
    (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf)) x_1 = 0 → x_1 = 0

Tactic:
intro t ht

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
t : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))
ht : (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf)) t = 0
⊢ t = 0