mathlib-initiative/mathlib-tactics huggingface dataset:
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 := 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 U x ⋯)) (φRX.hom' a) = (ConcreteCategory.hom (φRX ≫ X.presheaf.germ U x hxU)) a

Tactic:
]

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 U x ⋯)) (φRX.hom' a) = (ConcreteCategory.hom (φRX ≫ X.presheaf.germ U x hxU)) a
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
⊢ S.presheaf.germ U (sY y) ⋯ ≫ S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x =
    Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU

Tactic:
]

Goal state after:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
⊢ S.presheaf.germ U (sY y) ⋯ ≫ S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x =
    Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_1
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ Spec.map φ ≫ Y.fromSpecStalk y = Spec.map φ ≫ Y.fromSpecStalk y

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ hW.fromSpec ≫ sX = hW.fromSpec ≫ sX

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_1
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ sX x = sX x

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ Spec.map (Scheme.Hom.stalkMap sY (φ (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))) ≫ Scheme.stalkClosedPointTo φ) ≫
      S.fromSpecStalk (sY (φ (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)))) =
    Spec.map (S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x) ≫
      S.fromSpecStalk (sY (φ (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))))

Tactic:
]

Goal state after:
case refine_2
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ Spec.map (Scheme.Hom.stalkMap sY (φ (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))) ≫ Scheme.stalkClosedPointTo φ) ≫
      S.fromSpecStalk (sY (φ (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)))) =
    Spec.map (S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x) ≫
      S.fromSpecStalk (sY (φ (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))))
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: 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

Tactic:
]

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
inst✝ : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = (CommRingCat.Hom.hom (X.presheaf.germ U x hx)) 0
⊢ y = 0

Tactic:
]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ Set.univ ⊆ closure (⇑f '' Set.univ)

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ Set.univ ⊆ closure (⇑f '' Set.univ)
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: case e'_4
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ Set.range ⇑f = Set.range ⇑f

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝¹ : IrreducibleSpace ↥X
U : X.Opens
x : ↥U
inst✝ : Nonempty ↥↑U
⊢ CommRingCat.Hom.hom (X.germToFunctionField U) = CommRingCat.Hom.hom (X.presheaf.germ U (genericPoint ↥X) ⋯)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: R : CommRingCat
inst✝ : IsDomain ↑R
⊢ closure {⊥} = Set.univ

Tactic:
]

Goal state after:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ closure {⊥} = Set.univ
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: R : CommRingCat
inst✝ : IsDomain ↑R
⊢ PrimeSpectrum.zeroLocus ↑⊥.asIdeal = Set.univ

Tactic:
]

Goal state after:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ PrimeSpectrum.zeroLocus ↑⊥.asIdeal = Set.univ
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: R : CommRingCat
inst✝ : IsDomain ↑R
⊢ PrimeSpectrum.zeroLocus ↑⊥.asIdeal = PrimeSpectrum.zeroLocus {0}

Tactic:
]

Goal state after:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ PrimeSpectrum.zeroLocus ↑⊥.asIdeal = PrimeSpectrum.zeroLocus {0}
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ nonZeroDivisors ↑R = ⊥.asIdeal.primeCompl

Tactic:
]

Goal state after:
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ nonZeroDivisors ↑R = ⊥.asIdeal.primeCompl
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: case e'_3
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↥↑U
⊢ nonZeroDivisors ↑Γ(X, U) = ⊥.asIdeal.primeCompl

Tactic:
]

Goal state after:
case e'_3
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↥↑U
⊢ nonZeroDivisors ↑Γ(X, U) = ⊥.asIdeal.primeCompl
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
⊢ f ≠ 0

Tactic:
]

Goal state after:
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
⊢ f ≠ 0
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f g : X.PartialMap Y
e : f.domain = g.domain
H : f.hom = (X.isoOfEq e).hom ≫ g.hom
⊢ ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom

Tactic:
]

Goal state after:
X Y : Scheme
f g : X.PartialMap Y
e : f.domain = g.domain
H : f.hom = (X.isoOfEq e).hom ≫ g.hom
⊢ ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom
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
⊢ ⟨x, ⋯⟩ = (ConcreteCategory.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE hU'))) ⟨x, hx⟩

Tactic:
]

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
⊢ ⟨x, ⋯⟩ = (ConcreteCategory.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE hU'))) ⟨x, hx⟩
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⟩)) ≫
      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

Tactic:
]

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: case e_a.e_a
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⟩
⊢ Hom.stalkMap f.domain.ι ⟨x, ⋯⟩ ≫ ((↑f.domain).presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ =
    (X.presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (X.homOfLE hU' ≫ f.domain.ι) ⟨x, hx⟩

Tactic:
]

Goal state after:
case e_a.e_a
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⟩
⊢ Hom.stalkMap f.domain.ι ⟨x, ⋯⟩ ≫ ((↑f.domain).presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ =
    (X.presheaf.stalkCongr ⋯).hom ≫ Hom.stalkMap (X.homOfLE hU' ≫ f.domain.ι) ⟨x, hx⟩
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case e_a.e_a
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⟩
⊢ X.presheaf.stalkSpecializes ⋯ ≫
      Hom.stalkMap f.domain.ι ((X.homOfLE hU') ⟨x, hx⟩) ≫ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ =
    X.presheaf.stalkSpecializes ⋯ ≫
      Hom.stalkMap f.domain.ι ((X.homOfLE hU') ⟨x, hx⟩) ≫ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩

Tactic:
]

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

Goal state before:
pp: case refine_2
X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
U : (↑(f.domain ⊓ g.domain)).Opens
hxU : ⟨x, ⋯⟩ ∈ U
e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
⊢ (Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom =
    (Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom

Tactic:
]

Goal state after:
case refine_2
X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
U : (↑(f.domain ⊓ g.domain)).Opens
hxU : ⟨x, ⋯⟩ ∈ U
e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
⊢ (Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom =
    (Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case e'_2
X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
U : (↑(f.domain ⊓ g.domain)).Opens
hxU : ⟨x, ⋯⟩ ∈ U
e : (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom
⊢ ((Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ X.homOfLE ⋯) ≫ f.domain.ι = (U.ι ≫ X.homOfLE ⋯) ≫ f.domain.ι

Tactic:
]

Goal state after:
case e'_2
X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
U : (↑(f.domain ⊓ g.domain)).Opens
hxU : ⟨x, ⋯⟩ ∈ U
e : (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom
⊢ ((Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ X.homOfLE ⋯) ≫ f.domain.ι = (U.ι ≫ X.homOfLE ⋯) ≫ f.domain.ι
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case e'_3
X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
U : (↑(f.domain ⊓ g.domain)).Opens
hxU : ⟨x, ⋯⟩ ∈ U
e : (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom
⊢ ((Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ X.homOfLE ⋯) ≫ g.domain.ι = (U.ι ≫ X.homOfLE ⋯) ≫ g.domain.ι

Tactic:
]

Goal state after:
case e'_3
X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
U : (↑(f.domain ⊓ g.domain)).Opens
hxU : ⟨x, ⋯⟩ ∈ U
e : (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom
⊢ ((Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ X.homOfLE ⋯) ≫ g.domain.ι = (U.ι ≫ X.homOfLE ⋯) ≫ g.domain.ι
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case refine_1
X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
hdense : Dense (↑f.domain ⊓ ↑g.domain)
H :
  (f.restrict (f.domain ⊓ g.domain) hdense ⋯).fromSpecStalkOfMem ⋯ =
    (g.restrict (f.domain ⊓ g.domain) hdense ⋯).fromSpecStalkOfMem ⋯
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
⊢ (↑(f.domain ⊓ g.domain)).fromSpecStalk ⟨x, ⋯⟩ ≫ X.homOfLE ⋯ ≫ f.hom =
    (↑(f.domain ⊓ g.domain)).fromSpecStalk ⟨x, ⋯⟩ ≫ X.homOfLE ⋯ ≫ g.hom

Tactic:
]

Goal state after:
case refine_1
X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
hdense : Dense (↑f.domain ⊓ ↑g.domain)
H :
  (f.restrict (f.domain ⊓ g.domain) hdense ⋯).fromSpecStalkOfMem ⋯ =
    (g.restrict (f.domain ⊓ g.domain) hdense ⋯).fromSpecStalkOfMem ⋯
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
⊢ (↑(f.domain ⊓ g.domain)).fromSpecStalk ⟨x, ⋯⟩ ≫ X.homOfLE ⋯ ≫ f.hom =
    (↑(f.domain ⊓ g.domain)).fromSpecStalk ⟨x, ⋯⟩ ≫ X.homOfLE ⋯ ≫ g.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
hfg : f.domain = g.domain
inst✝¹ : IsOver S f
inst✝ : IsOver S g
⊢ (f.restrict f.domain ⋯ ⋯).hom = (g.restrict f.domain ⋯ ⋯).hom ↔ f = g

Tactic:
]

Goal state after:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f g : X.PartialMap Y
hfg : f.domain = g.domain
inst✝¹ : IsOver S f
inst✝ : IsOver S g
⊢ (f.restrict f.domain ⋯ ⋯).hom = (g.restrict f.domain ⋯ ⋯).hom ↔ f = g
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 : X.PartialMap Y
g : X ⟶ Y
inst✝¹ : IsOver S f
inst✝ : Hom.IsOver g S
⊢ (f.restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom =
      ((Hom.toPartialMap g).restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom ↔
    (X.isoOfEq ⋯).hom ≫ f.hom = (X.isoOfEq ⋯).hom ≫ f.domain.ι ≫ g

Tactic:
]

Goal state after:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst✝¹ : IsOver S f
inst✝ : Hom.IsOver g S
⊢ (f.restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom =
      ((Hom.toPartialMap g).restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom ↔
    (X.isoOfEq ⋯).hom ≫ f.hom = (X.isoOfEq ⋯).hom ≫ f.domain.ι ≫ g
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
⊢ f.toRationalMap = f.toRationalMap

Tactic:
]

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

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
g : Y ⟶ Z
f₁ f₂ : X.PartialMap Y
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f₁.domain
hWr : W ≤ f₂.domain
e : X.homOfLE hWl ≫ f₁.hom = X.homOfLE hWr ≫ f₂.hom
⊢ X.homOfLE hWr ≫ f₂.hom ≫ g = X.homOfLE hWr ≫ f₂.hom ≫ g

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: X Y S : Scheme
inst✝² : X.Over S
inst✝¹ : Y.Over S
f : X.PartialMap Y
inst✝ : RationalMap.IsOver S f.toRationalMap
f' : X.PartialMap Y
hf₁ : IsOver S f'
hf₂ : f'.toRationalMap = f.toRationalMap
U : X.Opens
hU : Dense ↑U
hUl : U ≤ f'.domain
hUr : U ≤ f.domain
e : (f'.restrict U hU hUl).hom = (f.restrict U hU hUr).hom
⊢ Hom.IsOver (f'.restrict U hU hUl).hom S

Tactic:
]

Goal state after:
X Y S : Scheme
inst✝² : X.Over S
inst✝¹ : Y.Over S
f : X.PartialMap Y
inst✝ : RationalMap.IsOver S f.toRationalMap
f' : X.PartialMap Y
hf₁ : IsOver S f'
hf₂ : f'.toRationalMap = f.toRationalMap
U : X.Opens
hU : Dense ↑U
hUl : U ≤ f'.domain
hUr : U ≤ f.domain
e : (f'.restrict U hU hUl).hom = (f.restrict U hU hUr).hom
⊢ Hom.IsOver (f'.restrict U hU hUl).hom S
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case mp
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
h : IsOver S f
g : X.PartialMap Y
hg : PartialMap.IsOver S g
e : g.toRationalMap = f
⊢ (Hom.toPartialMap (X ↘ S)).toRationalMap = (Hom.toPartialMap (X ↘ S)).toRationalMap

Tactic:
]

Goal state after: