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

Goal state before:
pp: case restrict
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f →
      topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U)

Tactic:
intro X

Goal state after:
case restrict
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
X : Scheme
⊢ ∀ {Y : Scheme} (f : X ⟶ Y) (U : Y.Opens),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f →
      topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U i)) →
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f

Tactic:
intro X

Goal state after:
case of_sSup_eq_top
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
X : Scheme
⊢ ∀ {Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U i)) →
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
          ∀ (i : ι), P ((algebraMap S' (Sₜ i)).comp (IsLocalization.map S' f ⋯))

Tactic:
let Mₐ (a : s) : Submonoid (Localization.Away a.val) :=
    (M.map f).map (algebraMap S (Localization.Away a.val))

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
Mₐ : (a : ↑s) → Submonoid (Localization.Away ↑a) :=
  fun a ↦ Submonoid.map (algebraMap S (Localization.Away ↑a)) (Submonoid.map f M)
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
          ∀ (i : ι), P ((algebraMap S' (Sₜ i)).comp (IsLocalization.map S' f ⋯))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case restrict
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens),
    stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f → stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ U)

Tactic:
intro X

Goal state after:
case restrict
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X : Scheme
⊢ ∀ {Y : Scheme} (f : X ⟶ Y) (U : Y.Opens),
    stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f → stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ U)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ U i)) →
        stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
intro X

Goal state after:
case of_sSup_eq_top
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X : Scheme
⊢ ∀ {Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ U i)) →
        stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: case h₁
X Y : Scheme
f : X ⟶ Y
inst✝ : SurjectiveOnStalks f
hf : Function.Injective ⇑f
⊢ Function.Injective
    ⇑(ConcreteCategory.hom
        ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f).hom.base)

Tactic:
exact hf

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

Goal state before:
pp: case restrict
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens),
    stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (U.ι ≫ f)

Tactic:
intro X

Goal state after:
case restrict
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X : Scheme
⊢ ∀ {Y : Scheme} (f : X ⟶ Y) (U : X.Opens),
    stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (U.ι ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)) →
        stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
intro X

Goal state after:
case of_sSup_eq_top
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X : Scheme
⊢ ∀ {Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)) →
        stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case to_basicOpen
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ ∀ {X Y : Scheme} [inst : IsAffine Y] (f : X ⟶ Y) (r : ↑Γ(Y, ⊤)),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ Y.basicOpen r)

Tactic:
intro X

Goal state after:
case to_basicOpen
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
X : Scheme
⊢ ∀ {Y : Scheme} [inst : IsAffine Y] (f : X ⟶ Y) (r : ↑Γ(Y, ⊤)),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ Y.basicOpen r)
Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
x✝¹ : HasPullback f g
x✝ : IsPreimmersion g
this : SurjectiveOnStalks (pullback.fst f g)
x : ↥(pullback f g)
⊢ ((pullback.fst f g) x, (pullback.snd f g) x) ∈ {x | f x.1 = g x.2}

Tactic:
simp only [Set.mem_ofPred, ← Scheme.Hom.comp_apply, pullback.condition]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)
S : Set ↑Y.affineOpens
hS : S.Finite
hU : IsOpen (⋃ i ∈ S, ↑↑i)
hU' : IsCompact (⋃ i ∈ S, ↑↑i)
⊢ IsCompact (⋃ i ∈ S, ⇑f ⁻¹' ↑↑i)

Tactic:
exact Set.Finite.isCompact_biUnion hS (fun i _ => H i i.prop)

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X := ⋯
⊢ ∀ ⦃X Y S : Scheme⦄ [IsAffine S] [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), CompactSpace ↥Y → CompactSpace ↥(pullback f g)

Tactic:
intro X

Goal state after:
X✝ Y : Scheme
f : X✝ ⟶ Y
this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
X : Scheme
⊢ ∀ ⦃Y S : Scheme⦄ [IsAffine S] [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), CompactSpace ↥Y → CompactSpace ↥(pullback f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f ↔
      ∀ (i : 𝒰.I₀), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (𝒰.f i ≫ f)

Tactic:
intro X

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
⊢ ∀ {Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f ↔
      ∀ (i : 𝒰.I₀), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (𝒰.f i ≫ f)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : J.IsPrime
e : I ≤ J
e' : J.primeHeight = I.height
inst✝ : J.FiniteHeight
⊢ J ∈ I.minimalPrimes

Tactic:
rw [← J.height_eq_primeHeight] at e'

Goal state after:
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : J.IsPrime
e : I ≤ J
e' : J.height = I.height
inst✝ : J.FiniteHeight
⊢ J ∈ I.minimalPrimes
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal := ⋯
⊢ ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (pullback.fst f g)

Tactic:
intro X

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X : Scheme
⊢ ∀ ⦃Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (pullback.fst f g)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: P : (X : Scheme) → ↥X → Prop
h₁ : ∀ (R : CommRingCat) (x : ↥(Spec R)), P (Spec R) x
h₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)
⊢ ∀ (X : Scheme) (x : ↥X), P X x

Tactic:
intro X

Goal state after:
P : (X : Scheme) → ↥X → Prop
h₁ : ∀ (R : CommRingCat) (x : ↥(Spec R)), P (Spec R) x
h₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)
X : Scheme
⊢ ∀ (x : ↥X), P X x
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
hf : P f
x : ↥X
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
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
HasRingHomProperty.iff_appLE (P := P),

Goal state after:
case refine_1
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
x : ↥X
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
hf :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
n : ℕ
hn : n ≠ 0
⊢ (I ^ n).support = I.support

Tactic:
cases n <;> simp_all

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↥(I.glueDataObj U)
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((I.glueDataObjι U) p) ∈ X.basicOpen f
this : IsIso (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f))
⊢ (CommRingCat.Hom.hom
        (Hom.appLE (I.glueDataObjι (X.affineBasicOpen f) ≫ X.homOfLE ⋯ ≫ (↑U).ι) (↑V)
          (I.glueDataObjMap ⋯ ⁻¹ᵁ I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f) ⋯))
      x =
    0

Tactic:
rw [Scheme.Hom.appLE]

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↥(I.glueDataObj U)
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((I.glueDataObjι U) p) ∈ X.basicOpen f
this : IsIso (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f))
⊢ (CommRingCat.Hom.hom
        (Hom.app (I.glueDataObjι (X.affineBasicOpen f) ≫ X.homOfLE ⋯ ≫ (↑U).ι) ↑V ≫
          (I.glueDataObj (X.affineBasicOpen f)).presheaf.map (homOfLE ⋯).op))
      x =
    0
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := Y.isBasis_affineOpens.exists_subset_of_mem_open
    (Set.mem_univ (f x)) isOpen_univ

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x : ↥X
⊢ Set.range ⇑(X.fromSpecStalk x) = {y | y ⤳ x}

Tactic:
ext y
  constructor
  · rintro ⟨y, rfl⟩
    exact ((IsLocalRing.specializes_closedPoint y).map (X.fromSpecStalk x).continuous).trans
      (specializes_of_eq fromSpecStalk_closedPoint)
  · rintro (hy : y ⤳ x)
    have := fromSpecStalk_closedPoint (x := y)
    rw [← SpecMap_stalkSpecializes_fromSpecStalk hy] at this
    exact ⟨_, this⟩

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

Goal state before:
pp: case a.inr.refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ (𝒰.f i) x ∈
    Y.zeroLocus
        (⇑(CommRingCat.Hom.hom (appIso (𝒰.f i) ↑⟨⊤, ⋯⟩).inv) ''
          ⇑(CommRingCat.Hom.hom (appIso (𝒰.f i) ↑⟨⊤, ⋯⟩).inv) ⁻¹' ↑((ker f).ideal ⟨𝒰.f i ''ᵁ ↑⟨⊤, ⋯⟩, ⋯⟩)) ∩
      Set.range ⇑(𝒰.f i)

pp: case a.inr.refine_1.H
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ IsPullback (Cover.pullbackHom 𝒰 f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (𝒰.f i) f

Tactic:
Set.image_preimage_eq

Goal state after:
case a.inr.refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ (𝒰.f i) x ∈ Y.zeroLocus ↑((ker f).ideal ⟨𝒰.f i ''ᵁ ↑⟨⊤, ⋯⟩, ⋯⟩) ∩ Set.range ⇑(𝒰.f i)

case a.inr.refine_1.h
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (appIso (𝒰.f i) ↑⟨⊤, ⋯⟩).inv)

case a.inr.refine_1.H
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ IsPullback (Cover.pullbackHom 𝒰 f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (𝒰.f i) f
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case refine_2
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥Y
x✝ : x ∈ ⇑g ⁻¹' Set.range ⇑f
y : ↥X
hy : f y = g x
⊢ x ∈ Set.range ⇑(pullback.snd f g)

Tactic:
· obtain ⟨a, ha⟩ := Triplet.exists_preimage (Triplet.mk' y x hy)
    use a, ha.right

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

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