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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (⇑(ConcreteCategory.hom ((pullback.snd (𝒰.f i) f).base ≫ f.base)) ⁻¹' s)

Tactic:
TopCat.coe_comp,

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (⇑f ∘ ⇑(pullback.snd (𝒰.f i) f) ⁻¹' s)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥(Spec R)),
    IsOpen (⇑f ⁻¹' s) → (∃ S, X = Spec S) → IsOpen s
hX : ¬∃ S, X = Spec S
x✝ : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun i ↦ 𝒰.X i) ⟶ X := Sigma.desc fun i ↦ 𝒰.f i
⊢ IsOpen (⇑(ConcreteCategory.hom (((∐ fun i ↦ 𝒰.X i).isoSpec.inv ≫ p).base ≫ f.base)) ⁻¹' s)

Tactic:
TopCat.coe_comp,

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥(Spec R)),
    IsOpen (⇑f ⁻¹' s) → (∃ S, X = Spec S) → IsOpen s
hX : ¬∃ S, X = Spec S
x✝ : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun i ↦ 𝒰.X i) ⟶ X := Sigma.desc fun i ↦ 𝒰.f i
⊢ IsOpen (⇑f ∘ ⇑((∐ fun i ↦ 𝒰.X i).isoSpec.inv ≫ p) ⁻¹' s)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥(Spec R)),
    IsOpen (⇑f ⁻¹' s) → (∃ S, X = Spec S) → IsOpen s
hX : ¬∃ S, X = Spec S
⊢ IsOpen s

pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (⇑f ⁻¹' s)
hX : ∃ S, X = Spec S
⊢ IsOpen s

Tactic:
· have _ : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    let 𝒰 := X.affineCover.finiteSubcover
    let p : ∐ (fun i : 𝒰.I₀ ↦ 𝒰.X i) ⟶ X := Sigma.desc (fun i ↦ 𝒰.f i)
    refine this (f := (∐ (fun i : 𝒰.I₀ ↦ 𝒰.X i)).isoSpec.inv ≫ p ≫ f) _ _ ?_ ⟨_, rfl⟩
    rw [← Category.assoc, Scheme.Hom.comp_base, TopCat.coe_comp, Set.preimage_comp]
    exact hs.preimage (_ ≫ p).continuous

Goal state after:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (⇑f ⁻¹' s)
hX : ∃ S, X = Spec S
⊢ IsOpen s
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : Surjective f
⊢ ∀ (x : ↑↑(LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj X)).toPresheafedSpace),
    Mono
      (PresheafedSpace.Hom.stalkMap
        (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f)).hom x)

Tactic:
intro x

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : Surjective f
x : ↑↑(LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj X)).toPresheafedSpace
⊢ Mono
    (PresheafedSpace.Hom.stalkMap
      (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f)).hom x)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₂
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑S))).inv) (X i✝) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑S))).inv)
      ((MvPolynomial.map (CommRingCat.Hom.hom φ)) (X i✝))

Tactic:
map_X

Goal state after:
case h₂
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑S))).inv) (X i✝) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑S))).inv) (X i✝)
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: case refine_2
X Y : Scheme
K : Type u
inst✝⁵ : Field K
inst✝⁴ : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst✝³ : IsSeparated i
inst✝² : LocallyOfFiniteType i
inst✝¹ : IsReduced X
inst✝ : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed {x} → f x = g x
H' : f ≫ i = g ≫ i
this : JacobsonSpace ↥X
⊢ ∀ x ∈ S ∩ closedPoints ↥X, X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g

Tactic:
intro x

Goal state after:
case refine_2
X Y : Scheme
K : Type u
inst✝⁵ : Field K
inst✝⁴ : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst✝³ : IsSeparated i
inst✝² : LocallyOfFiniteType i
inst✝¹ : IsReduced X
inst✝ : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed {x} → f x = g x
H' : f ≫ i = g ≫ i
this : JacobsonSpace ↥X
x : ↥X
⊢ x ∈ S ∩ closedPoints ↥X → X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case refine_1
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
H : ¬∃ i, (e.val i).Monic ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
i : Fin n
hi : e.val i ≠ 0
i_min : ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
j : Fin n
⊢ (Polynomial.degree ∘ { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {(e.val i).leadingCoeff}))) ∘ e.val }.val)
      j ≤
    (Polynomial.degree ∘ e.val) j

Tactic:
simpa using degree_map_le

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case left
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
⊢ Function.support (f + g) ⊆ U

Tactic:
intro x

Goal state after:
case left
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
x : X
⊢ x ∈ Function.support (f + g) → x ∈ U
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeSup Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
⊢ (Function.support fun z ↦ D₁ z ⊔ D₂ z) ⊆ U

Tactic:
intro x

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeSup Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ (x ∈ Function.support fun z ↦ D₁ z ⊔ D₂ z) → x ∈ U
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeInf Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
⊢ (Function.support fun z ↦ D₁ z ⊓ D₂ z) ⊆ U

Tactic:
intro x

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeInf Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ (x ∈ Function.support fun z ↦ D₁ z ⊓ D₂ z) → x ∈ U
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
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
⊢ (colimit.cocone D).pt = UX

Tactic:
simpa [CompleteLattice.colimit_eq_iSup]

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Lattice Y
inst✝ : Zero Y
D₁ D₂ D₃ : locallyFinsuppWithin U Y
h₁₃ : D₁ ≤ D₃
h₂₃ : D₂ ≤ D₃
x : X
⊢ (D₁ ⊔ D₂) x ≤ D₃ x

Tactic:
by simp [h₁₃ x, h₂₃ x]

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Lattice Y
inst✝ : Zero Y
D₁ D₂ D₃ : locallyFinsuppWithin U Y
h₁₃ : D₁ ≤ D₂
h₂₃ : D₁ ≤ D₃
x : X
⊢ D₁ x ≤ (D₂ ⊓ D₃) x

Tactic:
by simp [h₁₃ x, h₂₃ x]

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ (f₁ + f₂) ⊔ 0 ≤ f₁ ⊔ 0 + f₂ ⊔ 0

Tactic:
intro x

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
⊢ ((f₁ + f₂) ⊔ 0) x ≤ (f₁ ⊔ 0 + f₂ ⊔ 0) x
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ -(f₁ + f₂) ⊔ 0 ≤ -f₁ ⊔ 0 + -f₂ ⊔ 0

Tactic:
intro x

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
⊢ (-(f₁ + f₂) ⊔ 0) x ≤ (-f₁ ⊔ 0 + -f₂ ⊔ 0) x
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
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
G : X.Opens ⥤ Y.Opens :=
  { obj := fun U ↦ g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map := fun {X_1 Y_1} h ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
let αF : F ⟶ D.op ⋙ G.op ⋙ Y.presheaf :=
  { app i := (pushout.congrHom (by simp) rfl).hom ≫
      pushoutSection H hUST (by grw [← hUSX, ← h]; exact le_iSup D.obj i.unop) rfl }

Goal state after:
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
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
G : X.Opens ⥤ Y.Opens :=
  { obj := fun U ↦ g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map := fun {X_1 Y_1} h ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
αF : F ⟶ D.op ⋙ G.op ⋙ Y.presheaf :=
  { app := fun i ↦ (pushout.congrHom ⋯ ⋯).hom ≫ pushoutSection H hUST ⋯ ⋯, naturality := ⋯ }
⊢ IsIso (pushoutSection H hUST hUSX hUY)
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
⊢ (Function.support fun z ↦ if hz : z ∈ V then D z else 0) ⊆ V

Tactic:
intro x

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x : X
⊢ (x ∈ Function.support fun z ↦ if hz : z ∈ V then D z else 0) → x ∈ V
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), (𝒰.X i).IsGermInjective
⊢ X.IsGermInjective

Tactic:
intro x

Goal state after:
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), (𝒰.X i).IsGermInjective
x : ↥X
⊢ X.IsGermInjectiveAt x
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ ∀ (x : ↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f)))),
    (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf)) x = 0 → x = 0

Tactic:
intro x

Goal state after:
case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f)))
⊢ (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf)) x = 0 → x = 0
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst✝ : IsLocallyNoetherian X
⊢ ∀ (R : CommRingCat), IsNoetherianRing ↑R → (Spec R).IsGermInjective

Tactic:
refine fun R hR ↦ Scheme.IsGermInjective.Spec fun I hI ↦ ?_

Goal state after:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
⊢ ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⟶ Y
inst✝ : IsDominant f
⊢ IsDominant (Hom.toPartialMap f).hom

Tactic:
dsimp
  have := Opens.isDominant_ι (X := X) (U := ⊤) dense_univ
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ (Spec.map (inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫ (↑U).fromSpecStalk ⟨x, hx⟩) ≫ X.homOfLE hU' ≫ f.hom =
    (Spec.map (inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫ (↑f.domain).fromSpecStalk ⟨x, ⋯⟩) ≫ f.hom

Tactic:
rw [Category.assoc, ← SpecMap_stalkMap_fromSpecStalk_assoc,
    ← SpecMap_stalkSpecializes_fromSpecStalk (Inseparable.of_eq e).specializes,
    ← TopCat.Presheaf.stalkCongr_inv _ (Inseparable.of_eq e)]

Goal state after:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ Spec.map (inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫
      Spec.map (Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩) ≫ (↑f.domain).fromSpecStalk ((X.homOfLE hU') ⟨x, hx⟩) ≫ f.hom =
    (Spec.map (inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫
        Spec.map ((↑f.domain).presheaf.stalkCongr ⋯).inv ≫ (↑f.domain).fromSpecStalk ((X.homOfLE hU') ⟨x, hx⟩)) ≫
      f.hom
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f g : X.PartialMap Y
inst✝¹ : IsOver S f
inst✝ : IsOver S g
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
x✝ : f.equiv g
V : X.Opens
hV : Dense ↑V
hVl : V ≤ f.domain
hVr : V ≤ g.domain
e : (f.restrict V hV hVl).hom = (g.restrict V hV hVr).hom
this : IsDominant (X.homOfLE ⋯)
⊢ X.homOfLE ⋯ ≫ (f.restrict W hW hWl).hom = X.homOfLE ⋯ ≫ (g.restrict W hW hWr).hom

Tactic:
simpa using congr(X.homOfLE (inf_le_right : W ⊓ V ≤ V) ≫ $e)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
⊢ ∀ (x y : f.openCoverDomain.I₀),
    Limits.pullback.fst (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom =
      Limits.pullback.snd (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom

Tactic:
intro x

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x : f.openCoverDomain.I₀
⊢ ∀ (y : f.openCoverDomain.I₀),
    Limits.pullback.fst (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom =
      Limits.pullback.snd (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case H
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y ⟶ Z
⊢ (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ ⊤)).inv ≫ f.hom ∣_ ⊤ ≫ Y.topIso.hom ≫ g = (X.isoOfEq ⋯).hom ≫ (f.compHom g).hom

Tactic:
compHom_hom,

Goal state after:
case H
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y ⟶ Z
⊢ (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ ⊤)).inv ≫ f.hom ∣_ ⊤ ≫ Y.topIso.hom ≫ g = (X.isoOfEq ⋯).hom ≫ f.hom ≫ g
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : ↥(𝒰.X i)
xj : ↥(𝒰.X j)
h : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (ConcreteCategory.hom ((𝒰.trans fi).base ≫ (𝒰.f k).base)) xi =
    (ConcreteCategory.hom ((𝒰.trans fj).base ≫ (𝒰.f k).base)) xj

Tactic:
ConcreteCategory.comp_apply,

Goal state after:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : ↥(𝒰.X i)
xj : ↥(𝒰.X j)
h : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (𝒰.f k) ((𝒰.trans fi) xi) = (ConcreteCategory.hom ((𝒰.trans fj).base ≫ (𝒰.f k).base)) xj
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_2.refine_1
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
h : ((opensDiagram D i U).map f) x ∈ V
⊢ (D.map (Over.Hom.left f)) ↑x ∈ D.map k.hom ⁻¹ᵁ U

Tactic:
change (D.map f.left ≫ D.map k.hom).base x.1 ∈ U

Goal state after:
case e'_2.refine_1
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
h : ((opensDiagram D i U).map f) x ∈ V
⊢ (D.map (Over.Hom.left f) ≫ D.map k.hom) ↑x ∈ U
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : (𝒰.functorOfLocallyDirected ⋙ forget).obj i
xj : (𝒰.functorOfLocallyDirected ⋙ forget).obj j
hxij : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (ConcreteCategory.hom ((𝒰.trans fi).base ≫ (𝒰.f k).base)) xi =
    (ConcreteCategory.hom ((𝒰.trans fj).base ≫ (𝒰.f k).base)) xj

Tactic:
ConcreteCategory.comp_apply,

Goal state after:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : (𝒰.functorOfLocallyDirected ⋙ forget).obj i
xj : (𝒰.functorOfLocallyDirected ⋙ forget).obj j
hxij : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (𝒰.f k) ((𝒰.trans fi) xi) = (ConcreteCategory.hom ((𝒰.trans fj).base ≫ (𝒰.f k).base)) xj
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
hf : Function.Surjective ⇑(pullback.diagonal f)
this : UniversallyInjective f
⊢ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable

Tactic:
intro x

Goal state after:
X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
hf : Function.Surjective ⇑(pullback.diagonal f)
this : UniversallyInjective f
x : ↥X
⊢ (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable