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

Goal state before:
pp: case h.inl
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥X
⊢ ∃ y,
    (Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr)
          (Sum.elim (fun x ↦ Sum.inl PUnit.unit) (fun x ↦ Sum.inr PUnit.unit) (Sum.inl x)))
        y =
      (coprodMk X Y) (Sum.inl x)

Tactic:
simp only [Sum.elim_inl, coprodMk_inl, exists_apply_eq_apply]

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
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact TopologicalSpace.Opens.mem_iSup.mpr ⟨⟨l, fj, fk⟩, ⟨z, rfl⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ IsPullback (pullback.fst fWX (𝒰.f i)) (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯)
    (pullback.lift fWX fWY h) f

Tactic:
← IsPullback.paste_vert_iff this.flip (by ext <;> simp [f])

Goal state after:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ IsPullback (pullback.fst fWX (𝒰.f i))
    (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ pullback.fst (𝒰.f i ≫ fXZ) fYZ)
    (pullback.lift fWX fWY h ≫ pullback.fst fXZ fYZ) (𝒰.f i)
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
m : (cocone F).pt ⟶ s.pt
hm : ∀ (j : J), (cocone F).ι.app j ≫ m = s.ι.app j
i : (MultispanShape.prod (glueData F).J).R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [← hm ↓i, cocone, reassoc_of% glueDataι_naturality]
    rfl

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

Goal state before:
pp: X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
α✝ β✝ : Type u_1
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β✝
f : α✝ → β✝
ι : Type u_1
U : ι → Opens β✝
H : IsOpenCover U
x✝ : Continuous[inst✝¹, inst✝] f
hf : ∀ (i : ι), Function.Injective ((U i).carrier.restrictPreimage f)
x₁ x₂ : α✝
e : f x₁ = f x₂
⊢ x₁ = x₂

Tactic:
obtain ⟨i, hxi⟩ : ∃ i, f x₁ ∈ U i := by simpa using congr(f x₁ ∈ $H)

Goal state after:
X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
α✝ β✝ : Type u_1
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β✝
f : α✝ → β✝
ι : Type u_1
U : ι → Opens β✝
H : IsOpenCover U
x✝ : Continuous[inst✝¹, inst✝] f
hf : ∀ (i : ι), Function.Injective ((U i).carrier.restrictPreimage f)
x₁ x₂ : α✝
e : f x₁ = f x₂
i : ι
hxi : f x₁ ∈ U i
⊢ x₁ = x₂
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsDominant f
hf : IsClosed (Set.range ⇑f)
⊢ Function.Surjective ⇑f

Tactic:
by rw [← Set.range_eq_univ, ← hf.closure_eq, f.denseRange.closure_range]

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

Goal state before:
pp: case refine_2
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
ι : Type u_1
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)
⊢ P.diagonal f

Tactic:
· change P _
    refine IsZariskiLocalAtSource.of_iSup_eq_top U hU fun i ↦ ?_
    rw [pullback.comp_diagonal]
    exact RespectsRight.postcomp (P := P) (Q := @IsOpenImmersion) (g _ _) inferInstance _ (hf i)

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)
⊢ SurjectiveOnStalks f

Tactic:
refine ⟨fun x ↦ ?_⟩
  have := (f ≫ g).stalkMap_surjective x
  rw [Scheme.Hom.stalkMap_comp] at this
  exact Function.Surjective.of_comp this

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

Goal state before:
pp: case e'_5.fst
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := ⋯
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := ⋯
algInst✝ : Algebra ↑R ↑B := ⋯
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))
⊢ (L ((pullback.map (Spec.map φ) (Spec.map ψ) f g iX iY iS e₁ e₂) ((pullbackSpecIso ↑R ↑A ↑B).symm.hom x))).1 =
    (Prod.map (⇑iX) (⇑iY)
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B)
          ((pullbackSpecIso ↑R ↑A ↑B).hom ((pullbackSpecIso ↑R ↑A ↑B).symm.hom x)))).1

pp: case e'_5.snd
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := ⋯
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := ⋯
algInst✝ : Algebra ↑R ↑B := ⋯
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))
⊢ (L ((pullback.map (Spec.map φ) (Spec.map ψ) f g iX iY iS e₁ e₂) ((pullbackSpecIso ↑R ↑A ↑B).symm.hom x))).2 =
    (Prod.map (⇑iX) (⇑iY)
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B)
          ((pullbackSpecIso ↑R ↑A ↑B).hom ((pullbackSpecIso ↑R ↑A ↑B).symm.hom x)))).2

Tactic:
· simp only [L, ← Scheme.Hom.comp_apply, pullback.lift_fst, Iso.symm_hom,
        Iso.inv_hom_id]
      erw [← Scheme.Hom.comp_apply, pullbackSpecIso_inv_fst_assoc]
      rfl

Goal state after:
case e'_5.snd
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := ⋯
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := ⋯
algInst✝ : Algebra ↑R ↑B := ⋯
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))
⊢ (L ((pullback.map (Spec.map φ) (Spec.map ψ) f g iX iY iS e₁ e₂) ((pullbackSpecIso ↑R ↑A ↑B).symm.hom x))).2 =
    (Prod.map (⇑iX) (⇑iY)
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B)
          ((pullbackSpecIso ↑R ↑A ↑B).hom ((pullbackSpecIso ↑R ↑A ↑B).symm.hom x)))).2
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: 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₂) ⋯)) ⋯
⊢ (algebraMap ↑Γ(X, ↑S) ↑Γ(X, X.basicOpen ((f |_ ↑S) ⋯))) ((((f |_ U₁) ⋯ ^ n₂ * y₁) |_ ↑S) h₁) =
    (algebraMap ↑Γ(X, ↑S) ↑Γ(X, X.basicOpen ((f |_ ↑S) ⋯))) ((((f |_ U₂) ⋯ ^ n₁ * y₂) |_ ↑S) h₂)

Tactic:
apply exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux (e₁ := e₁) (e₂ := e₂)

Goal state after:
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₂) ⋯)) ⋯
⊢ X.basicOpen ((f |_ ↑S) ⋯) ≤ X.basicOpen ((f |_ U₁) ⋯)

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₂) ⋯)) ⋯
⊢ X.basicOpen ((f |_ ↑S) ⋯) ≤ X.basicOpen ((f |_ U₂) ⋯)
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
inst✝ : IsOpenImmersion f
H :
  ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (↑V) e))
U : ↑Z.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U
this : IsIso (Scheme.Hom.appLE f (f ''ᵁ ↑V) ↑V ⋯)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U) (↑V) e))

Tactic:
← Scheme.Hom.appLE_comp_appLE _ _ _ (f ''ᵁ V) V.1
    (Set.image_subset_iff.mpr e) (f.preimage_image_eq _).ge,

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
inst✝ : IsOpenImmersion f
H :
  ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (↑V) e))
U : ↑Z.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U
this : IsIso (Scheme.Hom.appLE f (f ''ᵁ ↑V) ↑V ⋯)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (f ''ᵁ ↑V) ⋯ ≫ Scheme.Hom.appLE f (f ''ᵁ ↑V) ↑V ⋯))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.FiniteHeight
inst✝ : I.IsPrime
⊢ I.primeHeight < ⊤

Tactic:
by
  rw [← I.height_eq_primeHeight]
  exact Ideal.height_lt_top ‹I.IsPrime›.ne_top

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ I.height = 0 ↔ I ∈ minimalPrimes R

Tactic:
rw [Ideal.height_eq_primeHeight, Ideal.primeHeight, Order.height_eq_zero,
    minimalPrimes_eq_minimals]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ IsMin { asIdeal := I, isPrime := inst✝ } ↔ I ∈ {x | Minimal IsPrime x}
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
e : R ≃+* S
I : Ideal S
⊢ (comap e I).height = I.height

Tactic:
by
  refine (Equiv.iInf_congr e.idealComapOrderIso fun J ↦ (Equiv.iInf_congr ?_ fun h ↦ ?_).symm).symm
  · refine .ofIff ?_
    rw [← Ideal.comap_coe,
      Ideal.comap_minimalPrimes_eq_of_surjective (f := (↑e : R →+* S)) e.surjective]
    exact e.idealComapOrderIso.injective.mem_set_image.symm
  · have : J.IsPrime := h.isPrime
    simp only [EquivLike.coe_coe, RingEquiv.idealComapOrderIso_apply,
      ← Ideal.height_eq_primeHeight, RingEquiv.height_comap_of_isPrime]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case inr
X : Scheme
inst✝ : IsReduced X
this :
  ∀ (X : Scheme) (x : ↥X),
    closure {x} ∈ irreducibleComponents ↥X → ∀ [IsReduced X], (∃ R, X = Spec R) → IsField ↑(X.presheaf.stalk x)
hX : ¬∃ R, X = Spec R
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
hx : closure {(X.affineCover.f i) x} ∈ irreducibleComponents ↥X
inst : IsReduced (X.affineCover.X i)
⊢ ⇑(X.affineCover.f i) ⁻¹' closure {(X.affineCover.f i) x} ∈ irreducibleComponents ↥(X.affineCover.X i)

Tactic:
exact preimage_mem_irreducibleComponents hx (X.affineCover.f i).isOpenEmbedding
      ⟨X.affineCover.f i x, subset_closure rfl, _, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
H : ∃ x x_1, ∃ (_ : IsClosed x) (_ : IsClosed x_1) (_ : Set.univ ⊆ x ∪ x_1), ¬Set.univ ⊆ x ∧ ¬Set.univ ⊆ x_1
⊢ False

Tactic:
rcases H with ⟨S, T, hS, hT, h₁, h₂, h₃⟩

Goal state after:
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ¬Set.univ ⊆ S
h₃ : ¬Set.univ ⊆ T
⊢ False
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ↑I.support ∩ Set.range ⇑(IsAffineOpen.fromSpec ⋯) = ⇑(IsAffineOpen.fromSpec ⋯) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
IsAffineOpen.range_fromSpec,

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ↑I.support ∩ ↑↑U = ⇑(IsAffineOpen.fromSpec ⋯) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : f (closedPoint ↑R) ∈ ↑U
this : (Spec R).isoSpec.hom ≫ Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = f
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk (f (closedPoint ↑R)) = f

Tactic:
isoSpec_Spec_hom

Goal state after:
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : f (closedPoint ↑R) ∈ ↑U
this : Spec.map (ΓSpecIso R).hom ≫ Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = f
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk (f (closedPoint ↑R)) = f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case inl
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
h✝ : IsEmpty 𝒰.I₀
⊢ ⋃ i, ↑(ker (𝒰.f i ≫ f)).support = ↑f.ker.support

pp: case inr
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
h✝ : Nonempty 𝒰.I₀
⊢ ⋃ i, ↑(ker (𝒰.f i ≫ f)).support = ↑f.ker.support

Tactic:
· have : IsEmpty X := Function.isEmpty 𝒰.idx
    simp [ker_eq_top_of_isEmpty]

Goal state after:
case inr
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
h✝ : Nonempty 𝒰.I₀
⊢ ⋃ i, ↑(ker (𝒰.f i ≫ f)).support = ↑f.ker.support
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V W U₀ : ↑X.affineOpens
hU₀ : ↑U ⊓ ↑W ≤ ↑U₀
⊢ Set.range ⇑(↑U ⊓ ↑W).ι ⊆ ↑↑U₀

Tactic:
simpa using! hU₀

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

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ closure (Set.range ⇑f) ⊆ ↑(ker f).support

Tactic:
rw [(support _).isClosed.closure_subset_iff]

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ Set.range ⇑f ⊆ ↑(ker f).support
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ IsPreimmersion (I.gluedTo ∣_ ↑U)

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso @IsPreimmersion (I.glueDataObjIso U).hom,
    glueDataObjIso_hom_restrict]

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ IsPreimmersion (I.glueDataObjι U)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V₁ : X.Opens
hV₁ : V₁ ≤ f ⁻¹ᵁ U
V₂ : X.Opens
hV₂ : V₂ ≤ f ⁻¹ᵁ U
⊢ IsAffineOpen (f ⁻¹ᵁ U ⊓ V₁) → IsAffineOpen (f ⁻¹ᵁ U ⊓ V₂) → IsAffineOpen (f ⁻¹ᵁ U ⊓ (V₁ ⊓ V₂)) ↔
    IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)

Tactic:
rw [inf_eq_right.mpr hV₁, inf_eq_right.mpr hV₂, inf_eq_right.mpr (inf_le_left.trans hV₁)]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this : IsClosedImmersion (Scheme.Hom.toImage f)
⊢ Function.Surjective ⇑(Scheme.Hom.toImage f)

Tactic:
rw [← Set.range_eq_univ, ← f.toImage.isClosedEmbedding.isClosed_range.closure_eq]
      exact f.toImage.denseRange.closure_eq

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

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ ⇑f '' ↑Z ⊆ ⇑f '' ↑(vanishingIdeal Z).support

Tactic:
coe_support_vanishingIdeal

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ ⇑f '' ↑Z ⊆ ⇑f '' ↑Z
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
t : Finset A := Finset.image (fun g ↦ (Ideal.Quotient.mk I) (g' g)) Finset.univ
⊢ 1 ∈ Ideal.span ↑t

Tactic:
have : ∑ g : { x // x ∈ s }, g' g * h' g = (1 : A) := by
      apply eq_of_sub_eq_zero
      rw [← map_one (Ideal.Quotient.mk I), ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
      apply Ideal.subset_span
      simp

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
t : Finset A := Finset.image (fun g ↦ (Ideal.Quotient.mk I) (g' g)) Finset.univ
this : (Ideal.Quotient.mk I) (∑ g, g' g * h' g) = 1
⊢ 1 ∈ Ideal.span ↑t
Module: Mathlib.LinearAlgebra.Charpoly.BaseChange

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ LinearMap.det f = (-1) ^ Module.finrank R M * f.charpoly.coeff 0

Tactic:
by
  nontriviality R
  rw [← LinearMap.det_toMatrix (Module.Free.chooseBasis R M), Matrix.det_eq_sign_charpoly_coeff,
    ← Module.finrank_eq_card_chooseBasisIndex, charpoly_def]

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

Goal state before:
pp: R S : CommRingCat
inst✝ : Subsingleton ↥(Spec S)
φ : S ⟶ R
ψ : R ⟶ S
hg : φ ≫ ψ = 𝟙 S
⊢ Function.Surjective ⇑(ConcreteCategory.hom ψ)

Tactic:
apply Function.LeftInverse.surjective (g := φ)

Goal state after:
R S : CommRingCat
inst✝ : Subsingleton ↥(Spec S)
φ : S ⟶ R
ψ : R ⟶ S
hg : φ ≫ ψ = 𝟙 S
⊢ Function.LeftInverse ⇑(ConcreteCategory.hom ψ) ⇑(ConcreteCategory.hom φ)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ IsCompact (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑↑U ∩ ↑↑V ∩ Set.range ⇑(IsAffineOpen.fromSpec ⋯)))

Tactic:
IsAffineOpen.range_fromSpec,

Goal state after:
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ IsCompact (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑↑U ∩ ↑↑V ∩ ↑↑U))
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: case inr
Z S X Y : Scheme
f : X ⟶ Y
this : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y), (∃ R, Y = Spec R) → IsIntegralHom f → topologically (@IsClosedMap) f
hY : ¬∃ R, Y = Spec R
⊢ IsIntegralHom f → topologically (@IsClosedMap) f

pp: Z S X Y : Scheme
f : X ⟶ Y
hY : ∃ R, Y = Spec R
⊢ IsIntegralHom f → topologically (@IsClosedMap) f

Tactic:
· rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := topologically _) Y.affineCover]
    exact fun a i ↦ this _ ⟨_, rfl⟩ (a i)

Goal state after:
Z S X Y : Scheme
f : X ⟶ Y
hY : ∃ R, Y = Spec R
⊢ IsIntegralHom f → topologically (@IsClosedMap) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
x✝ : IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
left✝ : IsAffine X
right✝ : (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
⊢ Epi (Scheme.Hom.appTop f) ↔ Mono (Scheme.Hom.app f ⊤).op

Tactic:
exact ⟨fun h ↦ inferInstance, fun h ↦ show Epi (f.app ⊤).op.unop by infer_instance⟩

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)
f : Spec R ⟶ Spec S
h✝ : Nonempty ↥(Spec R)
this : IrreducibleSpace ↥(Spec R)
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
have : IsDomain R := (affine_isIntegral_iff R).mp (isIntegral_of_irreducibleSpace_of_isReduced _)

Goal state after:
case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
f : Spec R ⟶ Spec S
h✝ : Nonempty ↥(Spec R)
this✝ : IrreducibleSpace ↥(Spec R)
this : IsDomain ↑R
⊢ IsFinite f ↔ LocallyOfFiniteType f
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
⊢ IsOpenImmersion X.toSpecΓ

Tactic:
have : IsIso X.toSpecΓ.imageι := by delta Hom.imageι Hom.image; rw [X.ker_toSpecΓ]; infer_instance
  rw [← X.toSpecΓ.toImage_imageι]
  infer_instance

Goal state after: