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

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑X.isoSpec.inv ⁻¹' X.zeroLocus s = PrimeSpectrum.zeroLocus s

Tactic:
rw [← toSpecΓ_preimage_zeroLocus, ← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base,
    X.isoSpec_inv_toSpecΓ]

Goal state after:
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑(𝟙 (Spec Γ(X, ⊤))) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus s
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_2
X : Scheme
inst✝ : IsAffine X
s : Set ↥X
⊢ (∃ I, s = X.zeroLocus ↑I) → IsClosed s

Tactic:
rintro ⟨I, rfl⟩

Goal state after:
case refine_2
X : Scheme
inst✝ : IsAffine X
I : Ideal ↑Γ(X, ⊤)
⊢ IsClosed (X.zeroLocus ↑I)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
⊢ (ConcreteCategory.hom (U i).inclusion') ⟨x, hx'⟩ ∈ ⋃ i, ↑(U i)

Tactic:
exact Set.subset_iUnion _ i hx'

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i) ≫
      (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace.inv ≫
          SheafedSpace.forgetToPresheafedSpace.map
            (D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv ≫
              (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv)) =
    (D.ι i).base

Tactic:
SheafedSpace.forgetToPresheafedSpace_map,

Goal state after:
D : GlueData
i : D.J
⊢ (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i) ≫
      (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace.inv ≫
          (D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv ≫
              (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).hom) =
    (D.ι i).base
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ fst (𝒰.f i) (𝒰.f j) ≫ inv (snd f (𝒰.f i)) ≫ fst f (𝒰.f i) = snd (𝒰.f i) (𝒰.f j) ≫ inv (snd f (𝒰.f j)) ≫ fst f (𝒰.f j)

Tactic:
by
    rw [← cancel_epi ((pullbackRightPullbackFstIso _ _ _).hom ≫ map (fst f (𝒰.f i) ≫ f)
      (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd _ _) (𝟙 _) (𝟙 _) (by simp) (by simp))]
    simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁.h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.fst (𝒰.f i ≫ f) g =
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.fst (𝒰.f i ≫ f) g

pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.snd (𝒰.f i ≫ f) g =
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.snd (𝒰.f i ≫ f) g

Tactic:
· simp_rw [Category.assoc, cocycle_snd_fst_fst 𝒰 f g i j k]

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.snd (𝒰.f i ≫ f) g =
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.snd (𝒰.f i ≫ f) g
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : ι
⊢ P (f ∣_ U i)

Tactic:
exact H i

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
i : ι
⊢ P ((X.openCoverOfIsOpenCover Subtype.val ⋯).f ⟨U i, ⋯⟩ ≫ f)

Tactic:
exact H i

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : 𝒰.I₀
⊢ P ((Scheme.Hom.opensRange (𝒰.f i)).ι ≫ f)

Tactic:
rw [← IsOpenImmersion.isoOfRangeEq_inv_fac (𝒰.f i) (Scheme.Opens.ι _)
    (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm), Category.assoc,
    P.cancel_left_of_respectsIso]

Goal state after:
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ f)

Tactic:
exact H i

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
X : Scheme
ι : Type v
inst✝ : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
hf : ∀ (i : ι), P (f i)
⊢ P (Sigma.desc f)

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (Scheme.IsLocallyDirected.openCover _)]
  exact fun i ↦ by simp [hf]

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
⊢ pullback (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅ ?m.62

Tactic:
refine pullbackSymmetry _ _ ≪≫ pullbackRightPullbackFstIso f g _ ≪≫ ?_ ≪≫
          (pullbackRightPullbackFstIso (S.affineCover.f i) g
            (pullback.snd f (S.affineCover.f i))).symm
        exact asIso
          (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simpa using! pullback.condition) (by simp))

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

Goal state before:
pp: case mpr.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V : X.Opens
hV : IsCompact V.carrier
⊢ ∀ (S : X.Opens),
    IsCompact S.carrier → ∀ (U_1 : ↑X.affineOpens), IsCompact (U ⊓ S).carrier → IsCompact (U ⊓ (S ⊔ ↑U_1)).carrier

Tactic:
intro S

Goal state after:
case mpr.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V : X.Opens
hV : IsCompact V.carrier
S : X.Opens
⊢ IsCompact S.carrier → ∀ (U_1 : ↑X.affineOpens), IsCompact (U ⊓ S).carrier → IsCompact (U ⊓ (S ⊔ ↑U_1)).carrier
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
𝒰 : S.OpenCover := S.affineOpenCover.openCover
⊢ IsEmbedding fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)

Tactic:
let 𝒱 (i) := ((𝒰.pullback₁ f).X i).affineOpenCover.openCover

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
𝒰 : S.OpenCover := S.affineOpenCover.openCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).affineOpenCover.openCover
⊢ IsEmbedding fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mpr.refine_2.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
⊢ ∀ (S : X.Opens),
    IsCompact S.carrier → ∀ (U : ↑X.affineOpens), IsCompact (S.carrier ∩ ↑↑V) → IsCompact ((S ⊔ ↑U).carrier ∩ ↑↑V)

Tactic:
intro S

Goal state after:
case mpr.refine_2.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S✝ : X.Opens
x✝ : IsCompact S✝.carrier
V : ↑X.affineOpens
S : X.Opens
⊢ IsCompact S.carrier → ∀ (U : ↑X.affineOpens), IsCompact (S.carrier ∩ ↑↑V) → IsCompact ((S ⊔ ↑U).carrier ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

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

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

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
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H :
  ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (↑V) e))
U : ↑Z.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U
this : IsIso (Scheme.Hom.appLE f (f ''ᵁ ↑V) ↑V ⋯)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (f ''ᵁ ↑V) ⋯))

Tactic:
exact H _ ⟨_, V.2.image_of_isOpenImmersion _⟩ _

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

Goal state before:
pp: case refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
⊢ ∀ (S : X.Opens),
    IsCompact S.carrier →
      ∀ (U : ↑X.affineOpens),
        (IsQuasiSeparated S.carrier →
            ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
              ∃ n y,
                (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
                  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x) →
          IsQuasiSeparated (S ⊔ ↑U).carrier →
            ∀ (f : ↑Γ(X, S ⊔ ↑U)) (x : ↑Γ(X, X.basicOpen f)),
              ∃ n y,
                (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
                  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x

Tactic:
intro S

Goal state after:
case refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
S : X.Opens
⊢ IsCompact S.carrier →
    ∀ (U : ↑X.affineOpens),
      (IsQuasiSeparated S.carrier →
          ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
            ∃ n y,
              (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
                (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x) →
        IsQuasiSeparated (S ⊔ ↑U).carrier →
          ∀ (f : ↑Γ(X, S ⊔ ↑U)) (x : ↑Γ(X, X.basicOpen f)),
            ∃ n y,
              (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
                (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : FiniteRingKrullDim R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ I = IsLocalRing.maximalIdeal R → ↑I.height = ringKrullDim R

Tactic:
· rintro rfl
    exact IsLocalRing.maximalIdeal_height_eq_ringKrullDim

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

Goal state before:
pp: case ofLocalizationSpanTarget
P : MorphismProperty Scheme
inst✝³ : IsZariskiLocalAtTarget P
inst✝² : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f)))
      ((algebraMap S (Localization.Away ↑r)).comp f)
i : (Scheme.affineOpenCoverOfSpanRangeEqTop (fun i ↦ ↑i) ⋯).openCover.I₀
⊢ P (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap S (Localization.Away ↑i))))

Tactic:
exact H i

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ ↑(r + 1) ∧ ↑(r + 1) ≤ J.height

Tactic:
| succ r ih =>

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

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this✝ : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : P g
this : ∀ ⦃Y : Scheme⦄ (g : Y ⟶ S), P g → IsAffine Y → P (pullback.fst f g)
hX : ¬IsAffine Y
i : (Scheme.Pullback.openCoverOfRight Y.affineCover f g).I₀
⊢ P (pullback.fst f (Y.affineCover.f i ≫ g))

Tactic:
apply this _ (comp_of_isOpenImmersion _ _ _ H) inferInstance

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

Goal state before:
pp: X : Scheme
s : Set X.IdealSheafData
this : sSup (ideal '' s) = ⨆ i, (↑i).ideal
⊢ ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (sSup (ideal '' s) U) =
      sSup (ideal '' s) (X.affineBasicOpen f)

Tactic:
simp only [this, iSup_apply, Ideal.map_iSup, map_ideal_basicOpen, implies_true]

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

Goal state before:
pp: X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
inst✝ : Finite ι
⊢ (⨅ i, I i).ideal = ⨅ i, (I i).ideal

Tactic:
simpa using ideal_biInf I Set.finite_univ

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
this✝ : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f)) :=
  (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯).toAlgebra
f' : ↑Γ(X, ↑V) ⧸ I.ideal V := (Ideal.Quotient.mk (I.ideal V)) f
this :
  IsLocalization.Away ((Ideal.Quotient.mk (I.ideal V)) f)
    (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f))
⊢ ↑(PrimeSpectrum.basicOpen f') = ↑(I.glueDataObjι V ⁻¹ᵁ (↑V).ι ⁻¹ᵁ X.basicOpen f)

Tactic:
rw [← comap_basicOpen, ← V.2.fromSpec_preimage_basicOpen,
    ← Scheme.Hom.comp_preimage, glueDataObjι_ι]

Goal state after:
X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
this✝ : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f)) :=
  (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯).toAlgebra
f' : ↑Γ(X, ↑V) ⧸ I.ideal V := (Ideal.Quotient.mk (I.ideal V)) f
this :
  IsLocalization.Away ((Ideal.Quotient.mk (I.ideal V)) f)
    (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f))
⊢ ↑((Opens.comap { toFun := comap (Ideal.Quotient.mk (I.ideal V)), continuous_toFun := ⋯ })
        (IsAffineOpen.fromSpec ⋯ ⁻¹ᵁ X.basicOpen f)) =
    ↑((Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ X.basicOpen f)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this✝ : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
this :
  ∃ V, ∃ (hV : V = X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)), ((CommRingCat.Hom.hom (f.app ↑U)) x |_ V) ⋯ = 0
⊢ ∃ s_1 ∈ Submonoid.powers s, s_1 * x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))

Tactic:
obtain ⟨_, rfl, H⟩ := this

Goal state after:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
H : ((CommRingCat.Hom.hom (f.app ↑U)) x |_ X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)) ⋯ = 0
⊢ ∃ s_1 ∈ Submonoid.powers s, s_1 * x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑X.toTopCat
f : ↑(X.presheaf.obj (op U))
⊢ X.toRingedSpace.basicOpen f = ⊥ ↔ ∀ (x : ↥U), (ConcreteCategory.hom (X.evaluation x)) f = 0

Tactic:
simp only [evaluation_eq_zero_iff_notMem_basicOpen, Subtype.forall]
  exact ⟨fun h ↦ h ▸ fun a _ hc ↦ hc,
    fun h ↦ eq_bot_iff.mpr <| fun a ha ↦ h a (X.toRingedSpace.basicOpen_le f ha) ha⟩

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
⊢ ⨅ i, ker (𝒰.f i ≫ f) = ker f

Tactic:
by
  refine le_antisymm ?_ (le_iInf fun i ↦ (𝒰.f i).le_ker_comp f)
  refine iInf_le_iff.mpr fun I hI U ↦ ?_
  rw [← f.iInf_ker_openCover_map_comp_apply 𝒰, le_iInf_iff]
  exact fun i ↦ hI i U

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x₁ x₂ : ↥X
e : x₁ = x₂
⊢ residueFieldMap f x₁ ≫ (residueFieldCongr e).hom = (residueFieldCongr ⋯).hom ≫ residueFieldMap f x₂

Tactic:
subst e
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X✝¹ : Scheme
U : X✝¹.Opens
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
x : ↥X
⊢ IsPreimmersion (X.fromSpecResidueField x)

Tactic:
dsimp only [Scheme.fromSpecResidueField]
  rw [IsPreimmersion.comp_iff]
  infer_instance

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

Goal state before:
pp: case a.inr.refine_1
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)
⊢ (𝒰.f i) x ∈ Y.zeroLocus ↑((ker f).ideal ⟨𝒰.f i ''ᵁ ↑⟨⊤, ⋯⟩, ⋯⟩) ∩ Set.range ⇑(𝒰.f i)

Tactic:
exact ⟨((coe_support_inter _ _).le ⟨hx, by simp⟩).1, ⟨_, rfl⟩⟩

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ glueDataObjHom ⋯ U = 𝟙 (I.glueDataObj U)

Tactic:
rw [← cancel_mono (I.glueDataObjι U)]
  simp

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

Goal state before:
pp: X : Scheme
I J K : X.IdealSheafData
hIJ : I ≤ J
hJK : J ≤ K
U : ↑X.affineOpens
⊢ glueDataObjHom hJK U ≫ glueDataObjHom hIJ U = glueDataObjHom ⋯ U

Tactic:
rw [← cancel_mono (I.glueDataObjι U)]
  simp

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

Goal state before:
pp: ⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.Finite

Tactic:
intros

Goal state after:
R✝ S✝ : Type u_1
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
e✝ : R✝ ≃+* S✝
⊢ e✝.toRingHom.Finite
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: ⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Module.Finite R T → Module.Finite S (S ⊗[R] T)

Tactic:
intros

Goal state after:
R✝ S✝ T✝ : Type u_1
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S✝
inst✝² : CommRing T✝
inst✝¹ : Algebra R✝ S✝
inst✝ : Algebra R✝ T✝
a✝ : Module.Finite R✝ T✝
⊢ Module.Finite S✝ (S✝ ⊗[R✝] T✝)
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]

Goal state after:
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.unop
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: case h₂
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Algebra.FinitePresentation R T → Algebra.FinitePresentation S (S ⊗[R] T)

Tactic:
intros

Goal state after:
case h₂
R✝ S✝ T✝ : Type u_1
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S✝
inst✝² : CommRing T✝
inst✝¹ : Algebra R✝ S✝
inst✝ : Algebra R✝ T✝
a✝ : Algebra.FinitePresentation R✝ T✝
⊢ Algebra.FinitePresentation S✝ (S✝ ⊗[R✝] T✝)
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
⊢ LinearMap.det (baseChange A f) = (algebraMap R A) (LinearMap.det f)

Tactic:
rw [LinearMap.det_eq_sign_charpoly_coeff, LinearMap.det_eq_sign_charpoly_coeff]

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
⊢ (-1) ^ Module.finrank A (TensorProduct R A M) * (baseChange A f).charpoly.coeff 0 =
    (algebraMap R A) ((-1) ^ Module.finrank R M * f.charpoly.coeff 0)