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

Goal state before:
pp: case h₁
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map
      ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
        (opProdIsoCoprod R S).inv.unop ≫ coprod.inl.unop) =
    Spec.map (CommRingCat.ofHom (RingHom.fst ↑R ↑S))

Tactic:
opProdIsoCoprod_inv_inl,

Goal state after:
case h₁
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫ prod.fst) =
    Spec.map (CommRingCat.ofHom (RingHom.fst ↑R ↑S))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case H
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := ⋯
⊢ ∀ (x y : (a : ι) → R a),
    (algebraMap ((a : ι) → R a) (R i)) x = (algebraMap ((a : ι) → R a) (R i)) y ↔
      Function.update 0 i 1 * x = Function.update 0 i 1 * y

pp: case H'
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := ⋯
⊢ Function.Surjective ⇑(algebraMap ((a : ι) → R a) (R i))

Tactic:
· intro x y
      constructor
      · intro e; ext j; by_cases h : j = i <;> aesop
      · intro e; simpa using! congr_fun e i

Goal state after:
case H'
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := ⋯
⊢ Function.Surjective ⇑(algebraMap ((a : ι) → R a) (R i))
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝³ : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : IsIso g
inst✝¹ : IsAffine Z
inst✝ : IsAffine Y
⊢ P (f ≫ g) ↔ P f

Tactic:
by rw [← P.toProperty_apply, ← P.toProperty_apply,
      P.toProperty.cancel_right_of_respectsIso]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ (pullbackSpecIso R S T).hom ≫ Spec.map (ofHom (algebraMap R (S ⊗[R] T))) =
    pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))) ≫
      Spec.map (ofHom (algebraMap R S))

Tactic:
simp [Algebra.TensorProduct.algebraMap_def]

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ (∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)) →
    Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
intro ⟨s, hsone, hs⟩
    use s, hsone, hs

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝ : Q.IsLocal
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : ↥s), Q.diagonal (f ∣_ Y.basicOpen ↑r)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun f ↦ Y.basicOpen ↑f) ⋯
⊢ (targetAffineLocally Q).diagonal f

Tactic:
have (i : _) : IsAffine (𝒰.X i) := (isAffineOpen_top Y).basicOpen i.1

Goal state after:
Q : AffineTargetMorphismProperty
inst✝ : Q.IsLocal
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : ↥s), Q.diagonal (f ∣_ Y.basicOpen ↑r)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun f ↦ Y.basicOpen ↑f) ⋯
this : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ (targetAffineLocally Q).diagonal f
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
⊢ IsZariskiLocalAtSource P.diagonal

Tactic:
let g {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) :=
    pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) (by simp) (by simp)

Goal state after:
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y} f U ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
⊢ IsZariskiLocalAtSource P.diagonal
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
φ : R ⟶ S
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (Spec.map φ) ↔
    ∀ (p : PrimeSpectrum ↑S),
      P (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom φ) ⋯)

pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
φ : R ⟶ S
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ (∀ (p : PrimeSpectrum ↑S),
      P
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom φ)
          ⋯)) ↔
    ∀ (p : Ideal ↑S) (x : p.IsPrime),
      P (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯)

Tactic:
· exact forall_congr' fun p ↦
      (RingHom.toMorphismProperty P).arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso _ _)

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
φ : R ⟶ S
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ (∀ (p : PrimeSpectrum ↑S),
      P
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom φ)
          ⋯)) ↔
    ∀ (p : Ideal ↑S) (x : p.IsPrime),
      P (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case to_basicOpen
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
U : ↑X.affineOpens
hU : ↑U ≤ f ⁻¹ᵁ Y.basicOpen r
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑U) hU))

Tactic:
have : X.basicOpen (f.appLE ⊤ U (by simp) r) = U := by
      simp only [Scheme.Hom.appLE, Opens.map_top, CommRingCat.comp_apply]
      rw [Scheme.basicOpen_res]
      simpa using hU

Goal state after:
case to_basicOpen
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
U : ↑X.affineOpens
hU : ↑U ≤ f ⁻¹ᵁ Y.basicOpen r
this : X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) r) = ↑U
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑U) hU))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
this : ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier
⊢ ∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)

Tactic:
intro U V hU hU' hV hV'

Goal state after:
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
this : ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier
U V : Set ↥X
hU : IsOpen U
hU' : IsCompact U
hV : IsOpen V
hV' : IsCompact V
⊢ IsCompact (U ∩ V)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsQuasiSeparated ↑U

Tactic:
rw [isQuasiSeparated_iff_quasiSeparatedSpace]
  exacts [@AlgebraicGeometry.quasiSeparatedSpace_of_isAffine _ hU, U.isOpen]

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

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) 0
n : ℕ
e : f ^ n * x = f ^ n * 0
⊢ ∃ n, f ^ n * x = 0

Tactic:
exact ⟨n, by simpa [mul_comm x] using e⟩

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

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
⊢ ∃ n, f ^ n * x = 0

Tactic:
obtain ⟨s, hs, e⟩ := isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens.mp ⟨hU, U.2⟩
  replace e : U = iSup fun i : s => (i : X.Opens) := by
    ext1; simpa using e
  have h₁ (i : s) : i.1.1 ≤ U := by
    rw [e]
    exact le_iSup (fun (i : s) => (i : Opens (X.toPresheafedSpace))) _
  have H' := fun i : s =>
    exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen X i.1.2
      (X.presheaf.map (homOfLE (h₁ i)).op x) (X.presheaf.map (homOfLE (h₁ i)).op f) ?_
  swap
  · change (X.presheaf.map (homOfLE _).op) ((X.presheaf.map (homOfLE _).op).hom x) = 0
    have H : (X.presheaf.map (homOfLE _).op) x = 0 := H
    convert! congr_arg (X.presheaf.map (homOfLE _).op).hom H
    · simp only [← CommRingCat.comp_apply, ← Functor.map_comp]
      · rfl
    · rw [map_zero]
    · simp only [Scheme.basicOpen_res, inf_le_right]
  choose n hn using H'
  have := hs.to_subtype
  cases nonempty_fintype s
  use Finset.univ.sup n
  suffices ∀ i : s, X.presheaf.map (homOfLE (h₁ i)).op (f ^ Finset.univ.sup n * x) = 0 by
    subst e
    apply TopCat.Sheaf.eq_of_locally_eq X.sheaf fun i : s => (i : X.Opens)
    intro i
    change _ = (X.sheaf.obj.map _) 0
    rw [map_zero]
    apply this
  intro i
  replace hn :=
    congr_arg (fun x => X.presheaf.map (homOfLE (h₁ i)).op (f ^ (Finset.univ.sup n - n i)) * x)
      (hn i)
  dsimp at hn
  simp only [← map_mul, ← map_pow] at hn
  rwa [mul_zero, ← mul_assoc, ← pow_add, tsub_add_cancel_of_le] at hn
  apply Finset.le_sup (Finset.mem_univ i)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
⊢ ↑(maximalIdeal R).primeHeight = ringKrullDim R

Tactic:
simp [← Ideal.height_eq_primeHeight]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
x : ↥(Spec R)
hx : x ∈ ⊤
hs : s = 0
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0

Tactic:
rw [hs, map_zero]

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

Goal state before:
pp: case inst
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ IsLocalization (Submonoid.powers f) ↑Γ(X, X.basicOpen f)

pp: case hf
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ (ConcreteCategory.hom (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (eqToHom ⋯).op)).comp
      (algebraMap ↑Γ(X, ⊤) ↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f)) =
    algebraMap ↑Γ(X, ⊤) ↑Γ(X, X.basicOpen f)

pp: case inst
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ Algebra ↑Γ(X, ⊤) ↑Γ(X, X.basicOpen f)

Tactic:
· refine isLocalization_basicOpen_of_qcqs ?_ ?_ _
    · exact isCompact_univ
    · exact isQuasiSeparated_univ

Goal state after:
case hf
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ (ConcreteCategory.hom (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (eqToHom ⋯).op)).comp
      (algebraMap ↑Γ(X, ⊤) ↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f)) =
    algebraMap ↑Γ(X, ⊤) ↑Γ(X, X.basicOpen f)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

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

pp: case refine_2
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f →
      ∀ (x : ↥X),
        IsAffine X → IsAffine Y → (∃ R S, Y = Spec R ∧ X = Spec S) → Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ R S, Y = Spec R ∧ X = Spec S
⊢ ∃ R S, Spec Γ(Y, ⊤) = Spec R ∧ Spec Γ(X, ⊤) = Spec S

Tactic:
· rwa [P.cancel_left_of_respectsIso, P.cancel_right_of_respectsIso]

Goal state after:
case refine_2
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f →
      ∀ (x : ↥X),
        IsAffine X → IsAffine Y → (∃ R S, Y = Spec R ∧ X = Spec S) → Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ R S, Y = Spec R ∧ X = Spec S
⊢ ∃ R S, Spec Γ(Y, ⊤) = Spec R ∧ Spec Γ(X, ⊤) = Spec S
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X✝ Y : Scheme
f : X✝ ⟶ Y
U✝ V : X✝.Opens
hU✝ : IsAffineOpen U✝
hV : IsAffineOpen V
X : Scheme
U : Opens ↥X
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
⊢ IsPreimmersion (hU.fromSpecStalk hx)

Tactic:
dsimp [IsAffineOpen.fromSpecStalk]
  have : IsPreimmersion (Spec.map (X.presheaf.germ U x hx)) :=
    letI : Algebra Γ(X, U) (X.presheaf.stalk x) := (X.presheaf.germ U x hx).hom.toAlgebra
    haveI := hU.isLocalization_stalk ⟨x, hx⟩
    IsPreimmersion.of_isLocalization (R := Γ(X, U)) (S := X.presheaf.stalk x)
      (hU.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl
  apply IsPreimmersion.comp

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

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

Tactic:
· rintro rfl; simp

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

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t₁ t₂ : Triplet f g
ex : t₁.x = t₂.x
ey : t₁.y = t₂.y
⊢ t₁ = t₂

Tactic:
cases t₁

Goal state after:
case mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t₂ : Triplet f g
x✝ : ↥X
y✝ : ↥Y
s✝ : ↥S
hx✝ : f x✝ = s✝
hy✝ : g y✝ = s✝
ex : { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x = t₂.x
ey : { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y = t₂.y
⊢ { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ } = t₂
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.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : Nonempty ↥X
inst✝¹ : Nonempty ↥Y
inst✝ : Subsingleton ↥S
this : Nonempty ↥S
⊢ ¬IsEmpty ↥(pullback f g)

Tactic:
AlgebraicGeometry.Scheme.isEmpty_pullback_iff,

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : Nonempty ↥X
inst✝¹ : Nonempty ↥Y
inst✝ : Subsingleton ↥S
this : Nonempty ↥S
⊢ ¬Disjoint (Set.range ⇑f) (Set.range ⇑g)
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hg : Set.range ⇑g = Set.univ
⊢ ⇑f ⁻¹' Set.range ⇑g = Set.univ

Tactic:
rw [hg, Set.preimage_univ]

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

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) f ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
simp only [targetAffineLocally, affineAnd_apply, morphismRestrict_app, CommRingCat.hom_comp,
    hQi.cancel_right_isIso]

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : ↑Y.affineOpens), IsAffine ↑(f ⁻¹ᵁ ↑U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U).ι ''ᵁ ⊤)))) ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥Y
⊢ JacobsonSpace ↥X

Tactic:
wlog hY : ∃ S, Y = Spec S
  · rw [(Scheme.OpenCover.isOpenCover_opensRange (Y.affineCover.pullback₁ f)).jacobsonSpace_iff]
    intro i
    have inst : LocallyOfFiniteType (Y.affineCover.pullbackHom f i) :=
      MorphismProperty.pullback_snd _ _ inferInstance
    have inst : JacobsonSpace Y := ‹_› -- TC gets stuck on the WLOG hypothesis without it.
    have inst : JacobsonSpace (Y.affineCover.X i) :=
      .of_isOpenEmbedding (Y.affineCover.f i).isOpenEmbedding
    let e := ((Y.affineCover.pullback₁ f).f i).isOpenEmbedding.isEmbedding.toHomeomorph
    have := this (Y.affineCover.pullbackHom f i) ⟨_, rfl⟩
    exact .of_isClosedEmbedding e.symm.isClosedEmbedding
  obtain ⟨R, rfl⟩ := hY
  wlog hX : ∃ S, X = Spec S
  · have inst : JacobsonSpace (Spec R) := ‹_› -- TC gets stuck on the WLOG hypothesis without it.
    rw [X.affineCover.isOpenCover_opensRange.jacobsonSpace_iff]
    intro i
    have := this _ (X.affineCover.f i ≫ f) ⟨_, rfl⟩
    let e := (X.affineCover.f i).isOpenEmbedding.isEmbedding.toHomeomorph
    exact .of_isClosedEmbedding e.symm.isClosedEmbedding
  obtain ⟨S, rfl⟩ := hX
  obtain ⟨φ, rfl : Spec.map φ = f⟩ := Spec.homEquiv.symm.surjective f
  have : RingHom.FiniteType φ.hom := HasRingHomProperty.Spec_iff.mp ‹_›
  algebraize [φ.hom]
  have := PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace.mpr ‹_›
  exact PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace.mp (isJacobsonRing_of_finiteType (A := R))

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
⊢ IsPullback (Hom.toImage f) (Hom.liftCoborder f) (Hom.imageι f) (Hom.coborderRange f).ι

Tactic:
refine (isPullback_of_isClosedImmersion _ _ _ _ (by simp) ?_).flip
  rw [Hom.imageι, IdealSheafData.ker_subschemeι]
  ext U : 2
  simp only [IdealSheafData.ideal_comap_of_isOpenImmersion, Opens.ι_appIso, Iso.refl_inv,
    Hom.ker_apply, RingHom.comap_ker, ← CommRingCat.hom_comp]
  dsimp [Opens.toScheme_presheaf_obj]
  rw [RingHomCompTriple.comp_eq, liftCoborder_app,
    CommRingCat.hom_comp, RingHom.ker_comp_of_injective]
  rw [← ConcreteCategory.mono_iff_injective_of_preservesPullback]
  infer_instance

Goal state after:
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
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Module.Basis I R M := Module.Free.chooseBasis R M
i j : I
⊢ (toMatrix (Module.Basis.baseChange A b) (Module.Basis.baseChange A b)) (baseChange A f) i j =
    ((toMatrix b b) f).map (⇑(algebraMap R A)) i j

Tactic:
simp [LinearMap.toMatrix_apply, ← Algebra.algebraMap_eq_smul_one]

Goal state after: