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
⊢ e ((CommRingCat.Hom.hom (φRX ≫ X.presheaf.map ⋯.hom.op)) a) =
    ((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯) (φRA.hom' a)

Tactic:
ext

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 := ⋯
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 := ⋯
a : ↑R
⊢ ↑(e ((CommRingCat.Hom.hom (φRX ≫ X.presheaf.map ⋯.hom.op)) a)) =
    ↑(((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯) (φRA.hom' a))
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: 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,
    ∃ (hxV : x ∈ V),
      ∃ φ', ∃ (i : V ≤ U), IsAffineOpen V ∧ φ = φ' ≫ X.presheaf.germ V x hxV ∧ φRX ≫ X.presheaf.map i.hom.op = φRA ≫ φ'

Tactic:
by
  obtain ⟨V, hxV, iVU, hV⟩ := exists_lift_of_germInjective_aux hxU φ φRA φRX hφRA e
  obtain ⟨V', hxV', hV', iV'V, H⟩ := X.exists_le_and_germ_injective x V hxV
  let f := X.presheaf.germ V' x hxV'
  have hf' : RingHom.range (X.presheaf.germ V x hxV).hom ≤ RingHom.range f.hom := by
    rw [← X.presheaf.germ_res iV'V.hom _ hxV']
    exact Set.range_comp_subset_range (X.presheaf.map iV'V.hom.op) f
  let e := RingEquiv.ofLeftInverse H.hasLeftInverse.choose_spec
  refine ⟨V', hxV', CommRingCat.ofHom (e.symm.toRingHom.comp
    (φ.hom.codRestrict _ (fun x ↦ hf' (hV ⟨x, rfl⟩)))), iV'V.trans iVU, hV', ?_, ?_⟩
  · ext a
    change φ a = (e (e.symm _)).1
    simp only [RingEquiv.apply_symm_apply]
    rfl
  · ext a
    apply e.injective
    change e _ = e (e.symm _)
    rw [RingEquiv.apply_symm_apply]
    ext
    change X.presheaf.germ _ _ _ (X.presheaf.map _ _) = (φRA ≫ φ) a
    rw [TopCat.Presheaf.germ_res_apply, ‹φRA ≫ φ = _›]
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

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

Tactic:
ext

Goal state after:
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
x✝ : ↑R
⊢ x✝ ∈ nonZeroDivisors ↑R ↔ x✝ ∈ ⊥.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:
ext

Goal state after:
case e'_3
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↥↑U
x✝ : ↑Γ(X, U)
⊢ x✝ ∈ nonZeroDivisors ↑Γ(X, U) ↔ x✝ ∈ ⊥.asIdeal.primeCompl
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

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

Tactic:
constructor

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

case mpr
X Y : Scheme
f g : X.PartialMap Y
⊢ (∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom) → f = g
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
⊢ f.compHom (𝟙 Y) = f

Tactic:
ext

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

case H
X Y : Scheme
f : X.PartialMap Y
⊢ (f.compHom (𝟙 Y)).hom = (X.isoOfEq ⋯).hom ≫ f.hom
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, ⋯⟩
this : ∃ U, ⟨x, ⋯⟩ ∈ U ∧ U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
⊢ f.equiv g

Tactic:
obtain ⟨U, hxU, e⟩ := this

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
⊢ f.equiv g
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
⊢ IsOver S f ↔ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)

Tactic:
constructor

Goal state after:
case mp
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
⊢ IsOver S f → f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)

case mpr
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S) → IsOver S f
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
⊢ PartialMap.IsOver S (f.restrict U hU hUl)

Tactic:
simpa using! e

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

Goal state before:
pp: X Y : Scheme
f g : X.PartialIso Y
⊢ f = g ↔ ∃ (e : f.source = g.source) (e' : g.target = f.target), f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e'

Tactic:
constructor

Goal state after:
case mp
X Y : Scheme
f g : X.PartialIso Y
⊢ f = g → ∃ (e : f.source = g.source) (e' : g.target = f.target), f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e'

case mpr
X Y : Scheme
f g : X.PartialIso Y
⊢ (∃ (e : f.source = g.source) (e' : g.target = f.target), f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e') → f = g
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
g : Y.PartialMap Z
⊢ (f.restrict U hU hU').comp g = (f.comp g).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain ⊓ U) ⋯ ⋯

Tactic:
ext

Goal state after:
case e
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
g : Y.PartialMap Z
x✝ : ↥X
⊢ x✝ ∈ ↑((f.restrict U hU hU').comp g).domain ↔
    x✝ ∈ ↑((f.comp g).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain ⊓ U) ⋯ ⋯).domain

case H
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
g : Y.PartialMap Z
⊢ ((f.restrict U hU hU').comp g).hom =
    (X.isoOfEq ⋯).hom ≫ ((f.comp g).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain ⊓ U) ⋯ ⋯).hom
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y.PartialMap Z
V : Y.Opens
hV : Dense ↑V
hV' : V ≤ g.domain
⊢ f.comp (g.restrict V hV hV') = (f.comp g).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ V) ⋯ ⋯

Tactic:
ext

Goal state after:
case e
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y.PartialMap Z
V : Y.Opens
hV : Dense ↑V
hV' : V ≤ g.domain
x✝ : ↥X
⊢ x✝ ∈ ↑(f.comp (g.restrict V hV hV')).domain ↔ x✝ ∈ ↑((f.comp g).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ V) ⋯ ⋯).domain

case H
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y.PartialMap Z
V : Y.Opens
hV : Dense ↑V
hV' : V ≤ g.domain
⊢ (f.comp (g.restrict V hV hV')).hom = (X.isoOfEq ⋯).hom ≫ ((f.comp g).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ V) ⋯ ⋯).hom
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
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
ext

Goal state after:
case e
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✝ : ↥X₁
⊢ x✝ ∈ ↑((f.comp g).comp h).domain ↔ x✝ ∈ ↑(f.comp (g.comp h)).domain

case H
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
⊢ ((f.comp g).comp h).hom = (X₁.isoOfEq ⋯).hom ≫ (f.comp (g.comp h)).hom
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case H
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y ⟶ Z
⊢ (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ (Hom.toPartialMap g).domain)).inv ≫
      f.hom ∣_ (Hom.toPartialMap g).domain ≫ (Hom.toPartialMap g).hom =
    (X.isoOfEq ⋯).hom ≫ (f.compHom g).hom

Tactic:
Hom.toPartialMap_domain,

Goal state after:
case H
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y ⟶ Z
⊢ (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ ⊤)).inv ≫ f.hom ∣_ ⊤ ≫ (Hom.toPartialMap g).hom =
    (X.isoOfEq ⋯).hom ≫ (f.compHom g).hom
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case e
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ (PartialMap.id X).domain.ι ''ᵁ (PartialMap.id X).hom ⁻¹ᵁ f.domain = f.domain

Tactic:
Hom.toPartialMap_domain,

Goal state after:
case e
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ ⊤.ι ''ᵁ (PartialMap.id X).hom ⁻¹ᵁ f.domain = f.domain
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case H
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ (Hom.isoImage (PartialMap.id X).domain.ι ((X.topIso.hom ≫ 𝟙 X) ⁻¹ᵁ f.domain)).inv ≫
      (X.topIso.hom ≫ 𝟙 X) ∣_ f.domain ≫ f.hom =
    (X.isoOfEq ⋯).hom ≫ f.hom

Tactic:
Hom.toPartialMap_domain,

Goal state after:
case H
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ (Hom.isoImage ⊤.ι ((X.topIso.hom ≫ 𝟙 X) ⁻¹ᵁ f.domain)).inv ≫ (X.topIso.hom ≫ 𝟙 X) ∣_ f.domain ≫ f.hom =
    (X.isoOfEq ⋯).hom ≫ f.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✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
U : c.pt.Opens
hU : IsCompact ↑U
⊢ ∃ i V, IsCompact ↑V ∧ c.π.app i ⁻¹ᵁ V = U

Tactic:
classical
  obtain ⟨s, hs, hsf, rfl⟩ := (isBasis_preimage_isAffineOpen D c hc).exists_finite_of_isCompact hU
  have : Finite s := hsf
  choose i V hV hVi using fun x : s ↦ hs x.2
  obtain ⟨j, fj⟩ := IsCofiltered.inf_objs_exists (hsf.toFinset.attach.image
    fun x ↦ i ⟨x.1, (by simpa only [Set.Finite.mem_toFinset] using x.2)⟩:)
  replace fj : ∀ b : s, j ⟶ i b := fun b ↦ (@fj (i b) (by simpa using ⟨b.1, b.2, rfl⟩)).some
  refine ⟨j, ⨆ (k : s), D.map (fj _) ⁻¹ᵁ V k, ?_, ?_⟩
  · simp only [TopologicalSpace.Opens.iSup_mk, TopologicalSpace.Opens.carrier_eq_coe,
      TopologicalSpace.Opens.map_coe, TopologicalSpace.Opens.coe_mk]
    exact isCompact_iUnion fun i ↦ ((hV i).preimage _).isCompact
  · simp [-TopologicalSpace.Opens.iSup_mk, Scheme.Hom.preimage_iSup,
      ← Scheme.Hom.comp_preimage, c.w, hVi, sSup_eq_iSup']

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

Goal state before:
pp: R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
⊢ coeff(f) = f.coeff '' Set.Iio (f.natDegree + 2)

pp: R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
⊢ f.coeff '' Set.Iio (f.natDegree + 2) = ⋃ i, ⋃ (_ : i < f.natDegree + 2), {f.coeff i}

Tactic:
· refine ((Set.image_subset_range _ _).antisymm ?_).symm
          rintro _ ⟨i, rfl⟩
          by_cases! hi : i ≤ f.natDegree
          · exact ⟨i, hi.trans_lt (by simp), rfl⟩
          · exact ⟨f.natDegree + 1, by simp, by simp [f.coeff_eq_zero_of_natDegree_lt hi]⟩

Goal state after:
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
⊢ f.coeff '' Set.Iio (f.natDegree + 2) = ⋃ i, ⋃ (_ : i < f.natDegree + 2), {f.coeff i}
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
⊢ f.coeff '' Set.Iio (f.natDegree + 2) = ⋃ i, ⋃ (_ : i < f.natDegree + 2), {f.coeff i}

Tactic:
ext

Goal state after:
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
x✝ : R
⊢ x✝ ∈ f.coeff '' Set.Iio (f.natDegree + 2) ↔ x✝ ∈ ⋃ i, ⋃ (_ : i < f.natDegree + 2), {f.coeff i}
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝³ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ).Nonempty
⊢ False

Tactic:
let Z (i' : I) (hii' : i' ⟶ A.i) :=
    (D.map hii' ≫ pullback.lift A.a A.b (A.ha.symm.trans A.hb)) ⁻¹' Wᶜ

Goal state after:
I : Type u
inst✝³ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ).Nonempty
Z : (i' : I) → (i' ⟶ A.i) → Set ↥(D.obj i') := fun i' hii' ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W)ᶜ
⊢ False
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝³ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ).Nonempty
Z : (i' : I) → (i' ⟶ A.i) → Set ↥(D.obj i') := fun i' hii' ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W)ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), (A.c.π.app i) s ∈ Z i hij
⊢ A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f = A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯

Tactic:
ext

Goal state after:
case h₀
I : Type u
inst✝³ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := ⋯
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ).Nonempty
Z : (i' : I) → (i' ⟶ A.i) → Set ↥(D.obj i') := ⋯
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), (A.c.π.app i) s ∈ Z i hij
⊢ (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) ≫ pullback.fst f f =
    (A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯) ≫ pullback.fst f f

case h₁
I : Type u
inst✝³ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := ⋯
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ).Nonempty
Z : (i' : I) → (i' ⟶ A.i) → Set ↥(D.obj i') := ⋯
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), (A.c.π.app i) s ∈ Z i hij
⊢ (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) ≫ pullback.snd f f =
    (A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯) ≫ pullback.snd f f
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: P : MorphismProperty Scheme
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝² : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝¹ : Category.{v_2, u_2} 𝒰.I₀
inst✝ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
i : 𝒰.I₀
j✝ : J
⊢ ((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j✝ ≫ d.transitionMap (𝟙 i) =
    ((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j✝ ≫
      (MorphismProperty.Over.mapId ⊤ (𝒰.X i) (Cover.trans 𝒰 (𝟙 i)) ⋯).hom.app (d.cocone i).pt

Tactic:
ext

Goal state after:
P : MorphismProperty Scheme
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝² : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝¹ : Category.{v_2, u_2} 𝒰.I₀
inst✝ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
i : 𝒰.I₀
j✝ : J
⊢ (((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j✝ ≫ d.transitionMap (𝟙 i)).left =
    (((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j✝ ≫
        (MorphismProperty.Over.mapId ⊤ (𝒰.X i) (Cover.trans 𝒰 (𝟙 i)) ⋯).hom.app (d.cocone i).pt).left
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: P : MorphismProperty Scheme
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝² : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝¹ : Category.{v_2, u_2} 𝒰.I₀
inst✝ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
i j k : 𝒰.I₀
hij : i ⟶ j
hjk : j ⟶ k
j✝ : J
⊢ ((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j✝ ≫ d.transitionMap (hij ≫ hjk) =
    ((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j✝ ≫
      (MorphismProperty.Over.mapComp ⊤ ⋯ ⋯ (Cover.trans 𝒰 (hij ≫ hjk)) ⋯).hom.app (d.cocone i).pt ≫
        (MorphismProperty.Over.map ⊤ ⋯).map (d.transitionMap hij) ≫ d.transitionMap hjk

Tactic:
ext

Goal state after:
P : MorphismProperty Scheme
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝² : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝¹ : Category.{v_2, u_2} 𝒰.I₀
inst✝ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
i j k : 𝒰.I₀
hij : i ⟶ j
hjk : j ⟶ k
j✝ : J
⊢ (((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j✝ ≫ d.transitionMap (hij ≫ hjk)).left =
    (((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app j✝ ≫
        (MorphismProperty.Over.mapComp ⊤ ⋯ ⋯ (Cover.trans 𝒰 (hij ≫ hjk)) ⋯).hom.app (d.cocone i).pt ≫
          (MorphismProperty.Over.map ⊤ ⋯).map (d.transitionMap hij) ≫ d.transitionMap hjk).left
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: P : MorphismProperty Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝² : Category.{v_2, u_2} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt :=
  (d.isColimit i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)) (d.isColimit j))
    (D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm)
a : J
⊢ (MorphismProperty.Over.map ⊤ ⋯).map
        ((D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
                (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
                    (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm).hom.app
          a) ≫
      (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans 𝒰 hij) ⋯ trivial).counit.app
          ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j)).obj a) ≫
        (d.cocone j).ι.app a =
    (d.trans hij).app a ≫ (d.cocone j).ι.app a

Tactic:
ext

Goal state after:
P : MorphismProperty Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝² : Category.{v_2, u_2} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt := ⋯
a : J
⊢ ((MorphismProperty.Over.map ⊤ ⋯).map
          ((D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
                  (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
                      (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm).hom.app
            a) ≫
        (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans 𝒰 hij) ⋯ trivial).counit.app
            ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j)).obj a) ≫
          (d.cocone j).ι.app a).left =
    ((d.trans hij).app a ≫ (d.cocone j).ι.app a).left