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

Goal state before:
pp: X : Scheme
x : ↥X
⊢ X.fromSpecStalk x ≫ X.toSpecΓ = Spec.map (X.presheaf.germ ⊤ x trivial)

Tactic:
rw [Scheme.toSpecΓ_naturality, ← SpecMap_ΓSpecIso_hom, ← Spec.map_comp,
    Scheme.fromSpecStalk_appTop]

Goal state after:
X : Scheme
x : ↥X
⊢ Spec.map
      ((X.presheaf.germ ⊤ x trivial ≫
          (ΓSpecIso (X.presheaf.stalk x)).inv ≫ (Spec (X.presheaf.stalk x)).presheaf.map (homOfLE ⋯).op) ≫
        (ΓSpecIso (X.presheaf.stalk x)).hom) =
    Spec.map (X.presheaf.germ ⊤ x trivial)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₁.h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ ((pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
            pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯) ≫
        pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) =
    (𝟙 (pullback (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
        pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)

Tactic:
rw [← cancel_mono (glueDataObjι _ _), ← cancel_mono (Scheme.Opens.ι _)]
        simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
          glueDataT'Aux_fst, limit.lift_π_assoc, cospan_left, glueDataT_fst, Scheme.homOfLE_ι,
          glueDataT'Aux_snd_ι, glueDataT'Aux_fst_assoc, glueDataT_fst_assoc, Category.id_comp]
        rw [← pullback.condition_assoc, pullback.condition_assoc (f := I.glueDataObjι i),
          X.homOfLE_ι]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Hom.opensRange (I.glueData.ι U ≫ I.subschemeIso.inv) = I.subschemeι ⁻¹ᵁ ↑U

Tactic:
by
  ext1
  simp [Set.range_comp, I.range_glueData_ι, subschemeι_def, ← coe_homeoOfIso_symm,
    ← homeoOfIso_symm, ← Homeomorph.coe_symm_toEquiv, Equiv.image_symm_eq_preimage]

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

Goal state before:
pp: W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this : IsSeparated Y'.hom
⊢ ι' ≫ f' = ι' ≫ g'

Tactic:
ext1; exact hU

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

Goal state before:
pp: case inr.mpr.inr.inl
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi✝ : i ≠ ((LinearMap.mul R A) f).charpoly.natDegree
hi : i < ((LinearMap.mul R A) f).charpoly.natDegree
⊢ (Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f))).coeff i =
    (X ^ ((LinearMap.mul R A) f).charpoly.natDegree).coeff i

pp: case inr.mpr.inr.inr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi✝ : i ≠ ((LinearMap.mul R A) f).charpoly.natDegree
hi : ((LinearMap.mul R A) f).charpoly.natDegree < i
⊢ (Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f))).coeff i =
    (X ^ ((LinearMap.mul R A) f).charpoly.natDegree).coeff i

Tactic:
· simpa [hi.ne, ← RingHom.mem_ker, Ideal.ker_algebraMap_residueField] using H i hi

Goal state after:
case inr.mpr.inr.inr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi✝ : i ≠ ((LinearMap.mul R A) f).charpoly.natDegree
hi : ((LinearMap.mul R A) f).charpoly.natDegree < i
⊢ (Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f))).coeff i =
    (X ^ ((LinearMap.mul R A) f).charpoly.natDegree).coeff i
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case mp
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f}) →
    ¬IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f)

pp: case mpr
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
⊢ ¬IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f) →
    x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f})

Tactic:
· rintro ⟨q, ⟨hqg, hqf⟩, rfl⟩ H
    simp only [mem_zeroLocus, Set.singleton_subset_iff, SetLike.mem_coe] at hqg hqf
    have hs : Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField) := by
      rwa [Ideal.span_le, Ideal.ker_algebraMap_residueField]
    let F : (A ⧸ Ideal.span s) ⊗[R] (q.asIdeal.comap (algebraMap R A)).ResidueField →ₐ[A]
        q.asIdeal.ResidueField :=
      Algebra.TensorProduct.lift
        (Ideal.Quotient.liftₐ (Ideal.span s) (Algebra.ofId A _) hs)
        (Ideal.ResidueField.mapₐ _ _ (Algebra.ofId _ _) rfl)
        fun _ _ ↦ .all _ _
    have := H.map F
    rw [AlgHom.commutes, isNilpotent_iff_eq_zero, ← RingHom.mem_ker,
      Ideal.ker_algebraMap_residueField] at this
    exact hqf this

Goal state after:
case mpr
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
⊢ ¬IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f) →
    x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f})
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case h
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
x : PrimeSpectrum R
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f}) ↔
    x ∈
      (zeroLocus
          ↑(Finset.image
              (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((Ideal.Quotient.mk (Ideal.span s)) f))).coeff
              (Finset.range (Module.finrank R (A ⧸ Ideal.span s)))))ᶜ

Tactic:
mem_image_comap_zeroLocus_sdiff,

Goal state after:
case h
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
x : PrimeSpectrum R
⊢ ¬IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f) ↔
    x ∈
      (zeroLocus
          ↑(Finset.image
              (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((Ideal.Quotient.mk (Ideal.span s)) f))).coeff
              (Finset.range (Module.finrank R (A ⧸ Ideal.span s)))))ᶜ
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case hK
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ IsCompact (↑↑U ∩ (↑↑U ∩ ↑↑V))

pp: case Kf
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ (↑↑U ∩ ↑↑V) ⊆ Set.range ⇑(IsAffineOpen.fromSpec ⋯)

Tactic:
· apply (noetherianSpace_set_iff _).mp
      · convert! noetherianSpace_of_isAffineOpen U.1 U.2
        apply IsLocallyNoetherian.component_noetherian
      · exact Set.inter_subset_left

Goal state after:
case Kf
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ (↑↑U ∩ ↑↑V) ⊆ Set.range ⇑(IsAffineOpen.fromSpec ⋯)
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
inst✝ : P.IsClosedUnderIsomorphisms
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : TopologicalSpace.IsOpenCover U
H : ∀ (i : ι), IsIntegral ↑(U i) → Subsingleton ↥↑(U i) → P ↑(f ⁻¹ᵁ U i)
x✝² : IsIntegral Y
x✝¹ : Subsingleton ↥Y
y : ↥Y
i : ι
hy : y ∈ U i
z : ↥Y
x✝ : z ∈ ⊤
⊢ z ∈ U i

Tactic:
Subsingleton.elim z y

Goal state after:
P : ObjectProperty Scheme
inst✝ : P.IsClosedUnderIsomorphisms
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : TopologicalSpace.IsOpenCover U
H : ∀ (i : ι), IsIntegral ↑(U i) → Subsingleton ↥↑(U i) → P ↑(f ⁻¹ᵁ U i)
x✝² : IsIntegral Y
x✝¹ : Subsingleton ↥Y
y : ↥Y
i : ι
hy : y ∈ U i
z : ↥Y
x✝ : z ∈ ⊤
⊢ y ∈ U i
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr.convert_3
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
i : ι
⊢ IsCompact (S i).1.carrier

Tactic:
apply isCompact_iff_isCompact_univ.mpr

Goal state after:
case mpr.convert_3
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
i : ι
⊢ IsCompact Set.univ
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: case refine_3
X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ (pullbackSymmetry (map (CommRingCat.ofHom (algebraMap R S))) ((Spec (CommRingCat.of R)).fromSpecResidueField p) ≪≫
          (pullback.congrHom ⋯ ⋯ ≪≫
              asIso
                (pullback.map
                  (map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv ≫
                    map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R)) p.asIdeal.ResidueField)))
                  (map (CommRingCat.ofHom (algebraMap R S)))
                  (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
                  (map (CommRingCat.ofHom (algebraMap R S)))
                  (map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv) (𝟙 (Spec (CommRingCat.of S)))
                  (𝟙 (Spec (CommRingCat.of R))) ⋯ ⋯)) ≪≫
            pullbackSpecIso R p.asIdeal.ResidueField S).hom ≫
      map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))) =
    Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p ≫
      (Scheme.Spec.mapIso (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).symm.op).hom

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ (∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)) → IsNoetherian X

Tactic:
intro hNoeth

Goal state after:
case mpr
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
⊢ IsNoetherian X
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
this : ∀ (U : Y.Opens), IsAffineOpen U → Function.Injective ⇑(ConcreteCategory.hom (app f U))
hU : ¬IsAffineOpen U
⊢ Function.Injective ⇑(ConcreteCategory.hom (app f U))

Tactic:
injective_iff_map_eq_zero

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
this : ∀ (U : Y.Opens), IsAffineOpen U → Function.Injective ⇑(ConcreteCategory.hom (app f U))
hU : ¬IsAffineOpen U
⊢ ∀ (a : ↑Γ(Y, U)), (ConcreteCategory.hom (app f U)) a = 0 → a = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : Surjective f
⊢ (topologically @IsClosedMap).universally g

Tactic:
intro X' Y' i₁ i₂ f' H

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : Surjective f
X' Y' : Scheme
i₁ : X' ⟶ Y
i₂ : Y' ⟶ Z
f' : X' ⟶ Y'
H : IsPullback f' i₁ i₂ g
⊢ topologically (@IsClosedMap) f'
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
X✝ Y✝ Z✝ : Type uᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { app := reindex ⇑(ConcreteCategory.hom (f ≫ g).unop), naturality := ⋯ } =
    { app := reindex ⇑(ConcreteCategory.hom f.unop), naturality := ⋯ } ≫
      { app := reindex ⇑(ConcreteCategory.hom g.unop), naturality := ⋯ }

Tactic:
by ext : 2; dsimp; exact reindex_comp _ _ _

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}
this : IsFinite (X.fromSpecResidueField x ≫ f)
⊢ (ConcreteCategory.hom (Spec.preimage (X.fromSpecResidueField x ≫ f))).IsIntegral

Tactic:
← IsIntegralHom.SpecMap_iff,

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}
this : IsFinite (X.fromSpecResidueField x ≫ f)
⊢ IsIntegralHom (Spec.map (Spec.preimage (X.fromSpecResidueField x ≫ f)))
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
n : ℕ
f : locallyFinsuppWithin U Y
⊢ (n • f)⁺ = n • f⁺

Tactic:
by
  ext x
  simp only [posPart, max_apply, coe_nsmul, Pi.smul_apply, coe_zero, Pi.zero_apply]
  by_cases h : f x < 0
  · simpa [max_eq_right_of_lt h] using nsmul_le_nsmul_right h.le n
  · simpa [not_lt.1 h] using nsmul_nonneg (not_lt.1 h) n

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
X : Scheme
R A : CommRingCat
x : ↥X
inst✝ : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e✝ : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ V' x hxV'))
f : X.presheaf.obj (Opposite.op V') ⟶ X.presheaf.stalk x := ⋯
hf' : (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range ≤ (CommRingCat.Hom.hom f).range
e : ↑(X.presheaf.obj (Opposite.op V')) ≃+* ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range := ⋯
a : ↑R
⊢ ↑(e ((CommRingCat.Hom.hom (φRX ≫ X.presheaf.map ⋯.hom.op)) a)) =
    ↑(((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯) (φRA.hom' a))

Tactic:
change X.presheaf.germ _ _ _ (X.presheaf.map _ _) = (φRA ≫ φ) a

Goal state after:
case refine_2
X : Scheme
R A : CommRingCat
x : ↥X
inst✝ : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e✝ : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ V' x hxV'))
f : X.presheaf.obj (Opposite.op V') ⟶ X.presheaf.stalk x := X.presheaf.germ V' x hxV'
hf' : (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range ≤ (CommRingCat.Hom.hom f).range
e : ↑(X.presheaf.obj (Opposite.op V')) ≃+* ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range :=
  RingEquiv.ofLeftInverse ⋯
a : ↑R
⊢ (ConcreteCategory.hom (X.presheaf.germ V' x hxV')) ((ConcreteCategory.hom (X.presheaf.map ⋯.hom.op)) (φRX.hom' a)) =
    (ConcreteCategory.hom (φRA ≫ φ)) a
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:
injective_iff_map_eq_zero

Goal state after:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
⊢ ∀ (a : ↑(X.presheaf.obj (op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) a = 0 → a = 0
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ IsFractionRing ↑R ↑(Spec R).functionField ↔
    IsLocalization.AtPrime (↑((Spec.structureSheaf ↑R).presheaf.stalk (genericPoint ↥(Spec R))))
      (genericPoint ↥(Spec R)).asIdeal

Tactic:
delta IsFractionRing IsLocalization.AtPrime

Goal state after:
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ IsLocalization (nonZeroDivisors ↑R) ↑(Spec R).functionField ↔
    IsLocalization (genericPoint ↥(Spec R)).asIdeal.primeCompl
      ↑((Spec.structureSheaf ↑R).presheaf.stalk (genericPoint ↥(Spec R)))
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
f : ↑X.functionField
hf : f ≠ 0
U : Opens ↥X
hU : genericPoint ↥X ∈ U
g : ToType (X.presheaf.obj (op U))
hg : (ConcreteCategory.hom (X.presheaf.germ U (genericPoint ↥X) hU)) g = f
A : Opens ↥X
hA : A ∈ X.affineOpens
hxA : genericPoint ↥X ∈ ↑A
hAU : ↑A ⊆ ↑U
this✝ : Nonempty ↥↑A
gA : ↑Γ(X, A) := (ConcreteCategory.hom (X.presheaf.map (homOfLE hAU).op)) g
h_germ_gA : (ConcreteCategory.hom (X.presheaf.germ A (genericPoint ↥X) hxA)) gA = f
hxV : genericPoint ↥X ∈ X.basicOpen gA
this : Nonempty ↥↑(X.basicOpen gA)
⊢ (ConcreteCategory.hom (X.germToFunctionField (X.basicOpen gA)))
      ((ConcreteCategory.hom (X.presheaf.map ⋯.hom.op)) gA) =
    f

Tactic:
simpa using h_germ_gA

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (id X).compHom f = Hom.toRationalMap f

Tactic:
by
  rw [RationalMap.id, ← compHom_toRationalMap, PartialMap.id_compHom]

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

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝³ : X.Over S
inst✝² : Y.Over S
inst✝¹ : IsIntegral X
inst✝ : LocallyOfFiniteType (Y ↘ S)
⊢ (fun f ↦ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)) = fun f ↦ IsOver S f

Tactic:
ext f; rw [RationalMap.isOver_iff]

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₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
⊢ (((X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯) ≫ (X.isoOfEq ⋯).inv) ≫ (g x).hom =
    (((X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯) ≫ (X.isoOfEq ⋯).inv) ≫ (g y).hom

Tactic:
convert! (PartialMap.equiv_iff_of_isSeparated (S := ⊤_ _) (f := g x) (g := g y)).mp ?_ using 1

Goal state after:
case e'_2
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₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
e_1✝ : (↑((g x).domain ⊓ (g y).domain) ⟶ Y) = (↑((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).domain ⟶ Y)
⊢ (((X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯) ≫ (X.isoOfEq ⋯).inv) ≫ (g x).hom =
    ((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom

case e'_3
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₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
e_1✝ : (↑((g x).domain ⊓ (g y).domain) ⟶ Y) = (↑((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).domain ⟶ Y)
⊢ (((X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯) ≫ (X.isoOfEq ⋯).inv) ≫ (g y).hom =
    ((g y).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom

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₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
⊢ (g x).equiv (g y)
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case e
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
g : Y.PartialMap Z
x✝ : ↥X
⊢ x✝ ∈ ↑((f.restrict U hU hU').comp g).domain ↔
    x✝ ∈ ↑((f.comp g).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain ⊓ U) ⋯ ⋯).domain

Tactic:
simp [ι_image_homOfLE_eq_ι_image_inf]

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
inst✝ : Flat iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact ↑UT
this : Mono (pushoutSection ⋯ hUSX hUST ⋯)
⊢ (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)).hom ≫
      pushoutSection H hUST hUSX hUY =
    pushoutSection ⋯ hUSX hUST ⋯

Tactic:
cat_disch

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
inst✝ : Flat iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)).hom ≫
      pushoutSection H hUST hUSX hUY =
    pushoutSection ⋯ hUSX hUST ⋯

Tactic:
cat_disch

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
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUX : IsCompact ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
this : Mono (pushoutSection ⋯ hUSX hUST ⋯)
⊢ (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)).hom ≫
      pushoutSection H hUST hUSX hUY =
    pushoutSection ⋯ hUSX hUST ⋯

Tactic:
cat_disch

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
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)).hom ≫
      pushoutSection H hUST hUSX hUY =
    pushoutSection ⋯ hUSX hUST ⋯

Tactic:
cat_disch

Goal state after: