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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : P.RespectsIso
H : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
this✝ : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤
this :
  f =
    X.topIso.inv ≫
      (X.isoOfEq this✝).inv ≫
        (f ≫ g) ∣_ Scheme.Hom.opensRange g ≫ (IsOpenImmersion.isoOfRangeEq (Scheme.Hom.opensRange g).ι g ⋯).hom
⊢ P ((f ≫ g) ∣_ Scheme.Hom.opensRange g)

Tactic:
exact H _ _ hfg

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

Goal state before:
pp: case h₁
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z],
    (∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ Y) (f₂ : U₂ ⟶ Y) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
        [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ f)) →
      ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
        [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ (e.hom ≫ f))

Tactic:
introv H _ _
    rw [pullback.mapDesc_comp, P.cancel_left_of_respectsIso, P.cancel_right_of_respectsIso]
    apply H

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : IsDominant (f ≫ g)
⊢ IsDominant g

Tactic:
rw [isDominant_iff, denseRange_iff_closure_range, ← Set.univ_subset_iff] at H ⊢
  exact H.trans (closure_mono (Set.range_comp_subset_range f g))

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

Goal state before:
pp: case hP₃
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
x✝ : Continuous[inst✝¹, inst✝] f
hsp :
  ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy✝ : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
hy : ⟨y, hi⟩ ∈ closure[instTopologicalSpaceSubtype] {⟨f x, hfx⟩}
a : ↑(f ⁻¹' (U i).carrier)
ha : a ∈ closure[instTopologicalSpaceSubtype] {⟨x, hfx⟩}
hay : (U i).carrier.restrictPreimage f a = ⟨y, hi⟩
⊢ y ∈ f '' closure[inst✝¹] {x}

Tactic:
closure_subtype

Goal state after:
case hP₃
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
x✝ : Continuous[inst✝¹, inst✝] f
hsp :
  ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy✝ : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
hy : ⟨y, hi⟩ ∈ closure[instTopologicalSpaceSubtype] {⟨f x, hfx⟩}
a : ↑(f ⁻¹' (U i).carrier)
ha : ↑a ∈ closure[inst✝¹] (Subtype.val '' {⟨x, hfx⟩})
hay : (U i).carrier.restrictPreimage f a = ⟨y, hi⟩
⊢ y ∈ f '' closure[inst✝¹] {x}
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f ↔
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
            P ((algebraMap S Sₜ).comp f)

Tactic:
by
  rw [locally_iff_finite P f]
  refine ⟨fun ⟨s, hsone, hs⟩ ↦ ⟨s, hsone, fun t ht Sₜ _ _ _ ↦ ?_⟩, fun ⟨s, hsone, hs⟩ ↦ ?_⟩
  · let e : Localization.Away t ≃+* Sₜ :=
      (IsLocalization.algEquiv (Submonoid.powers t) _ _).toRingEquiv
    have : algebraMap S Sₜ = e.toRingHom.comp (algebraMap S (Localization.Away t)) :=
      RingHom.ext (fun x ↦ (AlgEquiv.commutes (IsLocalization.algEquiv _ _ _) _).symm)
    rw [this, RingHom.comp_assoc]
    exact hP.left _ _ (hs t ht)
  · exact ⟨s, hsone, fun t ht ↦ hs t ht _⟩

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine ((𝒰' i).X j)
h𝒰' : ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀), Q (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i))
⊢ P.diagonal f

Tactic:
let := isLocal_affineProperty P
  let 𝒱 := (Scheme.Pullback.openCoverOfBase 𝒰 f f).bind fun i =>
    Scheme.Pullback.openCoverOfLeftRight.{u} (𝒰' i) (𝒰' i) (pullback.snd _ _) (pullback.snd _ _)
  have i1 : ∀ i, IsAffine (𝒱.X i) := fun i => by dsimp [𝒱]; infer_instance
  apply of_openCover 𝒱
  rintro ⟨i, j, k⟩
  dsimp [𝒱]
  convert!
    (Q.cancel_left_of_respectsIso
          ((pullbackDiagonalMapIso _ _ ((𝒰' i).f j) ((𝒰' i).f k)).inv ≫
            pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) _ _)
          (pullback.snd _ _)).mp
      _
      using 1
  · simp
  · ext1 <;> simp
  · simp only [Category.assoc, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app,
      Category.comp_id]
    convert! h𝒰' i j k
    ext1 <;> simp [Scheme.Cover.pullbackHom]

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

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝² : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
α β : Type u
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hf : Continuous f
hs : IsOpen s
H : P f
⊢ P (s.restrictPreimage f)

Tactic:
refine (hP f (![⊤, Opens.mk s hs] ∘ Equiv.ulift) ?_ hf).mp H ⟨1⟩

Goal state after:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝² : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
α β : Type u
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hf : Continuous f
hs : IsOpen s
H : P f
⊢ IsOpenCover (![⊤, { carrier := s, is_open' := hs }] ∘ ⇑Equiv.ulift)
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ RingHom.SurjectiveOnStalks

Tactic:
apply RingHom.IsStableUnderBaseChange.mk

Goal state after:
case h₁
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ RingHom.SurjectiveOnStalks

case h₂
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    (algebraMap R T).SurjectiveOnStalks → (algebraMap S (TensorProduct R S T)).SurjectiveOnStalks
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ IsSpectralMap ⇑f

Tactic:
by
  rwa [← quasiCompact_iff_isSpectralMap]

Goal state after:
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, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
U : ↑X.affineOpens
hU : ↑U ≤ f ⁻¹ᵁ Y.basicOpen r
this : X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r) = ↑U
⊢ P
    (CommRingCat.Hom.hom
      (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r)) ⋯))

Tactic:
IsAffineOpen.appLE_eq_away_map f (isAffineOpen_top Y) U.2 _ r

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 Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
U : ↑X.affineOpens
hU : ↑U ≤ f ⁻¹ᵁ Y.basicOpen r
this : X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r) = ↑U
⊢ P
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))))
          (↑(X.presheaf.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r)))))
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r)))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case h₇₅
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
⊢ ↑S ⊓ X.basicOpen f ≤ U₁ ⊓ X.basicOpen f

