mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
i : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen✝¹ :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (i U) = i (X.affineBasicOpen f)
s : Set ↥X
hs : s = ⋂ U, X.zeroLocus ↑(i U)
j : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen✝ :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (j U) = j (X.affineBasicOpen f)
t : Set ↥X
ht : t = ⋂ U, X.zeroLocus ↑(j U)
h :
  { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
        supportSet_eq_iInter_zeroLocus := hs }.ideal =
    { ideal := j, map_ideal_basicOpen := map_ideal_basicOpen✝, supportSet := t,
        supportSet_eq_iInter_zeroLocus := ht }.ideal
⊢ { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s, supportSet_eq_iInter_zeroLocus := hs } =
    { ideal := j, map_ideal_basicOpen := map_ideal_basicOpen✝, supportSet := t, supportSet_eq_iInter_zeroLocus := ht }

Tactic:
subst h

Goal state after:
X : Scheme
i : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen✝¹ :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (i U) = i (X.affineBasicOpen f)
s : Set ↥X
hs : s = ⋂ U, X.zeroLocus ↑(i U)
t : Set ↥X
map_ideal_basicOpen✝ :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
        ({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
              supportSet_eq_iInter_zeroLocus := hs }.ideal
          U) =
      { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
            supportSet_eq_iInter_zeroLocus := hs }.ideal
        (X.affineBasicOpen f)
ht :
  t =
    ⋂ U,
      X.zeroLocus
        ↑({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
                supportSet_eq_iInter_zeroLocus := hs }.ideal
            U)
⊢ { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s, supportSet_eq_iInter_zeroLocus := hs } =
    {
      ideal :=
        { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen✝¹, supportSet := s,
            supportSet_eq_iInter_zeroLocus := hs }.ideal,
      map_ideal_basicOpen := map_ideal_basicOpen✝, supportSet := t, supportSet_eq_iInter_zeroLocus := ht }
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
x : ↑Γ(X, V)
hx : (ConcreteCategory.hom (X.presheaf.map i.op)) x = 0
⊢ x = 0

Tactic:
← basicOpen_eq_bot_iff

Goal state after:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
x : ↑Γ(X, V)
hx : X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i.op)) x) = ⊥
⊢ X.basicOpen x = ⊥
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case e
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
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ P = P

pp: case e'
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
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f ↔ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
· rfl

Goal state after:
case e'
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
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f ↔ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
H : ((CommRingCat.Hom.hom (f.app ↑U)) x |_ X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)) ⋯ = 0
⊢ ∃ s_1 ∈ Submonoid.powers s, s_1 * x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))

Tactic:
obtain ⟨n, hn⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact
        X (U := f ⁻¹ᵁ U) (QuasiCompact.isCompact_preimage (f := f) _ U.1.2 U.2.isCompact)
        (f.app U x) (f.app U s) H

Goal state after:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n✝ : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n✝, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
H : ((CommRingCat.Hom.hom (f.app ↑U)) x |_ X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)) ⋯ = 0
n : ℕ
hn : (ConcreteCategory.hom (f.app ↑U)) s ^ n * (ConcreteCategory.hom (f.app ↑U)) x = 0
⊢ ∃ s_1 ∈ Submonoid.powers s, s_1 * x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case mpr
X : Scheme
R : CommRingCat
f₂ : (x : ↥X) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
x₁ : ↥X
f₁ : X.presheaf.stalk x₁ ⟶ R
h₁ : IsLocalHom (CommRingCat.Hom.hom f₁)
⊢ (∃ (h₁_1 : ⟨x₁, ⟨f₁, h₁⟩⟩.fst = f₂.fst), ↑⟨x₁, ⟨f₁, h₁⟩⟩.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑f₂.snd) →
    ⟨x₁, ⟨f₁, h₁⟩⟩ = f₂

Tactic:
obtain ⟨x₂, ⟨f₂, h₂⟩⟩ := f₂

Goal state after:
case mpr
X : Scheme
R : CommRingCat
x₁ : ↥X
f₁ : X.presheaf.stalk x₁ ⟶ R
h₁ : IsLocalHom (CommRingCat.Hom.hom f₁)
x₂ : ↥X
f₂ : X.presheaf.stalk x₂ ⟶ R
h₂ : IsLocalHom (CommRingCat.Hom.hom f₂)
⊢ (∃ (h₁_1 : ⟨x₁, ⟨f₁, h₁⟩⟩.fst = ⟨x₂, ⟨f₂, h₂⟩⟩.fst),
      ↑⟨x₁, ⟨f₁, h₁⟩⟩.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑⟨x₂, ⟨f₂, h₂⟩⟩.snd) →
    ⟨x₁, ⟨f₁, h₁⟩⟩ = ⟨x₂, ⟨f₂, h₂⟩⟩
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X✝ : Scheme
U : X✝.Opens
X Y : Scheme
f : X ⟶ Y
x y : ↥X
h : x = y
⊢ X.residueField x = X.residueField y

Tactic:
subst h

Goal state after:
X✝ : Scheme
U : X✝.Opens
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ X.residueField x = X.residueField x
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x y : ↥X
h : x = y
⊢ X.residue x ≫ (residueFieldCongr h).hom = (X.presheaf.stalkCongr ⋯).hom ≫ X.residue y

Tactic:
subst h

Goal state after:
X : Scheme
x : ↥X
⊢ X.residue x ≫ (residueFieldCongr ⋯).hom = (X.presheaf.stalkCongr ⋯).hom ≫ X.residue x
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x y : ↥X
h : x = y
⊢ Spec.map (residueFieldCongr h).hom ≫ X.fromSpecResidueField x = X.fromSpecResidueField y

Tactic:
subst h

Goal state after:
X : Scheme
x : ↥X
⊢ Spec.map (residueFieldCongr ⋯).hom ≫ X.fromSpecResidueField x = X.fromSpecResidueField x
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝² : QuasiCompact f'
this✝¹ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this✝ : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
e : Γ(X, f ⁻¹ᵁ iV ''ᵁ ↑W) ≅ Γ(U, f' ⁻¹ᵁ ↑W) := Functor.mapIso X.presheaf (eqToIso this✝).op ≪≫ Hom.appIso iU (f' ⁻¹ᵁ ↑W)
this : (Hom.appIso iV ↑W).inv ≫ Hom.app f (iV ''ᵁ ↑W) = Hom.app f' ↑W ≫ e.inv
⊢ x ∈ (Hom.ker f').ideal W ↔
    x ∈ Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Tactic:
simp only [Scheme.Hom.ker_apply, RingHom.mem_ker, Ideal.mem_comap, ← RingHom.comp_apply,
    ← CommRingCat.hom_comp, this]

Goal state after:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝² : QuasiCompact f'
this✝¹ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this✝ : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
e : Γ(X, f ⁻¹ᵁ iV ''ᵁ ↑W) ≅ Γ(U, f' ⁻¹ᵁ ↑W) := Functor.mapIso X.presheaf (eqToIso this✝).op ≪≫ Hom.appIso iU (f' ⁻¹ᵁ ↑W)
this : (Hom.appIso iV ↑W).inv ≫ Hom.app f (iV ''ᵁ ↑W) = Hom.app f' ↑W ≫ e.inv
⊢ (CommRingCat.Hom.hom (Hom.app f' ↑W)) x = 0 ↔ (CommRingCat.Hom.hom (Hom.app f' ↑W ≫ e.inv)) x = 0
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T T' : Triplet f g
h : T = T'
⊢ Spec.map (Triplet.tensorCongr h).hom ≫ T.SpecTensorTo = T'.SpecTensorTo

Tactic:
subst h

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ Spec.map (Triplet.tensorCongr ⋯).hom ≫ T.SpecTensorTo = T.SpecTensorTo
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
this : (Spec.map (Hom.residueFieldMap T.SpecTensorTo p)) ⊥ = ⊥
⊢ (Spec.map (Triplet.tensorCongr ⋯).inv)
      ((fun t ↦ ⟨Triplet.ofPoint t, SpecOfPoint t⟩) ((fun T ↦ T.fst.SpecTensorTo T.snd) ⟨T, p⟩)).snd =
    ⟨T, p⟩.snd

Tactic:
simp only [SpecOfPoint, Triplet.tensorCongr_inv, ← this, ← Scheme.Hom.comp_apply,
      ← Scheme.Hom.comp_apply]

Goal state after:
case h
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
this : (Spec.map (Hom.residueFieldMap T.SpecTensorTo p)) ⊥ = ⊥
⊢ ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫ Spec.map (ofPointTensor (T.SpecTensorTo p))) ≫
        Spec.map (Triplet.tensorCongr ⋯).hom)
      ⊥ =
    p
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
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
⊢ ∀ {Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z),
    (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty f →
      (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty (e.hom ≫ f)

Tactic:
Y

Goal state after:
case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
⊢ ∀ {Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z),
    (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty f →
      (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty (e.hom ≫ f)
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
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
⊢ ∀ {Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y),
    (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty f →
      (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty (f ≫ e.hom)

Tactic:
Y

Goal state after:
case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
⊢ ∀ {Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y),
    (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty f →
      (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty (f ≫ e.hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case to_basicOpen
X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
⊢ ∀ {Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (r : ↑Γ(Y, ⊤)), IsAffine X → IsAffine ↑(f ⁻¹ᵁ Y.basicOpen r)

Tactic:
Y

Goal state after:
case to_basicOpen
X✝ Y✝ Z : Scheme
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
⊢ ∀ [IsAffine Y] (f : X ⟶ Y) (r : ↑Γ(Y, ⊤)), IsAffine X → IsAffine ↑(f ⁻¹ᵁ Y.basicOpen r)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case of_basicOpenCover
X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
⊢ ∀ {Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (s : Finset ↑Γ(Y, ⊤)),
    Ideal.span ↑s = ⊤ → (∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)) → IsAffine X

Tactic:
Y

Goal state after:
case of_basicOpenCover
X✝ Y✝ Z : Scheme
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
⊢ ∀ [IsAffine Y] (f : X ⟶ Y) (s : Finset ↑Γ(Y, ⊤)),
    Ideal.span ↑s = ⊤ → (∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)) → 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
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 : Scheme
⊢ ∀ ⦃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)

Tactic:
Y

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 : Scheme
⊢ ∀ ⦃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.Affine

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

Tactic:
obtain ⟨x, rfl⟩ := hy

Goal state after:
case pos
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
x : ↥X
⊢ ∃ U, f x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

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

Tactic:
Y

Goal state after:
Q W : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQW : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → W f
X Y : Scheme
⊢ ∀ (f : X ⟶ Y),
    targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) f →
      targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ W) f
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
X : Scheme
⊢ ∀ ⦃Y : Scheme⦄ (f : X ⟶ Y), P f → IsAffineHom f

Tactic:
Y

Goal state after:
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)
X Y : Scheme
⊢ ∀ (f : X ⟶ Y), P f → IsAffineHom f
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: ⊢ OfLocalizationSpan @Finite

Tactic:
rw [RingHom.ofLocalizationSpan_iff_finite]

Goal state after:
⊢ OfLocalizationFiniteSpan @Finite
Module: Mathlib.RingTheory.RingHom.FiniteType

Goal state before:
pp: ⊢ OfLocalizationSpan @FiniteType

Tactic:
by
  refine OfLocalizationSpan.mk _ finiteType_respectsIso (fun s hs h ↦ ?_)
  simp_rw [finiteType_algebraMap] at h ⊢
  exact Algebra.FiniteType.of_span_eq_top_source s hs h

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

Goal state before:
pp: case hprecomp
X : Scheme
⊢ ∀ {Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z), IsClosedImmersion f → IsClosedImmersion (e.hom ≫ f)

Tactic:
Y

Goal state after:
case hprecomp
X Y : Scheme
⊢ ∀ {Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z), IsClosedImmersion f → IsClosedImmersion (e.hom ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: case hpostcomp
X : Scheme
⊢ ∀ {Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y), IsClosedImmersion f → IsClosedImmersion (f ≫ e.hom)

Tactic:
Y

Goal state after:
case hpostcomp
X Y : Scheme
⊢ ∀ {Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y), IsClosedImmersion f → IsClosedImmersion (f ≫ e.hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case inst.refine_1
X✝ Y Z : Scheme
f : X✝ ⟶ Y
X : Scheme
⊢ ∀ {Y Z : Scheme} (i : X ⟶ Y),
    MorphismProperty.isomorphisms Scheme i →
      ∀ (f : Y ⟶ Z),
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f →
          topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) (i ≫ f)

Tactic:
Y

Goal state after:
case inst.refine_1
X✝ Y✝ Z : Scheme
f : X✝ ⟶ Y✝
X Y : Scheme
⊢ ∀ {Z : Scheme} (i : X ⟶ Y),
    MorphismProperty.isomorphisms Scheme i →
      ∀ (f : Y ⟶ Z),
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f →
          topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) (i ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case inst.refine_2
X✝ Y Z : Scheme
f : X✝ ⟶ Y
X : Scheme
⊢ ∀ {Y Z : Scheme} (i : Y ⟶ Z),
    MorphismProperty.isomorphisms Scheme i →
      ∀ (f : X ⟶ Y),
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f →
          topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) (f ≫ i)

Tactic:
Y

Goal state after:
case inst.refine_2
X✝ Y✝ Z : Scheme
f : X✝ ⟶ Y✝
X Y : Scheme
⊢ ∀ {Z : Scheme} (i : Y ⟶ Z),
    MorphismProperty.isomorphisms Scheme i →
      ∀ (f : X ⟶ Y),
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f →
          topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) (f ≫ i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X✝ Y Z : Scheme
f : X✝ ⟶ Y
X : Scheme
⊢ ∀ {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:
Y

Goal state after:
X✝ Y✝ Z : Scheme
f : X✝ ⟶ Y✝
X Y : Scheme
⊢ ∀ {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.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
⊢ (ConcreteCategory.hom (Y.presheaf.Γgerm (f x))) g = 0

Tactic:
have h0 (i : 𝒰.I₀) : (𝒰.f i).appLE _ (W i) (by simp) (φ g) = 0 := by
    rw [← Scheme.Hom.appLE_map _ ((Opens.map _).map w).le (homOfLE <| hwle i).op,
      ← Scheme.Hom.map_appLE _ le_rfl w.op]
    simp only [CommRingCat.comp_apply]
    rw [hg]
    simp only [map_zero]

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
⊢ (ConcreteCategory.hom (Y.presheaf.Γgerm (f x))) g = 0
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
φ : S →+* T
ψ : R →+* S
x✝ : BasicConstructibleSetData R
⊢ map (φ.comp ψ) x✝ = (map φ ∘ map ψ) x✝

Tactic:
simp [map_comp]

Goal state after:
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))
X : Scheme
⊢ ∀ ⦃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)))

Tactic:
Y

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 : Scheme
⊢ ∀ ⦃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.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ UniversallyOpen f ↔ (topologically @IsOpenMap).universally f

Tactic:
universallyOpen_iff

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (topologically @IsOpenMap).universally f ↔ (topologically @IsOpenMap).universally f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
⊢ ∀ {Y : Scheme} (f : X ⟶ Y) {ι : Type u_1} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), topologically (@IsOpenMap) (f ∣_ U i)) → topologically (@IsOpenMap) f

Tactic:
Y

Goal state after:
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
X Y : Scheme
⊢ ∀ (f : X ⟶ Y) {ι : Type u_1} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), topologically (@IsOpenMap) (f ∣_ U i)) → topologically (@IsOpenMap) f