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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
| U

Tactic:
heq

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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
| sSup Us
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
⊢ I ≤ J → J.support ≤ I.support

Tactic:
h

Goal state after:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
⊢ J.support ≤ I.support
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (I.ideal U)

Tactic:
by
  let φ : Γ(X, U) ⟶ CommRingCat.of (Γ(X, U) ⧸ I.ideal U) :=
    CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
  rw [← Ideal.mk_ker (I := I.ideal _)]
  change RingHom.ker (Spec.map φ ≫ _).appTop.hom = (RingHom.ker φ.hom).comap _
  rw [← RingHom.ker_equiv_comp _ (Scheme.ΓSpecIso _).commRingCatIsoToRingEquiv, RingHom.comap_ker,
    RingEquiv.toRingHom_eq_coe, Iso.commRingCatIsoToRingEquiv_toRingHom, ← CommRingCat.hom_comp,
    ← CommRingCat.hom_comp]
  congr 2
  simp only [Scheme.Hom.comp_app, TopologicalSpace.Opens.map_top, Category.assoc,
    Scheme.ΓSpecIso_naturality, Scheme.Opens.topIso_hom]
  rw [← Scheme.Hom.appTop, U.2.isoSpec_inv_appTop, Category.assoc, Iso.inv_hom_id_assoc]
  simp only [Scheme.Opens.topIso_hom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case mp
X : Scheme
R : CommRingCat
f₁ f₂ : (x : ↥X) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
⊢ f₁ = f₂ → ∃ (h₁ : f₁.fst = f₂.fst), ↑f₁.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑f₂.snd

Tactic:
rintro rfl; simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
f✝ : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
hf : IsLocalHom (CommRingCat.Hom.hom f)
⊢ ⟨x, ⟨f, hf⟩⟩ =
    (fun f ↦ ⟨f (closedPoint ↑R), ⟨Scheme.stalkClosedPointTo f, ⋯⟩⟩)
      ((fun xf ↦ Spec.map ↑xf.snd ≫ X.fromSpecStalk xf.fst) ⟨x, ⟨f, hf⟩⟩)

Tactic:
refine SpecToEquivOfLocalRing_eq_iff.mpr ⟨?_, ?_⟩

Goal state after:
case refine_1
X Y : Scheme
f✝ : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
hf : IsLocalHom (CommRingCat.Hom.hom f)
⊢ ⟨x, ⟨f, hf⟩⟩.fst =
    ((fun f ↦ ⟨f (closedPoint ↑R), ⟨Scheme.stalkClosedPointTo f, ⋯⟩⟩)
        ((fun xf ↦ Spec.map ↑xf.snd ≫ X.fromSpecStalk xf.fst) ⟨x, ⟨f, hf⟩⟩)).fst

case refine_2
X Y : Scheme
f✝ : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
hf : IsLocalHom (CommRingCat.Hom.hom f)
⊢ ↑⟨x, ⟨f, hf⟩⟩.snd =
    (X.presheaf.stalkCongr ⋯).hom ≫
      ↑((fun f ↦ ⟨f (closedPoint ↑R), ⟨Scheme.stalkClosedPointTo f, ⋯⟩⟩)
            ((fun xf ↦ Spec.map ↑xf.snd ≫ X.fromSpecStalk xf.fst) ⟨x, ⟨f, hf⟩⟩)).snd
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: case pos
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 = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
h : l i = 0
⊢ l i ∈ adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

Tactic:
h

Goal state after:
case pos
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 = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
h : l i = 0
⊢ 0 ∈ adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
U' : Y.Opens
hU'U : U' ≤ U
hV : f ⁻¹ᵁ U' ∈ X.affineOpens
hxV : x ∈ ↑(f ⁻¹ᵁ U')
hVU : ↑(f ⁻¹ᵁ U') ⊆ ↑(f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
hrU' : Y.basicOpen r ≤ U'
hxr : ↑⟨f x, hxV⟩ ∈ Y.basicOpen r
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r) =
    X.basicOpen
      ((ConcreteCategory.hom (Scheme.Hom.app f U ≫ X.presheaf.map ((Opens.map f.base).map (homOfLE hU'U).op.unop).op))
        r)

Tactic:
simpa using ((Opens.map f.base).map (homOfLE hrU')).le

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

Goal state before:
pp: Q W : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQW : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → W f
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) f →
    targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ W) f

Tactic:
h

Goal state after:
Q W : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQW : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → W f
X Y : Scheme
f : X ⟶ Y
h : targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) f
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ W) f
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
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : P f
hg : P g
this : IsAffineHom f
⊢ P (Limits.coprod.desc f g)

Tactic:
have := HasAffineProperty.affineAnd_le_isAffineHom P hP g hg

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : P f
hg : P g
this✝ : IsAffineHom f
this : IsAffineHom g
⊢ P (Limits.coprod.desc f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case inst.refine_2
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
i : Y ⟶ Z
f : X ⟶ Y
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
⊢ IsLocallyClosed (Set.range ⇑i)

Tactic:
rw [Set.range_eq_univ.mpr i.surjective]

Goal state after:
case inst.refine_2
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
i : Y ⟶ Z
f : X ⟶ Y
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
⊢ IsLocallyClosed Set.univ
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 : ∑ i ∈ s.attach, l i • ↑i = 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
q : MvPolynomial (Fin n) R
⊢ (∑ x ∈ s.attach, ↑x * l x - 1) * f q = 0

Tactic:
← hl

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 : ∑ i ∈ s.attach, l i • ↑i = 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
q : MvPolynomial (Fin n) R
⊢ (∑ x ∈ s.attach, ↑x * l x - ∑ i ∈ s.attach, l i • ↑i) * f q = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂✝ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
hfinj₂ : ∀ (x : ↑Γ(Y, ⊤)), (ConcreteCategory.hom (Scheme.Hom.appTop f)) x = 0 → x = 0
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
h1 : ∀ (i : 𝒰.I₀), ∃ n, (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ n * g)) = 0
n : ℕ
hn : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ n * g)) = 0
⊢ s ^ ?m.636 x g h U w hx hg s hyv bsle hwle h0 h1 n hn * g = 0

Tactic:
exact hfinj₂ _ (Scheme.zero_of_zero_cover _ _ hn)

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

Goal state before:
pp: W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this✝² : IsSeparated Y'.hom
this✝¹ : IsDominant (Over.Hom.left (equalizer.ι f' g'))
this✝ : Surjective (Over.Hom.left (equalizer.ι f' g'))
this : IsIso (Over.Hom.left (equalizer.ι f' g'))
⊢ Over.Hom.left (equalizer.ι f' g') ≫ f = Over.Hom.left (equalizer.ι f' g') ≫ g

Tactic:
exact congr($(equalizer.condition f' g').left)

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

Goal state before:
pp: P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
y : Spec (of K) ⟶ Y
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
⊢ IsPullback fst snd f y → P Z

Tactic:
h

Goal state after:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
y : Spec (of K) ⟶ Y
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
h : IsPullback fst snd f y
⊢ P Z
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: X✝ Y Z S U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsIntegralHom f
inst✝ : IsIntegralHom g
⊢ IsIntegralHom (Limits.coprod.desc f g)

Tactic:
refine hasAffineProperty.coprodDesc_affineAnd RingHom.isIntegral_respectsIso ?_ _ _ ‹_› ‹_›

Goal state after:
X✝ Y Z S U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsIntegralHom f
inst✝ : IsIntegralHom g
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    f.IsIntegral → g.IsIntegral → (f.prod g).IsIntegral
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
⊢ IsFinite (Spec.map f) ↔ (CommRingCat.Hom.hom f).Finite

Tactic:
HasAffineProperty.iff_of_isAffine (P := @IsFinite),

Goal state after:
R S : CommRingCat
f : R ⟶ S
⊢ IsAffine (Spec S) ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))).Finite ↔ (CommRingCat.Hom.hom f).Finite
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

Tactic:
HasAffineProperty.iff_of_isAffine (P := @IsFinite),

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite ↔ IsIntegralHom f ∧ LocallyOfFiniteType f
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) ↔ IsFinite f ∧ Mono f

Tactic:
HasAffineProperty.iff_of_isAffine (P := @IsFinite),

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Mono f
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsAffine X ∧ Epi (Scheme.Hom.appTop f) ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Mono f

Tactic:
@and_comm (Epi _),

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite ∧ Epi (Scheme.Hom.appTop f) ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Mono f
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case refine_2
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
i : Fin n
hi : (e.val i).Monic
j : Fin n
hj : j ≠ i
hj' : e.val j ≠ 0
i_min : (e.val i).degree ≤ (e.val j).degree
⊢ Polynomial.degree ∘ { val := Function.update e.val j (e.val j %ₘ e.val i) }.val ≠ (ofLex v).1

Tactic:
· simp only [hv, ne_eq, not_forall, funext_iff,
            comp_apply]
          use j
          simp only [update_self]
          refine ((degree_modByMonic_lt _ hi).trans_le i_min).ne

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f✝ : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f✝.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j✝ : I
f : I → (s.pt ⟶ cF.pt) := fun i ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
i j j₁ j₂ : I
g : j₁ ⟶ j₂
⊢ s.π.app j₁ ≫ F.map g = s.π.app j₂

Tactic:
Cone.w

Goal state after:
I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f✝ : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f✝.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j✝ : I
f : I → (s.pt ⟶ cF.pt) := fun i ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
i j j₁ j₂ : I
g : j₁ ⟶ j₂
⊢ s.π.app j₂ = s.π.app j₂
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
h : Relation.EqvGen F.ColimitTypeRel x y
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd

Tactic:
induction h with

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
⊢ (Scheme.ΓSpecIso R).inv ≫
      CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
    CommRingCat.ofHom C

Tactic:
rw [Iso.inv_comp_eq]

Goal state after:
n : Type u
R : CommRingCat
⊢ CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
    (Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom C
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
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h✝ : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
X✝ Y✝ : X.Opens
h : X✝ ⟶ Y✝
⊢ g ⁻¹ᵁ X✝ ⊓ iY ⁻¹ᵁ UT ≤ g ⁻¹ᵁ Y✝ ⊓ iY ⁻¹ᵁ UT

Tactic:
gcongr; exact h.le

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
⊢ S.presheaf.germ U (sY y) ⋯ ≫ Scheme.Hom.stalkMap sY y ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU

Tactic:
h

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) ⋯ ≫ S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x =
    Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: R : CommRingCat
inst✝ : IsDomain ↑R
⊢ PrimeSpectrum.zeroLocus ↑⊥.asIdeal = Set.univ

Tactic:
← PrimeSpectrum.zeroLocus_singleton_zero

Goal state after:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ PrimeSpectrum.zeroLocus ↑⊥.asIdeal = PrimeSpectrum.zeroLocus {0}
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f g : X.PartialMap Y
e : f.domain = g.domain
H : f.hom = (X.isoOfEq e).hom ≫ g.hom
⊢ ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom

Tactic:
exact ⟨e, H⟩

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

Goal state before:
pp: case mp
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
⊢ IsOver S f → f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)

Tactic:
intro h
    obtain ⟨g, hg, e⟩ := f.exists_partialMap_over S
    rw [← e, Hom.toRationalMap, ← compHom_toRationalMap, PartialMap.isOver_iff_eq_restrict.mp hg,
      PartialMap.restrict_toRationalMap]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Over

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝⁶ : W.Over S
inst✝⁵ : X.Over S
inst✝⁴ : Cover.Over S 𝒰
inst✝³ : Hom.IsOver f S
Q : MorphismProperty Scheme
inst✝² : Q.HasOfPostcompProperty Q
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left,
        f := fun x ↦ (pullback.fst (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left }.presieve₀ ∈
    (precoverage P).coverings W

Tactic:
by
    rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, fun j ↦ ?_⟩
    · obtain ⟨i, hy⟩ := Cover.exists_eq (𝒰.pullback₁ f) x
      use i
      exact (mem_range_iff_of_surjective ((𝒰.pullback₁ f).f i) _
        ((PreservesPullback.iso (MorphismProperty.Over.forget Q _ _ ⋙ Over.forget S)
          (f.asOverProp S) ((𝒰.f _).asOverProp S)).inv)
        (PreservesPullback.iso_inv_fst _ _ _) x).mp hy
    · simp only [← CategoryTheory.Over.forget_map]
      rw [MorphismProperty.Comma.toCommaMorphism_eq_hom,
        ← MorphismProperty.Comma.forget_map, ← Functor.comp_map]
      rw [← PreservesPullback.iso_hom_fst, P.cancel_left_of_respectsIso]
      exact P.pullback_fst _ _ (𝒰.map_prop j)

Goal state after: