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

Goal state before:
pp: case of_basicOpenCover
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (s : Finset ↑Γ(Y, ⊤)),
    Ideal.span ↑s = ⊤ → (∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)) → IsAffine X

Tactic:
intro X Y _ f S hS hS'

Goal state after:
case of_basicOpenCover
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : ↥S), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)
⊢ IsAffine X
Module: Mathlib.RingTheory.RingHom.EssFiniteType

Goal state before:
pp: ⊢ HoldsForLocalization fun {R S} [CommRing R] [CommRing S] ↦ EssFiniteType

Tactic:
by
  introv R _
  rw [essFiniteType_algebraMap]
  exact .of_isLocalization _ M

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

Goal state before:
pp: case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hf : P f
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (P : MorphismProperty Scheme),
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y), P f → IsAffine Y → IsAffineHom f
hY : ¬IsAffine Y
⊢ IsAffineHom f

Tactic:
IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsAffineHom) _ (iSup_affineOpens_eq_top _)

Goal state after:
case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hf : P f
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (P : MorphismProperty Scheme),
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y), P f → IsAffine Y → IsAffineHom f
hY : ¬IsAffine Y
⊢ ∀ (i : ↑Y.affineOpens), IsAffineHom (f ∣_ ↑i)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
⊢ IsClosedEmbedding ⇑f

Tactic:
have h := (f ≫ g).isClosedEmbedding
    simp only [Scheme.Hom.comp_base, TopCat.coe_comp] at h
    refine .of_continuous_injective_isClosedMap (Scheme.Hom.continuous f) h.injective.of_comp ?_
    intro Z hZ
    rw [IsClosedEmbedding.isClosed_iff_image_isClosed g.isClosedEmbedding,
      ← Set.image_comp]
    exact h.isClosedMap _ hZ

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

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this✝ : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph ⇑(Scheme.Hom.toImage f)
x : ↥X
⊢ Function.Injective
    ⇑(CommRingCat.Hom.hom
        ((TopCat.Presheaf.stalkFunctor CommRingCat ((Scheme.Hom.toImage f) x)).map (Scheme.Hom.toImage f).c ≫
          TopCat.Presheaf.stalkPushforward CommRingCat (Scheme.Hom.toImage f).base X.presheaf x))

Tactic:
simp only [TopCat.Presheaf.stalkFunctor_obj, CommRingCat.hom_comp, RingHom.coe_comp]

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
this✝ : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph ⇑(Scheme.Hom.toImage f)
x : ↥X
⊢ Function.Injective
    (⇑(CommRingCat.Hom.hom (TopCat.Presheaf.stalkPushforward CommRingCat (Scheme.Hom.toImage f).base X.presheaf x)) ∘
      ⇑(CommRingCat.Hom.hom
          ((TopCat.Presheaf.stalkFunctor CommRingCat ((Scheme.Hom.toImage f) x)).map (Scheme.Hom.toImage f).c)))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst✝¹ : IsClosedImmersion iX
inst✝ : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
⊢ IsPullback iX Zf f iY

Tactic:
suffices IsIso (pullback.lift _ _ h) by
    simpa using (IsPullback.of_vert_isIso (show CommSq iX (pullback.lift iX Zf h)
      (𝟙 X) (pullback.fst _ _) from ⟨by simp⟩)).paste_vert (IsPullback.of_hasPullback f iY)
  refine IsClosedImmersion.isIso_of_ker_eq iX (pullback.fst f iY) _ (by simp) ?_
  rw [ker_fst_of_isClosedImmersion, h']

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

Goal state before:
pp: case a
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ I.map (f ≫ g) ≤ (I.map f).map g

Tactic:
rw [le_map_iff_comap_le, le_map_iff_comap_le, ← comap_comp]

Goal state after:
case a
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ (I.map (f ≫ g)).comap (f ≫ g) ≤ I
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h✝ : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h✝ True.intro
h : IsIso ((MorphismProperty.Over.forget @IsClosedImmersion ⊤ X).map f')
⊢ IsIso f

Tactic:
← isIso_iff_of_reflects_iso _ (Over.forget _)

Goal state after:
Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h✝ : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h✝ True.intro
h : IsIso ((Over.forget X).map ((MorphismProperty.Over.forget @IsClosedImmersion ⊤ X).map f'))
⊢ IsIso f
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z
S : Scheme
X Y : Over S
inst✝ : IsSeparated Y.hom
f g : X ⟶ Y
⊢ IsClosedImmersion (Over.Hom.left (equalizer.ι f g))

Tactic:
by
  refine MorphismProperty.of_isPullback
    ((Limits.isPullback_equalizer_prod f g).map (Over.forget _)).flip ?_
  rw [← MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion _
    (Over.prodLeftIsoPullback Y Y).hom]
  convert! (inferInstance : IsClosedImmersion (pullback.diagonal Y.hom))
  ext1 <;> simp [← Over.comp_left]

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

Goal state before:
pp: case inr
Y : Scheme
inst✝ : Subsingleton ↥Y
R : CommRingCat
f : Spec R ⟶ Y
g : Y ⟶ Spec R
hg : g ≫ f = 𝟙 Y
this :
  ∀ {Y : Scheme} [Subsingleton ↥Y] (R : CommRingCat) (f : Spec R ⟶ Y) (g : Y ⟶ Spec R),
    g ≫ f = 𝟙 Y → (∃ S, Y = Spec S) → IsClosedImmersion g
hY : ¬∃ S, Y = Spec S
⊢ IsClosedImmersion g

Tactic:
have inst := (Scheme.isoSpec Y).inv.homeomorph.injective.subsingleton

Goal state after:
case inr
Y : Scheme
inst✝ : Subsingleton ↥Y
R : CommRingCat
f : Spec R ⟶ Y
g : Y ⟶ Spec R
hg : g ≫ f = 𝟙 Y
this :
  ∀ {Y : Scheme} [Subsingleton ↥Y] (R : CommRingCat) (f : Spec R ⟶ Y) (g : Y ⟶ Spec R),
    g ≫ f = 𝟙 Y → (∃ S, Y = Spec S) → IsClosedImmersion g
hY : ¬∃ S, Y = Spec S
inst : Subsingleton ↥(Spec Γ(Y, ⊤))
⊢ IsClosedImmersion g
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case hU
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
i✝ : ι
⊢ IsNoetherianRing ↑Γ(X, ↑(S i✝))

Tactic:
exact hS' _

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsDominant f
inst✝ : IsReduced Y
⊢ ↑(Scheme.Hom.ker f).support = ↑⊤

Tactic:
TopologicalSpace.Closeds.coe_top,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsDominant f
inst✝ : IsReduced Y
⊢ ↑(Scheme.Hom.ker f).support = Set.univ
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, ⟨U, hU⟩).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : ↑Γ(Y, V)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V))
⊢ pullback.snd f g ⁻¹ᵁ V ≤ pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U

Tactic:
hVU

Goal state after:
X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, ⟨U, hU⟩).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : ↑Γ(Y, V)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V))
⊢ pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U ≤ pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
⊢ CompactSpace ↥X

Tactic:
obtain ⟨U', ⟨g, rfl⟩, htU', hU'le⟩ := Opens.isBasis_iff_nbhd.mp isBasis_basic_opens htZc

Goal state after:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : ↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K))
htU' : t ∈ basicOpen g
hU'le : basicOpen g ≤ Zc
⊢ CompactSpace ↥X
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: case refine_1
X Y : Scheme
K : Type u
inst✝⁵ : Field K
inst✝⁴ : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst✝³ : IsSeparated i
inst✝² : LocallyOfFiniteType i
inst✝¹ : IsReduced X
inst✝ : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed {x} → f x = g x
H' : f ≫ i = g ≫ i
this : JacobsonSpace ↥X
⊢ Dense (S ∩ closedPoints ↥X)

pp: case refine_2
X Y : Scheme
K : Type u
inst✝⁵ : Field K
inst✝⁴ : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst✝³ : IsSeparated i
inst✝² : LocallyOfFiniteType i
inst✝¹ : IsReduced X
inst✝ : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed {x} → f x = g x
H' : f ≫ i = g ≫ i
this : JacobsonSpace ↥X
⊢ ∀ x ∈ S ∩ closedPoints ↥X, X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g

Tactic:
· rwa [dense_iff_closure_eq, JacobsonSpace.closure_inter_closedPoints_eq_closure hS,
      ← dense_iff_closure_eq]

Goal state after:
case refine_2
X Y : Scheme
K : Type u
inst✝⁵ : Field K
inst✝⁴ : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst✝³ : IsSeparated i
inst✝² : LocallyOfFiniteType i
inst✝¹ : IsReduced X
inst✝ : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed {x} → f x = g x
H' : f ≫ i = g ≫ i
this : JacobsonSpace ↥X
⊢ ∀ x ∈ S ∩ closedPoints ↥X, X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
Module: Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic

Goal state before:
pp: X : Scheme
R : Type u_1
inst✝¹ : Semiring R
N : Type u_2
inst✝ : DecidableEq N
wx : ↥X → N
c : AlgebraicCycle X R
⊢ map (𝟙 X) wx wx c = c

Tactic:
apply Function.locallyFinsupp.map_id
  simp [mapCoeff]

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
⊢ Scheme.Hom.app sY U ≫ Y.presheaf.germ (sY ⁻¹ᵁ U) y ⋯ ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU

Tactic:
← Scheme.Hom.germ_stalkMap_assoc,

Goal state after:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
⊢ S.presheaf.germ U (sY y) ⋯ ≫ Scheme.Hom.stalkMap sY y ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (PartialMap.id X).compHom f = Hom.toPartialMap f

Tactic:
by
  apply PartialMap.ext _ _ rfl
  simp

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

Goal state before:
pp: 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
⊢ f.equiv g

Tactic:
by
  have hdense : Dense ((f.domain ⊓ g.domain) : Set X) :=
    f.dense_domain.inter_of_isOpen_left g.dense_domain f.domain.2
  have := (isGermInjectiveAt_iff_of_isOpenImmersion (f := (f.domain ⊓ g.domain).ι)
    (x := ⟨x, hxf, hxg⟩)).mp ‹_›
  have := spread_out_unique_of_isGermInjective' (X := (f.domain ⊓ g.domain).toScheme)
    (X.homOfLE inf_le_left ≫ f.hom) (X.homOfLE inf_le_right ≫ g.hom) (x := ⟨x, hxf, hxg⟩) ?_
  · obtain ⟨U, hxU, e⟩ := this
    refine ⟨(f.domain ⊓ g.domain).ι ''ᵁ U, ((f.domain ⊓ g.domain).ι ''ᵁ U).2.dense
      ⟨_, ⟨_, hxU, rfl⟩⟩,
      ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_left,
      ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_right, ?_⟩
    rw [← cancel_epi (Scheme.Hom.isoImage _ _).hom]
    simp only [restrict_hom, ← Category.assoc] at e ⊢
    convert! e using 2 <;> rw [← cancel_mono (Scheme.Opens.ι _)] <;> simp
  · rw [← f.fromSpecStalkOfMem_restrict hdense inf_le_left ⟨hxf, hxg⟩,
      ← g.fromSpecStalkOfMem_restrict hdense inf_le_right ⟨hxf, hxg⟩] at H
    simpa only [fromSpecStalkOfMem, restrict_domain, Opens.fromSpecStalkOfMem, Spec.map_inv,
      restrict_hom, Category.assoc, IsIso.eq_inv_comp, IsIso.hom_inv_id_assoc] using H

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

Goal state before:
pp: S X : Scheme
sX : X ⟶ S
⊢ PartialIso.IsOver sX sX (PartialIso.refl X)

Tactic:
by simp [PartialIso.IsOver]

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

Goal state before:
pp: X S : Scheme
U : X.Opens
sX : X ⟶ S
hU : Dense ↑U
⊢ PartialIso.IsOver (U.ι ≫ sX) sX (U.partialIsoOfDense hU)

Tactic:
by simp [PartialIso.IsOver]

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

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

Tactic:
Iso.inv_hom_id_assoc

Goal state after:
case H
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ X.homOfLE ⋯ ≫ f.hom = (X.isoOfEq ⋯).hom ≫ f.hom
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: 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))ᶜ

Tactic:
suffices Set.range f.coeff = ⋃ i < f.natDegree + 2, {f.coeff i} by
          simp [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet,
            ← Set.compl_eq_univ_sdiff, eq_compl_comm (y := zeroLocus _), ← zeroLocus_iUnion₂, this]
        trans f.coeff '' (Set.Iio (f.natDegree + 2))
        · 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]⟩
        · ext; simp [eq_comm]

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
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₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ g₁ ≫ (fun a ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) a₁ = g₂ ≫ (fun a ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) a₂

Tactic:
have := h a₁ a₂ (e.functor.map g₁) (e.functor.map g₂)
  simp only [← Functor.map_comp, hg] at this
  simpa using congrArg e.inverse.map (this (by trivial))

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 : Type u_3
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : G.PreservesEffectiveEpis
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : EffectiveEpi x✝¹
⊢ EffectiveEpi ((F ⋙ G).map x✝¹)

Tactic:
by dsimp; infer_instance

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 : Type u_3
inst✝³ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
inst✝² : F.PreservesFiniteEffectiveEpiFamilies
inst✝¹ : G.PreservesFiniteEffectiveEpiFamilies
α✝ : Type
inst✝ : Finite α✝
B✝ : C
x✝² : α✝ → C
x✝¹ : (a : α✝) → x✝² a ⟶ B✝
x✝ : EffectiveEpiFamily x✝² x✝¹
⊢ EffectiveEpiFamily (fun a ↦ (F ⋙ G).obj (x✝² a)) fun a ↦ (F ⋙ G).map (x✝¹ a)

Tactic:
by dsimp; infer_instance

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 : Type u_3
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.PreservesEffectiveEpiFamilies
inst✝ : G.PreservesEffectiveEpiFamilies
α✝ : Type u
B✝ : C
x✝² : α✝ → C
x✝¹ : (a : α✝) → x✝² a ⟶ B✝
x✝ : EffectiveEpiFamily x✝² x✝¹
⊢ EffectiveEpiFamily (fun a ↦ (F ⋙ G).obj (x✝² a)) fun a ↦ (F ⋙ G).map (x✝¹ a)

Tactic:
by dsimp; infer_instance

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

Goal state before:
pp: case zero
R : Type u_2
inst✝ : CommRing R
n : ℕ
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) d)
⊢ ∃ T,
    comap MvPolynomial.C '' S.toSet = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ numBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) 0 ∧
          ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) 0

Tactic:
refine ⟨(S.map (isEmptyRingEquiv _ _).toRingHom), ?_, ?_⟩

Goal state after:
case zero.refine_1
R : Type u_2
inst✝ : CommRing R
n : ℕ
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) d)
⊢ comap MvPolynomial.C '' S.toSet = (ConstructibleSetData.map (isEmptyRingEquiv R (Fin 0)).toRingHom S).toSet

case zero.refine_2
R : Type u_2
inst✝ : CommRing R
n : ℕ
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) d)
⊢ ∀ C ∈ ConstructibleSetData.map (isEmptyRingEquiv R (Fin 0)).toRingHom S,
    C.n ≤ numBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) 0 ∧
      ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: 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₂)
⊢ derivative (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) =
    -((X - C x₁) * (X - C x₂) + (X - C x₁) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) +
        (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

Tactic:
by
  rw [addPolynomial_slope h₁ h₂ hxy]
  derivative_simp
  ring1

Goal state after: