awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
xk : ↥(d.functor.obj k)
h2 : (d.natTrans.app k) xk = uk
h_1 :
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor))
h_2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) :
      ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
h :
  Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
    (d.toBase ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor)) : ↥S)
⊢ Eq (α := ↥(colimit d.functor))
    ((colimit.ι d.functor i) ((d.functor.map fi) xk : ↥(d.functor.obj i)) : ↥(colimit d.functor))
    ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor))

Tactic:
simp [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
y : ↥(d.functor.obj i)
h :
  Eq (α := ↥S)
    ((𝒰.f i)
        ((d.natTrans.app i) y :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)) :
      ↥S)
    (d.toBase ((colimit.ι d.functor i) y : ↥(colimit d.functor)) : ↥S)
⊢ Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor i) y : ↥(colimit d.functor))

Tactic:
use d.natTrans.app i y

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, CategoryTheory.NatTrans.app, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.natTrans
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
y : ↥(d.functor.obj i)
h :
  Eq (α := ↥S)
    ((𝒰.f i)
        ((d.natTrans.app i) y :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)) :
      ↥S)
    ((d.natTrans.app i ≫ 𝒰.f i) y : ↥S)
⊢ Eq (α := ↥S)
    ((𝒰.f i)
        ((d.natTrans.app i) y :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)) :
      ↥S)
    (d.toBase ((colimit.ι d.functor i) y : ↥(colimit d.functor)) : ↥S)

Tactic:
rw [← Scheme.Hom.comp_apply, ι_toBase]

Premises used: AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase, AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
y : ↥(d.functor.obj i)
⊢ Eq (α := ↥S)
    ((𝒰.f i)
        ((d.natTrans.app i) y :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)) :
      ↥S)
    ((d.natTrans.app i ≫ 𝒰.f i) y : ↥S)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
⊢ Eq (α := d.glued.Opens) (d.toBase ⁻¹ᵁ Hom.opensRange (𝒰.f i)) (Hom.opensRange (colimit.ι d.functor i))

Tactic:
TopologicalSpace.Opens.coe_inj.mp (preimage_toBase_eq_range_ι d i)

Premises used: Iff.mp, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι, TopologicalSpace.Opens.coe_inj
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
⊢ CommSq (Y := colimit d.functor) (d.natTrans.app i) (colimit.ι d.functor i : d.functor.obj i ⟶ colimit d.functor)
    (𝒰.f i) (d.toBase : d.glued ⟶ S)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
refine_1 : (s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)) → s.pt ⟶ d.functor.obj i
refine_2 :
  ∀ (s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)),
    IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i = s.fst
refine_3 :
  ∀ (s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)),
    IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ colimit.ι d.functor i = s.snd
refine_4 :
  ∀ (s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)) (m : s.pt ⟶ d.functor.obj i),
    m ≫ d.natTrans.app i = s.fst →
      m ≫ colimit.ι d.functor i = s.snd → m = IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯
⊢ IsPullback (Y := colimit d.functor) (d.natTrans.app i) (colimit.ι d.functor i : d.functor.obj i ⟶ colimit d.functor)
    (𝒰.f i) (d.toBase : d.glued ⟶ S)

Tactic:
refine ⟨by simp, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
refine_1 :
  Subset (α := Set ↥(colimit d.functor)) (Set.range (ι := ↥s.pt) ⇑s.snd)
    (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
⊢ s.pt ⟶ d.functor.obj i

Tactic:
apply IsOpenImmersion.lift (colimit.ι d.functor i) s.snd

Premises used: AlgebraicGeometry.IsOpenImmersion.lift, CategoryTheory.Limits.PullbackCone.snd, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
refine_1 :
  Subset (α := Set ↥(colimit d.functor)) (Set.range (ι := ↥s.pt) ⇑s.snd)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
⊢ Subset (α := Set ↥(colimit d.functor)) (Set.range (ι := ↥s.pt) ⇑s.snd)
    (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))

Tactic:
rw [← preimage_toBase_eq_range_ι]

Premises used: AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
x : ↥s.pt
h :
  Eq (α := ↥S)
    ((𝒰.f i) (s.fst x : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)) : ↥S)
    (d.toBase (s.snd x : ↥(colimit d.functor)) : ↥S)
⊢ Membership.mem (α := ↥(colimit d.functor)) (γ := Set ↥(colimit d.functor))
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))) (s.snd x : ↥(colimit d.functor))

Tactic:
use s.fst x

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.PullbackCone.fst, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
x : ↥s.pt
h :
  Eq (α := ↥S)
    ((𝒰.f i) (s.fst x : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)) : ↥S)
    ((s.fst ≫ 𝒰.f i) x : ↥S)
⊢ Eq (α := ↥S)
    ((𝒰.f i) (s.fst x : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)) : ↥S)
    (d.toBase (s.snd x : ↥(colimit d.functor)) : ↥S)

Tactic:
rw [← Scheme.Hom.comp_apply, ← s.condition]

Premises used: CategoryTheory.Limits.PullbackCone.condition, AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
x : ↥s.pt
⊢ Eq (α := ↥S)
    ((𝒰.f i) (s.fst x : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)) : ↥S)
    ((s.fst ≫ 𝒰.f i) x : ↥S)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
refine_2 : (IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i) ≫ 𝒰.f i = s.fst ≫ 𝒰.f i
refine_2₁ : IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i ≫ 𝒰.f i = s.fst ≫ 𝒰.f i
refine_2₂ :
  IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫
      CategoryStruct.comp (Y := colimit d.functor) (colimit.ι d.functor i : d.functor.obj i ⟶ colimit d.functor)
        (d.toBase : d.glued ⟶ S) =
    s.fst ≫ 𝒰.f i
refine_2₃ : s.snd ≫ d.toBase = s.fst ≫ 𝒰.f i
refine_2₄ refine_2₅ : s.snd ≫ d.toBase = s.snd ≫ d.toBase
⊢ IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i = s.fst

Tactic:
rw [← cancel_mono (𝒰.f i), Category.assoc, ← ι_toBase, IsOpenImmersion.lift_fac_assoc,
      s.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.PullbackCone.condition, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase, CategoryTheory.cancel_mono, AlgebraicGeometry.IsOpenImmersion.lift_fac_assoc, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
⊢ ∀ (s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)),
    IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ colimit.ι d.functor i = s.snd

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (Y := colimit d.functor) (𝒰.f i) (d.toBase : d.glued ⟶ S)
m : s.pt ⟶ d.functor.obj i
h1 : m ≫ d.natTrans.app i = s.fst
h2 : m ≫ colimit.ι d.functor i = s.snd
⊢ m = IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯

Tactic:
simpa [← cancel_mono (colimit.ι d.functor i)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X_1 : Scheme
U : X_1.Opens
X : Scheme
x : ↥X
⊢ IsPreimmersion (Spec.map (X.residue x))

Tactic:
IsPreimmersion.mk_SpecMap
    (PrimeSpectrum.isClosedEmbedding_comap_of_surjective _ _
      Ideal.Quotient.mk_surjective).isEmbedding
    (RingHom.surjectiveOnStalks_of_surjective (Ideal.Quotient.mk_surjective))

Premises used: AlgebraicGeometry.IsPreimmersion.mk_SpecMap, RingHom.surjectiveOnStalks_of_surjective, Topology.IsClosedEmbedding.isEmbedding, Ideal.Quotient.mk_surjective, PrimeSpectrum.isClosedEmbedding_comap_of_surjective
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x : ↥X
s : ↥(Spec (X.residueField x))
⊢ Eq (α := ↥(Spec (X.presheaf.stalk x))) ((Spec.map (X.residue x)) s : ↥(Spec (X.presheaf.stalk x)))
    (closedPoint (↑(X.presheaf.stalk x) : Type u) : PrimeSpectrum (↑(X.presheaf.stalk x) : Type u))

Tactic:
IsLocalRing.PrimeSpectrum.comap_residue _ s

Premises used: Ideal.Quotient.mk, IsLocalRing.residue, IsLocalRing.PrimeSpectrum.comap_residue, IsLocalRing.ResidueField, PrimeSpectrum.comap
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x : ↥X
⊢ Function.Surjective (α := (↑(X.presheaf.stalk x) : Type u)) (β := (↑(X.residueField x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X.residue x)) :
      (a : (↑(X.presheaf.stalk x) : Type u)) → (↑(X.residueField x) : Type u))

Tactic:
Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective, IsLocalRing.ResidueField
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X_1 : Scheme
U : X_1.Opens
X : Scheme
x : ↥X
⊢ Epi (X.residue x)

Tactic:
ConcreteCategory.epi_of_surjective _ (X.residue_surjective x)

Premises used: CategoryTheory.ConcreteCategory.epi_of_surjective, AlgebraicGeometry.Scheme.residue_surjective
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
K : Type u
inst : Field K
X : Scheme
x : ↥X
f : X.presheaf.stalk x ⟶ CommRingCat.of K
inst_1 :
  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑(CommRingCat.of K) : Type u)) (CommRingCat.Hom.hom f)
⊢ X.residue x ≫ descResidueField f = f

Tactic:
CommRingCat.hom_ext <| RingHom.ext fun _ ↦ rfl

Premises used: CommRingCat.hom_ext, RingHom.ext, rfl
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
U : X.Opens
x : ↥X
hx : x ∈ U
⊢ X.presheaf.germ U x hx ≫ X.residue x = X.evaluation U x hx

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.evaluation, rfl
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
U : X.Opens
x : ↥X
hx : x ∈ U
f : (↑Γ(X, U) : Type u)
⊢ Eq (α := (↑(X.residueField x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.evaluation U x hx) :
            (a : (↑Γ(X, U) : Type u)) → (↑(X.residueField x) : Type u))
          f :
        (↑(X.residueField x) : Type u))
      (0 : (↑(X.residueField x) : Type u)) ↔
    x ∉ X.basicOpen f

Tactic:
X.toLocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen ⟨x, hx⟩ f

Premises used: Set.Mem, setOf, Subtype.mk, AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
U : X.Opens
x : ↥X
hx : x ∈ U
f : (↑Γ(X, U) : Type u)
⊢ Ne (α := (↑(X.residueField x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.evaluation U x hx) :
            (a : (↑Γ(X, U) : Type u)) → (↑(X.residueField x) : Type u))
          f :
        (↑(X.residueField x) : Type u))
      (0 : (↑(X.residueField x) : Type u)) ↔
    x ∈ X.basicOpen f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
U : X.Opens
f : (↑(X.presheaf.obj (op U)) : Type u)
⊢ X.basicOpen f = ⊥ ↔
    ∀ (x : ↥U),
      Eq (α := (↑(X.residueField (↑x : ↥X)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.evaluation U (↑x : ↥X) ⋯) :
              (a : (↑Γ(X, U) : Type u)) → (↑(X.residueField (↑x : ↥X)) : Type u))
            f :
          (↑(X.residueField (↑x : ↥X)) : Type u))
        (0 : (↑(X.residueField (↑x : ↥X)) : Type u))

Tactic:
X.toLocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero f

Premises used: AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, Set.Mem, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Y.residue (f x) ≫ CommRingCat.ofHom (ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))) =
    Hom.stalkMap f x ≫ X.residue x

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x : ↥X
⊢ Hom.residueFieldMap (𝟙 X) x = 𝟙 (X.residueField x)

Tactic:
LocallyRingedSpace.residueFieldMap_id _

Premises used: AlgebraicGeometry.Scheme.Hom.residueFieldMap, AlgebraicGeometry.Scheme.residueField, AlgebraicGeometry.LocallyRingedSpace.residueFieldMap_id
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
x : ↥X
⊢ Hom.residueFieldMap (f ≫ g) x = Hom.residueFieldMap g (f x) ≫ Hom.residueFieldMap f x

Tactic:
LocallyRingedSpace.residueFieldMap_comp _ _ _

Premises used: AlgebraicGeometry.LocallyRingedSpace.residueFieldMap_comp, AlgebraicGeometry.Scheme.Hom.residueFieldMap, AlgebraicGeometry.Scheme.residueField
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X Y : Scheme
f : X ⟶ Y
V : Y.Opens
x : ↥X
hx : Membership.mem (α := ↥Y) V (f x : ↥Y)
⊢ Y.evaluation V (f x) hx ≫ Hom.residueFieldMap f x = Hom.app f V ≫ X.evaluation (f ⁻¹ᵁ V) x hx

Tactic:
LocallyRingedSpace.evaluation_naturality f.1 ⟨x, hx⟩

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.residueField, Subtype.mk, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X Y : Scheme
f : X ⟶ Y
V : Y.Opens
x : ↥X
hx : Membership.mem (α := ↥Y) V (f x : ↥Y)
s : (↑Γ(Y, V) : Type u)
⊢ Eq (α := (↑(X.residueField x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.residueFieldMap f x) :
          (a : (↑(Y.residueField (f x)) : Type u)) → (↑(X.residueField x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y.evaluation V (f x) hx) :
            (a : (↑Γ(Y, V) : Type u)) → (↑(Y.residueField (f x)) : Type u))
          s) :
      (↑(X.residueField x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, f ⁻¹ᵁ V)) (X.evaluation (f ⁻¹ᵁ V) x hx) :
          (a : (↑Γ(X, f ⁻¹ᵁ V) : Type u)) → (↑(X.residueField x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app f V) :
            (a : (↑Γ(Y, V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u))
          s) :
      (↑(X.residueField x) : Type u))

Tactic:
LocallyRingedSpace.evaluation_naturality_apply f.1 ⟨x, hx⟩ s

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom', Subtype.mk, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Y.Γevaluation (f x) ≫ Hom.residueFieldMap f x = Hom.appTop f ≫ X.Γevaluation x

Tactic:
LocallyRingedSpace.Γevaluation_naturality f.toLRSHom x

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom, Set.Mem, Set.univ, setOf, AlgebraicGeometry.Scheme.residueField, Set.preimage, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
a : (↑(Y.presheaf.obj (op ⊤)) : Type u)
⊢ Eq (α := (↑(X.residueField x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.residueFieldMap f x) :
          (a : (↑(Y.residueField (f x)) : Type u)) → (↑(X.residueField x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Y.residueField (f x)) (Y.Γevaluation (f x)) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑(Y.residueField (f x)) : Type u))
          a) :
      (↑(X.residueField x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.Γevaluation x) :
          (a : (↑Γ(X, ⊤) : Type u)) → (↑(X.residueField x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          a) :
      (↑(X.residueField x) : Type u))

Tactic:
LocallyRingedSpace.Γevaluation_naturality_apply f.toLRSHom x a

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X_1 : Scheme
U : X_1.Opens
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
x : ↥X
⊢ IsIso (Hom.residueFieldMap f x)

Tactic:
(IsLocalRing.ResidueField.mapEquiv
    (asIso (f.stalkMap x)).commRingCatIsoToRingEquiv).toCommRingCatIso.isIso_hom

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, AlgebraicGeometry.Scheme.Hom.residueFieldMap, IsLocalRing.ResidueField.map, Quotient.liftOn', Set.Mem, AddCon.liftOn, RingEquiv.toCommRingCatIso, MonoidHomClass.toMonoidHom, AlgebraicGeometry.Scheme.residueField, CategoryTheory.Iso.isIso_hom, IsLocalRing.ResidueField, RingHomClass.toRingHom, Ideal.Quotient.lift, Submodule.quotientRel, AlgebraicGeometry.Scheme.Hom.stalkMap, AddAction.orbitRel, IsLocalRing.ResidueField.mapEquiv, AddCon.Quotient, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X_1 : Scheme
U : X_1.Opens
X Y : Scheme
f : X ⟶ Y
x y : ↥X
h : x = y
subst : X.residueField x = X.residueField x
⊢ X.residueField x = X.residueField y

Tactic:
subst h
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X_1 : Scheme
U : X_1.Opens
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ X.residueField x = X.residueField x

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x : ↥X
⊢ residueFieldCongr ⋯ = Iso.refl (X.residueField x)

Tactic:
rfl

Premises used: Eq.mpr, AlgebraicGeometry.Scheme.residueFieldCongr, CategoryTheory.eqToHom, CategoryTheory.eqToIso, CategoryTheory.Iso.refl, rfl