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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) := CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ ((↑U).topIso.hom ≫ (ΓSpecIso Γ(X, ↑U)).inv) ≫ (ΓSpecIso Γ(X, ↑U)).hom ≫ φ = X.presheaf.map (eqToHom ⋯).op ≫ φ

Tactic:
Category.assoc,

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) := CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ (↑U).topIso.hom ≫ (ΓSpecIso Γ(X, ↑U)).inv ≫ (ΓSpecIso Γ(X, ↑U)).hom ≫ φ = X.presheaf.map (eqToHom ⋯).op ≫ φ
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
⊢ Spec.map (X.presheaf.germ V x hxV) ≫
      Spec.map (X.presheaf.map (homOfLE hVU).op) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU =
    (Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f

Tactic:
Category.assoc,

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
⊢ Spec.map (X.presheaf.germ V x hxV) ≫
      Spec.map (X.presheaf.map (homOfLE hVU).op) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU =
    Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV ≫ f
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case mpr
X : Scheme
x y : ↥X
hy : y ⤳ x
this : (X.fromSpecStalk y) (closedPoint ↑(X.presheaf.stalk y)) = y
⊢ y ∈ Set.range ⇑(X.fromSpecStalk x)

Tactic:
rw [← SpecMap_stalkSpecializes_fromSpecStalk hy] at this

Goal state after:
case mpr
X : Scheme
x y : ↥X
hy : y ⤳ x
this : (Spec.map (X.presheaf.stalkSpecializes hy) ≫ X.fromSpecStalk x) (closedPoint ↑(X.presheaf.stalk y)) = y
⊢ y ∈ Set.range ⇑(X.fromSpecStalk x)
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
P' : MorphismProperty Scheme
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q'
h : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
f Y✝ : Scheme
f✝ : f ⟶ Y✝
⊢ (∀ (U : ↑Y✝.affineOpens) (V : ↑f.affineOpens) (e : ↑V ≤ f✝ ⁻¹ᵁ ↑U),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f✝ (↑U) (↑V) e))) ↔
    ∀ (U : ↑Y✝.affineOpens) (V : ↑f.affineOpens) (e : ↑V ≤ f✝ ⁻¹ᵁ ↑U),
      Q' (CommRingCat.Hom.hom (Scheme.Hom.appLE f✝ (↑U) (↑V) e))

Tactic:
simp only [h]

Goal state after:
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
P' : MorphismProperty Scheme
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q'
h : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
⊢ P = P'

Tactic:
ext f
  rw [HasRingHomProperty.eq_affineLocally (P := P), HasRingHomProperty.eq_affineLocally (P := P'),
    affineLocally_iff_affineOpens_le, affineLocally_iff_affineOpens_le]
  simp only [h]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ (Spec.map (inv (Hom.stalkMap U.ι ⟨x, hxU⟩)) ≫ (↑U).fromSpecStalk ⟨x, hxU⟩) ≫ (↑U).toSpecΓ ≫ Spec.map U.topIso.inv =
    Spec.map (X.presheaf.germ U x hxU)

Tactic:
Category.assoc,

Goal state after:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ Spec.map (inv (Hom.stalkMap U.ι ⟨x, hxU⟩)) ≫ (↑U).fromSpecStalk ⟨x, hxU⟩ ≫ (↑U).toSpecΓ ≫ Spec.map U.topIso.inv =
    Spec.map (X.presheaf.germ U x hxU)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ ⊤ ≤ ((F ≫ X.homOfLE ⋯) ≫ (↑U).ι) ⁻¹ᵁ ↑V

Tactic:
Category.assoc,

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ ⊤ ≤ (F ≫ X.homOfLE ⋯ ≫ (↑U).ι) ⁻¹ᵁ ↑V
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ ((Scheme.ΓSpecIso R).hom ≫ (stalkClosedPointIso R).inv) ≫ (stalkClosedPointIso R).hom = (Scheme.ΓSpecIso R).hom

Tactic:
Category.assoc,

Goal state after:
R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ (Scheme.ΓSpecIso R).hom ≫ (stalkClosedPointIso R).inv ≫ (stalkClosedPointIso R).hom = (Scheme.ΓSpecIso R).hom
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case e_a
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : X.Opens
hU : f (closedPoint ↑R) ∈ U
⊢ (Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint ↑R) hU =
    ((Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op).hom ≫ (ΓSpecIso R).hom) ≫ (stalkClosedPointIso R).inv

Tactic:
Category.assoc,

Goal state after:
case e_a
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : X.Opens
hU : f (closedPoint ↑R) ∈ U
⊢ (Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint ↑R) hU =
    (Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op).hom ≫ (ΓSpecIso R).hom ≫ (stalkClosedPointIso R).inv
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case refine_2
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
⊢ (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫ (IsAffineOpen.isoSpec ⋯).inv = (F ≫ X.homOfLE ⋯) ≫ X.homOfLE ⋯

Tactic:
Category.assoc,

Goal state after:
case refine_2
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
⊢ F ≫ (X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫ (IsAffineOpen.isoSpec ⋯).inv = (F ≫ X.homOfLE ⋯) ≫ X.homOfLE ⋯
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case refine_2
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
⊢ F ≫ (X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫ (IsAffineOpen.isoSpec ⋯).inv = (F ≫ X.homOfLE ⋯) ≫ X.homOfLE ⋯

Tactic:
Category.assoc,

Goal state after:
case refine_2
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
⊢ F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom ≫ (IsAffineOpen.isoSpec ⋯).inv = (F ≫ X.homOfLE ⋯) ≫ X.homOfLE ⋯
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case refine_2
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
⊢ F ≫ X.homOfLE ⋯ = (F ≫ X.homOfLE ⋯) ≫ X.homOfLE ⋯

Tactic:
Category.assoc,

Goal state after:
case refine_2
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
⊢ F ≫ X.homOfLE ⋯ = F ≫ X.homOfLE ⋯ ≫ X.homOfLE ⋯
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Spec.map (residueFieldMap f x) ≫ Spec.map (Y.residue (f x)) ≫ Y.fromSpecStalk (f x) =
    (Spec.map (X.residue x) ≫ X.fromSpecStalk x) ≫ f

Tactic:
Category.assoc,

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Spec.map (residueFieldMap f x) ≫ Spec.map (Y.residue (f x)) ≫ Y.fromSpecStalk (f x) =
    Spec.map (X.residue x) ≫ X.fromSpecStalk x ≫ f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫
      (IsAffineOpen.isoSpec ⋯).inv =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯

Tactic:
Category.assoc,

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫
      (X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫
      (X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯

Tactic:
Category.assoc,

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫
      X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom ≫ (IsAffineOpen.isoSpec ⋯).inv =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
          Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
        Spec.map T.tensorInl) ≫
      X.fromSpecResidueField T.x =
    ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl) ≫ X.fromSpecResidueField T.x

Tactic:
Category.assoc,

Goal state after:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫
        Spec.map (tensorCongr ⋯).hom ≫ Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
          Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
        Spec.map T.tensorInr) ≫
      Y.fromSpecResidueField T.y =
    ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr) ≫ Y.fromSpecResidueField T.y

Tactic:
Category.assoc,

Goal state after:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫
        Spec.map (tensorCongr ⋯).hom ≫ Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
⊢ (∃ (e : T₁.fst = T₂.fst), (Spec.map (Triplet.tensorCongr e).inv) T₁.snd = T₂.snd) → T₁ = T₂

Tactic:
· obtain ⟨T, _⟩ := T₁
    obtain ⟨T', _⟩ := T₂
    rintro ⟨rfl : T = T', e⟩
    simpa [e]

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

Goal state before:
pp: case a.inr.refine_1.h
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (appIso (𝒰.f i) ↑⟨⊤, ⋯⟩).inv)

pp: case a.inr.refine_1.H
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ IsPullback (Cover.pullbackHom 𝒰 f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (𝒰.f i) f

Tactic:
· exact (ConcreteCategory.bijective_of_isIso ((𝒰.f i).appIso ⊤).inv).2

Goal state after:
case a.inr.refine_1.H
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ IsPullback (Cover.pullbackHom 𝒰 f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (𝒰.f i) f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this✝ : IsIso (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V =
    pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueData.ι U
⊢ I.glueDataObjMap h ≫ I.glueData.ι V = I.glueData.ι U

Tactic:
rw [← IsIso.inv_comp_eq] at this

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this✝ : IsIso (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V =
    I.glueData.ι U
⊢ I.glueDataObjMap h ≫ I.glueData.ι V = I.glueData.ι U
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case of_basicOpenCover
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
⊢ Ideal.span ↑S = ⊤ → (∀ (r : ↥S), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)) → IsAffine X

Tactic:
hS

Goal state after:
case of_basicOpenCover
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS : Ideal.span ↑S = ⊤
⊢ (∀ (r : ↥S), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)) → IsAffine X
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison forget f g))

Tactic:
refine .of_comp_left (fun x ↦ ?_) <|
    injective_of_mono (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom
  obtain ⟨z, h1, h2⟩ := Pullback.exists_preimage_pullback (f := f) (g := g) x.1.1 x.1.2 x.2
  use z
  ext
  · simp only [Function.comp_apply, Types.pullbackIsoPullback_hom_fst]
    rwa [← types_comp_apply (g := pullback.fst _ _), pullbackComparison_comp_fst]
  · simp only [Function.comp_apply, Types.pullbackIsoPullback_hom_snd]
    rwa [← types_comp_apply (g := pullback.snd _ _), pullbackComparison_comp_snd]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ IsPreimmersion I.gluedTo

Tactic:
by
  rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsPreimmersion)
    _ (iSup_affineOpens_eq_top X)]
  intro U
  rw [← MorphismProperty.cancel_left_of_respectsIso @IsPreimmersion (I.glueDataObjIso U).hom,
    glueDataObjIso_hom_restrict]
  infer_instance

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
⊢ IsAffineHom f

Tactic:
by
  apply isAffineHom_of_forall_exists_isAffineOpen
  intro y
  by_cases hy : y ∈ Set.range f
  · obtain ⟨x, rfl⟩ := hy
    obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ
    obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open hxU (f ⁻¹ᵁ U).isOpen
    obtain ⟨U', hU'U, rfl⟩ : ∃ U' : Y.Opens, U' ≤ U ∧ f ⁻¹ᵁ U' = V := by
      obtain ⟨U', hU', e⟩ := hf₁.isOpen_iff.mp V.2
      exact ⟨⟨U', hU'⟩ ⊓ U, inf_le_right, Opens.ext (by simpa [e] using hVU)⟩
    obtain ⟨r, hrU', hxr⟩ := hU.exists_basicOpen_le ⟨f x, hxV⟩ hxU
    refine ⟨_, hxr, hU.basicOpen r, ?_⟩
    convert hV.basicOpen (f.app _ (Y.presheaf.map (homOfLE hU'U).op r))
    simp only [Scheme.preimage_basicOpen, ← CommRingCat.comp_apply, f.naturality]
    simpa using ((Opens.map f.base).map (homOfLE hrU')).le
  · obtain ⟨_, ⟨U, hU, rfl⟩, hyU, hU'⟩ :=
      Y.isBasis_affineOpens.exists_subset_of_mem_open hy hf₂.isOpen_compl
    rw [Set.subset_compl_iff_disjoint_right, ← Set.preimage_eq_empty_iff] at hU'
    refine ⟨U, hyU, hU, ?_⟩
    convert isAffineOpen_bot _
    exact Opens.ext hU'

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(pullback f (↑U).ι, ⊤) :=
  Functor.mapIso X.presheaf (eqToIso ⋯).op ≪≫ Hom.appIso (pullback.fst f (↑U).ι) ⊤
⊢ Hom.app f ↑U ≫ e.hom =
    ((↑U).topIso.inv ≫ Hom.appTop (IsAffineOpen.isoSpec ⋯).inv) ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)

Tactic:
Category.assoc,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(pullback f (↑U).ι, ⊤) :=
  Functor.mapIso X.presheaf (eqToIso ⋯).op ≪≫ Hom.appIso (pullback.fst f (↑U).ι) ⊤
⊢ Hom.app f ↑U ≫ e.hom =
    (↑U).topIso.inv ≫ Hom.appTop (IsAffineOpen.isoSpec ⋯).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : (Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f U ≫ toImageAux f ≫ imageι f =
    (Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f U ≫ f

Tactic:
simp only [Hom.toImageAux, Cover.ι_glueMorphisms_assoc]

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : (Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).I₀
⊢ (liftQuotient (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ) ((ker f).ideal U) ⋯ ≫ (ker f).subschemeCover.f U) ≫ imageι f =
    (Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f U ≫ f
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case refine_1
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'
S : P.CostructuredArrow ⊤ Scheme.Spec X
f : ↥(Spec (unop (F.obj S))) → ↑(unop (F.obj S))
hqf : ∀ (q : ↥(Spec (unop (F.obj S)))), q ∈ PrimeSpectrum.basicOpen (f q)
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q'.isoClosure (CommRingCat.of (Localization.Away f))

Tactic:
refine ⟨Set.range f, PrimeSpectrum.iSup_basicOpen_eq_top_iff.mp ?_, Set.forall_mem_range.mpr ?_⟩

Goal state after:
case refine_1.refine_1
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'
S : P.CostructuredArrow ⊤ Scheme.Spec X
f : ↥(Spec (unop (F.obj S))) → ↑(unop (F.obj S))
hqf : ∀ (q : ↥(Spec (unop (F.obj S)))), q ∈ PrimeSpectrum.basicOpen (f q)
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ ⨆ i, PrimeSpectrum.basicOpen (f i) = ⊤

case refine_1.refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
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'
S : P.CostructuredArrow ⊤ Scheme.Spec X
f : ↥(Spec (unop (F.obj S))) → ↑(unop (F.obj S))
hqf : ∀ (q : ↥(Spec (unop (F.obj S)))), q ∈ PrimeSpectrum.basicOpen (f q)
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ ∀ (i : ↥(Spec (unop (F.obj S)))), Q'.isoClosure (CommRingCat.of (Localization.Away (f i)))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X✝ : Scheme
X Y : (MorphismProperty.Over @IsClosedImmersion ⊤ X✝)ᵒᵖ
f : X ⟶ Y
⊢ (inv (Scheme.Hom.toImage (unop Y).hom) ≫ (MorphismProperty.Comma.Hom.hom f.unop).left) ≫
      Scheme.Hom.toImage (unop X).hom =
    Scheme.IdealSheafData.inclusion ⋯

Tactic:
Category.assoc,

Goal state after:
X✝ : Scheme
X Y : (MorphismProperty.Over @IsClosedImmersion ⊤ X✝)ᵒᵖ
f : X ⟶ Y
⊢ inv (Scheme.Hom.toImage (unop Y).hom) ≫
      (MorphismProperty.Comma.Hom.hom f.unop).left ≫ Scheme.Hom.toImage (unop X).hom =
    Scheme.IdealSheafData.inclusion ⋯
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsClosedImmersion f
H : Scheme.Hom.ker f ≤ Scheme.Hom.ker g
⊢ lift f g H ≫ Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f = g

Tactic:
simp [lift, -Scheme.Hom.toImage_imageι, g.toImage_imageι]

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun i ↦ (pullback f (𝒰.f i)).affineCover
H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
this : IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
⊢ IsImmersion (pullback.diagonal f)

Tactic:
have : IsImmersion ((pullback.diagonal f ∣_
    diagonalCoverDiagonalRange f 𝒰 𝒱) ≫ Scheme.Opens.ι _) := inferInstance

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun i ↦ (pullback f (𝒰.f i)).affineCover
H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
this✝ : IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
this : IsImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱 ≫ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι)
⊢ IsImmersion (pullback.diagonal f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ IsImmersion (prod.lift (𝟙 X) (𝟙 X))

Tactic:
← MorphismProperty.cancel_right_of_respectsIso @IsImmersion _ (prodIsoPullback X X).hom

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
⊢ IsImmersion (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom)
Module: Mathlib.LinearAlgebra.Charpoly.BaseChange

Goal state before:
pp: R : Type u_3
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
⊢ (baseChange A f).charpoly = Polynomial.map (algebraMap R A) f.charpoly

Tactic:
have := (algebraMap R A).domain_nontrivial

Goal state after:
R : Type u_3
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
⊢ (baseChange A f).charpoly = Polynomial.map (algebraMap R A) f.charpoly