mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (R ⧸ Ideal.span {c}) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
T₂ : ConstructibleSetData (R ⧸ Ideal.span {c})
hT₁ : comap Polynomial.C '' (zeroLocus (Set.range e₁.val) \ zeroLocus {(mapRingHom ↑q₁) f}) = T₁.toSet
hT₁deg : ∀ x ∈ T₁, x.n ≤ e₁.degBound
hT₂ : comap Polynomial.C '' (zeroLocus (Set.range e₂.val) \ zeroLocus {(mapRingHom ↑q₂) f}) = T₂.toSet
hT₂deg : ∀ x ∈ T₂, x.n ≤ e₂.degBound
x✝² : Invertible (q₁ c) := { invOf := IsLocalization.Away.invSelf c, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
he₁span :
  coeffSubmodule R₀ e₁ ^ e₁.powBound =
    ⅟(q₁ c ^ e₁.powBound) • Submodule.map q₁.toLinearMap (span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
g₁ : (x : BasicConstructibleSetData (Localization.Away c)) → Fin x.n → R
hg₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), g₁ x i ∈ ↑(span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
hq₁g₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), q₁.toLinearMap (g₁ x i) = q₁ c ^ e₁.powBound * x.g i
n₁ : Localization.Away c → ℕ
f₁ : Localization.Away c → R
hf₁ : ∀ (x : Localization.Away c), x * q₁ c ^ n₁ x = q₁ (f₁ x)
g₂ : (x : BasicConstructibleSetData (R ⧸ Ideal.span {c})) → Fin x.n → R
hg₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), g₂ x i ∈ ↑(coeffSubmodule R₀ e ^ e₂.powBound)
hq₂g₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), q₂.toLinearMap (g₂ x i) = x.g i
f₂ : R ⧸ Ideal.span {c} → R
hf₂ : ∀ (x : R ⧸ Ideal.span {c}), q₂ (f₂ x) = x
S₁ : Finset (BasicConstructibleSetData R) := Finset.image (fun x ↦ { f := c * f₁ x.f, n := x.n, g := g₁ x }) T₁
S₂ : Finset (BasicConstructibleSetData R) :=
  Finset.image (fun x ↦ { f := f₂ x.f, n := x.n + 1, g := Fin.cons c (g₂ x) }) T₂
x✝¹ : PrimeSpectrum (Localization.Away c)[X]
x✝ : R
⊢ x✝ ∈ ((comap Polynomial.C ∘ comap (mapRingHom q₁.toRingHom)) x✝¹).asIdeal ↔
    x✝ ∈ ((comap ↑q₁ ∘ comap Polynomial.C) x✝¹).asIdeal

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp.Pushforward

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
hf✝ : IsSpectralMap f
w : X → R
inst✝¹ : Semiring R
W : Set Y
hW : IsOpen[inst✝²] W
c✝ : locallyFinsupp X R
inst✝ : PrespectralSpace Y
hf : IsSpectralMap f
c : locallyFinsupp X R
⊢ (support fun z ↦ ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {z}), c x * w x) ⊆ univ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp.Pushforward

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
hf✝ : IsSpectralMap f
w : X → R
inst✝¹ : Semiring R
W : Set Y
hW : IsOpen[inst✝²] W
c✝ : locallyFinsupp X R
inst✝ : PrespectralSpace Y
hf : IsSpectralMap f
c : locallyFinsupp X R
y : Y
x✝ : y ∈ univ
⊢ y ∈ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp.Pushforward

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
hf✝ : IsSpectralMap f
w : X → R
inst✝¹ : Semiring R
W : Set Y
hW : IsOpen[inst✝²] W
c✝ : locallyFinsupp X R
inst✝ : PrespectralSpace Y
hf : IsSpectralMap f
c : locallyFinsupp X R
y : Y
x✝ : y ∈ univ
⊢ IsOpen[inst✝²] ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp.Pushforward

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
hf✝ : IsSpectralMap f
w : X → R
inst✝¹ : Semiring R
W : Set Y
hW : IsOpen[inst✝²] W
c✝ : locallyFinsupp X R
inst✝ : PrespectralSpace Y
hf : IsSpectralMap f
c : locallyFinsupp X R
y : Y
x✝ : y ∈ univ
U : Set Y
hU : U ∈ {U | IsOpen[inst✝²] U ∧ IsCompact U} ∧ y ∈ U ∧ U ⊆ ⊤
⊢ f ⁻¹' (U ∩ {z | (f ⁻¹' {z} ∩ locallyFinsuppWithin.support c).Nonempty}) ∩ locallyFinsuppWithin.support c ⊆
    f ⁻¹' U ∩ support c.toFun

Tactic:
simp

Goal state after:
X : Type u_1
Y : Type u_2
R : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
hf✝ : IsSpectralMap f
w : X → R
inst✝¹ : Semiring R
W : Set Y
hW : IsOpen[inst✝²] W
c✝ : locallyFinsupp X R
inst✝ : PrespectralSpace Y
hf : IsSpectralMap f
c : locallyFinsupp X R
y : Y
x✝ : y ∈ univ
U : Set Y
hU : U ∈ {U | IsOpen[inst✝²] U ∧ IsCompact U} ∧ y ∈ U ∧ U ⊆ ⊤
⊢ f ⁻¹' U ∩ {a | (f ⁻¹' {f a} ∩ locallyFinsuppWithin.support c).Nonempty} ∩ locallyFinsuppWithin.support c ⊆ f ⁻¹' U
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
t : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))
ht : (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf)) t = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ t = 0

Tactic:
obtain ⟨t, s, rfl⟩ := IsLocalization.exists_mk'_eq (.powers f) t

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht :
  (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
      (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s) =
    0
⊢ IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s = 0
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (R ⧸ Ideal.span {c}) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
T₂ : ConstructibleSetData (R ⧸ Ideal.span {c})
hT₁ : comap Polynomial.C '' (zeroLocus (Set.range e₁.val) \ zeroLocus {(mapRingHom ↑q₁) f}) = T₁.toSet
hT₁deg : ∀ x ∈ T₁, x.n ≤ e₁.degBound
hT₂ : comap Polynomial.C '' (zeroLocus (Set.range e₂.val) \ zeroLocus {(mapRingHom ↑q₂) f}) = T₂.toSet
hT₂deg : ∀ x ∈ T₂, x.n ≤ e₂.degBound
x✝² : Invertible (q₁ c) := { invOf := IsLocalization.Away.invSelf c, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
he₁span :
  coeffSubmodule R₀ e₁ ^ e₁.powBound =
    ⅟(q₁ c ^ e₁.powBound) • Submodule.map q₁.toLinearMap (span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
g₁ : (x : BasicConstructibleSetData (Localization.Away c)) → Fin x.n → R
hg₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), g₁ x i ∈ ↑(span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
hq₁g₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), q₁.toLinearMap (g₁ x i) = q₁ c ^ e₁.powBound * x.g i
n₁ : Localization.Away c → ℕ
f₁ : Localization.Away c → R
hf₁ : ∀ (x : Localization.Away c), x * q₁ c ^ n₁ x = q₁ (f₁ x)
g₂ : (x : BasicConstructibleSetData (R ⧸ Ideal.span {c})) → Fin x.n → R
hg₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), g₂ x i ∈ ↑(coeffSubmodule R₀ e ^ e₂.powBound)
hq₂g₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), q₂.toLinearMap (g₂ x i) = x.g i
f₂ : R ⧸ Ideal.span {c} → R
hf₂ : ∀ (x : R ⧸ Ideal.span {c}), q₂ (f₂ x) = x
S₁ : Finset (BasicConstructibleSetData R) := Finset.image (fun x ↦ { f := c * f₁ x.f, n := x.n, g := g₁ x }) T₁
S₂ : Finset (BasicConstructibleSetData R) :=
  Finset.image (fun x ↦ { f := f₂ x.f, n := x.n + 1, g := Fin.cons c (g₂ x) }) T₂
x✝¹ : PrimeSpectrum (R ⧸ Ideal.span {c})[X]
x✝ : R
⊢ x✝ ∈ ((comap Polynomial.C ∘ comap (mapRingHom q₂.toRingHom)) x✝¹).asIdeal ↔
    x✝ ∈ ((comap ↑q₂ ∘ comap Polynomial.C) x✝¹).asIdeal

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case e_a.eU
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
this✝ : IsAffine ↑V
this :
  ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯
⊢ U = U.ι ''ᵁ Scheme.Hom.resLE f V U ⋯ ⁻¹ᵁ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case e_a.eV
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
this✝ : IsAffine ↑V
this :
  ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯
⊢ V = V.ι ''ᵁ ⊤

Tactic:
simp

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

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
⊢ closure {genericPoint ↥X} ∈ irreducibleComponents ↥X

Tactic:
by simp [irreducibleComponents_eq_singleton]

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty ↥↑U
⊢ hU.isoSpec.hom ⟨genericPoint ↥X, ⋯⟩ = genericPoint ↥(Spec Γ(X, U))

Tactic:
convert!
    genericPoint_eq_of_isOpenImmersion
      (U.toScheme.isoSpec.hom ≫ Spec.map (X.presheaf.map (eqToHom U.isOpenEmbedding_obj_top).op))

Goal state after:
case e'_2.e'_6
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty ↥↑U
e_1✝ : PrimeSpectrum ↑Γ(X, U) = ↥(Spec (X.presheaf.obj (op U)))
⊢ ⟨genericPoint ↥X, ⋯⟩ = genericPoint ↥↑U
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

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

Tactic:
simp

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

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
⊢ (f.restrict f.domain ⋯ ⋯).hom = f.hom

Tactic:
simp

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

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
V : X.Opens
hV : Dense ↑V
hV' : V ≤ U
⊢ ((f.restrict U hU hU').restrict V hV hV').hom = (f.restrict V hV ⋯).hom

Tactic:
simp

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

Goal state before:
pp: case e
X Y : Scheme
f : X.PartialMap Y
x✝ : ↥X
⊢ x✝ ∈ ↑(f.compHom (𝟙 Y)).domain ↔ x✝ ∈ ↑f.domain

Tactic:
simp

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

Goal state before:
pp: case H
X Y : Scheme
f : X.PartialMap Y
⊢ (f.compHom (𝟙 Y)).hom = (X.isoOfEq ⋯).hom ≫ f.hom

Tactic:
simp

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ ((PartialMap.id X).compHom f).hom = (X.isoOfEq ⋯).hom ≫ ((PartialMap.id X).compHom f).hom

Tactic:
simp

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
⊢ IsOver S f ↔ (f.compHom (Y ↘ S)).hom = f.domain.ι ≫ X ↘ S

Tactic:
simp

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
f : X.PartialMap Y
⊢ f.domain ≤ (Hom.toPartialMap (X ↘ S)).domain

Tactic:
simp

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

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
⊢ ∃ (hWl : f.domain ≤ f.domain) (hWr : f.domain ≤ f.domain),
    (f.restrict f.domain ⋯ hWl).hom = (f.restrict f.domain ⋯ hWr).hom

Tactic:
simp

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

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
⊢ ((f.restrict U hU hU').restrict U hU ⋯).hom = (f.restrict U hU hU').hom

Tactic:
simp

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

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

Goal state after:
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)
Uf : X.Opens
dense_domain✝¹ : Dense ↑Uf
f : ↑Uf ⟶ Y
inst✝¹ : IsOver S { domain := Uf, dense_domain := dense_domain✝¹, hom := f }
dense_domain✝ : Dense ↑Uf
g : ↑Uf ⟶ Y
inst✝ : IsOver S { domain := Uf, dense_domain := dense_domain✝, hom := g }
⊢ ({ domain := Uf, dense_domain := dense_domain✝¹, hom := f }.restrict
          { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain ⋯ ⋯).hom =
      ({ domain := Uf, dense_domain := dense_domain✝, hom := g }.restrict
          { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain ⋯ ⋯).hom ↔
    { domain := Uf, dense_domain := dense_domain✝¹, hom := f } =
      { domain := Uf, dense_domain := dense_domain✝, hom := g }

Tactic:
simp

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

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
⊢ X.homOfLE ⋯ ≫ f.hom = (f.domain ⊓ ⊤).ι ≫ g ↔ (X.isoOfEq ⋯).hom ≫ f.hom = (f.domain ⊓ ⊤).ι ≫ g
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
i' : 𝒰.I₀ → I
f : (j : 𝒰.I₀) → i' j ⟶ i
hf : ∀ (j : 𝒰.I₀), IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)
j✝ : I
j : 𝒰.I₀
⊢ i' j ∈ insert i (Finset.image i' Finset.univ)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
i' : 𝒰.I₀ → I
f : (j : 𝒰.I₀) → i' j ⟶ i
hf : ∀ (j : 𝒰.I₀), IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)
j✝ : I
j : 𝒰.I₀
⊢ i ∈ insert i (Finset.image i' Finset.univ)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
i' : 𝒰.I₀ → I
f : (j : 𝒰.I₀) → i' j ⟶ i
hf : ∀ (j : 𝒰.I₀), IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)
g : (j : I) →
  j ∈ insert i (Finset.image i' Finset.univ) →
    (IsCofiltered.inf (insert i (Finset.image i' Finset.univ))
        (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ) ⟶
      j) :=
  fun j ↦
    IsCofiltered.infTo (insert i (Finset.image i' Finset.univ))
      (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ)
j : 𝒰.I₀
⊢ i ∈ insert i (Finset.image i' Finset.univ)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
i' : 𝒰.I₀ → I
f : (j : 𝒰.I₀) → i' j ⟶ i
hf : ∀ (j : 𝒰.I₀), IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)
g : (j : I) →
  j ∈ insert i (Finset.image i' Finset.univ) →
    (IsCofiltered.inf (insert i (Finset.image i' Finset.univ))
        (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ) ⟶
      j) :=
  fun j ↦
    IsCofiltered.infTo (insert i (Finset.image i' Finset.univ))
      (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ)
j : 𝒰.I₀
⊢ i' j ∈ insert i (Finset.image i' Finset.univ)

Tactic:
simp

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
e✝ : f.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
U : X.Opens
hU : Dense ↑U
hUl : U ≤ ((fun x ↦ x.compHom (Y ↘ S)) f).domain
hUr : U ≤ (Hom.toPartialMap (X ↘ S)).domain
e : (((fun x ↦ x.compHom (Y ↘ S)) f).restrict U hU hUl).hom = ((Hom.toPartialMap (X ↘ S)).restrict U hU hUr).hom
⊢ (f.restrict U hU hUl).toRationalMap = f.toRationalMap

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case mY
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
i' : 𝒰.I₀ → I
f : (j : 𝒰.I₀) → i' j ⟶ i
hf : ∀ (j : 𝒰.I₀), IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)
g : (j : I) →
  j ∈ insert i (Finset.image i' Finset.univ) →
    (IsCofiltered.inf (insert i (Finset.image i' Finset.univ))
        (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ) ⟶
      j) :=
  fun j ↦
    IsCofiltered.infTo (insert i (Finset.image i' Finset.univ))
      (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ)
j : 𝒰.I₀
⊢ i ∈ insert i (Finset.image i' Finset.univ)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
i' : 𝒰.I₀ → I
f : (j : 𝒰.I₀) → i' j ⟶ i
hf : ∀ (j : 𝒰.I₀), IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)
g : (j : I) →
  j ∈ insert i (Finset.image i' Finset.univ) →
    (IsCofiltered.inf (insert i (Finset.image i' Finset.univ))
        (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ) ⟶
      j) :=
  fun j ↦
    IsCofiltered.infTo (insert i (Finset.image i' Finset.univ))
      (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ)
j : 𝒰.I₀
⊢ 𝒰.f j ≫ 𝟙 (D.obj i) = 𝟙 (𝒰.X j) ≫ 𝒰.f j

Tactic:
simp

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

Goal state before:
pp: case H
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝ : IrreducibleSpace ↥X
f✝ : X ⤏ Y
f g : X.PartialMap Y
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
e : (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
⊢ (g.restrict W hW hWr).hom = (X.isoOfEq ⋯).hom ≫ (g.restrict W hW hWr).hom

Tactic:
simp

Goal state after: