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

Goal state before:
pp: case inr
X✝ Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f],
    (∃ R, X = Spec R) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hX : ¬∃ R, X = Spec R
x : ↥(Spec S)
hx : x ∈ ↑(ker f).support
inst : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ x ∈ closure (Set.range ⇑f)

Tactic:
obtain ⟨_, ⟨i, rfl⟩, hx⟩ := (f.iUnion_support_ker_openCover_map_comp 𝒰).ge hx

Goal state after:
case inr
X✝ Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f],
    (∃ R, X = Spec R) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hX : ¬∃ R, X = Spec R
x : ↥(Spec S)
hx✝ : x ∈ ↑(ker f).support
inst : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
hx : x ∈ (fun i ↦ ↑(ker (𝒰.f i ≫ f)).support) i
⊢ x ∈ closure (Set.range ⇑f)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x : ↥I.subscheme
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).I₀ := Cover.idx (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯) ↑x
⊢ x ∈ Set.range ⇑(I.glueData.ι (Cover.idx (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯) ↑x) ≫ I.subschemeIso.inv)

Tactic:
obtain ⟨⟨y, hy : y ∈ U.1⟩, rfl : y = x.1⟩ :=
      (X.openCoverOfIsOpenCover _ (iSup_affineOpens_eq_top X)).covers x.1

Goal state after:
X : Scheme
I : X.IdealSheafData
x : ↥I.subscheme
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).I₀ := Cover.idx (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯) ↑x
hy : ↑x ∈ ↑U
⊢ x ∈ Set.range ⇑(I.glueData.ι (Cover.idx (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯) ↑x) ≫ I.subschemeIso.inv)
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ (@IsAffineHom ⊓ affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q) = @IsAffineHom ⊓ P'

pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q

Tactic:
HasRingHomProperty.eq_affineLocally (P := P')

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ (@IsAffineHom ⊓ affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q) =
    @IsAffineHom ⊓ affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q

Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: case hprecomp
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z), IsClosedImmersion f → IsClosedImmersion (e.hom ≫ f)

Tactic:
intro X Y Z e f hf

Goal state after:
case hprecomp
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
hf : IsClosedImmersion f
⊢ IsClosedImmersion (e.hom ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: case hpostcomp
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y), IsClosedImmersion f → IsClosedImmersion (f ≫ e.hom)

Tactic:
intro X Y Z e f hf

Goal state after:
case hpostcomp
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
hf : IsClosedImmersion f
⊢ IsClosedImmersion (f ≫ e.hom)
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: case h₂
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], (algebraMap R T).FinitePresentation → (algebraMap S (S ⊗[R] T)).FinitePresentation

Tactic:
simp only [finitePresentation_algebraMap]

Goal state after:
case h₂
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Algebra.FinitePresentation R T → Algebra.FinitePresentation S (S ⊗[R] T)
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒱 i).I₀), IsAffine ((𝒱 i).X j)
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)

Tactic:
let U : (Σ i, (𝒱 i).I₀) → (diagonalCoverDiagonalRange f 𝒰 𝒱).toScheme.Opens := fun i ↦
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ ((diagonalCover f 𝒰 𝒱).f ⟨i.1, i.2, i.2⟩).opensRange

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒱 i).I₀), IsAffine ((𝒱 i).X j)
U : (i : 𝒰.I₀) × (𝒱 i).I₀ → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i ↦ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case openCover
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
x✝ : Ideal.span ↑s = ⊤
hN : ∀ (f : ↥s), IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen ↑f))
⊢ IsNoetherianRing ↑Γ(X, ↑U)

Tactic:
apply isNoetherianRing_of_away s ‹_›

Goal state after:
case openCover
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
x✝ : Ideal.span ↑s = ⊤
hN : ∀ (f : ↥s), IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen ↑f))
⊢ ∀ (s_1 : ↥s), IsNoetherianRing (Localization.Away ↑s_1)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ IsLocallyNoetherian X ↔ ∀ (i : 𝒰.I₀), IsLocallyNoetherian (𝒰.X i)

Tactic:
refine ⟨fun _ ↦ inferInstance, ?_⟩

Goal state after:
X : Scheme
𝒰 : X.OpenCover
⊢ (∀ (i : 𝒰.I₀), IsLocallyNoetherian (𝒰.X i)) → IsLocallyNoetherian X
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: R : CommRingCat
⊢ IsArtinianScheme (Spec R) ↔ IsArtinianRing ↑R

Tactic:
by
  simp [isArtinianScheme_iff, (inferInstance : CompactSpace (Spec R))]

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

Goal state before:
pp: case inr
X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyIrreducible f
hf : IsOpenMap ⇑f
s : Set ↥S
hs : IsIrreducible s
this : ∀ {s : Set ↥S}, IsIrreducible s → (∃ x, s = {x}) → IsIrreducible (⇑f ⁻¹' s)
H : ¬∃ x, s = {x}
⊢ s.Nonempty

Tactic:
exact hs.nonempty

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : GeometricallyIrreducible f
inst✝² : GeometricallyIrreducible g
inst✝¹ : UniversallyOpen f
inst✝ : UniversallyOpen g
⊢ GeometricallyIrreducible (f ≫ g)

Tactic:
refine ⟨geometrically_iff_of_isClosedUnderIsomorphisms.mpr fun K _ x ↦ ?_⟩
  rw [← (pullbackRightPullbackFstIso g x f).hom.homeomorph.irreducibleSpace_iff]
  infer_instance

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

Goal state before:
pp: X✝ Y Z S U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsIntegralHom f
inst✝ : IsIntegralHom g
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    f.IsIntegral → g.IsIntegral → (f.prod g).IsIntegral

Tactic:
intros R S T _ _ _ f g _ _

Goal state after:
X✝ Y Z S✝ U V X : Scheme
f✝ : U ⟶ X
g✝ : V ⟶ X
inst✝⁴ : IsIntegralHom f✝
inst✝³ : IsIntegralHom g✝
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : R →+* T
a✝¹ : f.IsIntegral
a✝ : g.IsIntegral
⊢ (f.prod g).IsIntegral
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsFinite f
inst✝ : IsFinite g
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    f.Finite → g.Finite → (f.prod g).Finite

Tactic:
intros R S T _ _ _ f g _ _

Goal state after:
X✝ Y Z : Scheme
f✝¹ : X✝ ⟶ Y
U V X : Scheme
f✝ : U ⟶ X
g✝ : V ⟶ X
inst✝⁴ : IsFinite f✝
inst✝³ : IsFinite g✝
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : R →+* T
a✝¹ : f.Finite
a✝ : g.Finite
⊢ (f.prod g).Finite
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
inst✝ : Finite n
⊢ LocallyOfFinitePresentation (terminal.from (Spec ℤ[n]))

Tactic:
by
  have := isIso_of_isTerminal specULiftZIsTerminal.{u} terminalIsTerminal (terminal.from _)
  rw [← terminal.comp_from (Spec.map (CommRingCat.ofHom C)),
    MorphismProperty.cancel_right_of_respectsIso (P := @LocallyOfFinitePresentation),
    HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation), RingHom.FinitePresentation]
  convert! (inferInstance : Algebra.FinitePresentation (ULift ℤ) ℤ[n])
  exact Algebra.algebra_ext _ _ fun _ ↦ rfl

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

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ Function.Injective (F.descColimitType c) ↔
    ∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'

Tactic:
rw [descColimitType_injective_iff_of_isFiltered]
  constructor
  · intro h j x x' eq
    obtain ⟨k, f, f', eq⟩ := h _ _ _ _ eq
    refine ⟨coeq f f', f ≫ coeqHom f f', ?_⟩
    rw [map_comp, comp_apply, eq]
    simp only [← comp_apply, ← map_comp]
    rw [coeq_condition]
  · intro h j j' x x' eq
    obtain ⟨k, g, eq⟩ := h (max j j') (F.map (leftToMax _ _) x)
      (F.map (rightToMax _ _) x') (by simpa only [c.ι_naturality_apply])
    exact ⟨k, leftToMax _ _ ≫ g, rightToMax _ _ ≫ g, by simp [eq]⟩

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

Goal state before:
pp: case hUU'
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 := ⋯
h✝ : iSup D.obj = UX
c₀ : Cocone D := ⋯
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat := ⋯
X✝ Y✝ : X.Opens
h : X✝ ⟶ Y✝
⊢ X✝ ≤ Y✝

Tactic:
exact h.le

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 ⊆ ⊤
h : (U ∩ {z | (f ⁻¹' {z} ∩ support ⇑c).Nonempty}).Finite
y : Y
hy : y ∈ support fun z ↦ ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {z}), c x * w x
x : X
hx : f x = y
h' : c x * w x ≠ 0
⊢ y ∈ {z | (f ⁻¹' {z} ∩ support ⇑c).Nonempty}

Tactic:
use x

Goal state after:
case h
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 ⊆ ⊤
h : (U ∩ {z | (f ⁻¹' {z} ∩ support ⇑c).Nonempty}).Finite
y : Y
hy : y ∈ support fun z ↦ ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {z}), c x * w x
x : X
hx : f x = y
h' : c x * w x ≠ 0
⊢ x ∈ f ⁻¹' {y} ∩ support ⇑c
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
inst✝ : IsOpenImmersion f
H✝ : Y.IsGermInjectiveAt (f x)
U : Y.Opens
hxU : f x ∈ U
hU : IsAffineOpen U
hU' : U ≤ Scheme.Hom.opensRange f
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ U (f x) hxU))
V : ↑X.affineOpens
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨U, hU⟩, hU'⟩
⊢ X.IsGermInjectiveAt x

Tactic:
obtain rfl : f ''ᵁ V = U := Subtype.ext_iff.mp (Subtype.ext_iff.mp hV)

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
inst✝ : IsOpenImmersion f
H✝ : Y.IsGermInjectiveAt (f x)
V : ↑X.affineOpens
hxU : f x ∈ f ''ᵁ ↑V
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ (f ''ᵁ ↑V) (f x) hxU))
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
⊢ X.IsGermInjectiveAt x
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:
← SetLike.mem_coe,

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.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
inst✝¹ : IsOver S f
inst✝ : IsOver S g
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
x✝ : f.equiv g
V : X.Opens
hV : Dense ↑V
hVl : V ≤ f.domain
hVr : V ≤ g.domain
e : (f.restrict V hV hVl).hom = (g.restrict V hV hVr).hom
this : IsDominant (X.homOfLE ⋯)
⊢ (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom

Tactic:
apply ext_of_isDominant_of_isSeparated' S (X.homOfLE (inf_le_left : W ⊓ V ≤ W))

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
inst✝¹ : IsOver S f
inst✝ : IsOver S g
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
x✝ : f.equiv g
V : X.Opens
hV : Dense ↑V
hVl : V ≤ f.domain
hVr : V ≤ g.domain
e : (f.restrict V hV hVl).hom = (g.restrict V hV hVr).hom
this : IsDominant (X.homOfLE ⋯)
⊢ X.homOfLE ⋯ ≫ (f.restrict W hW hWl).hom = X.homOfLE ⋯ ≫ (g.restrict W hW hWr).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')
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)
this : ∀ (j : 𝒰.I₀), IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (g i ⋯)) 𝒰).X j)
x :
  ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (g i ⋯)) 𝒰).X
      (Cover.idx (Precoverage.ZeroHypercover.pullback₁ (D.map (g i ⋯)) 𝒰) ⋯.some))
⊢ False

Tactic:
exact (this _).elim x

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

Goal state before:
pp: X Y : Scheme
f : X ⤏ Y
x : ↥X
⊢ (∃ u ∈ {x | ∃ g, ∃ (_ : g.toRationalMap = f), g.domain = x}, x ∈ u) ↔ ∃ g, x ∈ g.domain ∧ g.toRationalMap = f

Tactic:
by simp [@and_comm (x ∈ _)]

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
x : ↥↑f.domain
⊢ ∃ i,
    x ∈
      Set.range
        ⇑({ I₀ := ↑{x | ∃ g, ∃ (_ : g.toRationalMap = f), g.domain = x}, X := fun U ↦ ↑↑U, f := fun U ↦ X.homOfLE ⋯ }.f
            i)

Tactic:
use ⟨_, (TopologicalSpace.Opens.mem_sSup.mp x.2).choose_spec.1⟩

Goal state after:
case h
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
x : ↥↑f.domain
⊢ x ∈
    Set.range
      ⇑({ I₀ := ↑{x | ∃ g, ∃ (_ : g.toRationalMap = f), g.domain = x}, X := fun U ↦ ↑↑U, f := fun U ↦ X.homOfLE ⋯ }.f
          ⟨⋯.choose, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: case refine_1
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
⊢ (s : PullbackCone (𝒰.f i) d.toBase) → s.pt ⟶ d.functor.obj i

Tactic:
intro s
    apply IsOpenImmersion.lift (colimit.ι d.functor i) s.snd
    rw [← preimage_toBase_eq_range_ι]
    rintro x ⟨x, rfl⟩
    use s.fst x
    rw [← Scheme.Hom.comp_apply, ← s.condition]
    simp

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

Goal state before:
pp: case neg
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝¹ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k✝ : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : c.val i = 1
k : Fin n
h✝ : ¬k = j
⊢ coeff(c.val k) ⊆ ↑(coeffSubmodule R₀ c)

Tactic:
· exact (Set.subset_iUnion (fun i ↦ coeff(c.val i)) k).trans
                  (Set.subset_union_right.trans Submodule.subset_span)

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C✝ : Type u_1
inst✝³ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝² : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst✝¹ : EffectiveEpiFamily Z fun i ↦ g i ≫ f i
inst✝ : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
T : C
i₁ i₂ : I
g₁ : T ⟶ Z i₁
g₂ : T ⟶ Z i₂
eq : g₁ ≫ g i₁ ≫ f i₁ = g₂ ≫ g i₂ ≫ f i₂
⊢ (g₁ ≫ g i₁) ≫ f i₁ = (g₂ ≫ g i₂) ≫ f i₂

Tactic:
simpa [assoc] using eq

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
e : C ≌ D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
W✝ : D
ε : (a : α) → e.functor.obj (X a) ⟶ W✝
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
m : e.functor.obj B ⟶ W✝
hm : ∀ (a : α), e.functor.map (π a) ≫ m = ε a
this : e.unit.app B ≫ e.inverse.map m = EffectiveEpiFamily.desc X π (fun a ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯
⊢ m = e.functor.map (EffectiveEpiFamily.desc X π (fun a ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯) ≫ e.counit.app W✝

Tactic:
simp [← this]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y S : Scheme
inst✝⁴ : IsAffine X
inst✝³ : IsAffine Y
π : X ⟶ Y
inst✝² : Surjective π
inst✝¹ : Flat π
f : X ⟶ S
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
inst✝ : IsAffine S
⊢ EffectiveEpi (AffineScheme.ofHom π)

Tactic:
apply AffineScheme.equivCommRingCat.functor.effectiveEpi_of_map

Goal state after:
X Y S : Scheme
inst✝⁴ : IsAffine X
inst✝³ : IsAffine Y
π : X ⟶ Y
inst✝² : Surjective π
inst✝¹ : Flat π
f : X ⟶ S
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
inst✝ : IsAffine S
⊢ EffectiveEpi (AffineScheme.equivCommRingCat.functor.map (AffineScheme.ofHom π))
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun V ↦ (↑V).1) ⋯
i : 𝒰.I₀
this : IsAffine (𝒰.X i)
⊢ Set.range (⇑(TopCat.Hom.hom f.base) ∘ ⇑(TopCat.Hom.hom (fst π (𝒰.f i)).base)) ⊆ Set.range ⇑(Opens.ι ↑(↑i).2)

Tactic:
rw [← hfac, ← TopCat.coe_comp, ← Scheme.Hom.comp_base_assoc, pullback.condition]

Goal state after:
X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun V ↦ (↑V).1) ⋯
i : 𝒰.I₀
this : IsAffine (𝒰.X i)
⊢ Set.range ⇑(ConcreteCategory.hom ((snd π (𝒰.f i) ≫ 𝒰.f i).base ≫ b)) ⊆ Set.range ⇑(Opens.ι ↑(↑i).2)
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun V ↦ (↑V).1) ⋯
i : 𝒰.I₀
this : IsAffine (𝒰.X i)
f' : pullback π (𝒰.f i) ⟶ ↑↑(↑i).2 := IsOpenImmersion.lift (Opens.ι ↑(↑i).2) (fst π (𝒰.f i) ≫ f) ⋯
h1 :
  fst (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i) =
    map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯ ≫ fst π π
h2 :
  snd (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i) =
    map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯ ≫ snd π π
⊢ fst (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ f' = snd (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ f'

Tactic:
simp only [← cancel_mono (Scheme.Opens.ι i.1.2.1),
      Category.assoc, IsOpenImmersion.lift_fac, f', reassoc_of% h1, reassoc_of% h2, hf]

Goal state after: