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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x✝¹ : ↥Y
x✝ : x✝¹ ∈ ⇑f '' U
x : ↥X
left✝ : x ∈ U
right✝ : f x = x✝¹
⊢ x✝¹ ∈ (⨆ i, (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }).carrier

Tactic:
have := 𝒰.exists_eq x

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x✝¹ : ↥Y
x✝ : x✝¹ ∈ ⇑f '' U
x : ↥X
left✝ : x ∈ U
right✝ : f x = x✝¹
this : ∃ i y, (𝒰.f i) y = x
⊢ x✝¹ ∈ (⨆ i, (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }).carrier
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I✝ : X.IdealSheafData
I : Ideal ↑Γ(X, ⊤)
U : ↑X.affineOpens
x : ↥X
hxU : x ∈ ↑U
⊢ x ∈ X.zeroLocus ↑I ↔ x ∈ X.zeroLocus ↑(Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) I)

Tactic:
by
      simp only [Ideal.map, zeroLocus_span, zeroLocus_map, Set.mem_union, Set.mem_compl_iff,
        SetLike.mem_coe, hxU, not_true_eq_false, iff_self_or, IsEmpty.forall_iff]

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

Goal state before:
pp: ⊢ IsOpenImmersion ⊓ @Surjective =
    (isomorphisms TopCat).inverseImage Scheme.forgetToTop ⊓
      stalkwise fun {R S} [CommRing R] [CommRing S] f ↦ Function.Bijective ⇑f

Tactic:
isOpenImmersion_eq_inf,

Goal state after:
⊢ ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
        stalkwise fun {R S} [CommRing R] [CommRing S] x ↦ Function.Bijective ⇑x) ⊓
      @Surjective =
    (isomorphisms TopCat).inverseImage Scheme.forgetToTop ⊓
      stalkwise fun {R S} [CommRing R] [CommRing S] f ↦ Function.Bijective ⇑f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
x : ↥X
hxU : x ∈ ↑U
⊢ x ∈ ↑Z ↔ x ∈ ⇑(IsAffineOpen.fromSpec ⋯) '' closure (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)

Tactic:
← U.2.fromSpec.isOpenEmbedding.isOpenMap.preimage_closure_eq_closure_preimage
            U.2.fromSpec.continuous,

Goal state after:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
x : ↥X
hxU : x ∈ ↑U
⊢ x ∈ ↑Z ↔ x ∈ ⇑(IsAffineOpen.fromSpec ⋯) '' ⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' closure ↑Z
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑X.toTopCat
x : ↥U
f : ↑(X.presheaf.obj (op U))
⊢ (ConcreteCategory.hom (X.evaluation x)) f ≠ 0 ↔ ↑x ∈ X.toRingedSpace.basicOpen f

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
Z : LocallyRingedSpace
g : Y ⟶ Z
x : ↑X.toTopCat
⊢ residueFieldMap (f ≫ g) x = residueFieldMap g ((ConcreteCategory.hom f.base) x) ≫ residueFieldMap f x

Tactic:
ext : 1
  simp only [residueFieldMap, stalkMap_comp]
  apply IsLocalRing.ResidueField.map_comp (Hom.stalkMap g (f.base x)).hom (Hom.stalkMap f x).hom

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
⊢ (ConcreteCategory.hom (X.evaluation U x hx)) f ≠ 0 ↔ x ∈ X.basicOpen f

Tactic:
by
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x : ↥X
⊢ Set.range ⇑(X.fromSpecResidueField x) = {x}

Tactic:
by
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: case mpr
K : Type u_1
inst✝ : Field K
X : Scheme
f : ↥X
snd✝¹ : X.residueField f ⟶ CommRingCat.of K
g : ↥X
snd✝ : X.residueField g ⟶ CommRingCat.of K
⊢ (∃ (e : ⟨f, snd✝¹⟩.fst = ⟨g, snd✝⟩.fst), ⟨f, snd✝¹⟩.snd = (residueFieldCongr e).hom ≫ ⟨g, snd✝⟩.snd) →
    ⟨f, snd✝¹⟩ = ⟨g, snd✝⟩

Tactic:
rintro ⟨(rfl : f = g), h⟩

Goal state after:
case mpr
K : Type u_1
inst✝ : Field K
X : Scheme
f : ↥X
snd✝¹ snd✝ : X.residueField f ⟶ CommRingCat.of K
h : ⟨f, snd✝¹⟩.snd = (residueFieldCongr ⋯).hom ≫ ⟨f, snd✝⟩.snd
⊢ ⟨f, snd✝¹⟩ = ⟨f, snd✝⟩
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) f ↔
    IsAffineHom f ∧ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
by
  have : HasRingHomProperty (affineLocally Q) Q := ⟨hQ, rfl⟩
  rw [targetAffineLocally_affineAnd_iff' hQ.respectsIso]
  simp only [and_congr_right_iff]
  intro hf
  constructor
  · wlog hY : IsAffine Y
    · intro h
      rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := affineLocally Q)
        _ (iSup_affineOpens_eq_top _)]
      intro U
      have : IsAffine (f ⁻¹ᵁ U) := hf.isAffine_preimage U U.2
      rw [HasRingHomProperty.iff_of_isAffine (P := affineLocally Q),
        morphismRestrict_appTop, CommRingCat.hom_comp, hQ.respectsIso.cancel_right_isIso]
      apply h
      rw [Scheme.Opens.ι_image_top]
      exact U.2
    intro h
    have : IsAffine X := isAffine_of_isAffineHom f
    rw [HasRingHomProperty.iff_of_isAffine (P := affineLocally Q)]
    exact h ⊤ (isAffineOpen_top Y)
  · intro h U hU
    rw [affineLocally_iff_affineOpens_le] at h
    rw [f.app_eq_appLE]
    exact h ⟨U, hU⟩ ⟨f ⁻¹ᵁ U, hf.isAffine_preimage U hU⟩ (by simp)

Goal state after:
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 : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQ : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
⊢ P (𝟙 X)

Tactic:
rw [eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi]
    intro U hU
    exact ⟨hU, hQ _⟩

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

Goal state before:
pp: case mpr
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
this : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f
⊢ J ≤ Hom.ker (I.subschemeι ≫ f)

Tactic:
← J.ker_subschemeι,

Goal state after:
case mpr
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
this : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f
⊢ Hom.ker J.subschemeι ≤ Hom.ker (I.subschemeι ≫ f)
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 f'.op
⊢ IsIso f

Tactic:
by
    rwa [isIso_op_iff, ← isIso_iff_of_reflects_iso _ (MorphismProperty.Over.forget ..),
      ← isIso_iff_of_reflects_iso _ (Over.forget _)] at h

Goal state after:
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: ⊢ IsStableUnderBaseChange @FinitePresentation

Tactic:
by
  apply IsStableUnderBaseChange.mk
  · exact finitePresentation_respectsIso
  · simp only [finitePresentation_algebraMap]
    intros
    infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : X.IsSeparated
⊢ IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X))

Tactic:
by
  rwa [← isSeparated_iff_isClosedImmersion_prod_lift]

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ HasAffineProperty @IsSeparated fun X x x_1 x_2 ↦ X.IsSeparated

Tactic:
convert! HasAffineProperty.of_isZariskiLocalAtTarget @IsSeparated with X Y f hY

Goal state after:
case e'_2
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ X.IsSeparated ↔ AffineTargetMorphismProperty.of (@IsSeparated) f
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr.convert_3
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ CompactSpace ↥X

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

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsDominant f
inst✝ : IsReduced Y
⊢ closure (Set.range ⇑f) ⊆ ↑(Scheme.Hom.ker f).support

Tactic:
f.ker.support.isClosed.closure_subset_iff

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
⊢ Function.Injective ⇑(ConcreteCategory.hom (app f U))

Tactic:
wlog hU : IsAffineOpen U generalizing U

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
this : ∀ (U : Y.Opens), IsAffineOpen U → Function.Injective ⇑(ConcreteCategory.hom (app f U))
hU : ¬IsAffineOpen U
⊢ Function.Injective ⇑(ConcreteCategory.hom (app f U))

X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
hU : IsAffineOpen U
⊢ Function.Injective ⇑(ConcreteCategory.hom (app f U))
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
this : ∀ (U : Y.Opens), IsAffineOpen U → Function.Injective ⇑(ConcreteCategory.hom (app f U))
hU : ¬IsAffineOpen U
s : ↑Γ(Y, U)
hs : (ConcreteCategory.hom (app f U)) s = 0
x : ↥Y
hx : x ∈ Opposite.unop (Opposite.op U)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : x ∈ ↑V
hVU : V ≤ U
⊢ (ConcreteCategory.hom
        (app f (Opposite.unop (Opposite.op U)) ≫
          X.presheaf.map ((TopologicalSpace.Opens.map f.base).map (homOfLE hVU).op.unop).op))
      s =
    (ConcreteCategory.hom (app f V)) ((ConcreteCategory.hom (Y.presheaf.map (homOfLE hVU).op)) 0)

Tactic:
simp [hs]

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {ι : Type u_1} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), topologically (@IsOpenMap) (f ∣_ U i)) → topologically (@IsOpenMap) f

Tactic:
ι

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
⊢ ∀ (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), topologically (@IsOpenMap) (f ∣_ U i)) → topologically (@IsOpenMap) f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {ι : Type u_1} (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), topologically (@IsClosedMap) (f ∣_ U i)) → topologically (@IsClosedMap) f

Tactic:
ι

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
⊢ ∀ (U : ι → Y.Opens),
    IsOpenCover U → (∀ (i : ι), topologically (@IsClosedMap) (f ∣_ U i)) → topologically (@IsClosedMap) f
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: ⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral

Tactic:
by
  refine IsStableUnderBaseChange.mk isIntegral_respectsIso ?_
  introv int
  rw [algebraMap_isIntegral_iff] at int ⊢
  infer_instance

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

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
inst✝² : CommRing R₀
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
n : ℕ
e : InductionObj R n
⊢ R₀ ∙ 1 ≤ coeffSubmodule R₀ e

Tactic:
Submodule.span_le,

Goal state after:
R₀ : Type u_1
R : Type u_2
inst✝² : CommRing R₀
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
n : ℕ
e : InductionObj R n
⊢ {1} ⊆ ↑(coeffSubmodule R₀ e)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
⊢ IsOpenMap ⇑(𝔸(n; S) ↘ S)

Tactic:
change topologically @IsOpenMap _
  wlog hS : ∃ R, S = Spec R
  · refine (IsZariskiLocalAtTarget.iff_of_openCover
      (P := topologically @IsOpenMap) S.affineCover).mpr ?_
    intro i
    have := this (n := n) (S.affineCover.X i) ⟨_, rfl⟩
    rwa [← (isPullback_map (n := n) (S.affineCover.f i)).isoPullback_hom_snd,
      MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)] at this
  obtain ⟨R, rfl⟩ := hS
  rw [← MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)
    (SpecIso n R).inv, SpecIso_inv_over]
  exact MvPolynomial.isOpenMap_comap_C

Goal state after:
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
⊢ ↑p (IsLocalRing.closedPoint K) ∈ closedPoints ↥X

Tactic:
have := isClosedImmersion_of_comp_eq_id _ _ p.2

Goal state after:
X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
this : IsClosedImmersion ↑p
⊢ ↑p (IsLocalRing.closedPoint K) ∈ closedPoints ↥X
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
z : X
hz : z ∈ U
⊢ ∃ t, t ∈ 𝓝 z

Tactic:
use Set.univ, univ_mem

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
f : locallyFinsuppWithin U Y
p : X
hp : p ∈ U
t : Set X
h₁t : t ∈ 𝓝 p
h₂t : (t ∩ f.support).Finite
⊢ t ∩ f.support ∈ 𝓝[f.support] p

Tactic:
mem_nhdsWithin_iff_exists_mem_nhds_inter

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
f : locallyFinsuppWithin U Y
p : X
hp : p ∈ U
t : Set X
h₁t : t ∈ 𝓝 p
h₂t : (t ∩ f.support).Finite
⊢ ∃ u ∈ 𝓝 p, u ∩ f.support ⊆ t ∩ f.support
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case e
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ f x = g x

Tactic:
simpa using congr($e (IsLocalRing.closedPoint _))

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

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

Tactic:
by
  simp

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

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
V : X.Opens
hV : Dense ↑V
hV' : V ≤ U
⊢ ((f.restrict U hU hU').restrict V hV hV').hom = (f.restrict V hV ⋯).hom

Tactic:
by
  simp

Goal state after:
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
⊢ IsOver S f ↔ (f.compHom (Y ↘ S)).hom = f.domain.ι ≫ X ↘ S

Tactic:
by
  simp

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

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝ : IrreducibleSpace ↥X
f✝ : X ⤏ Y
f g : X.PartialMap Y
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
e : (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
this : f.restrict W hW hWl = g.restrict W hW hWr
⊢ f.fromFunctionField = g.fromFunctionField

Tactic:
rw [← f.fromFunctionField_restrict hW hWl, this, g.fromFunctionField_restrict]

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

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
I : Set ↑X.affineOpens
hI : I.Finite
e : UX = ⨆ i ∈ I, ↑i
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
have hIUX (i : I) : i.1 ≤ UX := by rw [e]; intro i; aesop

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
I : Set ↑X.affineOpens
hI : I.Finite
e : UX = ⨆ i ∈ I, ↑i
hIUX : ∀ (i : ↑I), ↑↑i ≤ UX
⊢ IsIso (pushoutSection H hUST hUSX hUY)
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)
i : I
U V : (D.obj i).Opens
hU : IsCompact ↑U
H : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
⊢ ∃ j fji, D.map fji ⁻¹ᵁ U ≤ D.map fji ⁻¹ᵁ V

Tactic:
by
  have (j : Over i) : CompactSpace ↥((opensDiagram D i U).obj j) :=
    isCompact_iff_compactSpace.mp (QuasiCompact.isCompact_preimage (f := (D.map j.hom)) _ U.2 hU)
  have H : ((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V = ⊤ := by
    rw [Scheme.Hom.comp_preimage, ← top_le_iff]
    exact .trans (by simp) (Scheme.Hom.preimage_mono _ H)
  obtain ⟨j, fji, hj⟩ := exists_map_eq_top _ _ (isLimitOpensCone D c hc i U) (i := .mk (𝟙 i))
    (((Scheme.isoOfEq _ (by simp)).hom ≫ U.ι) ⁻¹ᵁ V)
    (by simpa [← Scheme.Hom.comp_preimage, -Scheme.Hom.comp_base])
  refine ⟨j.left, j.hom, ?_⟩
  replace hj : (D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map fji.left ⁻¹ᵁ V = ⊤ := by
    simpa [← Scheme.Hom.comp_preimage, -Scheme.Hom.comp_base] using hj
  replace hj : (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ D.map fji.left ⁻¹ᵁ V := Set.image_subset_iff.mpr hj.ge
  simpa [show fji.left = j.hom by simpa using fji.w] using hj

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

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

Tactic:
use xk

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

Goal state before:
pp: case refine_2
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
⊢ π ≫ Cover.glueMorphisms 𝒰 u ⋯ = f

Tactic:
· apply Cover.hom_ext (𝒰.pullback₁ π)
    intro i
    simp [pullback.condition_assoc, hfac]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹ = x✝

Tactic:
ext <;> apply_fun _ using hf <;> assumption

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ ↑(W.map f).Δ'⁻¹ = f ↑W.Δ'⁻¹

Tactic:
by
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ (W.map f).Δ'⁻¹ = (Units.map ↑f) W.Δ'⁻¹

Tactic:
by
  simp

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

Goal state before:
pp: case mul_X.refine_2
R : Type u_2
inst✝ : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg : g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) = ↑f
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
hσ' : ∀ (x : MvPolynomial (Fin m) R), g (σ x) = x
hg' : Surjective ⇑g
S' : ConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Finset.image
    (fun x ↦
      match x with
      | { f := fk, n := k, g := gk } =>
        { f := σ fk, n := k + n,
          g := fun s ↦
            Sum.elim (⇑σ ∘ gk) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
              (finSumFinEquiv.symm s) })
    S
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Set.range fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))
H : Ideal.span s₀ ≤ RingHom.ker g
i : Fin n
q₁ : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)
q₂ : MvPolynomial (Fin m) R
hq₁ : q₁ ∈ Ideal.span s₀
⊢ (q₁ + σ q₂) * MvPolynomial.C (MvPolynomial.X i) =
    q₁ * MvPolynomial.C (MvPolynomial.X i) + σ q₂ * (MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))) +
      σ (q₂ * f (MvPolynomial.X i))

Tactic:
simp; ring

Goal state after: