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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
b : ↥(I.glueDataObj ib)
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) a) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) b)
this : (I.glueData.ι ia ≫ I.gluedTo) a = (I.glueData.ι ib ≫ I.gluedTo) b
⊢ ↑((I.glueDataObjι ia) a) = ↑((I.glueDataObjι ib) b)

Tactic:
ι_gluedTo,

Goal state after:
X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
b : ↥(I.glueDataObj ib)
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) a) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) b)
this : (I.glueDataObjι ia ≫ (↑ia).ι) a = (I.glueData.ι ib ≫ I.gluedTo) b
⊢ ↑((I.glueDataObjι ia) a) = ↑((I.glueDataObjι ib) b)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
b : ↥(I.glueDataObj ib)
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) a) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) b)
this : ↑((I.glueDataObjι ia) a) = ↑((I.glueDataObjι ib) b)
f : ↑Γ(X, ↑ia)
g : ↑Γ(X, ↑ib)
hfg : X.basicOpen f = X.basicOpen g
H : ↑((I.glueDataObjι ia) a) ∈ X.basicOpen f
⊢ (I.glueData.ι ia) a = (I.glueData.ι ib) b

Tactic:
have hmem (W) (hW : W = X.affineBasicOpen g) :
      b ∈ Set.range (I.glueDataObjMap (hW.trans_le (X.affineBasicOpen_le g))) := by
    subst hW
    refine (I.opensRange_glueDataObjMap g).ge ?_
    change (I.glueDataObjι ib b).1 ∈ X.basicOpen g
    rwa [← this, ← hfg]

Goal state after:
X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
b : ↥(I.glueDataObj ib)
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) a) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) b)
this : ↑((I.glueDataObjι ia) a) = ↑((I.glueDataObjι ib) b)
f : ↑Γ(X, ↑ia)
g : ↑Γ(X, ↑ib)
hfg : X.basicOpen f = X.basicOpen g
H : ↑((I.glueDataObjι ia) a) ∈ X.basicOpen f
hmem : ∀ (W : ↑X.affineOpens) (hW : W = X.affineBasicOpen g), b ∈ Set.range ⇑(I.glueDataObjMap ⋯)
⊢ (I.glueData.ι ia) a = (I.glueData.ι ib) b
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Set.range ⇑(I.glueData.ι U ≫ I.gluedTo) = ⇑I.gluedTo '' ⇑I.gluedTo ⁻¹' ↑↑U

Tactic:
ι_gluedTo,

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Set.range ⇑(I.glueDataObjι U ≫ (↑U).ι) = ⇑I.gluedTo '' ⇑I.gluedTo ⁻¹' ↑↑U
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact ↑V
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
this✝¹ : IsAffine ↑U
this✝ : IsAffine ↑W
this : CompactSpace ↥↑V
f' : ↑U ⟶ ↑W := Scheme.Hom.resLE f W U hUW
⊢ IsCompact (↑(pullback.fst f g ⁻¹ᵁ U) ⊓ ↑(pullback.snd f g ⁻¹ᵁ V))

Tactic:
let q : Scheme.Opens.toScheme V ⟶ W :=
    IsOpenImmersion.lift W.ι (Scheme.Opens.ι _ ≫ g) <| by simpa [Set.range_comp]

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact ↑V
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
this✝¹ : IsAffine ↑U
this✝ : IsAffine ↑W
this : CompactSpace ↥↑V
f' : ↑U ⟶ ↑W := Scheme.Hom.resLE f W U hUW
q : ↑V ⟶ ↑W := IsOpenImmersion.lift W.ι (V.ι ≫ g) ⋯
⊢ IsCompact (↑(pullback.fst f g ⁻¹ᵁ U) ⊓ ↑(pullback.snd f g ⁻¹ᵁ V))
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme},
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q) →
        ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Z → P (f ≫ g)
hZ : ¬IsAffine Z
U : ↑Z.affineOpens
⊢ P ((f ≫ g) ∣_ ↑U)

Tactic:
rw [morphismRestrict_comp]

Goal state after:
case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme},
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q) →
        ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Z → P (f ≫ g)
hZ : ¬IsAffine Z
U : ↑Z.affineOpens
⊢ P (f ∣_ g ⁻¹ᵁ ↑U ≫ g ∣_ ↑U)
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: 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
Q' : ObjectProperty CommRingCat := fun S ↦ ∃ R ∈ Set.range fun U ↦ Γ(X, U), ∃ f, (CommRingCat.Hom.hom f).FiniteType
this✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} fun x ↦ x ∈ Set.range (unop ∘ F.obj)
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} F.essImage

Tactic:
rw [← ObjectProperty.essentiallySmall_unop_iff]
      refine .of_le (Q := .isoClosure (· ∈ Set.range (Opposite.unop ∘ F.obj))) ?_
      exact fun R ⟨S, e⟩ ↦ ⟨_, ⟨S, rfl⟩, ⟨e.some.unop⟩⟩

Goal state after:
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:
by
  have : IsClosedImmersion (I.inclusion h ≫ I.subschemeι) := by
    simp only [Scheme.IdealSheafData.inclusion_subschemeι]
    infer_instance
  exact .of_comp _ I.subschemeι

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

Goal state before:
pp: case pos
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
⊢ IsClosedImmersion (⋯.isoPullback.inv ≫ IsOpenImmersion.lift (X.affineCover.f i) g hxU)

Tactic:
MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion

Goal state after:
case pos
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
⊢ IsClosedImmersion (IsOpenImmersion.lift (X.affineCover.f i) g hxU)
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
s : Set (PrimeSpectrum R[X])
hs : IsConstructible s
⊢ IsConstructible (comap Polynomial.C '' s)

Tactic:
obtain ⟨S, rfl⟩ := exists_constructibleSetData_iff.mpr hs
  obtain ⟨T, hT, -⟩ := ChevalleyThm.chevalley_polynomialC _ Submodule.mem_top S (by simp)
  rw [hT]
  exact T.isConstructible_toSet

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case Kf
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ ↑U ∩ Set.range ⇑f ⊆ Set.range ⇑f

Tactic:
exact Set.inter_subset_right

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : UniversallyClosed f
⊢ IsProperMap ⇑f

Tactic:
rw [isProperMap_iff_isClosedMap_and_compact_fibers]
  refine ⟨f.continuous, f.isClosedMap, fun y ↦ ?_⟩
  have := compactSpace_of_universallyClosed (pullback.snd f (Y.fromSpecResidueField y))
  rw [← Scheme.range_fromSpecResidueField, ← Scheme.Pullback.range_fst]
  exact isCompact_range (Scheme.Hom.continuous _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hC
n : Type u
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
this :
  (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom
x : ℤ
⊢ ((CommRingCat.Hom.hom f).comp C) { down := x } = ((CommRingCat.Hom.hom g).comp C) { down := x }

Tactic:
simpa [-map_intCast, -eq_intCast] using! DFunLike.congr_fun this (C x)

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₂
⊢ f j₁ ≫ cF.π.app j₁ ≫ F.map g = s.π.app j₂

Tactic:
IsPullback.lift_fst_assoc,

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₁ ≫ F.map g = s.π.app j₂
Module: Mathlib.AlgebraicGeometry.AffineSpace

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

Tactic:
by
        ext1
        · simp only [Category.assoc, homOfVector_over, Category.id_comp]
          rw [← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp, eval₂Hom_comp_C,
            CommRingCat.ofHom_hom, ← Scheme.toSpecΓ_naturality_assoc]
          simp [Scheme.isoSpec]
        · simp

Goal state after:
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₀
j : J
x y : F.obj j
k : J
f f' : j ⟶ k
h : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y
⊢ ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) y

Tactic:
refine ⟨coeq f f', f ≫ coeqHom f f', ?_⟩

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
k : J
f f' : j ⟶ k
h : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y
⊢ (ConcreteCategory.hom (F.map (f ≫ coeqHom f f'))) x = (ConcreteCategory.hom (F.map (f ≫ coeqHom f f'))) y
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
⊢ F.ιColimitType j x = F.ιColimitType j y ↔
    ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) y

Tactic:
rw [ιColimitType_eq_iff_of_isFiltered]
  constructor
  · rintro ⟨k, f, f', h⟩
    refine ⟨coeq f f', f ≫ coeqHom f f', ?_⟩
    nth_rw 2 [coeq_condition]
    simp [h]
  · rintro ⟨k, f, h⟩
    exact ⟨k, f, f, h⟩

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
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV✝ : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝¹ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
this✝ : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
ψY : ↑Γ(Y, UY) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  RingHom.pi fun i ↦ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)
ψ : ↑Γ(X, UX) →ₐ[↑Γ(S, US)] (i : ι) → ↑Γ(X, VX i) :=
  AlgHom.pi fun i ↦ { toRingHom := CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op), commutes' := ⋯ }
hψ : Function.Injective ⇑ψ
hψ' : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id ↑Γ(T, UT) ↑Γ(T, UT)) ψ)
hV : ∀ (i : ι), Function.Injective ⇑(ConcreteCategory.hom (pushoutSection H hUST ⋯ ⋯))
val✝ : Fintype ι
φ : ↑Γ(T, UT) ⊗[↑Γ(S, US)] ((i : ι) → ↑Γ(X, VX i)) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  (RingHom.pi fun i ↦
        (CommRingCat.Hom.hom (pushoutSection H hUST ⋯ ⋯)).comp
          ((CommRingCat.Hom.hom ⋯.isoPushout.hom).comp
            (Pi.evalRingHom (fun i ↦ ↑Γ(T, UT) ⊗[↑Γ(S, US)] ↑Γ(X, VX i)) i))).comp
    (Algebra.TensorProduct.piRight ↑Γ(S, US) ↑Γ(S, US) ↑Γ(T, UT) fun i ↦ ↑Γ(X, VX i)).toRingEquiv.toRingHom
hφ : Function.Injective ⇑φ
e : pushout (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST) ≅
  CommRingCat.of (↑Γ(T, UT) ⊗[↑Γ(S, US)] ↑Γ(X, UX)) :=
  ⋯.isoPushout.symm
this :
  (ψY.comp (CommRingCat.Hom.hom (pushoutSection H hUST hUSX hUY))).comp (CommRingCat.Hom.hom e.inv) =
    φ.comp (Algebra.TensorProduct.map (AlgHom.id ↑Γ(T, UT) ↑Γ(T, UT)) ψ).toRingHom
⊢ Function.Injective ⇑(ConcreteCategory.hom (pushoutSection H hUST hUSX hUY))

Tactic:
by
    refine .of_comp (f := ψY) ?_
    convert (hφ.comp hψ').comp e.commRingCatIsoToRingEquiv.injective
    ext1 x; simpa using! congr($this (e.hom x))

Goal state after:
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₀
c : F.CoconeTypes
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
j : J
x x' : F.obj j
eq✝ : c.ι j x = c.ι j x'
k : J
f f' : j ⟶ k
eq : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
⊢ ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'

Tactic:
refine ⟨coeq f f', f ≫ coeqHom f f', ?_⟩

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
j : J
x x' : F.obj j
eq✝ : c.ι j x = c.ι j x'
k : J
f f' : j ⟶ k
eq : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
⊢ (ConcreteCategory.hom (F.map (f ≫ coeqHom f f'))) x = (ConcreteCategory.hom (F.map (f ≫ coeqHom f f'))) x'
Module: Mathlib.AlgebraicGeometry.AffineSpace

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

Tactic:
rw [geometricallyIrreducible_iff]
  introv K h
  apply ObjectProperty.prop_of_iso _
    ((h.isoIsPullback _ _ (isPullback_map _)) ≪≫ (SpecIso n (.of K))).symm
  infer_instance

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

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

Tactic:
exact fun x ↦ congr(p.1 $(Subsingleton.elim _ _))

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case neg
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
h : ¬f x < 0
⊢ max (n • f x) 0 = n • max (f x) 0

Tactic:
simpa [not_lt.1 h] using nsmul_nonneg (not_lt.1 h) n

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case neg
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
h : ¬-f x < 0
⊢ max (-(n • f x)) 0 = n • max (-f x) 0

Tactic:
simpa [not_lt.1 h] using nsmul_nonneg (not_lt.1 h) n

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝¹ : IrreducibleSpace ↥X
U : X.Opens
x : ↥U
inst✝ : Nonempty ↥↑U
⊢ IsScalarTower ↑Γ(X, U) ↑(X.presheaf.stalk ↑x) ↑X.functionField

Tactic:
apply IsScalarTower.of_algebraMap_eq'

Goal state after:
X : Scheme
inst✝¹ : IrreducibleSpace ↥X
U : X.Opens
x : ↥U
inst✝ : Nonempty ↥↑U
⊢ algebraMap ↑Γ(X, U) ↑X.functionField =
    (algebraMap ↑(X.presheaf.stalk ↑x) ↑X.functionField).comp (algebraMap ↑Γ(X, U) ↑(X.presheaf.stalk ↑x))
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

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

Tactic:
by rwa [iSup_subtype,
    eq_comm]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact ↑U
hV : IsCompact ↑V
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
⊢ ∃ j fji, D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V

Tactic:
obtain ⟨j₂, fj₂i, e₂⟩ := exists_map_preimage_le_map_preimage D c hc hV H.ge

Goal state after:
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact ↑U
hV : IsCompact ↑V
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
j₂ : I
fj₂i : j₂ ⟶ i
e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U
⊢ ∃ j fji, D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V
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)
⊢ Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable

Tactic:
have := tfae_1_iff_4.mpr hf
    refine ⟨f.injective, ?_⟩
    rw [surjective_iff] at hf
    intro x
    algebraize [(f.residueFieldMap x).hom]
    rw [RingHom.IsPurelyInseparable, isPurelyInseparable_iff_subsingleton_emb, subsingleton_iff]
    intro σ₁ σ₂
    apply AlgHom.coe_ringHom_injective
    let g₁ := (X.SpecToEquivOfField _).symm ⟨_, CommRingCat.ofHom σ₁.toRingHom⟩
    let g₂ := (X.SpecToEquivOfField _).symm ⟨_, CommRingCat.ofHom σ₂.toRingHom⟩
    suffices X.SpecToEquivOfField _ g₁ = X.SpecToEquivOfField _ g₂ by
      rw [Equiv.apply_symm_apply, Equiv.apply_symm_apply] at this
      exact congr($(this).2.hom)
    let q := pullback.lift (f := f) (g := f) g₁ g₂ <| by
      simp only [g₁, g₂, Scheme.SpecToEquivOfField_symm_apply, AlgHom.toRingHom_eq_coe,
        Category.assoc, ← f.SpecMap_residueFieldMap_fromSpecResidueField x, ← Spec.map_comp_assoc]
      congr 2
      ext a
      simp only [CommRingCat.hom_comp, RingHom.comp_apply]
      exact (AlgHom.commutes σ₁ a).trans (AlgHom.commutes σ₂ a).symm
    have q_fst : q ≫ pullback.fst f f = g₁ := pullback.lift_fst _ _ _
    have q_snd : q ≫ pullback.snd f f = g₂ := pullback.lift_snd _ _ _
    rw [Scheme.SpecToEquivOfField_eq_iff, ← q_fst, ← q_snd]
    obtain ⟨u, hu⟩ := hf (q (IsLocalRing.closedPoint _))
    have hux : u = x := by
      have := congr(pullback.fst f f $(hu))
      rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply] at this
      simpa [Scheme.SpecToEquivOfField_symm_apply, q_fst, g₁] using this
    refine ⟨by simp [g₁, g₂, q_fst, q_snd], ?_⟩
    dsimp
    simp only [Scheme.descResidueField_stalkClosedPointTo_comp, ← Category.assoc]
    congr 1
    rw [← cancel_mono (Scheme.residueFieldCongr (hux ▸ hu).symm).hom]
    have : Mono (Scheme.Hom.residueFieldMap (pullback.diagonal f) x) :=
      ConcreteCategory.mono_of_injective _ (RingHom.injective _)
    simp [← cancel_mono ((pullback.diagonal f).residueFieldMap x), ← Scheme.residueFieldMap_comp,
      (pullback.fst f f).residueFieldMap_congr', (pullback.snd f f).residueFieldMap_congr'_assoc,
      Scheme.Hom.residueFieldMap_congr (pullback.diagonal_snd f),
      Scheme.Hom.residueFieldMap_congr (pullback.diagonal_fst f)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: case refine_1
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (𝒰.f i) d.toBase
⊢ Set.range ⇑s.snd ⊆ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)

Tactic:
rintro x ⟨x, rfl⟩

Goal state after:
case refine_1
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (𝒰.f i) d.toBase
x : ↥s.pt
⊢ s.snd x ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)
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
⊢ { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
        f := fun x ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }.presieve₀ ∈
    (precoverage P).coverings W

Tactic:
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 (Over.forget S) (f.asOver S) ((𝒰.f _).asOver S)).inv)
        (PreservesPullback.iso_inv_fst _ _ _) x).mp hy
    · dsimp only
      rw [← Over.forget_map, ← PreservesPullback.iso_hom_fst, P.cancel_left_of_respectsIso]
      exact P.pullback_fst _ _ (𝒰.map_prop j)

Goal state after: