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

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f → ∀ (x : ↥X), IsAffine X ∧ IsAffine Y → Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : f x ∈ U
right✝ : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Scheme.Hom.resLE f U V e) ⟨x, hx⟩))

Tactic:
exact this (IsZariskiLocalAtSource.resLE _ hf) _ ⟨hV, hU⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : Nonempty ↥X
inst✝¹ : Nonempty ↥Y
inst✝ : Subsingleton ↥S
this : Nonempty ↥S
⊢ ∃ x ∈ Set.range ⇑f, x ∈ Set.range ⇑g

Tactic:
exact ⟨Nonempty.some ‹_›, Function.surjective_to_subsingleton _ _,
    Function.surjective_to_subsingleton _ _⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Set.range ⇑(pullback.snd f g) = ⇑g ⁻¹' Set.range ⇑f

Tactic:
by
  ext x
  refine ⟨?_, fun ⟨y, hy⟩ ↦ ?_⟩
  · rintro ⟨a, rfl⟩
    simp only [Set.mem_preimage, Set.mem_range, ← Scheme.Hom.comp_apply, ← pullback.condition]
    simp
  · obtain ⟨a, ha⟩ := Triplet.exists_preimage (Triplet.mk' y x hy)
    use a, ha.right

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

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ ↑(ker f).support ⊆ closure (Set.range ⇑f)

pp: case a
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ closure (Set.range ⇑f) ⊆ ↑(ker f).support

Tactic:
· wlog hY : ∃ S, Y = Spec S
    · intro x hx
      let 𝒰 := Y.affineCover
      obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
      have inst : QuasiCompact (𝒰.pullbackHom f i) :=
        MorphismProperty.pullback_snd _ _ inferInstance
      have := this (𝒰.pullbackHom f i) ⟨_, rfl⟩
        ((coe_support_inter _ ⟨⊤, isAffineOpen_top _⟩).ge ⟨?_, Set.mem_univ x⟩).1
      · have := image_closure_subset_closure_image (f := 𝒰.f i)
          (𝒰.f i).continuous (Set.mem_image_of_mem _ this)
        rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, 𝒰.pullbackHom_map] at this
        exact closure_mono (Set.range_comp_subset_range _ _) this
      · rw [← (𝒰.f i).isOpenEmbedding.injective.mem_set_image, Scheme.image_zeroLocus,
          ker_ideal_of_isPullback_of_isOpenImmersion f (𝒰.pullbackHom f i)
            ((𝒰.pullback₁ f).f i) (𝒰.f i),
          Ideal.coe_comap, Set.image_preimage_eq]
        · exact ⟨((coe_support_inter _ _).le ⟨hx, by simp⟩).1, ⟨_, rfl⟩⟩
        · exact (ConcreteCategory.bijective_of_isIso ((𝒰.f i).appIso ⊤).inv).2
        · exact (IsPullback.of_hasPullback _ _).flip
    obtain ⟨S, rfl⟩ := hY
    wlog hX : ∃ R, X = Spec R generalizing X S
    · intro x hx
      have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›
      let 𝒰 := X.affineCover.finiteSubcover
      obtain ⟨_, ⟨i, rfl⟩, hx⟩ := (f.iUnion_support_ker_openCover_map_comp 𝒰).ge hx
      have inst : QuasiCompact (𝒰.f i ≫ f) := HasAffineProperty.iff_of_isAffine.mpr
        (inferInstanceAs <| CompactSpace (Spec _))
      exact closure_mono (Set.range_comp_subset_range _ _) (this S (𝒰.f i ≫ f) ⟨_, rfl⟩ hx)
    obtain ⟨R, rfl⟩ := hX
    obtain ⟨φ, rfl⟩ := Spec.map_surjective f
    rw [ker_of_isAffine, coe_support_ofIdealTop, Spec_zeroLocus, ← Ideal.coe_comap,
      RingHom.comap_ker, ← PrimeSpectrum.closure_range_comap, ← CommRingCat.hom_comp,
      ← Scheme.ΓSpecIso_inv_naturality]
    simp only [CommRingCat.hom_comp, PrimeSpectrum.comap_comp]
    exact closure_mono (Set.range_comp_subset_range _ (Spec.map φ))

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ closure (Set.range ⇑f) ⊆ ↑(ker f).support
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
z : ↥(pullback f' g')
x : ↥X
hx : i₁ x = (pullback.fst f' g') z
y : ↥Y
hy : i₂ y = (pullback.snd f' g') z
T₁ : Triplet (pullback.fst f' g') i₁ := ⋯
w₁ : ↥(pullback (pullback.fst f' g') i₁)
hw₁ : (pullback.fst (pullback.fst f' g') i₁) w₁ = T₁.x ∧ (pullback.snd (pullback.fst f' g') i₁) w₁ = T₁.y
T₂ : Triplet (pullback.snd f' g') i₂ := ⋯
w₂ : ↥(pullback (pullback.snd f' g') i₂)
hw₂ : (pullback.fst (pullback.snd f' g') i₂) w₂ = T₂.x ∧ (pullback.snd (pullback.snd f' g') i₂) w₂ = T₂.y
T : Triplet (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) := ⋯
t : ↥(pullback (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂))
left✝ : (pullback.fst (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)) t = T.x
ht₂ : (pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)) t = T.y
⊢ (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) ((pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).hom t) = z

Tactic:
pullback_map_eq_pullbackFstFstIso_inv,

Goal state after:
case h
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
z : ↥(pullback f' g')
x : ↥X
hx : i₁ x = (pullback.fst f' g') z
y : ↥Y
hy : i₂ y = (pullback.snd f' g') z
T₁ : Triplet (pullback.fst f' g') i₁ := Triplet.mk' z x ⋯
w₁ : ↥(pullback (pullback.fst f' g') i₁)
hw₁ : (pullback.fst (pullback.fst f' g') i₁) w₁ = T₁.x ∧ (pullback.snd (pullback.fst f' g') i₁) w₁ = T₁.y
T₂ : Triplet (pullback.snd f' g') i₂ := Triplet.mk' z y ⋯
w₂ : ↥(pullback (pullback.snd f' g') i₂)
hw₂ : (pullback.fst (pullback.snd f' g') i₂) w₂ = T₂.x ∧ (pullback.snd (pullback.snd f' g') i₂) w₂ = T₂.y
T : Triplet (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) := Triplet.mk' w₁ w₂ ⋯
t : ↥(pullback (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂))
left✝ : (pullback.fst (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)) t = T.x
ht₂ : (pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)) t = T.y
⊢ ((pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv ≫
        pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) ≫
          pullback.fst (pullback.snd f' g') i₂)
      ((pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).hom t) =
    z
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderBaseChange @IsAffineHom

Tactic:
apply HasAffineProperty.isStableUnderBaseChange

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange fun X x x_1 x_2 ↦ IsAffine X
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : ∀ (P : MorphismProperty Scheme) {Q : outParam AffineTargetMorphismProperty} [self : HasAffineProperty P Q],
  Q.IsLocal :=
  HasAffineProperty.isLocal_affineProperty
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange fun X x x_1 x_2 ↦ IsAffine X

Tactic:
apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : ∀ (P : MorphismProperty Scheme) {Q : outParam AffineTargetMorphismProperty} [self : HasAffineProperty P Q],
  Q.IsLocal :=
  HasAffineProperty.isLocal_affineProperty
⊢ ∀ ⦃X Y S : Scheme⦄ [IsAffine S] [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), IsAffine Y → IsAffine (pullback f g)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
b : ↥(I.glueDataObj ib)
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) a) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) b)
this : (I.glueData.ι ia ≫ I.gluedTo) a = (I.glueData.ι ib ≫ I.gluedTo) b
⊢ ↑((I.glueDataObjι ia) a) = ↑((I.glueDataObjι ib) b)

Tactic:
rwa [ι_gluedTo, ι_gluedTo] at this

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
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso
⊢ (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).IsStableUnderBaseChange

Tactic:
apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso
⊢ ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) (Limits.pullback.fst f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
hf : ∀ (U : ↑Y.affineOpens), IsAffine ↑(f ⁻¹ᵁ ↑U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
obtain ⟨hfU, hf⟩ := hf ⟨U, hU⟩

Goal state after:
case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
hf✝ : ∀ (U : ↑Y.affineOpens), IsAffine ↑(f ⁻¹ᵁ ↑U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
hfU : IsAffine ↑(f ⁻¹ᵁ ↑⟨U, hU⟩)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑⟨U, hU⟩).ι ''ᵁ ⊤)))
⊢ IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ IsPreimmersion (I.gluedTo ∣_ ↑U)

Tactic:
← MorphismProperty.cancel_left_of_respectsIso @IsPreimmersion (I.glueDataObjIso U).hom,

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ IsPreimmersion ((I.glueDataObjIso U).hom ≫ I.gluedTo ∣_ ↑U)
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case mp.inr
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
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
    (RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      ∀ {X Y : Scheme} (f : X ⟶ Y),
        (HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q)
            fun {R S} [CommRing R] [CommRing S] ↦ Q) →
          IsAffineHom f →
            IsAffine Y →
              (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
                affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hY : ¬IsAffine Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
    affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
intro h

Goal state after:
case mp.inr
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
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
    (RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      ∀ {X Y : Scheme} (f : X ⟶ Y),
        (HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q)
            fun {R S} [CommRing R] [CommRing S] ↦ Q) →
          IsAffineHom f →
            IsAffine Y →
              (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
                affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
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
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
hY : IsAffine Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
    affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
intro h

Goal state after:
Q✝ 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
hY : IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case mpr
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
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f →
    ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
intro h

Goal state after:
case mpr
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 : affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
⊢ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case inr
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
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme},
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q) →
        ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Z → P (f ≫ g)
hZ : ¬IsAffine Z
U : ↑Z.affineOpens
⊢ P ((f ≫ g) ∣_ ↑U)

Tactic:
morphismRestrict_comp

Goal state after:
case inr
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
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme},
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q) →
        ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Z → P (f ≫ g)
hZ : ¬IsAffine Z
U : ↑Z.affineOpens
⊢ P (f ∣_ g ⁻¹ᵁ ↑U ≫ g ∣_ ↑U)
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: ⊢ IsStableUnderBaseChange @Finite

Tactic:
refine IsStableUnderBaseChange.mk finite_respectsIso ?_
  simp only [finite_algebraMap]
  intros
  infer_instance

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

Goal state before:
pp: X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ closure (⇑f ⁻¹' ↑I.support) = ⇑f ⁻¹' ↑I.support

Tactic:
(I.support.isClosed.preimage f.continuous).closure_eq

Goal state after:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ ⇑f ⁻¹' ↑I.support = ⇑f ⁻¹' ↑I.support
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(coborderRange f)).Opens
| f ⁻¹ᵁ (coborderRange f).ι ''ᵁ U

Tactic:
1

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(coborderRange f)).Opens
| TopologicalSpace.Opens.map f.base
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

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 = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
t : Finset A := Finset.image (fun g ↦ (Ideal.Quotient.mk I) (g' g)) Finset.univ
ht : Ideal.span ↑t = ⊤
⊢ FinitePresentation R A

Tactic:
apply Algebra.FinitePresentation.quotient

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := ⋯
A : Type u_1 := ⋯
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := ⋯
hf' : Function.Surjective ⇑f'
t : Finset A := ⋯
ht : Ideal.span ↑t = ⊤
⊢ I.FG
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y Z : Scheme
⊢ MorphismProperty.IsStableUnderBaseChange @IsClosedImmersion

Tactic:
apply HasAffineProperty.isStableUnderBaseChange

Goal state after:
X Y Z : Scheme
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Tactic:
apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk

Goal state after:
X Y Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ ∀ ⦃X Y S : Scheme⦄ [IsAffine S] [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    IsAffine Y ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g)) →
      IsAffine (Limits.pullback f g) ∧
        Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (Limits.pullback.fst f g)))
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case inr.mpr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
⊢ (∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I) →
    Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f)) =
      X ^ ((LinearMap.mul R A) f).charpoly.natDegree

Tactic:
intro H
    ext i
    obtain (hi | hi) := eq_or_ne i ((LinearMap.mul R A) f).charpoly.natDegree
    · simp only [Algebra.coe_lmul_eq_mul, hi, coeff_map, coeff_X_pow, ↓reduceIte]
      rw [← Polynomial.leadingCoeff, ((LinearMap.mul R A) f).charpoly_monic, map_one]
    obtain (hi | hi) := lt_or_gt_of_ne hi
    · simpa [hi.ne, ← RingHom.mem_ker, Ideal.ker_algebraMap_residueField] using H i hi
    · simp [hi.ne', coeff_eq_zero_of_natDegree_lt hi]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mp
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ IsLocallyNoetherian X → ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)

Tactic:
intro h

Goal state after:
case mp
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
h : IsLocallyNoetherian X
⊢ ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mp
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
h : IsLocallyNoetherian X
i : 𝒰.I₀
U : X.Opens := ⋯
this : IsNoetherianRing ↑Γ(X, ↑⟨U, ⋯⟩)
⊢ Γ(X, U) ≅ Γ(𝒰.X i, ⊤)

Tactic:
exact (IsOpenImmersion.ΓIsoTop (𝒰.f i)).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ (∀ (i : 𝒰.I₀), IsLocallyNoetherian (𝒰.X i)) →
    ∀ (i : 𝒰.affineRefinement.openCover.I₀), IsNoetherianRing ↑Γ(𝒰.affineRefinement.openCover.X i, ⊤)

Tactic:
intro h

Goal state after:
X : Scheme
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), IsLocallyNoetherian (𝒰.X i)
⊢ ∀ (i : 𝒰.affineRefinement.openCover.I₀), IsNoetherianRing ↑Γ(𝒰.affineRefinement.openCover.X i, ⊤)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mp
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
⊢ IsNoetherian X → ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))

Tactic:
intro h

Goal state after:
case mp
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : IsNoetherian X
⊢ ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
⊢ (∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))) → IsNoetherian X

Tactic:
intro h

Goal state after:
case mpr
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ IsNoetherian X