mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set R
hs✝ : Ideal.span s✝ = ⊤
s : Finset R
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away ↑i) (Localization.Away ↑i ⊗[R] S)
f : R →+* S := algebraMap R S
this : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away ↑r ⊗[R] S)
s₂ : ∀ (r : ↥s), adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
t✝ : Set S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away ↑r ⊗[R] S)) ((algebraMap R S) ↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ * x) ∈ adjoin R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  (↑⟨(fun x ↦ ↑r ^ x) n₂, ⋯⟩ * ↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩) • x ∈
    adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, adjoin R ↑(sf x))

Tactic:
← pow_add

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set R
hs✝ : Ideal.span s✝ = ⊤
s : Finset R
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away ↑i) (Localization.Away ↑i ⊗[R] S)
f : R →+* S := algebraMap R S
this : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away ↑r ⊗[R] S)
s₂ : ∀ (r : ↥s), adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
t✝ : Set S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away ↑r ⊗[R] S)) ((algebraMap R S) ↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ * x) ∈ adjoin R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ↑r ^ (n₂ + n₁) • x ∈
    adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, adjoin R ↑(sf x))
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : ↥s), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  (↑⟨(fun x ↦ ↑r ^ x) n₂, ⋯⟩ * ↑⟨↑r ^ n₁, ⋯⟩) • x ∈
    Submodule.span R
      ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)

Tactic:
← pow_add

Goal state after:
R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : ↥s), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ↑r ^ (n₂ + n₁) • x ∈
    Submodule.span R
      ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: R : CommRingCat
inst✝¹ : JacobsonSpace ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFiniteType (Spec.map φ)
this✝ : (CommRingCat.Hom.hom φ).FiniteType
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
this : IsJacobsonRing ↑R
⊢ JacobsonSpace ↥(Spec S)

Tactic:
exact PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace.mp (isJacobsonRing_of_finiteType (A := R))

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

Goal state before:
pp: Z : Scheme
I : Z.IdealSheafData
⊢ I.map (𝟙 Z) = I

Tactic:
simp [map]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
⊢ IsSeparated f

Tactic:
wlog hY : IsAffine Y

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [h : IsAffineHom f], IsAffine Y → IsSeparated f
hY : ¬IsAffine Y
⊢ IsSeparated f

X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
hY : IsAffine Y
⊢ IsSeparated f
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: ⊢ @IsImmersion = @IsPreimmersion ⊓ topologically fun {x x_1} x_2 x_3 f ↦ IsLocallyClosed (Set.range f)

Tactic:
ext; exact isImmersion_iff _

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
⊢ IsPullback (Hom.toImage f) (Hom.liftCoborder f) (Hom.imageι f) (Hom.coborderRange f).ι

Tactic:
refine (isPullback_of_isClosedImmersion _ _ _ _ (by simp) ?_).flip

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
⊢ (Hom.ker (Hom.imageι f)).comap (Hom.coborderRange f).ι = Hom.ker (Hom.liftCoborder f)
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
C : BasicConstructibleSetData R
⊢ map (RingHom.id R) C = C

Tactic:
simp [map]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : ConstructibleSetData R
⊢ map (RingHom.id R) s = s

Tactic:
simp [map]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ x ∈ comap C '' ↑(basicOpen f) ↔ (map (algebraMap R x.asIdeal.ResidueField)) f ≠ 0

pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ (map (algebraMap R x.asIdeal.ResidueField)) f ≠ 0 ↔ ∃ i, coeff i f ∉ x.asIdeal

Tactic:
· refine (mem_image_comap_basicOpen _ _).trans (not_iff_not.mpr ?_)
    let e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField]
        MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
    rw [← IsNilpotent.map_iff (Algebra.TensorProduct.comm ..).injective,
      ← IsNilpotent.map_iff e.injective, isNilpotent_iff_eq_zero]
    change (e.toAlgHom.toRingHom.comp (Algebra.TensorProduct.comm ..).toRingHom).comp
      (algebraMap _ _) f = 0 ↔ MvPolynomial.map _ f = 0
    congr!
    ext
    · simp [scalarRTensorAlgEquiv, e, Algebra.smul_def]
    · simp [e, scalarRTensorAlgEquiv, coeff, map, X, monomial]

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ (map (algebraMap R x.asIdeal.ResidueField)) f ≠ 0 ↔ ∃ i, coeff i f ∉ x.asIdeal
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))
⊢ CompactSpace ↥X

Tactic:
· constructor
      rw [← Opens.coe_top, ← hS, Opens.iSup_mk]
      apply isCompact_iUnion
      intro i
      apply isCompact_iff_isCompact_univ.mpr
      convert! CompactSpace.isCompact_univ
      have : NoetherianSpace (S i) := by
        apply noetherianSpace_of_isAffineOpen (S i).1 (S i).2
      apply NoetherianSpace.compactSpace (S i)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ IsNoetherianRing ↑(CommRingCat.of R)

Tactic:
assumption

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Integral

Goal state before:
pp: ⊢ @GeometricallyIntegral = geometrically IsIntegral

Tactic:
ext; exact geometricallyIntegral_iff _

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

Goal state before:
pp: ⊢ HasAffineProperty @IsFinite fun X x f x_1 ↦ IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Tactic:
change HasAffineProperty @IsFinite (affineAnd RingHom.Finite)
  rw [HasAffineProperty.affineAnd_iff _ RingHom.finite_respectsIso
    RingHom.finite_localizationPreserves.away RingHom.finite_ofLocalizationSpan]
  simp [isFinite_iff]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

Tactic:
wlog hY : IsAffine Y

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
hY : ¬IsAffine Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f

Tactic:
wlog hY : IsAffine Y

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
hY : ¬IsAffine Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f

X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
inst✝ : X.Over S
f : { f // Scheme.Hom.IsOver f S }
⊢ (fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩) ((fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) f) = f

Tactic:
ext : 2
    · simp [f.2.1]
    · rw [homOfVector_appTop_coord]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

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

Tactic:
rw [map_comp, comp_apply, eq]

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

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
let G : X.Opens ⥤ Y.Opens :=
    { obj U := g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map h := homOfLE (by gcongr; exact h.le) }

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
G : X.Opens ⥤ Y.Opens :=
  { obj := fun U ↦ g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map := fun {X_1 Y_1} h ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
⊢ IsIso (pushoutSection H hUST hUSX hUY)
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↥X
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
⊢ x ∈ ↑(s.inf W ⊓ U)

Tactic:
TopologicalSpace.Opens.coe_inf,

Goal state after:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↥X
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
⊢ x ∈ ↑(s.inf W) ∩ ↑U
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
⊢ ⇑f '' Set.univ = Set.univ ∩ Set.range ⇑f

Tactic:
Set.univ_inter,

Goal state after:
case e'_4
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ ⇑f '' Set.univ = Set.range ⇑f
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

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

Tactic:
by
  ext1 <;> simp [restrict_domain]

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' = f.restrict V hV ⋯

Tactic:
by
  ext1 <;> simp [restrict_domain]

Goal state after:
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
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
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:
← f.fromSpecStalkOfMem_restrict hdense inf_le_left ⟨hxf, hxg⟩,

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.fromSpecStalkOfMem hxg
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.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')
⊢ ∃ j, ∀ {i' : I} (f : i' ⟶ i), Nonempty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map f) 𝒰).X j)

Tactic:
by
      by_contra! H
      choose i' f hf using H
      let g (j) := IsCofiltered.infTo (insert i (Finset.univ.image i'))
        (Finset.univ.image fun j : 𝒰.I₀ ↦ ⟨_, _, by simp, by simp, f j⟩) (X := j)
      have (j : 𝒰.I₀) : IsEmpty ((𝒰.pullback₁ (D.map (g i (by simp)))).X j) := by
        let F : (𝒰.pullback₁ (D.map (g i (by simp)))).X j ⟶
            (𝒰.pullback₁ (D.map (f j))).X j :=
          pullback.map _ _ _ _ (D.map (g _ (by simp))) (𝟙 _) (𝟙 _) (by
            rw [← D.map_comp, IsCofiltered.infTo_commutes]
            · simp [g]
            · simp
            · exact Finset.mem_image_of_mem _ (Finset.mem_univ _)) (by simp)
        exact Function.isEmpty F
      obtain ⟨x, -⟩ :=
        Cover.covers (𝒰.pullback₁ (D.map (g i (by simp)))) (Nonempty.some inferInstance)
      exact (this _).elim x

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

Goal state before:
pp: S X Y : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝ : IsRationalOver sY
h : BirationalOver sX sY
⊢ IsRationalOver sX

Tactic:
obtain ⟨n, hn⟩ := IsRationalOver.exists_birationalOver_affineSpace sY
  exact ⟨n, h.trans hn⟩

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

Goal state before:
pp: X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
| (X₁.isoOfEq ⋯).hom ≫
    (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
      (↑f.domain).homOfLE ⋯ ≫
        (Hom.isoImage (f.hom ⁻¹ᵁ g.domain).ι ((f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
          f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom

Tactic:
rw [← Category.assoc, ← Category.assoc, ← Category.assoc]

Goal state after:
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
| ((((X₁.isoOfEq ⋯).hom ≫ (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv) ≫
        (↑f.domain).homOfLE ⋯) ≫
      (Hom.isoImage (f.hom ⁻¹ᵁ g.domain).ι ((f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain)).inv) ≫
    f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
hf : Function.Surjective ⇑(pullback.diagonal f)
this : UniversallyInjective f
x : ↥X
algInst✝ : Algebra ↑(Y.residueField (f x)) ↑(X.residueField x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).toAlgebra
σ₁ : Field.Emb ↑(Y.residueField (f x)) ↑(X.residueField x)
⊢ ∀ (y : Field.Emb ↑(Y.residueField (f x)) ↑(X.residueField x)), σ₁ = y

Tactic:
σ₂

Goal state after:
X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
hf : Function.Surjective ⇑(pullback.diagonal f)
this : UniversallyInjective f
x : ↥X
algInst✝ : Algebra ↑(Y.residueField (f x)) ↑(X.residueField x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).toAlgebra
σ₁ σ₂ : Field.Emb ↑(Y.residueField (f x)) ↑(X.residueField x)
⊢ σ₁ = σ₂
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁷ : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : IsAffine X
inst✝³ : ∀ (i : I), IsAffine (D.obj i)
inst✝² : IsAffine c.pt
i : I
a : D.obj i ⟶ X
j : I
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsAffine (Spec R)
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
this :
  ∀ {X : Scheme} [IsAffine X] (a : D.obj i ⟶ X) (b : D.obj j ⟶ X),
    c.π.app i ≫ a = c.π.app j ≫ b →
      ∀ (f : X ⟶ Spec R) [LocallyOfFiniteType f],
        t.app i = a ≫ f → t.app j = b ≫ f → (∃ S, X = Spec S) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hX : ¬∃ S, X = Spec S
⊢ c.π.app i ≫ a ≫ X.isoSpec.hom = c.π.app j ≫ b ≫ X.isoSpec.hom

Tactic:
simp [hab]

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{?u.7, ?u.73} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, ?u.73} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : d.cover.I₀
x : ↥(pullback (d.cover.f i) (d.cover.f j))
xi : ↥(d.cover.X i) := (pullback.fst (d.cover.f i) (d.cover.f j)) x
xj : ↥(d.cover.X j) := (pullback.snd (d.cover.f i) (d.cover.f j)) x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 : (trans 𝒰 fi) uk = (d.natTrans.app i) xi
h2 : (trans 𝒰 fj) uk = (d.natTrans.app j) xj
⊢ (d.natTrans.app j) xj = ((functorOfLocallyDirected 𝒰).map fj) uk

Tactic:
apply (𝒰.f j).injective

Goal state after:
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{?u.7, ?u.114} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, ?u.114} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : d.cover.I₀
x : ↥(pullback (d.cover.f i) (d.cover.f j))
xi : ↥(d.cover.X i) := ⋯
xj : ↥(d.cover.X j) := ⋯
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 : (trans 𝒰 fi) uk = (d.natTrans.app i) xi
h2 : (trans 𝒰 fj) uk = (d.natTrans.app j) xj
⊢ (𝒰.f j) ((d.natTrans.app j) xj) = (𝒰.f j) (((functorOfLocallyDirected 𝒰).map fj) uk)