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

Goal state before:
pp: case mp.refine_1
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ Function.Bijective ⇑φ.hom'.kerLift

pp: case mp.refine_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ f =
    (X.isoSpec ≪≫ Scheme.Spec.mapIso (RingEquiv.ofBijective φ.hom'.kerLift ?mp.refine_1).toCommRingCatIso.op).hom ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.hom')))

Tactic:
· exact ⟨φ.1.kerLift_injective, Ideal.Quotient.lift_surjective_of_surjective _ _
        (h₂.comp (Scheme.ΓSpecIso R).commRingCatIsoToRingEquiv.symm.surjective)⟩

Goal state after:
case mp.refine_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ f =
    (X.isoSpec ≪≫ Scheme.Spec.mapIso (RingEquiv.ofBijective φ.hom'.kerLift ⋯).toCommRingCatIso.op).hom ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.hom')))
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case basicOpen
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
hN : IsNoetherianRing ↑Γ(X, ↑U)
⊢ IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen f))

Tactic:
| basicOpen U f hN =>

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsCompact (comap C '' (zeroLocus {g} \ zeroLocus {f}))

Tactic:
rw [ht, ← (t : Set R).iUnion_of_singleton_coe, zeroLocus_iUnion, Set.compl_iInter]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsCompact (⋃ i, (zeroLocus {↑i})ᶜ)
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y Z S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : IsSchemeTheoreticallyDominant g
⊢ IsSchemeTheoreticallyDominant (f ≫ g)

Tactic:
isSchemeTheoreticallyDominant_iff,

Goal state after:
X Y Z S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : IsSchemeTheoreticallyDominant g
⊢ Scheme.Hom.ker (f ≫ g) = ⊥
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsDominant f
inst✝ : IsReduced Y
⊢ IsSchemeTheoreticallyDominant f

Tactic:
isSchemeTheoreticallyDominant_iff,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsDominant f
inst✝ : IsReduced Y
⊢ Scheme.Hom.ker f = ⊥
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
U : { x // x.1 ∈ Y.affineOpens ∧ x.1 ≤ (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base)) ↑x.2 }
⊢ (↑U).1 ∈ Y.affineOpens

Tactic:
by exact U.2.1

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ S
g : Y ⟶ S
pX : Z ⟶ X
pY : Z ⟶ Y
H : IsPullback pX pY f g
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
⊢ IsSchemeTheoreticallyDominant pY

Tactic:
rw [← H.isoPullback_hom_snd]
  infer_instance

Goal state after:
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 s

Tactic:
refine this (f := (∐ (fun i : 𝒰.I₀ ↦ 𝒰.X i)).isoSpec.inv ≫ p ≫ f) _ _ ?_ ⟨_, rfl⟩

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 (⇑((∐ fun i ↦ 𝒰.X i).isoSpec.inv ≫ p ≫ f) ⁻¹' s)
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h : Function.Injective (F.descColimitType c)
j j' : J
x : F.obj j
⊢ ∀ (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'

Tactic:
x'

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h : Function.Injective (F.descColimitType c)
j j' : J
x : F.obj j
x' : F.obj j'
⊢ c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
x : F.ColimitType
⊢ ∀ ⦃a₂ : F.ColimitType⦄, F.descColimitType c x = F.descColimitType c a₂ → x = a₂

Tactic:
x'

Goal state after:
case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
x x' : F.ColimitType
⊢ F.descColimitType c x = F.descColimitType c x' → x = x'
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
j : J
x : F.obj j
⊢ ∀ (x' : F.obj j), c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'

Tactic:
x'

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
j : J
x x' : F.obj j
⊢ c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x') →
    ∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'

pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x') →
    ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'

Tactic:
· intro h j x x' eq
    obtain ⟨k, f, f', eq⟩ := h _ _ _ _ eq
    refine ⟨coeq f f', f ≫ coeqHom f f', ?_⟩
    rw [map_comp, comp_apply, eq]
    simp only [← comp_apply, ← map_comp]
    rw [coeq_condition]

Goal state after:
case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x') →
    ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j : J) (x x' : F.obj j),
    c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'
j j' : J
x : F.obj j
⊢ ∀ (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'

Tactic:
x'

Goal state after:
case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j : J) (x x' : F.obj j),
    c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'
j j' : J
x : F.obj j
x' : F.obj j'
⊢ c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case inr
n : Type u
S : Scheme
this✝ : ∀ {n : Type u} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
i : S.affineCover.toPreZeroHypercover.1
this : topologically (@IsOpenMap) (𝔸(n; S.affineCover.X i) ↘ S.affineCover.X i)
⊢ topologically (@IsOpenMap) (Scheme.Cover.pullbackHom S.affineCover (𝔸(n; S) ↘ S) i)

Tactic:
rwa [← (isPullback_map (n := n) (S.affineCover.f i)).isoPullback_hom_snd,
      MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)] at this

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
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
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
let c₀ : Cocone D := (colimit.cocone _).extend
    (eqToIso (Y := UX) (by simpa [CompleteLattice.colimit_eq_iSup])).hom

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
⊢ IsIso (pushoutSection H hUST hUSX hUY)
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case H
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x

Tactic:
· apply Spec.map_injective
    rw [← cancel_mono (Y.fromSpecStalk _)]
    simpa [Scheme.SpecMap_stalkSpecializes_fromSpecStalk]

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this✝² : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↥X
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
H : x ∈ s.inf W ⊓ U
this✝¹ : Algebra ↑R ↑Γ(X, U) := (CommRingCat.Hom.hom φRX).toAlgebra
this✝ : Algebra ↑R ↑(X.presheaf.stalk x) := (CommRingCat.Hom.hom (φRX ≫ X.presheaf.germ U x hxU)).toAlgebra
this : Algebra ↑R ↑(X.presheaf.obj (Opposite.op (s.inf W ⊓ U))) :=
  (CommRingCat.Hom.hom (φRX ≫ X.presheaf.map (homOfLE ⋯).op)).toAlgebra
φ' : ↑A →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom φ;
  { toRingHom := __src, commutes' := ⋯ }
ψ : ↑Γ(X, s.inf W ⊓ U) →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H);
  { toRingHom := __src, commutes' := ⋯ }
⊢ (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H)).range

Tactic:
change AlgHom.range φ' ≤ AlgHom.range ψ

Goal state after:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this✝² : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↥X
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
H : x ∈ s.inf W ⊓ U
this✝¹ : Algebra ↑R ↑Γ(X, U) := (CommRingCat.Hom.hom φRX).toAlgebra
this✝ : Algebra ↑R ↑(X.presheaf.stalk x) := (CommRingCat.Hom.hom (φRX ≫ X.presheaf.germ U x hxU)).toAlgebra
this : Algebra ↑R ↑(X.presheaf.obj (Opposite.op (s.inf W ⊓ U))) :=
  (CommRingCat.Hom.hom (φRX ≫ X.presheaf.map (homOfLE ⋯).op)).toAlgebra
φ' : ↑A →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom φ;
  { toRingHom := __src, commutes' := ⋯ }
ψ : ↑Γ(X, s.inf W ⊓ U) →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H);
  { toRingHom := __src, commutes' := ⋯ }
⊢ φ'.range ≤ ψ.range
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hx))

Tactic:
by
  rw [injective_iff_map_eq_zero]
  intro y hy
  rw [← (X.presheaf.germ U x hx).hom.map_zero] at hy
  obtain ⟨W, hW, iU, iV, e⟩ := X.presheaf.germ_eq _ hx hx _ _ hy
  cases Subsingleton.elim iU iV
  have : Nonempty W := ⟨⟨_, hW⟩⟩
  exact map_injective_of_isIntegral X iU e

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IrreducibleSpace ↥X
x : ↥X
⊢ Algebra ↑(X.presheaf.stalk x) ↑X.functionField

Tactic:
apply RingHom.toAlgebra

Goal state after:
X : Scheme
inst✝ : IrreducibleSpace ↥X
x : ↥X
⊢ ↑(X.presheaf.stalk x) →+* ↑X.functionField
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
inst✝ : IsIntegral X
f g : X ⤏ Y
H : f.fromFunctionField = g.fromFunctionField
⊢ f = g

Tactic:
obtain ⟨f, rfl⟩ := f.exists_rep

Goal state after:
X Y : Scheme
inst✝ : IsIntegral X
g : X ⤏ Y
f : X.PartialMap Y
H : f.toRationalMap.fromFunctionField = g.fromFunctionField
⊢ f.toRationalMap = g
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsIntegral X
inst✝ : LocallyOfFiniteType sY
f : X ⤏ Y
hf : f.compHom sY = Hom.toRationalMap sX
⊢ (↑⟨f, hf⟩).fromFunctionField ≫ sY = X.fromSpecStalk (genericPoint ↥X) ≫ sX

Tactic:
obtain ⟨f, rfl⟩ := f.exists_rep

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsIntegral X
inst✝ : LocallyOfFiniteType sY
f : X.PartialMap Y
hf : f.toRationalMap.compHom sY = Hom.toRationalMap sX
⊢ (↑⟨f.toRationalMap, hf⟩).fromFunctionField ≫ sY = X.fromSpecStalk (genericPoint ↥X) ≫ sX
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
inst✝ : Flat iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact ↑UT
⊢ Mono (pushoutSection H hUST hUSX hUY)

Tactic:
suffices Mono (pushoutSection H.flip hUSX hUST (hUY.trans (inf_comm _ _))) by
    rw [← mono_comp_iff_of_isIso (pushoutSymmetry _ _).hom]; convert! this; cat_disch
  exact mono_pushoutSection_of_isCompact_of_flat_right _ _ _ _ hUS hUX hUT

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

Goal state before:
pp: X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X ⤏ Y
inst✝ : f.IsDominant
g : Y ⤏ Z
x✝¹ x✝ : Y.PartialMap Z
h : x✝¹ ≈ x✝
⊢ (f.representative.comp x✝¹).equiv (f.representative.comp x✝)

Tactic:
exact PartialMap.comp_equiv_of_equiv_right _ h

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝³ : Category.{v_1, ?u.75} 𝒰.I₀
inst✝² : 𝒰.LocallyDirected
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
⊢ ∃ i_1,
    x ∈
      Set.range
        ⇑({ I₀ := (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j), X := fun k ↦ 𝒰.X k.fst,
                f := fun k ↦ pullback.lift (𝒰.trans k.snd.1) (𝒰.trans k.snd.2) ⋯ }.f
            i_1)

Tactic:
use ⟨(𝒰.exists_lift_trans_eq x).choose, (𝒰.exists_lift_trans_eq x).choose_spec.choose,
        (𝒰.exists_lift_trans_eq x).choose_spec.choose_spec.choose⟩
      exact (𝒰.exists_lift_trans_eq x).choose_spec.choose_spec.choose_spec

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: 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
x : ↥(D.obj j.left)
h₁ : (D.map k.hom) ((D.map (Over.Hom.left f)) x) ∈ U
h₂ : ⟨(D.map (Over.Hom.left f)) x, h₁⟩ ∈ ↑V
e :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom.base)
      ⟨(D.map (Over.Hom.left f)) x, h₁⟩ =
    (D.map (Over.Hom.left f)) x
⊢ x ∈ D.map j.hom ⁻¹ᵁ U

Tactic:
rw [← Scheme.Hom.comp_apply] at h₁

Goal state after:
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
x : ↥(D.obj j.left)
h₁✝ : (D.map k.hom) ((D.map (Over.Hom.left f)) x) ∈ U
h₁ : (D.map (Over.Hom.left f) ≫ D.map k.hom) x ∈ U
h₂ : ⟨(D.map (Over.Hom.left f)) x, h₁✝⟩ ∈ ↑V
e :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom.base)
      ⟨(D.map (Over.Hom.left f)) x, h₁✝⟩ =
    (D.map (Over.Hom.left f)) x
⊢ x ∈ D.map j.hom ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
⊢ ∀ {i j : X.directedAffineCover.I₀},
    i ≤ j ↔ Hom.opensRange (X.directedAffineCover.f i) ≤ Hom.opensRange (X.directedAffineCover.f j)

Tactic:
intros

Goal state after:
P : MorphismProperty Scheme
X : Scheme
i✝ j✝ : X.directedAffineCover.I₀
⊢ i✝ ≤ j✝ ↔ Hom.opensRange (X.directedAffineCover.f i✝) ≤ Hom.opensRange (X.directedAffineCover.f j✝)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
inst✝² : CommRing R₀
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
n : ℕ
⊢ ∀ (S : InductionObj R n), Statement R₀ R n S

Tactic:
intro S

Goal state after:
R₀ : Type u_1
R : Type u_2
inst✝² : CommRing R₀
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
n : ℕ
S : InductionObj R n
⊢ Statement R₀ R n S
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝⁴ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝³ : LocallyOfFiniteType f
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
inst✝ : ∀ (i : I), IsAffineHom (A.c.π.app i)
j : A.𝒰D.I₀
this✝¹ : IsAffine (A.𝒰D.X j)
this✝ : ∀ (i : Over A.i'), IsAffine ((Over.post D ⋙ Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).obj i)
this : IsAffine ((Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).mapCone ((Over.conePost D A.i').obj A.c)).pt
⊢ LocallyOfFiniteType ((A.𝒰X j.fst.fst).f j.fst.snd ≫ Scheme.Cover.pullbackHom A.𝒰S f j.fst.fst)

Tactic:
dsimp [Scheme.Cover.pullbackHom]

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝⁴ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝³ : LocallyOfFiniteType f
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
inst✝ : ∀ (i : I), IsAffineHom (A.c.π.app i)
j : A.𝒰D.I₀
this✝¹ : IsAffine (A.𝒰D.X j)
this✝ : ∀ (i : Over A.i'), IsAffine ((Over.post D ⋙ Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).obj i)
this : IsAffine ((Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).mapCone ((Over.conePost D A.i').obj A.c)).pt
⊢ LocallyOfFiniteType ((A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.snd f (A.𝒰S.f j.fst.fst))
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
H : ∀ x ∈ U, ∃ t ⊆ U, x ∈ t ∧ IsOpen t ∧ IsCompactOpenCovered f t
⊢ IsCompactOpenCovered f U

Tactic:
by
  choose Us hU' hUx hUo hU'' using H
  refine of_biUnion_eq_of_isCompact hU { Us x h | (x : S) (h : x ∈ U) } ?_ ?_
  · refine subset_antisymm (fun x ↦ ?_) fun x hx ↦ ?_
    · simp [Opens.forall]
      grind
    · simpa using ⟨⟨Us x hx, hUo _ _⟩, ⟨x, by simpa⟩, hUx _ _⟩
  · grind

Goal state after: