mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
s : Cocone F
i j : (glueData F).J
k : (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).I₀
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [homOfLE_tAux_assoc F ↓i ↓j k.2.1 k.2.2, Iso.eq_inv_comp]

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
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
s : Cocone F
i j : (glueData F).J
k : (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).I₀
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.t i j ≫ D.f j i).c.app
      (op
        ((Opens.map
              (colimit.ι D.diagram.multispan
                  (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
          (⋯.functor.obj U))))

Tactic:
comp_c_app

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.f j i).c.app
        (op
          ((Opens.map
                (colimit.ι D.diagram.multispan
                    (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
            (⋯.functor.obj U))) ≫
      (D.t i j).c.app
        (op
          ((Opens.map (D.f j i).base).obj
            (unop
              (op
                ((Opens.map
                      (colimit.ι D.diagram.multispan
                          (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
                  (⋯.functor.obj U)))))))
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Injective)

Tactic:
by
  refine topologically_isZariskiLocalAtTarget _ (fun _ s _ _ h ↦ h.restrictPreimage s)
    fun f ι U H _ hf x₁ x₂ e ↦ ?_
  obtain ⟨i, hxi⟩ : ∃ i, f x₁ ∈ U i := by simpa using congr(f x₁ ∈ $H)
  exact congr(($(@hf i ⟨x₁, hxi⟩ ⟨x₂, show f x₂ ∈ U i from e ▸ hxi⟩ (Subtype.ext e))).1)

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

Goal state before:
pp: case hP₂
⊢ ∀ {α β γ : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ]
    (f : α → β) (g : β → γ), SpecializingMap f → SpecializingMap g → SpecializingMap (g ∘ f)

Tactic:
introv hf hg
    exact hf.comp hg

Goal state after:
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: case tmul
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : T
⊢ ∃ a, (algebraMap S (S ⊗[R] T)) a = x ⊗ₜ[R] y

Tactic:
obtain ⟨y, rfl⟩ := h y

Goal state after:
case tmul
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : R
⊢ ∃ a, (algebraMap S (S ⊗[R] T)) a = x ⊗ₜ[R] (algebraMap R T) y
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
⊢ Function.Surjective ⇑f

Tactic:
rw [← Set.range_eq_univ, Set.eq_univ_iff_forall]

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
⊢ ∀ (x : S), x ∈ Set.range ⇑f
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y} f U ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P (pullback.diagonal (U.ι ≫ f))

Tactic:
apply P.of_postcomp (W' := @IsOpenImmersion) (pullback.diagonal (U.ι ≫ f)) (g f U) inferInstance

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f := ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P (pullback.diagonal (U.ι ≫ f) ≫ g f U)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
hP :
  ∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β)
    (g : β → γ), P f → P g → P (g ∘ f)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
hg : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) g
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ≫ g)

Tactic:
by
    simp only [topologically, Scheme.Hom.comp_base, TopCat.coe_comp]
    exact hP _ _ hf hg

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
⊢ ∃ r s,
    ∃ (_ : x ∈ X.basicOpen s) (e : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))

Tactic:
obtain ⟨r, r', hBrr', hBfx⟩ := exists_basicOpen_le_affine_inter U₁.2 U₂.2 (f x)
    ⟨hfx₁, e₂ hx₂⟩

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
⊢ ∃ r s,
    ∃ (_ : x ∈ X.basicOpen s) (e : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
this✝ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
this : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine ((X.openCoverOfIsOpenCover U hU).X i)
⊢ AffineTargetMorphismProperty.diagonal (fun X x x_1 x_2 ↦ CompactSpace ↥X) X.toSpecΓ

Tactic:
refine AffineTargetMorphismProperty.diagonal_of_openCover_source _
    (Scheme.openCoverOfIsOpenCover _ _ hU) fun i j ↦ ?_

Goal state after:
X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
this✝ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
this : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine ((X.openCoverOfIsOpenCover U hU).X i)
i j : (X.openCoverOfIsOpenCover U hU).I₀
⊢ CompactSpace ↥(pullback ((X.openCoverOfIsOpenCover U hU).f i) ((X.openCoverOfIsOpenCover U hU).f j))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
this✝ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
this : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine ((X.openCoverOfIsOpenCover U hU).X i)
i j : (X.openCoverOfIsOpenCover U hU).I₀
⊢ CompactSpace ↥(pullback ((X.openCoverOfIsOpenCover U hU).f i) ((X.openCoverOfIsOpenCover U hU).f j))

Tactic:
rw [← isCompact_univ_iff, (pullback.fst ((X.openCoverOfIsOpenCover U hU).f i)
    ((X.openCoverOfIsOpenCover U hU).f j) ≫
    (X.openCoverOfIsOpenCover U hU).f i).isOpenEmbedding.isCompact_iff, Set.image_univ,
    IsOpenImmersion.range_pullback_to_base_of_left]

Goal state after:
X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
this✝ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
this : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine ((X.openCoverOfIsOpenCover U hU).X i)
i j : (X.openCoverOfIsOpenCover U hU).I₀
⊢ IsCompact (Set.range ⇑((X.openCoverOfIsOpenCover U hU).f i) ∩ Set.range ⇑((X.openCoverOfIsOpenCover U hU).f j))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op U₃))
h₄₁ : U₄ ≤ U₁
h₄₂ : U₄ ≤ U₂
h₅₁ : U₅ ≤ U₁
h₅₃ : U₅ ≤ U₃
h₆₂ : U₆ ≤ U₂
h₆₃ : U₆ ≤ U₃
h₇₄ : U₇ ≤ U₄
h₇₅ : U₇ ≤ U₅
h₇₆ : U₇ ≤ U₆
e₁ : (y₁ |_ U₅) h₅₁ = ((f |_ U₁) ⋯ |_ U₅) h₅₁ ^ n₁ * (x |_ U₅) h₅₃
e₂ : (y₂ |_ U₆) h₆₂ = ((f |_ U₂) ⋯ |_ U₆) h₆₂ ^ n₂ * (x |_ U₆) h₆₃
⊢ ((((f |_ U₁) ⋯ ^ n₂ * y₁) |_ U₄) h₄₁ |_ U₇) h₇₄ = ((((f |_ U₂) ⋯ ^ n₁ * y₂) |_ U₄) h₄₂ |_ U₇) h₇₄

Tactic:
apply_fun (fun x : F.obj (op U₅) ↦ x |_ U₇) at e₁
  apply_fun (fun x : F.obj (op U₆) ↦ x |_ U₇) at e₂
  dsimp only [TopCat.Presheaf.restrictOpenCommRingCat_apply] at e₁ e₂ ⊢
  simp only [map_mul, map_pow, ← op_comp, ← F.map_comp, homOfLE_comp, ← CommRingCat.comp_apply]
    at e₁ e₂ ⊢
  rw [e₁, e₂, mul_left_comm]

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
R S : CommRingCat
φ : R ⟶ S
H : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)

Tactic:
rw [iff_of_isAffine (P := P), ← H.cancel_right_isIso _ (Scheme.ΓSpecIso _).hom,
    ← CommRingCat.hom_comp, Scheme.ΓSpecIso_naturality, CommRingCat.hom_comp, H.cancel_left_isIso]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
e : I ≤ J
inst✝¹ : J.IsPrime
inst✝ : J.FiniteHeight
e' : J.height ≤ I.height
p : Ideal R
h₁ : p ∈ I.minimalPrimes
h₂ : p ≤ J
h₃ : p < J
⊢ False

Tactic:
have := h₁.isPrime

Goal state after:
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
e : I ≤ J
inst✝¹ : J.IsPrime
inst✝ : J.FiniteHeight
e' : J.height ≤ I.height
p : Ideal R
h₁ : p ∈ I.minimalPrimes
h₂ : p ≤ J
h₃ : p < J
this : p.IsPrime
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
U : Opens ↥X
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f g s : ↑Γ(X, U)
hfg : (f |_ X.basicOpen s) ⋯ = (g |_ X.basicOpen s) ⋯
⊢ ∃ n, s ^ n * f = s ^ n * g

Tactic:
obtain ⟨n, hc⟩ := (isLocalization_basicOpen_of_qcqs hU hU' s).exists_of_eq s hfg

Goal state after:
X : Scheme
U : Opens ↥X
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f g s : ↑Γ(X, U)
hfg : (f |_ X.basicOpen s) ⋯ = (g |_ X.basicOpen s) ⋯
n : ℕ
hc : s ^ n * f = s ^ n * g
⊢ ∃ n, s ^ n * f = s ^ n * g
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

Tactic:
simp_all

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

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

Tactic:
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))
⊢ (X.homOfLE ⋯ ≫ (↑U).ι) ⁻¹ᵁ ↑V = ⊤

Tactic:
simp only [Scheme.homOfLE_ι, ← top_le_iff]

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))
⊢ ⊤ ≤ (X.basicOpen f).ι ⁻¹ᵁ ↑V
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U : Y.Opens
V : ↑(↑U).affineOpens
⊢ (Hom.ker (f ∣_ U)).ideal V = f.ker.ideal ⟨U.ι ''ᵁ ↑V, ⋯⟩

Tactic:
ext x
  simpa [Scheme.Hom.appLE] using! map_eq_zero_iff _
    (ConcreteCategory.bijective_of_isIso
      (X.presheaf.map (eqToHom (image_morphismRestrict_preimage f U V)).op)).1

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

Goal state before:
pp: X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ IsCompact (↑↑U ∩ ↑↑V ∩ ↑⊤)

Tactic:
← iSup_basicOpen_of_span_eq_top _ _ e,

Goal state after:
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ IsCompact (↑↑U ∩ ↑↑V ∩ ↑(⨆ i ∈ ↑s', X.basicOpen i))
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑U ∩ ↑(X.basicOpen ↑i))

Tactic:
rw [← Opens.coe_inf, ← X.basicOpen_res _ (homOfLE le_top).op]
    exact (U.2.basicOpen _).isCompact

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↥Y → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ ∀ (i : ↥Y), IsAffine ↑(f ⁻¹ᵁ ↑⟨U i, ⋯⟩)

Tactic:
exact hfU

Goal state after:
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 Y : Scheme
f : X ⟶ Y
h : targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) f
U : ↑Y.affineOpens
⊢ affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ W) (f ∣_ ↑U)

Tactic:
exact ⟨(h U).1, hQW (h U).2⟩

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
⊢ ⊥.subschemeι ≫ Hom.toImage (𝟙 X) ≫ IdealSheafData.inclusion ⋯ = 𝟙 ⊥.subscheme

Tactic:
by simp [← cancel_mono (IdealSheafData.subschemeι _)]

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

Goal state before:
pp: x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsSeparated x✝ ↔ MorphismProperty.diagonal (@IsClosedImmersion) x✝

Tactic:
exact isSeparated_iff _

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

Goal state before:
pp: case hP
X Y Z : Scheme
f : X ⟶ Y
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1}
    (U : ι → TopologicalSpace.Opens β),
    TopologicalSpace.IsOpenCover U →
      Continuous f →
        (IsLocallyClosed (Set.range f) ↔ ∀ (i : ι), IsLocallyClosed (Set.range ((U i).carrier.restrictPreimage f)))

Tactic:
simp_rw [Set.range_restrictPreimage]

Goal state after:
case hP
X Y Z : Scheme
f : X ⟶ Y
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1}
    (U : ι → TopologicalSpace.Opens β),
    TopologicalSpace.IsOpenCover U →
      Continuous f → (IsLocallyClosed (Set.range f) ↔ ∀ (i : ι), IsLocallyClosed (Subtype.val ⁻¹' Set.range f))
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case inr
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
this : ∀ {X : Scheme} (f : X ⟶ Y), (∃ S, X = Spec S) → UniversallyOpen f
hX : ¬∃ S, X = Spec S
⊢ UniversallyOpen f

Tactic:
refine (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ this _ ⟨_, rfl⟩

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

Goal state before:
pp: ⊢ @UniversallyClosed = (topologically @IsClosedMap).universally

Tactic:
ext X Y f; rw [universallyClosed_iff]

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

Goal state before:
pp: case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
h✝ : Nonempty ↥(Spec R)
this✝⁴ : IrreducibleSpace ↥(Spec R)
this✝³ : IsDomain ↑R
φ : S ⟶ R
this✝² : IsField ↑R
this✝¹ : Field ↑R := this✝².toField
this✝ : Algebra ↑S ↑R := (CommRingCat.Hom.hom φ).toAlgebra
this : IsJacobsonRing ↑S
⊢ Module.Finite ↑S ↑R ↔ Algebra.FiniteType ↑S ↑R

Tactic:
exact ⟨fun _ ↦ inferInstance, fun _ ↦ finite_of_finite_type_of_isJacobsonRing _ _⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ (CommRingCat.Hom.hom
          (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)) ≫
            Scheme.Hom.app
              (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
                (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
              ⊤)).comp
      C =
    (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv).comp C

Tactic:
change _ = (CommRingCat.ofHom C ≫ _).hom
          rw [CommRingCat.hom_comp, RingHom.comp_assoc, CommRingCat.hom_ofHom, eval₂Hom_comp_C,
            ← CommRingCat.hom_comp, ← CommRingCat.hom_ext_iff,
            ← cancel_mono (Scheme.ΓSpecIso _).hom]
          rw [← Scheme.Hom.comp_appTop, homOfVector_over, Scheme.Hom.comp_appTop]
          simp only [Category.assoc, Scheme.ΓSpecIso_naturality, CommRingCat.of_carrier,
            ← Scheme.toSpecΓ_appTop]
          rw [← Scheme.Hom.comp_appTop_assoc, Scheme.isoSpec, asIso_inv, IsIso.hom_inv_id]
          simp

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

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV✝ : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
ψY : ↑Γ(Y, UY) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  RingHom.pi fun i ↦ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)
ψ : ↑Γ(X, UX) →ₐ[↑Γ(S, US)] (i : ι) → ↑Γ(X, VX i) :=
  AlgHom.pi fun i ↦ { toRingHom := CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op), commutes' := ⋯ }
hψ : Function.Injective ⇑ψ
hψ' : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id ↑Γ(T, UT) ↑Γ(T, UT)) ψ)
hV : ∀ (i : ι), Function.Injective ⇑(ConcreteCategory.hom (pushoutSection H hUST ⋯ ⋯))
val✝ : Fintype ι
φ : ↑Γ(T, UT) ⊗[↑Γ(S, US)] ((i : ι) → ↑Γ(X, VX i)) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  (RingHom.pi fun i ↦
        (CommRingCat.Hom.hom (pushoutSection H hUST ⋯ ⋯)).comp
          ((CommRingCat.Hom.hom ⋯.isoPushout.hom).comp
            (Pi.evalRingHom (fun i ↦ ↑Γ(T, UT) ⊗[↑Γ(S, US)] ↑Γ(X, VX i)) i))).comp
    (Algebra.TensorProduct.piRight ↑Γ(S, US) ↑Γ(S, US) ↑Γ(T, UT) fun i ↦ ↑Γ(X, VX i)).toRingEquiv.toRingHom
hφ : Function.Injective ⇑φ
e : pushout (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST) ≅
  CommRingCat.of (↑Γ(T, UT) ⊗[↑Γ(S, US)] ↑Γ(X, UX)) :=
  ⋯.isoPushout.symm
H₁ :
  (CommRingCat.Hom.hom e.inv).comp Algebra.TensorProduct.includeLeftRingHom =
    CommRingCat.Hom.hom (pushout.inr (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST))
x : ↑Γ(T, UT)
j : ι
⊢ VX j ≤ iX ⁻¹ᵁ US

Tactic:
simp_all

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

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
pf✝¹ : IsLocalRing ↑(CommRingCat.of K)
h : IsClosed {↑p (IsLocalRing.closedPoint K)}
pf✝ : IsLocalHom (CommRingCat.Hom.hom (Scheme.stalkClosedPointTo ↑p))
⊢ Spec.map (𝟙 (CommRingCat.of K)) =
    Spec.map
      ((residueFieldIsoBase f (↑p (IsLocalRing.closedPoint K)) h).inv ≫
        Scheme.descResidueField (Scheme.stalkClosedPointTo ↑p))

Tactic:
simp only [Spec.map_id, Spec.map_comp, SpecMap_residueFieldIsoBase_inv]

Goal state after:
X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
pf✝¹ : IsLocalRing ↑(CommRingCat.of K)
h : IsClosed {↑p (IsLocalRing.closedPoint K)}
pf✝ : IsLocalHom (CommRingCat.Hom.hom (Scheme.stalkClosedPointTo ↑p))
⊢ 𝟙 (Spec (CommRingCat.of K)) =
    Spec.map (Scheme.descResidueField (Scheme.stalkClosedPointTo ↑p)) ≫
      X.fromSpecResidueField (↑p (IsLocalRing.closedPoint K)) ≫ f