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

Goal state before:
pp: X : Scheme
inst✝ : X.IsQuasiAffine
⊢ Opens.IsBasis {x | ∃ r, ∃ (_ : IsAffineOpen (X.basicOpen r)), X.basicOpen r = x}

Tactic:
refine Opens.isBasis_iff_nbhd.mpr fun {U x} hxU ↦ ?_
  obtain ⟨_, ⟨_, ⟨r, rfl⟩, rfl⟩, hxr, hrU⟩ := (PrimeSpectrum.isBasis_basic_opens
    (R := Γ(X, ⊤))).exists_subset_of_mem_open (Set.mem_image_of_mem _ hxU) (X.toSpecΓ ''ᵁ U).2
  simp_rw [← toSpecΓ_preimage_basicOpen]
  refine ⟨_, ⟨r, ?_, rfl⟩, hxr, (Set.preimage_mono hrU).trans_eq
    (Set.preimage_image_eq _ X.toSpecΓ.isEmbedding.injective)⟩
  rw [← Hom.isAffineOpen_iff_of_isOpenImmersion X.toSpecΓ]
  convert! IsAffineOpen.Spec_basicOpen r
  exact SetLike.coe_injective (Set.image_preimage_eq_of_subset
    (hrU.trans (Set.image_subset_range _ _)))

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this✝ : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
⊢ IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r).ι ≫ X.toSpecΓ)

Tactic:
convert! this <;> rw [toSpecΓ_preimage_basicOpen]

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this : CompactSpace ↥X
x : ↥X
r : ↑Γ(Y, ⊤)
hr : IsAffineOpen (Y.basicOpen r)
hxr : f x ∈ ↑(Y.basicOpen r)
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ∧
    x ∈ X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)

Tactic:
rw [← preimage_basicOpen_top]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this : CompactSpace ↥X
x : ↥X
r : ↑Γ(Y, ⊤)
hr : IsAffineOpen (Y.basicOpen r)
hxr : f x ∈ ↑(Y.basicOpen r)
⊢ IsAffineOpen (f ⁻¹ᵁ Y.basicOpen r) ∧ x ∈ f ⁻¹ᵁ Y.basicOpen r
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : Surjective f
x : ↑↑(LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj X)).toPresheafedSpace
algInst✝ : Algebra ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
⊢ Function.Injective
    ⇑(ConcreteCategory.hom
        (PresheafedSpace.Hom.stalkMap
          (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f)).hom x))

Tactic:
have : Module.FaithfullyFlat (Y.presheaf.stalk (f x)) (X.presheaf.stalk x) :=
    @Module.FaithfullyFlat.of_flat_of_isLocalHom _ _ _ _ _ _ _
      (Flat.stalkMap f x) (f.toLRSHom.prop x)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : Surjective f
x : ↑↑(LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj X)).toPresheafedSpace
algInst✝ : Algebra ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this : Module.FaithfullyFlat ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x)
⊢ Function.Injective
    ⇑(ConcreteCategory.hom
        (PresheafedSpace.Hom.stalkMap
          (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f)).hom x))
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : IsAffineHom f
inst✝¹ : X.IsQuasiAffine
inst✝ : Y.IsQuasiAffine
⊢ Spec.map (Hom.appTop f) ⁻¹ᵁ Hom.opensRange Y.toSpecΓ = Hom.opensRange X.toSpecΓ

Tactic:
by
  simpa using (IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback
    (isPullback_toSpecΓ_toSpecΓ f) ⊤).symm

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case pos
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support.Finite
this : (Function.support fun x ↦ restrict (single x (F x)) ⋯) ⊆ ↑h.toFinset
z : X
hz : z ∉ U
⊢ (∑ i ∈ h.toFinset, restrict (single i (F i)) ⋯) z = F z

pp: case neg
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support.Finite
this : (Function.support fun x ↦ restrict (single x (F x)) ⋯) ⊆ ↑h.toFinset
z : X
hz : ¬z ∉ U
⊢ (∑ i ∈ h.toFinset, restrict (single i (F i)) ⋯) z = F z

Tactic:
· aesop

Goal state after:
case neg
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support.Finite
this : (Function.support fun x ↦ restrict (single x (F x)) ⋯) ⊆ ↑h.toFinset
z : X
hz : ¬z ∉ U
⊢ (∑ i ∈ h.toFinset, restrict (single i (F i)) ⋯) z = F z
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case pos
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support.Finite
this : (Function.support fun x ↦ restrict (single x (F x)) ⋯) ⊆ ↑h.toFinset
z : X
hz✝ : ¬z ∉ U
hz : z ∈ F.support
⊢ (if z ∈ U then if z ∈ h.toFinset then F z else 0 else 0) = F z

pp: case neg
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support.Finite
this : (Function.support fun x ↦ restrict (single x (F x)) ⋯) ⊆ ↑h.toFinset
z : X
hz✝ : ¬z ∉ U
hz : z ∉ F.support
⊢ (if z ∈ U then if z ∈ h.toFinset then F z else 0 else 0) = F z

Tactic:
· aesop

Goal state after:
case neg
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support.Finite
this : (Function.support fun x ↦ restrict (single x (F x)) ⋯) ⊆ ↑h.toFinset
z : X
hz✝ : ¬z ∉ U
hz : z ∉ F.support
⊢ (if z ∈ U then if z ∈ h.toFinset then F z else 0 else 0) = F z
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case neg
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support.Finite
this : (Function.support fun x ↦ restrict (single x (F x)) ⋯) ⊆ ↑h.toFinset
z : X
hz✝ : ¬z ∉ U
hz : z ∉ F.support
⊢ (if z ∈ U then if z ∈ h.toFinset then F z else 0 else 0) = F z

Tactic:
· aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝¹ : IrreducibleSpace ↥X
U : X.Opens
x : ↥U
inst✝ : Nonempty ↥↑U
⊢ algebraMap ↑Γ(X, U) ↑X.functionField =
    (algebraMap ↑(X.presheaf.stalk ↑x) ↑X.functionField).comp (algebraMap ↑Γ(X, U) ↑(X.presheaf.stalk ↑x))

Tactic:
RingHom.algebraMap_toAlgebra

Goal state after:
X : Scheme
inst✝¹ : IrreducibleSpace ↥X
U : X.Opens
x : ↥U
inst✝ : Nonempty ↥↑U
⊢ CommRingCat.Hom.hom (X.germToFunctionField U) =
    (CommRingCat.Hom.hom (X.presheaf.stalkSpecializes ⋯)).comp (CommRingCat.Hom.hom (X.presheaf.germ U ↑x ⋯))
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
f : ↑X.functionField
hf : f ≠ 0
⊢ ∃ U ∈ X.affineOpens, ∃ f', ∃ (x : Nonempty ↥↑U), (ConcreteCategory.hom (X.germToFunctionField U)) f' = f ∧ IsUnit f'

Tactic:
by
  obtain ⟨U, hU, g, hg⟩ := X.presheaf.exists_germ_eq f
  obtain ⟨_, ⟨A, hA, rfl⟩, hxA, hAU⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open hU U.isOpen
  have : Nonempty A := ⟨_, hxA⟩
  let gA : Γ(X, A) := X.presheaf.map (homOfLE hAU).op g
  have h_germ_gA : X.presheaf.germ A (genericPoint X) hxA gA = f := by
    simp only [← hg, ← X.presheaf.germ_res_apply (homOfLE hAU) (genericPoint X) hxA g, gA]
    rfl
  have hxV : genericPoint X ∈ X.basicOpen gA := by
    rwa [Scheme.mem_basicOpen X gA (genericPoint X) hxA, h_germ_gA, isUnit_iff_ne_zero]
  have : Nonempty (X.basicOpen gA) := ⟨⟨_, hxV⟩⟩
  refine ⟨X.basicOpen gA, hA.basicOpen gA,
    X.presheaf.map (X.basicOpen_le gA).hom.op gA, ‹_›, ?_,
    X.toRingedSpace.isUnit_res_basicOpen gA⟩
  simpa using h_germ_gA

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

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsIntegral X
inst✝ : LocallyOfFiniteType sY
f : { f // f ≫ sY = X.fromSpecStalk (genericPoint ↥X) ≫ sX }
⊢ (((fun x ↦ x.compHom sY) (PartialMap.ofFromSpecStalk sX sY ↑f ⋯)).restrict
        ((fun x ↦ x.compHom sY) (PartialMap.ofFromSpecStalk sX sY ↑f ⋯)).domain ⋯ ⋯).hom =
    ((Hom.toPartialMap sX).restrict ((fun x ↦ x.compHom sY) (PartialMap.ofFromSpecStalk sX sY ↑f ⋯)).domain ⋯ ⋯).hom

Tactic:
simp [PartialMap.ofFromSpecStalk_comp]

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)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  { obj := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subscheme,
    map := fun {X Y} f ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D'.map f)
x✝¹ : ∀ (i : I), Nonempty ↥(D'.obj i)
x✝ : ∀ (i : I), CompactSpace ↥(D'.obj i)
i j : I
f : i ⟶ j
⊢ ((Functor.const I).obj (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subscheme).map f ≫
      (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subschemeMap
        (vanishingIdeal { carrier := Z j, isClosed' := ⋯ }) (c.π.app j) ⋯ =
    (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subschemeMap
        (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }) (c.π.app i) ⋯ ≫
      D'.map f

Tactic:
simp [D', ← cancel_mono (subschemeι _)]

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

Goal state before:
pp: X Y : Scheme
f : X ⤏ Y
inst✝ : f.IsDominant
⊢ f.representative.toRationalMap.IsDominant

Tactic:
f.toRationalMap_representative

Goal state after:
X Y : Scheme
f : X ⤏ Y
inst✝ : f.IsDominant
⊢ f.IsDominant
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)
j : I
Z : (i : I) → (i ⟶ j) → Set ↥(D.obj i)
hZc : ∀ (i : I) (hij : i ⟶ j), IsClosed (Z i hij)
hZne : ∀ (i : I) (hij : i ⟶ j), (Z i hij).Nonempty
hZcpt : ∀ (i : I) (hij : i ⟶ j), IsCompact (Z i hij)
hstab : ∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j), Set.MapsTo (⇑(D.map hi'i)) (Z i' (hi'i ≫ hij)) (Z i hij)
this : ∀ {i₁ i₂ : Over j} (f : i₁ ⟶ i₂), IsAffineHom ((Over.forget j ⋙ D).map f)
⊢ ∃ s, ∀ (i : I) (hij : i ⟶ j), (c.π.app i) s ∈ Z i hij

Tactic:
simpa [Over.forall_iff] using! exists_mem_of_isClosed_of_nonempty (Over.forget j ⋙ D) _
    ((Functor.Initial.isLimitWhiskerEquiv (Over.forget j) c).symm hc)
    (fun i ↦ Z i.left i.hom) (fun _ ↦ hZc _ _) (fun _ ↦ hZne _ _) (fun _ ↦ hZcpt _ _)
    (fun {i₁ i₂} f ↦ by dsimp; rw [← Over.w f]; exact hstab ..)

Goal state after:
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
c : Cone D
hc : IsLimit c
inst✝ : IsCofiltered I
i : I
U : (D.obj i).Opens
⊢ (Cone.postcompose (opensDiagramι D i U)).obj (opensCone D c i U) ⟶ Cone.whisker (Over.forget i) c

Tactic:
by exact { hom := (c.π.app i ⁻¹ᵁ U).ι }

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inr
I : Type u
inst✝⁸ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁷ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁶ : IsCofiltered I
inst✝⁵ : ∀ (i : I), IsAffine (D.obj i)
inst✝⁴ : IsAffine c.pt
i j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝³ : IsAffine (Spec R)
S : CommRingCat
inst✝² : IsAffine (Spec S)
a : D.obj i ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst✝¹ : LocallyOfFiniteType (Spec.map φ)
ha : t.app i = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), IsAffine (D.obj i)]
    [IsAffine c.pt] (t : D ⟶ (Functor.const I).obj (Spec R)) (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S),
    c.π.app i ≫ a = c.π.app j ≫ b →
      t.app i = a ≫ Spec.map φ →
        t.app j = b ≫ Spec.map φ → (∃ D', D = D' ⋙ Scheme.Spec) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst✝ : ∀ (i : I), IsIso (e.app i)
inst : IsIso e
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

Tactic:
have inst (i) : IsAffine ((D ⋙ Scheme.Γ.rightOp ⋙ Scheme.Spec).obj i) := by
      dsimp; infer_instance

Goal state after:
case inr
I : Type u
inst✝⁹ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁸ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁷ : IsCofiltered I
inst✝⁶ : ∀ (i : I), IsAffine (D.obj i)
inst✝⁵ : IsAffine c.pt
i j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝⁴ : IsAffine (Spec R)
S : CommRingCat
inst✝³ : IsAffine (Spec S)
a : D.obj i ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst✝² : LocallyOfFiniteType (Spec.map φ)
ha : t.app i = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), IsAffine (D.obj i)]
    [IsAffine c.pt] (t : D ⟶ (Functor.const I).obj (Spec R)) (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S),
    c.π.app i ≫ a = c.π.app j ≫ b →
      t.app i = a ≫ Spec.map φ →
        t.app j = b ≫ Spec.map φ → (∃ D', D = D' ⋙ Scheme.Spec) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst✝¹ : ∀ (i : I), IsIso (e.app i)
inst✝ : IsIso e
inst : ∀ (i : I), IsAffine ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₁.refine_1
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]
⊢ comap Polynomial.C '' (zeroLocus (Set.range { val := 0 }.val) \ zeroLocus {f}) =
    ConstructibleSetData.toSet
      (Finset.image (fun j ↦ { f := f.coeff j, n := 0, g := 0 }) (Finset.range (f.natDegree + 2)))

Tactic:
convert! image_comap_C_basicOpen f

Goal state after:
case e'_2
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]
⊢ zeroLocus (Set.range { val := 0 }.val) \ zeroLocus {f} = ↑(basicOpen f)

case e'_3
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]
⊢ ConstructibleSetData.toSet
      (Finset.image (fun j ↦ { f := f.coeff j, n := 0, g := 0 }) (Finset.range (f.natDegree + 2))) =
    (zeroLocus coeff(f))ᶜ
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case refine_1.refine_3
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
⊢ (fun p ↦ f p.fst p.snd) '' { carrier := s.sigma fun i ↦ if h : i ∈ s then ↑(V i h) else ∅, is_open' := ⋯ }.carrier = U

Tactic:
· aesop

Goal state after:
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.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).ι.app a) ≫
      (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans 𝒰 hij) ⋯ trivial).counit.app (d.cocone j).pt =
    (MorphismProperty.Over.map ⊤ ⋯).map ((d.cocone i).ι.app a) ≫ d.transitionMap hij

Tactic:
Functor.mapCocone_ι_app,

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 :=
  (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.pullback P ⊤ (Cover.trans 𝒰 hij)).map ((d.cocone j).ι.app a)) ≫
      (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans 𝒰 hij) ⋯ trivial).counit.app (d.cocone j).pt =
    (MorphismProperty.Over.map ⊤ ⋯).map ((d.cocone i).ι.app a) ≫ d.transitionMap hij
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst✝ : EffectiveEpiFamily X f
W✝ : C
e : (a : α) → Y a ⟶ W✝
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z✝ : C
a₁ a₂ : α
g₁ : Z✝ ⟶ X a₁
g₂ : Z✝ ⟶ X a₂
x✝ : g₁ ≫ f a₁ = g₂ ≫ f a₂
⊢ g₁ ≫ i a₁ ≫ e a₁ = g₂ ≫ i a₂ ≫ e a₂

Tactic:
by
    simp only [← Category.assoc]
    apply w _ _ (g₁ ≫ i a₁) (g₂ ≫ i a₂)
    simp only [Category.assoc]
    simp only [← Category.assoc, hi]
    simpa

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✝
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst✝² : EffectiveEpi f
F : C ⥤ D
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ IsColimit (Cofork.ofπ (F.map f) ⋯)

Tactic:
refine isColimitCoforkOfEffectiveEpi (F.map f) (.mk (F.map c.fst) (F.map c.snd) ?_) ?_

Goal state after:
case refine_1
C✝ : Type u_1
inst✝⁶ : Category.{v_1, u_1} C✝
D✝ : Type u_2
inst✝⁵ : Category.{v_2, u_2} D✝
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst✝² : EffectiveEpi f
F : C ⥤ D
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ F.map c.fst ≫ F.map f = F.map c.snd ≫ F.map f

case refine_2
C✝ : Type u_1
inst✝⁶ : Category.{v_1, u_1} C✝
D✝ : Type u_2
inst✝⁵ : Category.{v_2, u_2} D✝
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst✝² : EffectiveEpi f
F : C ⥤ D
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ IsLimit (PullbackCone.mk (F.map c.fst) (F.map c.snd) ?refine_1)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆
hx : x₁ = x₂
⊢ y₁ = y₂ ∨ y₁ = W.negY x₂ y₂

Tactic:
← sub_eq_zero,

Goal state after:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆
hx : x₁ = x₂
⊢ y₁ - y₂ = 0 ∨ y₁ = W.negY x₂ y₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ { a := 1, b := -W.slope x₁ x₂ y₁ y₂ ^ 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
      c := 2 * x₁ * W.slope x₁ x₂ y₁ y₂ ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ + (-W.a₁ * y₁ + W.a₄),
      d :=
        -x₁ ^ 2 * W.slope x₁ x₂ y₁ y₂ ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
          (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
      d := -(x₁ * x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) }

Tactic:
rcases hx, Y_eq_of_Y_ne h₁ h₂ hx hy with ⟨rfl, rfl⟩

Goal state after:
case pos
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ h₂ : W.Equation x₁ y₁
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ ≠ W.negY x₁ y₁
⊢ { a := 1, b := -W.slope x₁ x₁ y₁ y₁ ^ 2 - W.a₁ * W.slope x₁ x₁ y₁ y₁ + W.a₂,
      c := 2 * x₁ * W.slope x₁ x₁ y₁ y₁ ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₁ y₁ y₁ + (-W.a₁ * y₁ + W.a₄),
      d :=
        -x₁ ^ 2 * W.slope x₁ x₁ y₁ y₁ ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₁ y₁ y₁ -
          (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } =
    { a := 1, b := -(x₁ + x₁ + W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)),
      c := x₁ * x₁ + x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁) + x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁),
      d := -(x₁ * x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)) }