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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
I : (diagonalCover f 𝒰 𝒱).I₀
⊢ (diagonalCover f 𝒰 𝒱).f I =
    pullback.map ((𝒱 I.fst).f I.snd.1 ≫ Cover.pullbackHom 𝒰 f I.fst) ((𝒱 I.fst).f I.snd.2 ≫ Cover.pullbackHom 𝒰 f I.fst)
      f f ((𝒱 I.fst).f I.snd.1 ≫ pullback.fst f (𝒰.f I.fst)) ((𝒱 I.fst).f I.snd.2 ≫ pullback.fst f (𝒰.f I.fst))
      (𝒰.f I.fst) ⋯ ⋯

Tactic:
cases I

Goal state after:
case mk
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
fst✝ : (openCoverOfBase 𝒰 f f).I₀
snd✝ :
  ((fun i ↦
        ((fun i ↦ openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom 𝒰 f i) (Cover.pullbackHom 𝒰 f i))
            i).toPreZeroHypercover)
      fst✝).I₀
⊢ (diagonalCover f 𝒰 𝒱).f ⟨fst✝, snd✝⟩ =
    pullback.map ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst)
      ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst) f f
      ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst))
      ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst)) (𝒰.f ⟨fst✝, snd✝⟩.fst) ⋯ ⋯
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case mpr
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : J
xi : ↥(F.obj i)
xj : ↥(F.obj j)
⊢ (∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj) → (colimit.ι F i) xi = (colimit.ι F j) xj

Tactic:
rintro ⟨k, fi, fj, x, rfl, rfl⟩; simp only [← Scheme.Hom.comp_apply, colimit.w]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
⊢ PresheafedSpace.IsOpenImmersion (D.toPresheafedSpaceGlueData.ι i ≫ D.isoPresheafedSpace.inv)

Tactic:
have := D.toPresheafedSpaceGlueData.ιIsOpenImmersion i

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
this : PresheafedSpace.IsOpenImmersion (D.toPresheafedSpaceGlueData.ι i)
⊢ PresheafedSpace.IsOpenImmersion (D.toPresheafedSpaceGlueData.ι i ≫ D.isoPresheafedSpace.inv)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case mpr
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ targetAffineLocally Q.diagonal f → P.diagonal f

Tactic:
· exact fun H ↦ HasAffineProperty.diagonal_of_openCover_diagonal P f Y.affineCover
        (fun i ↦ of_targetAffineLocally_of_isPullback (.of_hasPullback _ _) H)

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

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y} f U ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)
⊢ P.diagonal f

Tactic:
change P _
    refine IsZariskiLocalAtSource.of_iSup_eq_top U hU fun i ↦ ?_
    rw [pullback.comp_diagonal]
    exact RespectsRight.postcomp (P := P) (Q := @IsOpenImmersion) (g _ _) inferInstance _ (hf i)

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

Goal state before:
pp: case of_sSup_eq_top
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U i)) →
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f

Tactic:
intro X Y f ι U hU hf
    apply hP₃ f U hU f.continuous fun i ↦ ?_
    rw [← morphismRestrict_base]
    exact hf i

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

Goal state before:
pp: case of_sSup_eq_top
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U i)) →
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f

Tactic:
· intro X Y f ι U hU hf
    apply hP₃ f U hU f.continuous fun i ↦ ?_
    rw [← morphismRestrict_base]
    exact hf i

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

Goal state before:
pp: case e'_2
X : Scheme
U : X.Opens
s : Set ↑X.affineOpens
⊢ U = ⨆ i ∈ s, ↑i ↔ U.carrier = ⋃ i ∈ s, ↑↑i

Tactic:
convert! SetLike.coe_injective.eq_iff.symm; simp

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : CompactSpace ↥Y
⊢ IsCompact Set.univ

Tactic:
← Set.preimage_univ (f := f)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : CompactSpace ↥Y
⊢ IsCompact (⇑f ⁻¹' Set.univ)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
h : IsMin { asIdeal := I, isPrime := inst✝ }
⊢ ∀ ⦃y : Ideal R⦄, y.IsPrime → y ≤ I → I ≤ y

Tactic:
by_contra! ⟨P, ⟨hP₁, ⟨hP₂, hP₃⟩⟩⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
h : IsMin { asIdeal := I, isPrime := inst✝ }
P : Ideal R
hP₁ : P.IsPrime
hP₂ : P ≤ I
hP₃ : ¬I ≤ P
⊢ False
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case hS'
X : Scheme
x : ↥X
⊢ x ∈ ⋃ x, Set.range ⇑(X.affineCover.f x)

Tactic:
exact ⟨_, ⟨_, rfl⟩, X.affineCover.covers x⟩

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
f : ↑Γ(X, ↑U)
hV : V = X.affineBasicOpen f
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) = I.ideal V

Tactic:
subst hV; exact I.map_ideal_basicOpen _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
z : ↥X
n : ℕ
hz : coheight z ≤ ↑n
⊢ Ring.KrullDimLE n ↑(X.presheaf.stalk z)

Tactic:
rw [Ring.krullDimLE_iff, ringKrullDim_stalk_eq_coheight z]

Goal state after:
X : Scheme
z : ↥X
n : ℕ
hz : coheight z ≤ ↑n
⊢ ↑(coheight z) ≤ ↑n
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X✝ Y : Scheme
f : X✝ ⟶ Y
U✝ V : X✝.Opens
hU✝ : IsAffineOpen U✝
hV : IsAffineOpen V
X : Scheme
U : Opens ↥X
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
⊢ IsPreimmersion (Spec.map (X.presheaf.germ U x hx) ≫ hU.fromSpec)

Tactic:
have : IsPreimmersion (Spec.map (X.presheaf.germ U x hx)) :=
    letI : Algebra Γ(X, U) (X.presheaf.stalk x) := (X.presheaf.germ U x hx).hom.toAlgebra
    haveI := hU.isLocalization_stalk ⟨x, hx⟩
    IsPreimmersion.of_isLocalization (R := Γ(X, U)) (S := X.presheaf.stalk x)
      (hU.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl

Goal state after:
X✝ Y : Scheme
f : X✝ ⟶ Y
U✝ V : X✝.Opens
hU✝ : IsAffineOpen U✝
hV : IsAffineOpen V
X : Scheme
U : Opens ↥X
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
this : IsPreimmersion (Spec.map (X.presheaf.germ U x hx))
⊢ IsPreimmersion (Spec.map (X.presheaf.germ U x hx) ≫ hU.fromSpec)
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInl ≫ X.fromSpecResidueField (Triplet.ofPoint t).x =
    Spec.map (Hom.residueFieldMap (pullback.fst f g) t) ≫ X.fromSpecResidueField ((pullback.fst f g) t)

Tactic:
← pushout.inl_desc _ _ (residueFieldCongr_inv_residueFieldMap_ofPoint t),

Goal state after:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInl ≫ X.fromSpecResidueField (Triplet.ofPoint t).x =
    Spec.map
        (pushout.inl ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x)
            ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y) ≫
          pushout.desc (Hom.residueFieldMap (pullback.fst f g) t) (Hom.residueFieldMap (pullback.snd f g) t) ⋯) ≫
      X.fromSpecResidueField ((pullback.fst f g) t)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
h : I ≤ J
U : ↑X.affineOpens
⊢ glueDataObjHom h U ≫ I.glueDataObjι U = J.glueDataObjι U

Tactic:
glueDataObjHom,

Goal state after:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
U : ↑X.affineOpens
⊢ Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫ I.glueDataObjι U = J.glueDataObjι U
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set R
hs✝ : Ideal.span s✝ = ⊤
s : Finset R
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away ↑i) (Localization.Away ↑i ⊗[R] S)
⊢ FiniteType R S

Tactic:
classical
  let := fun r : s => (Localization.awayMap (algebraMap R S) r).toAlgebra
  set f := algebraMap R S
  constructor
  replace H := fun r => (h r).1
  choose s₁ s₂ using H
  let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f x)) (s₁ x)
  use s.attach.biUnion sf
  convert! (Algebra.adjoin_attach_biUnion (R := R) sf).trans _
  rw [eq_top_iff]
  rintro x -
  apply (⨆ x : s, Algebra.adjoin R (sf x : Set S)).toSubmodule.mem_of_span_eq_top_of_smul_pow_mem
    _ hs _ _
  intro r
  obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
    multiple_mem_adjoin_of_mem_localization_adjoin (Submonoid.powers (r : R))
      (Localization.Away (r : R)) (s₁ r : Set (Localization.Away r.val ⊗[R] S))
      (algebraMap S _ x) (by rw [s₂ r]; trivial)
  rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁
  obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
    IsLocalization.lift_mem_adjoin_finsetIntegerMultiple (Submonoid.powers (r : R)) _ (s₁ r) hn₁
  rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂
  simp_rw [Submonoid.map_powers] at hn₂
  use n₂ + n₁
  exact le_iSup (fun x : s => Algebra.adjoin R (sf x : Set S)) r hn₂

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

Goal state before:
pp: case refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
R : CommRingCatᵒᵖ
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} fun x ↦ Nonempty (F.obj x ≅ R)

Tactic:
refine ⟨.ofObj fun f : { f : Spec R.unop ⟶ X // P f } ↦ .mk _ f.1 f.2, inferInstance, ?_⟩

Goal state after:
case refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
R : CommRingCatᵒᵖ
⊢ (fun x ↦ Nonempty (F.obj x ≅ R)) ≤
    (ObjectProperty.ofObj fun f ↦ MorphismProperty.CostructuredArrow.mk ⊤ ↑f ⋯).isoClosure
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
e_2✝ : ↥s = ↑↑s
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C).g)
f : R ⧸ I := (Ideal.Quotient.mk I) (↑C).f
⊢ ↑(basicOpen (↑C).f) ∩ zeroLocus ↑(RingHom.ker (Ideal.Quotient.mk I)) =
    zeroLocus (Set.range (↑C).g) \ zeroLocus {(↑C).f}

Tactic:
Set.sdiff_eq_compl_inter,

Goal state after:
R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
e_2✝ : ↥s = ↑↑s
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C).g)
f : R ⧸ I := (Ideal.Quotient.mk I) (↑C).f
⊢ ↑(basicOpen (↑C).f) ∩ zeroLocus ↑(RingHom.ker (Ideal.Quotient.mk I)) =
    (zeroLocus {(↑C).f})ᶜ ∩ zeroLocus (Set.range (↑C).g)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y Z : Scheme
⊢ HasAffineProperty @IsClosedImmersion fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Tactic:
convert! HasAffineProperty.of_isZariskiLocalAtTarget @IsClosedImmersion
  refine ⟨fun ⟨h₁, h₂⟩ ↦ of_surjective_of_isAffine _ h₂, by apply isAffine_surjective_of_isAffine⟩

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

Goal state before:
pp: case inr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
⊢ (LinearMap.baseChange I.ResidueField ((Algebra.lmul R A) f)).charpoly =
      X ^ Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) ↔
    ∀ i < Module.finrank R A, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I

Tactic:
LinearMap.charpoly_baseChange,

Goal state after:
case inr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
⊢ Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f)) =
      X ^ Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) ↔
    ∀ i < Module.finrank R A, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
Module: Mathlib.AlgebraicGeometry.Noetherian

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

Tactic:
apply noetherianSpace_of_isAffineOpen (S i).1 (S i).2

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr.convert_3
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
⊢ CompactSpace ↥X

Tactic:
exact Scheme.OpenCover.compactSpace 𝒰

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : IsLocallyNoetherian Y
⊢ IsReduced X

Tactic:
apply +allowSynthFailures @IsReduced.of_openCover (𝒰 := Y.affineCover.pullback₁ f)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : IsLocallyNoetherian Y
⊢ ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    IsReduced ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case inr
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
this : ∀ {X : Scheme} (f : X ⟶ Y), (∃ S, X = Spec S) → UniversallyOpen f
hX : ¬∃ S, X = Spec S
⊢ UniversallyOpen f

pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y : Scheme
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
X : Scheme
f : X ⟶ Y
hX : ∃ S, X = Spec S
⊢ UniversallyOpen f

Tactic:
· refine (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ this _ ⟨_, rfl⟩

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y : Scheme
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
X : Scheme
f : X ⟶ Y
hX : ∃ S, X = Spec S
⊢ UniversallyOpen f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: case a
⊢ universally @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally

Tactic:
exact universally_mono fun X Y f H ↦ ⟨f.isClosedMap.specializingMap, inferInstance⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
this : IsIso (Hom.imageι X.toSpecΓ)
⊢ IsOpenImmersion X.toSpecΓ

Tactic:
rw [← X.toSpecΓ.toImage_imageι]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
this : IsIso (Hom.imageι X.toSpecΓ)
⊢ IsOpenImmersion (Hom.toImage X.toSpecΓ ≫ Hom.imageι X.toSpecΓ)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
f : X ⟶ S
v : n → ↑Γ(X, ⊤)
i : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (homOfVector f v))) (coord S i) = v i

Tactic:
coord,

Goal state after:
n : Type u
S X : Scheme
f : X ⟶ S
v : n → ↑Γ(X, ⊤)
i : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (homOfVector f v))) ((toSpecMvPolyIntEquiv n) (toSpecMvPoly n S) i) = v i
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S✝ : Scheme
R S : CommRingCat
φ : R ⟶ S
⊢ (SpecIso n S).hom ≫ (Arrow.mk (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))))).hom =
    (Arrow.mk (map n (Spec.map φ))).hom ≫ (SpecIso n R).hom

Tactic:
have := (SpecIso n R).inv_hom_id

Goal state after:
n : Type u
S✝ : Scheme
R S : CommRingCat
φ : R ⟶ S
this : (SpecIso n R).inv ≫ (SpecIso n R).hom = 𝟙 (Spec (CommRingCat.of (MvPolynomial n ↑R)))
⊢ (SpecIso n S).hom ≫ (Arrow.mk (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))))).hom =
    (Arrow.mk (map n (Spec.map φ))).hom ≫ (SpecIso n R).hom
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
Y : Type u_2
inst✝² : DecidableEq X
inst✝¹ : Zero Y
inst✝ : Preorder Y
x : X
y : Y
⊢ 0 < single x y ↔ 0 < y

Tactic:
rw [lt_def, coe_single]
  exact Pi.single_pos

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✝¹ : Lattice Y
inst✝ : Zero Y
D₁ D₂ D₃ : locallyFinsuppWithin U Y
h₁₃ : D₁ ≤ D₃
h₂₃ : D₂ ≤ D₃
x : X
⊢ (D₁ ⊔ D₂) x ≤ D₃ x

Tactic:
simp [h₁₃ x, h₂₃ x]

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✝¹ : Lattice Y
inst✝ : Zero Y
D₁ D₂ D₃ : locallyFinsuppWithin U Y
h₁₃ : D₁ ≤ D₂
h₂₃ : D₁ ≤ D₃
x : X
⊢ D₁ x ≤ (D₂ ⊓ D₃) x

Tactic:
simp [h₁₃ x, h₂₃ x]

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

Goal state before:
pp: X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f g : X.PartialMap Y
hfg : f.domain = g.domain
inst✝¹ : IsOver S f
inst✝ : IsOver S g
⊢ f.equiv g ↔ f = g

Tactic:
rw [equiv_iff_of_isSeparated_of_le (S := S) f.dense_domain le_rfl hfg.le]

Goal state after:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f g : X.PartialMap Y
hfg : f.domain = g.domain
inst✝¹ : IsOver S f
inst✝ : IsOver S g
⊢ (f.restrict f.domain ⋯ ⋯).hom = (g.restrict f.domain ⋯ ⋯).hom ↔ f = g
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst✝¹ : IsOver S f
inst✝ : Hom.IsOver g S
⊢ f.equiv (Hom.toPartialMap g) ↔ f.hom = f.domain.ι ≫ g

Tactic:
equiv_iff_of_isSeparated (S := S),

Goal state after:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst✝¹ : IsOver S f
inst✝ : Hom.IsOver g S
⊢ (f.restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom =
      ((Hom.toPartialMap g).restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom ↔
    f.hom = f.domain.ι ≫ g
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
inst✝ : RationalMap.IsOver S f.toRationalMap
f' : X.PartialMap Y
hf₁ : IsOver S f'
hf₂ : f'.toRationalMap = f.toRationalMap
U : X.Opens
hU : Dense ↑U
hUl : U ≤ f'.domain
hUr : U ≤ f.domain
e : (f'.restrict U hU hUl).hom = (f.restrict U hU hUr).hom
⊢ IsOver S (f.restrict U hU hUr)

Tactic:
rw [IsOver, ← e]; infer_instance

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

Goal state before:
pp: X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X ⤏ Y
⊢ (id X).comp f = f

Tactic:
rw [← f.toRationalMap_representative, toRationalMap_comp, PartialMap.id_comp]

Goal state after:
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
x✝² : (a : α) → Y a ⟶ W✝
x✝¹ :
  ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ x✝² a₁ = g₂ ≫ x✝² a₂
x✝ : B ⟶ W✝
hm : ∀ (a : α), (g a ≫ f a) ≫ x✝ = x✝² a
⊢ x✝ = EffectiveEpiFamily.desc X f (fun a ↦ i a ≫ x✝² a) ⋯

Tactic:
apply EffectiveEpiFamily.uniq _ f
    intro a
    rw [← hm a, ← Category.assoc, ← Category.assoc, hi, Category.id_comp]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
hu : IsUnit 2
⊢ IsUnit W.twoTorsionPolynomial.discr ↔ IsUnit W.Δ

Tactic:
twoTorsionPolynomial_discr,

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
hu : IsUnit 2
⊢ IsUnit (16 * W.Δ) ↔ IsUnit W.Δ
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ C⁻¹ * C = 1

Tactic:
rw [mul_def, one_def, inv_def]

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ { u := { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.u * C.u,
      r :=
        { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * ↑C.u ^ 2 +
          C.r,
      s :=
        ↑C.u * { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.s + C.s,
      t :=
        { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.t * ↑C.u ^ 3 +
            { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }.r * C.s *
              ↑C.u ^ 2 +
          C.t } =
    { u := 1, r := 0, s := 0, t := 0 }