Tactic:
exact inf_le_inf h₁ le_rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
q : Ideal R
hq : q ∈ (span {x}).minimalPrimes
⊢ 1 ≤ q.height

Tactic:
have : q.IsPrime := hq.isPrime

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
q : Ideal R
hq : q ∈ (span {x}).minimalPrimes
this : q.IsPrime
⊢ 1 ≤ q.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
h1 : p.height = 1
x : R
hx : x ∈ p
hxp : Prime x
this✝ : (span {x}).IsPrime
this : p.FiniteHeight
hne : p ≠ span {x}
⊢ span {x} = ⊥

Tactic:
← height_eq_zero_iff_eq_bot,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
h1 : p.height = 1
x : R
hx : x ∈ p
hxp : Prime x
this✝ : (span {x}).IsPrime
this : p.FiniteHeight
hne : p ≠ span {x}
⊢ (span {x}).height = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: P : {X : Scheme} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U
h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [inst : IsOpenImmersion f], ∃ U V, U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat), P ⊤
x : ↥U
j : X.affineBasisCover.I₀
hx : ↑x ∈ Set.range ⇑(X.affineBasisCover.f j)
i : Set.range ⇑(X.affineBasisCover.f j) ⊆ ↑U
U' : Opens ↥X := { carrier := Set.range ⇑(X.affineBasisCover.f j), is_open' := ⋯ }
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V

Tactic:
let i' : U' ⟶ U := homOfLE i

Goal state after:
P : {X : Scheme} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U
h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [inst : IsOpenImmersion f], ∃ U V, U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat), P ⊤
x : ↥U
j : X.affineBasisCover.I₀
hx : ↑x ∈ Set.range ⇑(X.affineBasisCover.f j)
i : Set.range ⇑(X.affineBasisCover.f j) ⊆ ↑U
U' : Opens ↥X := { carrier := Set.range ⇑(X.affineBasisCover.f j), is_open' := ⋯ }
i' : U' ⟶ U := homOfLE i
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₁
X✝ X : Scheme
U : X.Opens
H✝ :
  ∀ (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V),
        ∃ x,
          ∀ [hX : IsReduced X] (s : ↑Γ(X, V)),
            X.basicOpen s = ⊥ → ∀ (x : ↥X) (hx : x ∈ V), (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) s = 0
hX : IsReduced X
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↥X
hx✝ : x ∈ U
V : X.Opens
hx : ↑⟨x, hx✝⟩ ∈ V
i : V ⟶ U
H :
  X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i.op)) s) = ⊥ →
    ∀ (x : ↥X) (hx : x ∈ V),
      (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) ((ConcreteCategory.hom (X.presheaf.map i.op)) s) = 0
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx✝)) s = 0

Tactic:
Scheme.basicOpen_res,

Goal state after:
case h₁
X✝ X : Scheme
U : X.Opens
H✝ :
  ∀ (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V),
        ∃ x,
          ∀ [hX : IsReduced X] (s : ↑Γ(X, V)),
            X.basicOpen s = ⊥ → ∀ (x : ↥X) (hx : x ∈ V), (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) s = 0
hX : IsReduced X
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↥X
hx✝ : x ∈ U
V : X.Opens
hx : ↑⟨x, hx✝⟩ ∈ V
i : V ⟶ U
H :
  V ⊓ X.basicOpen s = ⊥ →
    ∀ (x : ↥X) (hx : x ∈ V),
      (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) ((ConcreteCategory.hom (X.presheaf.map i.op)) s) = 0
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx✝)) s = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case refine_2
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
e : Γ(X, { carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ }) ≅
  CommRingCat.of
    ↑((X.sheaf.obj.obj (op { carrier := Sᶜ, is_open' := ⋯ })).prodFan
          (X.sheaf.obj.obj (op { carrier := Tᶜ, is_open' := ⋯ }))).1 :=
  (X.sheaf.isProductOfDisjoint { carrier := Sᶜ, is_open' := ⋯ } { carrier := Tᶜ, is_open' := ⋯ }
        ?refine_1).conePointUniqueUpToIso
    ((X.sheaf.obj.obj (op { carrier := Sᶜ, is_open' := ⋯ })).prodFanIsLimit
      (X.sheaf.obj.obj (op { carrier := Tᶜ, is_open' := ⋯ })))
⊢ False

pp: case refine_1
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
⊢ { carrier := Sᶜ, is_open' := ⋯ } ⊓ { carrier := Tᶜ, is_open' := ⋯ } = ⊥

Tactic:
· have : IsDomain (Γ(X, ⟨Sᶜ, hS.1⟩) × Γ(X, ⟨Tᶜ, hT.1⟩)) :=
      e.symm.commRingCatIsoToRingEquiv.toMulEquiv.isDomain _
    exact false_of_nontrivial_of_product_domain Γ(X, ⟨Sᶜ, hS.1⟩) Γ(X, ⟨Tᶜ, hT.1⟩)

Goal state after:
case refine_1
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
⊢ { carrier := Sᶜ, is_open' := ⋯ } ⊓ { carrier := Tᶜ, is_open' := ⋯ } = ⊥
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
z : ↥X
n : ℕ
hz : coheight z ≤ ↑n
⊢ ↑(coheight z) ≤ ↑n

Tactic:
exact_mod_cast hz

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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
⊢ IsOpenImmersion (Spec.map f) ↔ ∃ e, IsIdempotentElem e ∧ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}

Tactic:
by
  constructor
  · intro H
    obtain ⟨e, he, he'⟩ := PrimeSpectrum.isClopen_iff_zeroLocus.mp
      ⟨PrimeSpectrum.isClosed_range_comap_of_surjective _ _ hf,
        (Spec.map f).isOpenEmbedding.isOpen_range⟩
    refine ⟨e, he, ?_⟩
    let φ : R ⟶ _ := (CommRingCat.ofHom (Ideal.Quotient.mk (.span {e})))
    have : IsOpenImmersion (Spec.map φ) :=
      have : IsLocalization.Away (1 - e) (↑R ⧸ Ideal.span {e}) :=
        IsLocalization.away_of_isIdempotentElem he.one_sub (by simp) Ideal.Quotient.mk_surjective
      IsOpenImmersion.of_isLocalization (1 - e)
    have H : Set.range (Spec.map φ) = Set.range (Spec.map f) :=
      ((range_comap_of_surjective _ _
        Ideal.Quotient.mk_surjective).trans (by simp)).trans he'.symm
    let i : S ≅ .of _ := (Scheme.Spec.preimageIso
      (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
    have hi : Function.Injective i.inv.hom := (ConcreteCategory.bijective_of_isIso i.inv).1
    have : f = φ ≫ i.inv := by apply Spec.map_injective; simp [i, ← Scheme.Spec_map]
    rw [this, CommRingCat.hom_comp, RingHom.ker_eq_comap_bot, ← Ideal.comap_comap,
      ← RingHom.ker_eq_comap_bot, (RingHom.injective_iff_ker_eq_bot i.inv.hom).mp hi,
      ← RingHom.ker_eq_comap_bot]
    simp [φ]
  · rintro ⟨e, he, he'⟩
    let := f.hom.toAlgebra
    have : IsLocalization.Away (1 - e) S :=
      IsLocalization.away_of_isIdempotentElem he.one_sub (by simpa using! he') hf
    exact IsOpenImmersion.of_isLocalization (1 - e)

Goal state after:
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✝
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hY : IsAffine Y
this : ∀ {X : Scheme} {f : X ⟶ Y}, (∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) → IsAffine X → P f
hX : ¬IsAffine X
U : ↑X.affineOpens
x : ↥↑↑U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f ((↑U).ι x)))

Tactic:
exact H x.val

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (I.ideal U)

Tactic:
let φ : Γ(X, U) ⟶ CommRingCat.of (Γ(X, U) ⧸ I.ideal U) :=
    CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
  rw [← Ideal.mk_ker (I := I.ideal _)]
  change RingHom.ker (Spec.map φ ≫ _).appTop.hom = (RingHom.ker φ.hom).comap _
  rw [← RingHom.ker_equiv_comp _ (Scheme.ΓSpecIso _).commRingCatIsoToRingEquiv, RingHom.comap_ker,
    RingEquiv.toRingHom_eq_coe, Iso.commRingCatIsoToRingEquiv_toRingHom, ← CommRingCat.hom_comp,
    ← CommRingCat.hom_comp]
  congr 2
  simp only [Scheme.Hom.comp_app, TopologicalSpace.Opens.map_top, Category.assoc,
    Scheme.ΓSpecIso_naturality, Scheme.Opens.topIso_hom]
  rw [← Scheme.Hom.appTop, U.2.isoSpec_inv_appTop, Category.assoc, Iso.inv_hom_id_assoc]
  simp only [Scheme.Opens.topIso_hom]

Goal state after:
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✝ : 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 ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
h : IsAffine X ∧ IsAffine Y
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
obtain ⟨hX, hY⟩ := h

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✝ : 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 ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
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)
⊢ p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V)) →
    ∃ V_1,
      ∃ (hV : V_1 ≤ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))),
        p ∈ V_1 ∧
          (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE hV).op))
              ((CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V))) x) =
            (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE hV).op)) 0

Tactic:
hp

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))
⊢ ∃ V_1,
    ∃ (hV : V_1 ≤ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))),
      p ∈ V_1 ∧
        (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE hV).op))
            ((CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V))) x) =
          (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE hV).op)) 0
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))
⊢ (ConcreteCategory.hom (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f)))
      ((ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE ⋯).op))
        ((CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V))) x)) =
    (ConcreteCategory.hom (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f)))
      ((ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE ⋯).op)) 0)

Tactic:
simp only [map_zero, ← RingHom.comp_apply,
    ← CommRingCat.hom_comp, Category.assoc]

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 (↑U).ι ↑V ≫
          Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V) ≫
            (I.glueDataObj U).presheaf.map (homOfLE ⋯).op ≫
              Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f)))
      x =
    0