mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : IsAffineHom g
⊢ P (Limits.coprod.desc f g)

Tactic:
rw [HasAffineProperty.eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi] at hf 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 : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this✝ : IsAffineHom f
this : IsAffineHom g
⊢ ∀ (U_1 : X.Opens),
    IsAffineOpen U_1 →
      IsAffineOpen (Limits.coprod.desc f g ⁻¹ᵁ U_1) ∧
        Q (CommRingCat.Hom.hom (Scheme.Hom.app (Limits.coprod.desc f g) U_1))
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: R S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝⁵ : Algebra R S := f.toAlgebra
this✝⁴ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝³ : Algebra R' S' := f'.toAlgebra
this✝² : IsScalarTower R R' S'
this✝¹ : IsScalarTower R S S'
this✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) S'
this : Module.Finite R S
⊢ (IsLocalization.map S' f ⋯).Finite

Tactic:
exact .of_isLocalization R S M

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

Goal state before:
pp: X Y Z : Scheme
I : Z.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ I.comap (f ≫ g) = (I.comap g).comap f

Tactic:
let e : pullback f (I.comap g).subschemeι ≅ pullback (f ≫ g) I.subschemeι :=
    asIso (pullback.map _ _ _ _ (𝟙 _) (I.comapIso g).hom (𝟙 _) (by simp) (by simp)) ≪≫
      pullbackRightPullbackFstIso _ _ _
  rw [comap, comap, ← Scheme.Hom.ker_comp_of_isIso e.hom]
  simp [e]

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

Goal state before:
pp: X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst✝ : IsClosedImmersion i
⊢ Hom.ker (pullback.fst f i) = (Hom.ker i).comap f

Tactic:
delta IdealSheafData.comap

Goal state after:
X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst✝ : IsClosedImmersion i
⊢ Hom.ker (pullback.fst f i) = Hom.ker (pullback.fst f (Hom.ker i).subschemeι)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
⊢ ∀ {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X}, IsPullback f' g' g f → IsImmersion g → IsImmersion g'

Tactic:
g

Goal state after:
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ ∀ {f' : Y' ⟶ Y} {g' : Y' ⟶ X}, IsPullback f' g' g f → IsImmersion g → IsImmersion g'
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 = g

Tactic:
let f' : X' ⟶ Y' := Over.homMk f

Goal state after:
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 ⋯
⊢ f = g
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X✝ Y✝ Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
⊢ ∀ (g : Y ⟶ S),
    IsAffine Y ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g)) →
      IsAffine (Limits.pullback f g) ∧
        Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (Limits.pullback.fst f g)))

Tactic:
g

Goal state after:
X✝ Y✝ Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
⊢ IsAffine Y ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g)) →
    IsAffine (Limits.pullback f g) ∧
      Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (Limits.pullback.fst f g)))
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: case refine_2
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S✝
f✝ : R✝ →+* S✝
hf : f✝.FinitePresentation
s : Set (PrimeSpectrum S✝)
hs : IsConstructible s
R : Type u_1
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
T : Type u_2
inst✝ : CommRing T
f : R →+* S
⊢ ∀ (g : S →+* T),
    (∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)) →
      (∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)) →
        ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap (g.comp f) '' s)

Tactic:
g

Goal state after:
case refine_2
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S✝
f✝ : R✝ →+* S✝
hf : f✝.FinitePresentation
s : Set (PrimeSpectrum S✝)
hs : IsConstructible s
R : Type u_1
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
T : Type u_2
inst✝ : CommRing T
f : R →+* S
g : S →+* T
⊢ (∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)) →
    (∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)) →
      ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap (g.comp f) '' s)
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✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
⊢ IsReduced X

Tactic:
have hpt (Z : _) : IsField (pt Z) :=
    isField_stalk_of_closure_mem_irreducibleComponents _ _ (by
      rw [Z.property.1.closure_genericPoint (isClosed_of_mem_irreducibleComponents _ Z.property)]
      exact Z.property)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
hpt : ∀ (Z : ↑(irreducibleComponents ↥Y)), IsField ↑(pt Z)
⊢ IsReduced X
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst✝² : IsOpenImmersion f
inst✝¹ : GeometricallyIrreducible g
inst✝ : Surjective (f ≫ g)
⊢ GeometricallyIrreducible (f ≫ g)

Tactic:
rw [GeometricallyIrreducible.iff_geometricallyIrreducible_fiber]

Goal state after:
X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst✝² : IsOpenImmersion f
inst✝¹ : GeometricallyIrreducible g
inst✝ : Surjective (f ≫ g)
⊢ ∀ (s : ↥S), GeometricallyIrreducible (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s)
Module: Mathlib.AlgebraicGeometry.Geometrically.Integral

Goal state before:
pp: x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ GeometricallyIntegral x✝ ↔ geometrically IsIntegral x✝

Tactic:
exact geometricallyIntegral_iff _

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
⊢ UniversallyOpen f

Tactic:
wlog hX : ∃ S, X = Spec S generalizing X
  · refine (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ this _ ⟨_, rfl⟩
  obtain ⟨S, rfl⟩ := hX
  wlog hY : ∃ K, Y = Spec K ∧ IsField K generalizing Y
  · have inst : Subsingleton (Spec Γ(Y, ⊤)) := Y.isoSpec.inv.homeomorph.subsingleton
    exact (MorphismProperty.cancel_right_of_respectsIso _ _ Y.isoSpec.hom).mp
      (this _ ⟨_, rfl, isField_of_isIntegral_of_subsingleton _⟩)
  obtain ⟨K, rfl, hK⟩ := hY
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  refine ⟨universally_mk' _ _ fun {T} g _ ↦ ?_⟩
  wlog hT : ∃ R, T = Spec R generalizing T
  · refine (IsZariskiLocalAtTarget.iff_of_openCover T.affineCover).mpr fun i ↦ ?_
    refine (MorphismProperty.cancel_left_of_respectsIso _
      ((pullbackRightPullbackFstIso ..).inv ≫ (pullbackSymmetry ..).hom) _).mp ?_
    simpa [Scheme.Cover.pullbackHom] using! this _ _ ⟨_, rfl⟩
  obtain ⟨R, rfl⟩ := hT
  obtain ⟨ψ, rfl⟩ := Spec.map_surjective g
  algebraize [φ.hom, ψ.hom]
  refine (MorphismProperty.cancel_left_of_respectsIso _ (pullbackSpecIso K R S).inv _).mp ?_
  convert_to! topologically _ (Spec.map <| CommRingCat.ofHom (algebraMap R (TensorProduct K R S)))
  · exact pullbackSpecIso_inv_fst ..
  let := hK.toField
  exact PrimeSpectrum.isOpenMap_comap_algebraMap_tensorProduct_of_field

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

Goal state before:
pp: Z S✝ : Scheme
R S : CommRingCat
φ : R ⟶ S
⊢ IsIntegralHom (Spec.map φ) → topologically (@IsClosedMap) (Spec.map φ)

Tactic:
SpecMap_iff

Goal state after:
Z S✝ : Scheme
R S : CommRingCat
φ : R ⟶ S
⊢ (CommRingCat.Hom.hom φ).IsIntegral → topologically (@IsClosedMap) (Spec.map φ)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
⊢ IsIntegralHom (Spec.map φ)

Tactic:
SpecMap_iff

Goal state after:
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
⊢ (CommRingCat.Hom.hom φ).IsIntegral
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : ↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K))
htU' : t ∈ basicOpen g
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K := (aeval fun i ↦ if i ∈ σ then MvPolynomial.X i else 0).toRingHom
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : t' ∈ basicOpen g
z : ↥(pullback f q)
hzr : (pullback.snd f q) z = t'
hx : ∀ i ∈ σ, (pullback.fst f q) z ∉ (U i).carrier
i : 𝒰.I₀
hi₁ : t ∈ basicOpen (φ (MvPolynomial.X i))
hi₂ : p z ∈ U i
⊢ False

Tactic:
show φ (.X i) = 0 by simpa [φ] using (hx i · hi₂),

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

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
this :
  ∀ (r : ↑Γ(Y, ⊤)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
      (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen ↑r).ι ≅ Spec Γ(X, X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r)) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen ↑r) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ ((pullbackRestrictIsoRestrict f (Y.basicOpen ↑r)).hom ≫
        (X.isoOfEq ⋯).hom ≫ (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r)).toSpecΓ) ≫
      Spec.map (Hom.app f (Y.basicOpen ↑r) ≫ X.presheaf.map (homOfLE ⋯).op) =
    pullback.snd f (Y.basicOpen ↑r).ι ≫ (Y.basicOpen ↑r).toSpecΓ

Tactic:
simp only [homOfLE_leOfHom, Spec.map_comp, Category.assoc,
      Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, Scheme.Opens.toSpecΓ_naturality]

Goal state after:
case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
this :
  ∀ (r : ↑Γ(Y, ⊤)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
      (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen ↑r).ι ≅ Spec Γ(X, X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r)) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen ↑r) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ (pullbackRestrictIsoRestrict f (Y.basicOpen ↑r)).hom ≫
      (X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯ ≫ f ∣_ Y.basicOpen ↑r ≫ (Y.basicOpen ↑r).toSpecΓ =
    pullback.snd f (Y.basicOpen ↑r).ι ≫ (Y.basicOpen ↑r).toSpecΓ
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ (Scheme.Hom.appTop (𝔸(n; S) ↘ S) ≫
        Scheme.Hom.app
          (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
            (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
          ⊤) ≫
      (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).hom =
    (CommRingCat.ofHom C ≫ (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ≫
      (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).hom

Tactic:
rw [← Scheme.Hom.comp_appTop, homOfVector_over, Scheme.Hom.comp_appTop]

Goal state after:
case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ (Scheme.Hom.appTop S.isoSpec.inv ≫ Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom C))) ≫
      (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).hom =
    (CommRingCat.ofHom C ≫ (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ≫
      (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).hom
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

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

Tactic:
obtain ⟨f, h⟩ := h

Goal state after:
case mp.rel
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x✝ y✝ x y : (j : J) × F.obj j
f : x.fst ⟶ y.fst
h : y.snd = (ConcreteCategory.hom (F.map f)) x.snd
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
f : X → Y
h : support f ⊆ U
this : support f = U \ {x | f x = 0 x}
⊢ (∀ᶠ (x : X) in codiscreteWithin U, f x = 0 x) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite

Tactic:
Filter.Eventually,

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
f : X → Y
h : support f ⊆ U
this : support f = U \ {x | f x = 0 x}
⊢ {x | f x = 0 x} ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
W : Set X
inst✝ : Zero Y
f : X → Y
h : LocallyFiniteSupport f
hW : IsCompact W
⊢ (W ∩ support f).Finite

Tactic:
by
  have := LocallyFinite.finite_nonempty_inter_compact
    (LocallyFiniteSupport.locallyFinite_support f h) hW
  have lem {α : Type u_1} (s t : Set α) : {i : s | ({↑i} ∩ t).Nonempty} = (t ∩ s) := by aesop
  rw [← lem f.support W]
  exact Finite.image Subtype.val this

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
⊢ ∃ U, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g

Tactic:
have hxV' : g x ∈ V := e ▸ hxV

Goal state after:
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
⊢ ∃ U, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inl
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : IsEmpty I
⊢ Nonempty ↥c.pt

Tactic:
have e := (isLimitEquivIsTerminalOfIsEmpty _ _ hc).uniqueUpToIso specULiftZIsTerminal

Goal state after:
case inl
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : IsEmpty I
e : c.pt ≅ Spec (CommRingCat.of (ULift.{u, 0} ℤ))
⊢ Nonempty ↥c.pt
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✝ : S.IsSeparated
f : X.PartialMap Y
x✝ : RationalMap.IsOver S f.toRationalMap
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
H : IsOver S (f.restrict U hU hU')
this : IsDominant (X.homOfLE hU')
⊢ (f.compHom (Y ↘ S)).hom = f.domain.ι ≫ X ↘ S

Tactic:
exact ext_of_isDominant (ι := X.homOfLE hU') (by simpa using H.1)

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 : X.PartialMap Y
⊢ ∀ (b : X.PartialMap Y), f ≈ b → f.fromFunctionField = b.fromFunctionField

Tactic:
g

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝ : IrreducibleSpace ↥X
f✝ : X ⤏ Y
f g : X.PartialMap Y
⊢ f ≈ g → f.fromFunctionField = g.fromFunctionField
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsIntegral X
inst✝ : LocallyOfFiniteType sY
f : { f // f.compHom sY = Hom.toRationalMap sX }
⊢ (↑f).fromFunctionField ≫ sY = X.fromSpecStalk (genericPoint ↥X) ≫ sX

Tactic:
obtain ⟨f, hf⟩ := f

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsIntegral X
inst✝ : LocallyOfFiniteType sY
f : X ⤏ Y
hf : f.compHom sY = Hom.toRationalMap sX
⊢ (↑⟨f, hf⟩).fromFunctionField ≫ sY = X.fromSpecStalk (genericPoint ↥X) ≫ sX
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y.PartialMap Z
⊢ f.toRationalMap.comp g.toRationalMap = (f.comp g).toRationalMap

Tactic:
RationalMap.comp_def,

Goal state after:
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y.PartialMap Z
⊢ (f.toRationalMap.representative.comp g).toRationalMap = (f.comp g).toRationalMap
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₂
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
⊢ ∀ (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic →
      (∀ (j : Fin n), j ≠ i → e.val j = 0) →
        ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n e

Tactic:
g

Goal state after:
case hP₂
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
g : InductionObj R n
⊢ ∀ (i : Fin n),
    (g.val i).Monic →
      (∀ (j : Fin n), j ≠ i → g.val j = 0) →
        ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n g
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
U : Set S
κ : Type u_4
inst✝ : Finite κ
s : κ → Set S
hs : ⋃ i, s i = U
H : ∀ (i : κ), IsCompactOpenCovered f (s i)
V : κ → Opens ((i : ι) × X i)
hVeq : ∀ (i : κ), IsCompact (V i).carrier
hVc : ∀ (i : κ), (fun x ↦ f x.fst x.snd) '' (V i).carrier = s i
⊢ IsCompact (⨆ i, V i).carrier

Tactic:
by simpa using isCompact_iUnion hVeq

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
a : α
⊢ f a ≫ x✝ = (𝟙 (X a) ≫ f a) ≫ x✝

Tactic:
Category.id_comp

Goal state after:
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
a : α
⊢ f a ≫ x✝ = f a ≫ x✝