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

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this✝ : HasPullback (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ pullback (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g ⟶ pullback (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g

Tactic:
refine pullback.map _ _ _ _ (pullbackSymmetry _ _).hom (𝟙 _) (𝟙 _) ?_ ?_

Goal state after:
case refine_1
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this✝ : HasPullback (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) ≫ 𝟙 Z =
    (pullbackSymmetry (𝒰.f j) (𝒰.f i)).hom ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f

case refine_2
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this✝ : HasPullback (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥Y
this : IsEmpty ↥X
x : ↥Y
⊢ ∃ a, f a = x

Tactic:
exact isEmptyElim x

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝² : Category.{v, w} J
F : J ⥤ Scheme
inst✝¹ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝ : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst
hlk : l ⟶ k₂.fst
z : (F ⋙ forget).obj l
hy₁ : (F.map k₁.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hli)) z) = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
hy₂ : (F.map k₂.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hlk)) z) = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯)
    ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯) ⋯
⊢ ∃ l fi fj fk α z,
    IsOpenImmersion α ∧
      α ≫ pullback.fst (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧
        α ≫ pullback.snd (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧ α z = x

Tactic:
have : IsOpenImmersion α := by
    apply +allowSynthFailures IsOpenImmersion.of_comp
    · exact (inferInstance : IsOpenImmersion (pullback.fst (V F i j).ι (V F i k).ι))
    · simp only [limit.lift_π, PullbackCone.mk_π_app, α]
      infer_instance

Goal state after:
J : Type w
inst✝² : Category.{v, w} J
F : J ⥤ Scheme
inst✝¹ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝ : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst
hlk : l ⟶ k₂.fst
z : (F ⋙ forget).obj l
hy₁ : (F.map k₁.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hli)) z) = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
hy₂ : (F.map k₂.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hlk)) z) = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯)
    ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯) ⋯
this : IsOpenImmersion α
⊢ ∃ l fi fj fk α z,
    IsOpenImmersion α ∧
      α ≫ pullback.fst (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧
        α ≫ pullback.snd (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧ α z = x
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
⊢ Hom.opensRange ι₁ ⊓ U ⊔ Hom.opensRange ι₂ ⊓ U = U

Tactic:
rw [← inf_sup_right, (isCompl_opensRange_inl_inr X Y).sup_eq_top, top_inf_eq]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
this :
  Scheme.Hom.stalkMap (coprod.inl ≫ coprodSpec R S) x ≫ inv (Scheme.Hom.stalkMap coprod.inl x) =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inl x)
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inl x)))

Tactic:
Scheme.Hom.stalkMap_congr_hom _ (Spec.map _) (coprodSpec_inl R S)

Goal state after:
case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
this :
  (((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x) =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inl x)
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inl x)))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCatᵒᵖ
⊢ IsIso (coprodComparison Scheme.Spec R S)

Tactic:
by
  obtain ⟨R⟩ := R; obtain ⟨S⟩ := S
  have : coprodComparison Scheme.Spec (.op R) (.op S) ≫ (Spec.map
    ((limit.isoLimitCone ⟨_, CommRingCat.prodFanIsLimit R S⟩).inv ≫
      (opProdIsoCoprod R S).unop.inv)) = coprodSpec R S := by
    ext1
    · rw [coprodComparison_inl_assoc, coprodSpec, coprod.inl_desc, Scheme.Spec_map,
        ← Spec.map_comp, Category.assoc, Iso.unop_inv, opProdIsoCoprod_inv_inl,
        limit.isoLimitCone_inv_π]
      rfl
    · rw [coprodComparison_inr_assoc, coprodSpec, coprod.inr_desc, Scheme.Spec_map,
        ← Spec.map_comp, Category.assoc, Iso.unop_inv, opProdIsoCoprod_inv_inr,
        limit.isoLimitCone_inv_π]
      rfl
  rw [(IsIso.eq_comp_inv _).mpr this]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
I : (diagonalCover f 𝒰 𝒱).I₀
⊢ (diagonalCover f 𝒰 𝒱).f I =
    pullback.map ((𝒱 I.fst).f I.snd.1 ≫ Cover.pullbackHom 𝒰 f I.fst) ((𝒱 I.fst).f I.snd.2 ≫ Cover.pullbackHom 𝒰 f I.fst)
      f f ((𝒱 I.fst).f I.snd.1 ≫ pullback.fst f (𝒰.f I.fst)) ((𝒱 I.fst).f I.snd.2 ≫ pullback.fst f (𝒰.f I.fst))
      (𝒰.f I.fst) ⋯ ⋯

Tactic:
by
  cases I
  ext1 <;> simp [diagonalCover, Cover.pullbackHom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case mp
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i : Shrink.{u, w} J
xi : ↥(F.obj ↓i)
j : Shrink.{u, w} J
xj : ↥(F.obj ↓j)
⊢ ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv ((colimit.ι F ↓i) xi) =
      ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv ((colimit.ι F ↓j) xj) →
    ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj

Tactic:
simp only [Limits.colimit, ← Scheme.Hom.comp_apply,
    colimit.comp_coconePointUniqueUpToIso_inv, cocone, glueDataι_naturality]

Goal state after:
case mp
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i : Shrink.{u, w} J
xi : ↥(F.obj ↓i)
j : Shrink.{u, w} J
xj : ↥(F.obj ↓j)
⊢ ((glueData F).ι i) xi = ((glueData F).ι j) xj → ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case mp
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
⊢ ∃ k fi fj x_1, (F.map fi) x_1 = ((glueData F).f i j) x ∧ (F.map fj) x_1 = ((glueData F).t i j ≫ (glueData F).f j i) x

Tactic:
obtain ⟨⟨k, ki, kj⟩, y, hy : F.map ki y = (glueData F).f i j x⟩ := mem_iSup.mp x.2

Goal state after:
case mp
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : J
ki : k ⟶ ↓(i, j).1
kj : k ⟶ ↓(i, j).2
y : ↥(F.obj ⟨k, (ki, kj)⟩.fst)
hy : (F.map ki) y = ((glueData F).f i j) x
⊢ ∃ k fi fj x_1, (F.map fi) x_1 = ((glueData F).f i j) x ∧ (F.map fj) x_1 = ((glueData F).t i j ≫ (glueData F).f j i) x
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
⊢ ↑sg ⊆
    ↑(Ideal.span
        (Set.range fun x ↦
          match x with
          | (a, b) => g ↑a * ↑b))

Tactic:
intro t

Goal state after:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
t : T
⊢ t ∈ ↑sg →
    t ∈
      ↑(Ideal.span
          (Set.range fun x ↦
            match x with
            | (a, b) => g ↑a * ↑b))
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap T (Localization.Away t)).comp f)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp (algebraMap R S))

Tactic:
refine ⟨s, hsone, fun t ht ↦ ?_⟩

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
f : S →+* T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap T (Localization.Away t)).comp f)
t : T
ht : t ∈ s
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap T (Localization.Away t)).comp (f.comp (algebraMap R S)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ → (∀ (i : ι), P.universally (f ∣_ U i)) → P.universally f

Tactic:
· intro X Y f ι U hU H X' Y' i₁ i₂ f' h
    apply hP₂ _ (fun i ↦ i₂ ⁻¹ᵁ U i)
    · simp only [IsOpenCover, ← top_le_iff] at hU ⊢
      rintro x -
      simpa using @hU (i₂ x) trivial
    · rintro i
      refine H _ ((X'.isoOfEq ?_).hom ≫ i₁ ∣_ _) (i₂ ∣_ _) _ ?_
      · exact congr($(h.1.1) ⁻¹ᵁ U i)
      · rw [← (isPullback_morphismRestrict f _).paste_vert_iff]
        · simp only [Category.assoc, morphismRestrict_ι, Scheme.isoOfEq_hom_ι_assoc]
          exact (isPullback_morphismRestrict f' (i₂ ⁻¹ᵁ U i)).paste_vert h
        · rw [← cancel_mono (Scheme.Opens.ι _)]
          simp [morphismRestrict_ι_assoc, h.1.1]

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

Goal state before:
pp: x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ SurjectiveOnStalks x✝ ↔ stalkwise (fun {R S} [CommRing R] [CommRing S] x ↦ Function.Surjective ⇑x) x✝

Tactic:
exact surjectiveOnStalks_iff _

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

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

Tactic:
exact Function.Surjective.of_comp this

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

Goal state before:
pp: 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
⊢ IsZariskiLocalAtSource (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P)

Tactic:
let := stalkwise_respectsIso hP
  apply IsZariskiLocalAtSource.mk'
  · intro X Y f U hf x
    rw [Scheme.Hom.stalkMap_comp, CommRingCat.hom_comp, hP.cancel_right_isIso]
    exact hf _
  · intro X Y f ι U hU hf x
    have hy : x ∈ iSup U := by rw [hU]; trivial
    obtain ⟨i, hi⟩ := Opens.mem_iSup.mp hy
    rw [← hP.cancel_right_isIso _ ((U i).ι.stalkMap ⟨x, hi⟩)]
    simpa [Scheme.Hom.stalkMap_comp] using hf i ⟨x, hi⟩

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

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

Tactic:
by
    have h := (f ≫ g).isEmbedding
    rwa [← g.isEmbedding.of_comp_iff]

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

Goal state before:
pp: case hb
X : Scheme
U : Set ↥X
⊢ Opens.IsBasis (Set.range fun U ↦ ↑U)

Tactic:
rw [Subtype.range_coe]

Goal state after:
case hb
X : Scheme
U : Set ↥X
⊢ Opens.IsBasis X.affineOpens
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U V : ↑X.affineOpens
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
⊢ IsCompact (↑↑U ∩ ↑↑V)

Tactic:
have e := g.isOpenEmbedding.isEmbedding.toHomeomorph

Goal state after:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U V : ↑X.affineOpens
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
e : ↥(pullback (↑U).ι (↑V).ι) ≃ₜ ↑(Set.range ⇑g)
⊢ IsCompact (↑↑U ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
⊢ CompactSpace ↥(pullback f₁ f₂)

Tactic:
have e := g.isOpenEmbedding.isEmbedding.toHomeomorph

Goal state after:
case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
e : ↥(pullback f₁ f₂) ≃ₜ ↑(Set.range ⇑g)
⊢ CompactSpace ↥(pullback f₁ f₂)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ ↑(r + 1) ∧ ↑(r + 1) ≤ J.height

Tactic:
refine ⟨J ⊔ Ideal.span {x}, sup_le h₁ ?_, ?_, ?_⟩

Goal state after:
case succ.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
⊢ span {x} ≤ I

case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
⊢ Submodule.spanRank (J ⊔ span {x}) ≤ ↑(r + 1)

case succ.refine_3
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
⊢ ↑(r + 1) ≤ (J ⊔ span {x}).height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ↑(⨆ I, ⨆ (_ : I.IsMaximal), I.height) = ringKrullDim R

Tactic:
by
  rw [← Ideal.sup_height_eq_ringKrullDim, WithBot.coe_inj]
  apply le_antisymm
  · exact iSup_mono fun I => iSup_mono' fun hI => ⟨hI.isPrime.ne_top , le_rfl⟩
  · refine iSup_mono' fun I => ?_
    obtain rfl | I_top := eq_or_ne I ⊤
    · exact ⟨⊥, by grind [iSup_le_iff, Ideal.IsPrime.ne_top]⟩
    · obtain ⟨M, hM, hIM⟩ := exists_le_maximal I I_top
      exact ⟨M, iSup_mono' (fun hI ↦ ⟨hM, height_mono hIM⟩)⟩

Goal state after:
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
⊢ p = span {x}

Tactic:
by_contra! hne

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}
⊢ False
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case refine_1.mp
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' := ⋯ })
x : ↥X
⊢ x ∈ ↑({ carrier := Sᶜ, is_open' := ⋯ } ⊓ { carrier := Tᶜ, is_open' := ⋯ }) → x ∈ ↑⊥

pp: case refine_1.mpr
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' := ⋯ })
x : ↥X
⊢ x ∈ ↑⊥ → x ∈ ↑({ carrier := Sᶜ, is_open' := ⋯ } ⊓ { carrier := Tᶜ, is_open' := ⋯ })

Tactic:
· rintro ⟨hS, hT⟩
      rcases h₁ (show x ∈ ⊤ by trivial) with h | h
      exacts [hS h, hT h]

Goal state after:
case refine_1.mpr
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' := ⋯ })
x : ↥X
⊢ x ∈ ↑⊥ → x ∈ ↑({ carrier := Sᶜ, is_open' := ⋯ } ⊓ { carrier := Tᶜ, is_open' := ⋯ })
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ IsIso (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (eqToHom ⋯).op)

Tactic:
rw [ConcreteCategory.isIso_iff_bijective]

Goal state after:
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ Function.Bijective
    ⇑(ConcreteCategory.hom (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (eqToHom ⋯).op))
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
⊢ IsOpenImmersion f

Tactic:
by
  refine IsOpenImmersion.iff_isIso_stalkMap.mpr
    ⟨.of_continuous_injective_isOpenMap f.continuous hf ?_, ?_⟩
  · intro U hU
    convert! (⨆ i, ((𝒰.f i ≫ f) ''ᵁ (𝒰.f i ⁻¹ᵁ ⟨U, hU⟩))).2
    ext x
    exact ⟨fun ⟨x, _, _⟩ ↦ by have := 𝒰.exists_eq x; simp; grind, by simp; grind⟩
  · intro x
    obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
    rw [← (IsIso.comp_inv_eq _).mpr (Scheme.Hom.stalkMap_comp (𝒰.f i) f x)]
    infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x y : ↥X
h : x ⤳ y
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hyU : y ∈ ↑U
hxU : x ∈ U
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x

Tactic:
rw [← hU.fromSpecStalk_eq_fromSpecStalk hyU, ← hU.fromSpecStalk_eq_fromSpecStalk hxU,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpecStalk, ← Category.assoc, ← Spec.map_comp,
    TopCat.Presheaf.germ_stalkSpecializes]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
⊢ (∀ (U : ↑X.affineOpens), ↑Z ∩ ↑↑U ⊆ ↑I.support ∩ ↑↑U) ↔
    ∀ (U : ↑X.affineOpens), ⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z ⊆ PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
refine forall_congr' fun U ↦ ?_

Goal state after:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
⊢ ↑Z ∩ ↑↑U ⊆ ↑I.support ∩ ↑↑U ↔ ⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z ⊆ PrimeSpectrum.zeroLocus ↑(I.ideal U)
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
xf : (x : ↥X) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
⊢ (fun f ↦ ⟨f (closedPoint ↑R), ⟨Scheme.stalkClosedPointTo f, ⋯⟩⟩)
      ((fun xf ↦ Spec.map ↑xf.snd ≫ X.fromSpecStalk xf.fst) xf) =
    xf

Tactic:
by
    obtain ⟨x, ⟨f, hf⟩⟩ := xf
    symm
    refine SpecToEquivOfLocalRing_eq_iff.mpr ⟨?_, ?_⟩
    · simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Function.comp_apply, Spec_closedPoint,
        Scheme.fromSpecStalk_closedPoint]
    · refine TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ?_
      simp only [Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk,
        TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes_assoc]

Goal state after: