mathlib-initiative/mathlib-tactics huggingface dataset:
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 = ⊤
H : ∀ (r : ↥s), (Localization.awayMap f ↑r).Finite
this✝ : Algebra R S := f.toAlgebra
this : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
r : ↥s
⊢ IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsAffineHom (pullback.diagonal f) ↔
    ∀ (U : Y.Opens),
      IsAffineOpen U → ∀ V₁ ≤ f ⁻¹ᵁ U, ∀ V₂ ≤ f ⁻¹ᵁ U, IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)

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
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
⊢ Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom ≫ Limits.prod.fst = Scheme.Hom.app f W

Tactic:
by

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

Goal state before:
pp: X : Scheme
inst✝ : IsAffineHom (pullback.diagonal (terminal.from X))
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
⊢ U ≤ terminal.from X ⁻¹ᵁ ⊤

Tactic:
by

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

Goal state before:
pp: X : Scheme
inst✝ : IsAffineHom (pullback.diagonal (terminal.from X))
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
⊢ V ≤ terminal.from X ⁻¹ᵁ ⊤

Tactic:
by

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

Goal state before:
pp: ⊢ StableUnderComposition @FiniteType

Tactic:
by

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

Goal state before:
pp: ⊢ RespectsIso @FiniteType

Tactic:
by

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

Goal state before:
pp: ⊢ IsStableUnderBaseChange @FiniteType

Tactic:
by

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

Goal state before:
pp: ⊢ OfLocalizationSpan @FiniteType

Tactic:
by

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

Goal state before:
pp: ⊢ HoldsForLocalizationAway @FiniteType

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
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
⊢ (algebraMap S (Localization.Away (f ↑r))) x ∈ Submodule.span (Localization.Away ↑r) ↑(s₁ r)

Tactic:
by

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

Goal state before:
pp: R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), ((algebraMap S (Localization.Away ↑r)).comp f).FiniteType
algInst✝ : Algebra R S := f.toAlgebra
⊢ ∀ r ∈ s, Algebra.FiniteType R (Localization.Away r)

Tactic:
by

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

Goal state before:
pp: ⊢ OfLocalizationSpanTarget @FiniteType

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ @LocallyOfFiniteType = affineLocally fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FiniteType

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f✝ f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : LocallyOfFiniteType f
⊢ LocallyOfFiniteType (Scheme.Hom.resLE f V U e)

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
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
⊢ Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom ≫ Limits.prod.snd = Scheme.Hom.app g W

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

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥Y
⊢ JacobsonSpace ↥X

Tactic:
by

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

Goal state before:
pp: 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'
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} fun x ↦ x ∈ Set.range (unop ∘ F.obj)
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} F.essImage

Tactic:
by

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

Goal state before:
pp: 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
q : ↥(Spec (unop (F.obj S)))
⊢ ∃ f, q ∈ PrimeSpectrum.basicOpen f ∧ Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen f)

Tactic:
by

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

Goal state before:
pp: ⊢ OfLocalizationSpan @Finite

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 : P f
hg : P g
⊢ P (Limits.coprod.desc f g)

Tactic:
by

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

Goal state before:
pp: X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
⊢ EssentiallySmall.{u, u, u + 1} (P.CostructuredArrow ⊤ Scheme.Spec X)

Tactic:
by

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

Goal state before:
pp: ⊢ @IsClosedImmersion =
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding) ⊓ @SurjectiveOnStalks

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ (I.comapIso f).hom ≫ pullback.fst f I.subschemeι = (I.comap f).subschemeι

Tactic:
by

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
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
by

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
⊢ (I.comap g).subschemeι ≫ 𝟙 Y = (I.comapIso g).hom ≫ pullback.fst g I.subschemeι

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔ IsPreimmersion f ∧ IsClosed (Set.range ⇑f)

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
inst✝ : IsEmpty ↥X
f : X ⟶ Y
⊢ IsClosed (Set.range ⇑f)

Tactic:
by

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
⊢ I.comap (f ≫ g) = (I.comap g).comap f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: Z : Scheme
I : Z.IdealSheafData
⊢ I.comap (𝟙 Z) = I

Tactic:
by

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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
h : Function.Surjective ⇑(ConcreteCategory.hom f)
x : ↥(Spec S)
⊢ (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ Function.Surjective ⇑f).RespectsIso

Tactic:
by

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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
h : Function.Surjective ⇑(ConcreteCategory.hom f)
x : ↥(Spec S)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (Spec.map f) x))

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ IsClosedImmersion f

Tactic:
MorphismProperty.arrow_mk_iso_iff @IsClosedImmersion (arrowIsoSpecΓOfIsAffine f)

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ IsClosedImmersion (Spec.map (Scheme.Hom.appTop f))
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:
by

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ IsClosedImmersion f

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst✝ : IsClosedImmersion i
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst✝ : IsClosedImmersion i
⊢ i ≫ 𝟙 Y = Hom.toImage i ≫ Hom.imageι i

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
x : ↥X
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
by

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

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

Goal state before:
pp: ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst✝¹ : IsClosedImmersion iX
inst✝ : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
this : IsIso (pullback.lift iX Zf h)
⊢ iX ≫ 𝟙 X = pullback.lift iX Zf h ≫ pullback.fst f iY

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this : IsClosedImmersion (Scheme.Hom.toImage f)
⊢ Function.Surjective ⇑(Scheme.Hom.toImage f)

Tactic:
← Set.range_eq_univ,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this : IsClosedImmersion (Scheme.Hom.toImage f)
⊢ Set.range ⇑(Scheme.Hom.toImage f) = Set.univ
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this : IsClosedImmersion (Scheme.Hom.toImage f)
⊢ Function.Surjective ⇑(Scheme.Hom.toImage f)

Tactic:
by

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

Goal state before:
pp: ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst✝¹ : IsClosedImmersion iX
inst✝ : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
this : IsIso (pullback.lift iX Zf h)
⊢ IsPullback iX Zf f iY

Tactic:
by

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

Goal state before:
pp: ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst✝¹ : IsClosedImmersion iX
inst✝ : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
⊢ pullback.lift iX Zf h ≫ pullback.fst f iY = iX

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ IsIso (Scheme.Hom.toImage f)

Tactic:
by

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

Goal state before:
pp: ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst✝¹ : IsClosedImmersion iX
inst✝ : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
⊢ IsPullback iX Zf f iY

Tactic:
by

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

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

Goal state before:
pp: X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J ≤ I.map f
⊢ I.subschemeι ≫ f = (Hom.toImage (I.subschemeι ≫ f) ≫ inclusion H) ≫ J.subschemeι

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
⊢ (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f

Tactic:
by

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ ⊥.map f = Hom.ker f

Tactic:
by

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ ({ 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 := ⋯ } ⋙
          (MorphismProperty.Over.forget @IsClosedImmersion ⊤ X).op ⋙ X.kerFunctor).obj
      I =
    (𝟭 X.IdealSheafData).obj I

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
H : Scheme.Hom.ker f = ⊥
⊢ IsIso (Scheme.Hom.imageι f)

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ ⊤.comap f = ⊤

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ IsIso f ↔ Scheme.Hom.ker f = ⊥

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsClosedImmersion f
H : Scheme.Hom.ker f ≤ Scheme.Hom.ker g
⊢ lift f g H ≫ f = g

Tactic:
by

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

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h✝ : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h✝ True.intro
h : IsIso f'.op
⊢ IsIso f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: Z : Scheme
I : Z.IdealSheafData
⊢ I.map (𝟙 Z) = I

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (Hom.ker f).map g = Hom.ker (f ≫ g)

Tactic:
by

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

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h True.intro
⊢ homOfLE ⋯ ≫ homOfLE ⋯ = 𝟙 (Scheme.Hom.ker i₂)

Tactic:
by

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

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h True.intro
⊢ homOfLE ⋯ ≫ homOfLE ⋯ = 𝟙 (Scheme.Hom.ker i₁)

Tactic:
by

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

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
⊢ IsIso f

Tactic:
by

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

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
h : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
⊢ lift i₁ i₂ ⋯ ≫ i₁ = i₂

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ (Scheme.Hom.ker f).ideal ⟨⊤, ⋯⟩ = ⊥.ideal ⟨⊤, ⋯⟩

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
this : Scheme.Hom.ker f = ⊥
⊢ DenseRange ⇑f

Tactic:
by

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

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ IsDominant f

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst✝ : QuasiCompact f
U : ↑Y.affineOpens
H : IsAffineOpen (f ⁻¹ᵁ ↑U)
⊢ (I.map f).ideal U = Ideal.comap (CommRingCat.Hom.hom (Hom.app f ↑U)) (I.ideal ⟨f ⁻¹ᵁ ↑U, H⟩)

Tactic:
by

Goal state after: