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

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
R S : CommRingCat
hY : IsAffine (Spec R)
x : ↥(Spec S)
hX : IsAffine (Spec S)
φ : R ⟶ S
hf : P (Spec.map φ)
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))

Tactic:
hQ'.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso φ _)

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
R S : CommRingCat
hY : IsAffine (Spec R)
x : ↥(Spec S)
hX : IsAffine (Spec S)
φ : R ⟶ S
hf : P (Spec.map φ)
⊢ Q'
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) x).asIdeal x.asIdeal
          (CommRingCat.Hom.hom φ) ⋯)))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))
      ((CommRingCat.Hom.hom (Hom.stalkMap f ↑x))
        ((ConcreteCategory.hom (Y.presheaf.germ V ((ConcreteCategory.hom f.base) ↑x) ⋯)) a)) =
    (ConcreteCategory.hom (X.residue ↑x))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a))

Tactic:
LocallyRingedSpace.stalkMap_germ_apply

Goal state after:
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a)) =
    (ConcreteCategory.hom (X.residue ↑x))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝¹ : QuasiCompact f'
this✝ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
e : Γ(X, f ⁻¹ᵁ iV ''ᵁ ↑W) ≅ Γ(U, f' ⁻¹ᵁ ↑W) := Functor.mapIso X.presheaf (eqToIso this).op ≪≫ Hom.appIso iU (f' ⁻¹ᵁ ↑W)
⊢ (Hom.appIso iV ↑W).inv ≫ Hom.app f (iV ''ᵁ ↑W) = Hom.app f' ↑W ≫ e.inv

Tactic:
Iso.inv_comp_eq,

Goal state after:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝¹ : QuasiCompact f'
this✝ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
e : Γ(X, f ⁻¹ᵁ iV ''ᵁ ↑W) ≅ Γ(U, f' ⁻¹ᵁ ↑W) := Functor.mapIso X.presheaf (eqToIso this).op ≪≫ Hom.appIso iU (f' ⁻¹ᵁ ↑W)
⊢ Hom.app f (iV ''ᵁ ↑W) = (Hom.appIso iV ↑W).hom ≫ Hom.app f' ↑W ≫ e.inv
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x) ≫ f = (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ≫ g

Tactic:
simp only [residueFieldCongr_inv, Category.assoc, tensorInl, tensorInr,
    ← Hom.SpecMap_residueFieldMap_fromSpecResidueField]

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ Spec.map
        (pushout.inl ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap f T.x) ≫ S.fromSpecResidueField (f T.x) =
    Spec.map
        (pushout.inr ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap g T.y) ≫ S.fromSpecResidueField (g T.y)
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) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.snd f g =
    (pullback f g).fromSpecResidueField t ≫ pullback.snd f g

Tactic:
· rw [← Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField]
    simp only [Category.assoc, Triplet.specTensorTo_snd]
    rw [← pushout.inr_desc _ _ (residueFieldCongr_inv_residueFieldMap_ofPoint t), Spec.map_comp]
    rfl

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

Goal state before:
pp: X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ QuasiSeparatedSpace ↥X

Tactic:
rw [quasiSeparatedSpace_iff_forall_affineOpens]
  intro U V
  obtain ⟨s', hs', e⟩ := (Ideal.span_eq_top_iff_finite _).mp hs
  rw [← Set.inter_univ (_ ∩ _), ← Opens.coe_top, ← iSup_basicOpen_of_span_eq_top _ _ e,
    ← iSup_subtype'', Opens.coe_iSup, Set.inter_iUnion]
  apply isCompact_iUnion
  intro i
  rw [Set.inter_inter_distrib_right]
  refine (hs₂ i (hs' i.2)).isQuasiSeparated _ _ Set.inter_subset_right
    (U.1.2.inter (X.basicOpen _).2) ?_ Set.inter_subset_right (V.1.2.inter (X.basicOpen _).2) ?_
  · rw [← Opens.coe_inf, ← X.basicOpen_res _ (homOfLE le_top).op]
    exact (U.2.basicOpen _).isCompact
  · rw [← Opens.coe_inf, ← X.basicOpen_res _ (homOfLE le_top).op]
    exact (V.2.basicOpen _).isCompact

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

Goal state before:
pp: case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y),
    (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty f →
      (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty (f ≫ e.hom)

Tactic:
intro X Y Z e f ⟨hZ, hf⟩

Goal state after:
case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
hZ : IsAffine Y
hf : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
⊢ (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty (f ≫ e.hom)
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' : Type u_4
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)
n : ℕ
hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ ↑A.toSubsemiring
hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)
a : ↥M
ha₂ : ↑a * x' = ↑a * (↑y ^ n * x)
⊢ ↑a * (↑y ^ n * x) = x' * ↑a

Tactic:
← ha₂,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
S' : Type u_4
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)
n : ℕ
hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ ↑A.toSubsemiring
hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)
a : ↥M
ha₂ : ↑a * x' = ↑a * (↑y ^ n * x)
⊢ ↑a * x' = x' * ↑a
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
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) ↔
    ∀ {X Y : Scheme} (f : X ⟶ Y),
      P f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
by
  simp_rw [isAffineHom_iff]
  refine ⟨fun h X Y f ↦ ?_, fun h ↦ ⟨affineAnd_isLocal hQi hQl hQs, ?_⟩⟩
  · rw [eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi]
    lia
  · ext X Y f
    rw [targetAffineLocally_affineAnd_iff hQi, h f]
    aesop

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

Goal state before:
pp: case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun X x x_1 x_2 ↦ IsAffine X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
⊢ IsAffineOpen (U ⊓ V)

Tactic:
dsimp at H

Goal state after:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁] [IsOpenImmersion f₂],
    IsAffine (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
⊢ IsAffineOpen (U ⊓ V)
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ map (RingHom.id R) = id

Tactic:
by ext : 1; simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
t : Finset A := Finset.image (fun g ↦ (Ideal.Quotient.mk I) (g' g)) Finset.univ
⊢ (Ideal.Quotient.mk I) (∑ g, g' g * h' g) - (Ideal.Quotient.mk I) 1 = 0

Tactic:
← map_sub,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
t : Finset A := Finset.image (fun g ↦ (Ideal.Quotient.mk I) (g' g)) Finset.univ
⊢ (Ideal.Quotient.mk I) (∑ g, g' g * h' g - 1) = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
I J : X.IdealSheafData
h : I ≤ J
⊢ IsClosedImmersion (Scheme.IdealSheafData.inclusion h)

Tactic:
have : IsClosedImmersion (I.inclusion h ≫ I.subschemeι) := by
    simp only [Scheme.IdealSheafData.inclusion_subschemeι]
    infer_instance

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
I J : X.IdealSheafData
h : I ≤ J
this : IsClosedImmersion (Scheme.IdealSheafData.inclusion h ≫ I.subschemeι)
⊢ IsClosedImmersion (Scheme.IdealSheafData.inclusion h)
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
h : topologicalKrullDim ↥X ≤ 0
U : ↑X.affineOpens
⊢ IsArtinianRing ↑Γ(X, ↑U)

Tactic:
have _ : IsNoetherianRing Γ(X, U) := IsLocallyNoetherian.component_noetherian U

Goal state after:
X : Scheme
inst✝ : IsLocallyNoetherian X
h : topologicalKrullDim ↥X ≤ 0
U : ↑X.affineOpens
x✝ : IsNoetherianRing ↑Γ(X, ↑U)
⊢ IsArtinianRing ↑Γ(X, ↑U)
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : GeometricallyIrreducible f
inst✝² : GeometricallyIrreducible g
inst✝¹ : UniversallyOpen f
inst✝ : UniversallyOpen g
K : Type u_1
x✝ : Field K
x : Spec (CommRingCat.of K) ⟶ Z
⊢ IrreducibleSpace ↥(pullback (f ≫ g) x)

Tactic:
rw [← (pullbackRightPullbackFstIso g x f).hom.homeomorph.irreducibleSpace_iff]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : GeometricallyIrreducible f
inst✝² : GeometricallyIrreducible g
inst✝¹ : UniversallyOpen f
inst✝ : UniversallyOpen g
K : Type u_1
x✝ : Field K
x : Spec (CommRingCat.of K) ⟶ Z
⊢ IrreducibleSpace ↥(pullback f (pullback.fst g x))
Module: Mathlib.AlgebraicGeometry.Geometrically.Integral

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝⁴ : GeometricallyIntegral f
inst✝³ : Flat f
inst✝² : UniversallyOpen f
inst✝¹ : IsIntegral S
inst✝ : IsLocallyNoetherian S
⊢ IsIntegral X

Tactic:
isIntegral_iff_irreducibleSpace_and_isReduced

Goal state after:
X S : Scheme
f : X ⟶ S
inst✝⁴ : GeometricallyIntegral f
inst✝³ : Flat f
inst✝² : UniversallyOpen f
inst✝¹ : IsIntegral S
inst✝ : IsLocallyNoetherian S
⊢ IrreducibleSpace ↥X ∧ IsReduced X
Module: Mathlib.AlgebraicGeometry.Geometrically.Integral

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝² : GeometricallyIntegral f
inst✝¹ : Subsingleton ↥S
inst✝ : IsIntegral S
⊢ IsIntegral X

Tactic:
isIntegral_iff_irreducibleSpace_and_isReduced

Goal state after:
X S : Scheme
f : X ⟶ S
inst✝² : GeometricallyIntegral f
inst✝¹ : Subsingleton ↥S
inst✝ : IsIntegral S
⊢ IrreducibleSpace ↥X ∧ IsReduced X
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
⊢ Scheme.Hom.appTop (SpecIso n R).hom =
    (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).hom ≫
      CommRingCat.ofHom
        (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
          (coord (Spec R)))

Tactic:
by
  ext i
  simp [SpecIso]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (SpecIso n R).inv)) (coord (Spec R) i) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i)

Tactic:
simp only [SpecIso, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv, Scheme.Spec_map,
    Quiver.Hom.unop_op, TopologicalSpace.Opens.map_top, Scheme.Hom.comp_app, CommRingCat.comp_apply]
  rw [isoOfIsAffine_inv_appTop_coord, ← CommRingCat.comp_apply, ← Scheme.ΓSpecIso_inv_naturality,
      CommRingCat.comp_apply]
  congr 1
  exact map_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✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
⊢ (Function.support fun z ↦ if hz : z ∈ V then D z else 0) ⊆ V

Tactic:
intro x hx
    simp_rw [dite_eq_ite, mem_support, ne_eq, ite_eq_right_iff, Classical.not_imp] at hx
    exact hx.1

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 iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
⊢ IsIso (pushoutSection ⋯ hUSX hUST ⋯)

Tactic:
exact isIso_pushoutSection_of_isQuasiSeparated_of_flat_right _ _ _ _ hUS hUX hUT hUT'

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ UniversallyInjective f ↔ Surjective (pullback.diagonal f)

Tactic:
by
  rw [universallyInjective_eq_diagonal]; rfl

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
hf : Surjective (pullback.diagonal f)
this : UniversallyInjective f
⊢ Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable

Tactic:
refine ⟨f.injective, ?_⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
hf : Surjective (pullback.diagonal f)
this : UniversallyInjective f
⊢ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
⊢ TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (X.directedAffineCover.f i))

Tactic:
by
    convert! X.isBasis_affineOpens
    simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inr
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✝³ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a b : D.obj i ⟶ X
ha : t.app i = a ≫ f
hb : t.app i = b ≫ f
hab : c.π.app i ≫ a = c.π.app i ≫ b
this : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover, h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
k : A.𝒰D.I₀ → I
hki' : (j : A.𝒰D.I₀) → k j ⟶ A.i'
heq :
  ∀ (j : A.𝒰D.I₀),
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b
𝒰Df : (D.obj A.i').OpenCover := A.𝒰D.finiteSubcover
h : Nonempty ↥(D.obj A.i')
⊢ ∃ k hik, D.map hik ≫ a = D.map hik ≫ b

Tactic:
let O : Finset I := {A.i'} ∪ Finset.univ.image (fun i : 𝒰Df.I₀ ↦ k <| A.𝒰D.idx i.1)

Goal state after:
case inr
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✝³ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a b : D.obj i ⟶ X
ha : t.app i = a ≫ f
hb : t.app i = b ≫ f
hab : c.π.app i ≫ a = c.π.app i ≫ b
this : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover, h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
k : A.𝒰D.I₀ → I
hki' : (j : A.𝒰D.I₀) → k j ⟶ A.i'
heq :
  ∀ (j : A.𝒰D.I₀),
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b
𝒰Df : (D.obj A.i').OpenCover := A.𝒰D.finiteSubcover
h : Nonempty ↥(D.obj A.i')
O : Finset I := {A.i'} ∪ Finset.image (fun i ↦ k (Cover.idx A.𝒰D ↑i)) Finset.univ
⊢ ∃ k hik, D.map hik ≫ a = D.map hik ≫ b
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_3
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.499} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.499} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
m : d.gluedCocone.pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone.ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
this :
  (d.pullbackGluedIso i).inv ≫ (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).map m =
    (d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)
⊢ 𝒱.f i ≫ m.left =
    ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
      pullback.fst s.pt.hom (𝒰.f i)

Tactic:
simp [𝒱, ← this]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W.map f).polynomialX = Polynomial.map (mapRingHom f) W.polynomialX

Tactic:
by
  simp only [polynomialX]
  map_simp

Goal state after: