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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f

Tactic:
by
  rw [Iso.eq_inv_comp, isoSpec, asIso_hom, ← Scheme.toSpecΓ_naturality_assoc, isoSpec,
    asIso_inv, IsIso.hom_inv_id, Category.comp_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
⊢ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x = 𝟙 ((structurePresheafInModuleCat R M).stalk x)

Tactic:
apply stalk_hom_ext

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
⊢ ∀ (U : Opens ↑(PrimeSpectrum.Top R)) (hxU : x ∈ U),
    (structurePresheafInModuleCat R M).germ U x hxU ≫ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x =
      (structurePresheafInModuleCat R M).germ U x hxU ≫ 𝟙 ((structurePresheafInModuleCat R M).stalk x)
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: D : GlueData (Type v)
x : D.glued
⊢ ∃ i y, (ConcreteCategory.hom (D.ι i)) y = x

Tactic:
delta CategoryTheory.GlueData.ι
  simp_rw [← Multicoequalizer.ι_sigmaπ D.diagram]
  rcases D.types_π_surjective x with ⟨x', rfl⟩
  rw [← dsimp% ConcreteCategory.congr_hom
    (colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom_inv_id x']
  rcases (colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom x' with ⟨i, y⟩
  refine ⟨i, y, ?_⟩
  simp
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : j = k
⊢ IsIso (pullback.snd (D.f' j k) (D.f' j i))

Tactic:
apply +allowSynthFailures pullback_snd_iso_of_left_iso

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : j = k
⊢ IsIso (D.f' j k)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
⊢ v 𝒰 f g i j ⟶ v 𝒰 f g j i

Tactic:
by
  have : HasPullback (pullback.snd _ _ ≫ 𝒰.f i ≫ f) g :=
    hasPullback_assoc_symm (𝒰.f j) (𝒰.f i) (𝒰.f i ≫ f) g
  have : HasPullback (pullback.snd _ _ ≫ 𝒰.f j ≫ f) g :=
    hasPullback_assoc_symm (𝒰.f i) (𝒰.f j) (𝒰.f j ≫ f) g
  refine (pullbackSymmetry ..).hom ≫ (pullbackAssoc ..).inv ≫ ?_
  refine ?_ ≫ (pullbackAssoc ..).hom ≫ (pullbackSymmetry ..).hom
  refine pullback.map _ _ _ _ (pullbackSymmetry _ _).hom (𝟙 _) (𝟙 _) ?_ ?_
  · rw [pullbackSymmetry_hom_comp_snd_assoc, pullback.condition_assoc, Category.comp_id]
  · rw [Category.comp_id, Category.id_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ { I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1}, X := fun x ↦ Sum.elim (fun x ↦ X) (fun x ↦ Y) x,
        f := fun x ↦ Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr) x }.presieve₀ ∈
    (Scheme.precoverage IsOpenImmersion).coverings (X ⨿ Y)

Tactic:
rw [Scheme.presieve₀_mem_precoverage_iff]

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ (∀ (x : ↥(X ⨿ Y)),
      ∃ i,
        x ∈
          Set.range
            ⇑({ I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1}, X := fun x ↦ Sum.elim (fun x ↦ X) (fun x ↦ Y) x,
                    f := fun x ↦ Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr) x }.f
                i)) ∧
    ∀
      (i :
        { I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1}, X := fun x ↦ Sum.elim (fun x ↦ X) (fun x ↦ Y) x,
            f := fun x ↦ Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr) x }.I₀),
      IsOpenImmersion
        ({ I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1}, X := fun x ↦ Sum.elim (fun x ↦ X) (fun x ↦ Y) x,
              f := fun x ↦ Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr) x }.f
          i)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X Y : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ
f' : X ⟶ Y
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop Y) =
    D.ιInvAppπApp U (unop X) ≫ (D.diagramOverOpen U).map f'

Tactic:
induction X with

Goal state after:
case op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
Y : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ
X : WalkingMultispan (MultispanShape.prod D.J)
f' : op X ⟶ Y
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop Y) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map f'
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case convert_2
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
⊢ ⨆ i, Scheme.Hom.opensRange (fi i) = ⊤

Tactic:
simpa [← WalkingPair.equivBool.symm.iSup_comp, iSup_bool_eq, ← codisjoint_iff] using hf.2

Goal state after:
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
⊢ coprod.inl ≫
      coprodComparison Scheme.Spec (op R) (op S) ≫
        Spec.map
          ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
            (opProdIsoCoprod R S).unop.inv) =
    coprod.inl ≫ coprodSpec ↑R ↑S

Tactic:
coprodComparison_inl_assoc,

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
⊢ Scheme.Spec.map coprod.inl ≫
      Spec.map
        ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
          (opProdIsoCoprod R S).unop.inv) =
    coprod.inl ≫ coprodSpec ↑R ↑S
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
H : Disjoint U V
⊢ ∀ (i : Unit ⊕ Unit), IsAffineOpen (Sum.elim (fun x ↦ U) (fun x ↦ V) i)

Tactic:
by simp_all

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:
← IsOpenImmersion.isoOfRangeEq_inv_fac (𝒰.f i) (Scheme.Opens.ι _)
    (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm),

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 (((IsOpenImmersion.isoOfRangeEq (𝒰.f i) (Scheme.Hom.opensRange (𝒰.f i)).ι ⋯).inv ≫ 𝒰.f i) ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
⊢ (targetAffineLocally P).RespectsIso

Tactic:
by
  apply MorphismProperty.RespectsIso.mk
  · introv H U
    rw [morphismRestrict_comp, P.cancel_left_of_respectsIso]
    exact H U
  · introv H
    rintro ⟨U, hU : IsAffineOpen U⟩; dsimp
    have : IsAffine _ := hU.preimage_of_isIso e.hom
    rw [morphismRestrict_comp, P.cancel_right_of_respectsIso]
    exact H ⟨(Opens.map e.hom.base).obj U, hU.preimage_of_isIso e.hom⟩

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:
by
        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.Pullbacks

Goal state before:
pp: R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ pullback.diagonal (Spec.map (ofHom (algebraMap R S))) =
    Spec.map (ofHom (lmul' R).toRingHom) ≫ (pullbackSpecIso R S S).inv

Tactic:
by
  ext1 <;> simp only [pullback.diagonal_fst, pullback.diagonal_snd, ← Spec.map_comp, ← Spec.map_id,
    AlgHom.toRingHom_eq_coe, Category.assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_snd]
  · congr 1; ext x; change x = Algebra.TensorProduct.lmul' R (S := S) (x ⊗ₜ[R] 1); simp
  · congr 1; ext x; change x = Algebra.TensorProduct.lmul' R (S := S) (1 ⊗ₜ[R] x); simp

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
hf : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
g : T
hg : P (algebraMap R (Localization.Away g))
e : S ⊗[R] Localization.Away g ≃ₐ[S] Localization.Away (1 ⊗ₜ[R] g) :=
  IsLocalization.Away.tensorProductEquivTMulRight R S g (Localization.Away g)
⊢ P (algebraMap S (Localization.Away (1 ⊗ₜ[R] g)))

Tactic:
← e.toAlgHom.comp_algebraMap

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
hf : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
g : T
hg : P (algebraMap R (Localization.Away g))
e : S ⊗[R] Localization.Away g ≃ₐ[S] Localization.Away (1 ⊗ₜ[R] g) :=
  IsLocalization.Away.tensorProductEquivTMulRight R S g (Localization.Away g)
⊢ P ((↑↑e).comp (algebraMap S (S ⊗[R] Localization.Away g)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case restrict
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
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens),
    stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f → stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ U)

Tactic:
intro X Y f U hf x

Goal state after:
case restrict
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
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
x : ↥↑(f ⁻¹ᵁ U)
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ∣_ U) x))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case restrict
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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens),
    stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (U.ι ≫ f)

Tactic:
intro X Y f U hf x

Goal state after:
case restrict
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
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
x : ↥↑U
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (U.ι ≫ f) x))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U V : ↑X.affineOpens
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
e : ↥(pullback (↑U).ι (↑V).ι) ≃ₜ ↑(Set.range ⇑g)
⊢ IsCompact (↑↑U ∩ ↑↑V)

Tactic:
IsOpenImmersion.range_pullback_to_base_of_left,

Goal state after:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U V : ↑X.affineOpens
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
e : ↥(pullback (↑U).ι (↑V).ι) ≃ₜ ↑(Set.range ⇑(↑U).ι ∩ Set.range ⇑(↑V).ι)
⊢ IsCompact (↑↑U ∩ ↑↑V)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
this : p.IsPrime
⊢ ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height

Tactic:
obtain ⟨q, hq, e⟩ := Ideal.exists_minimalPrimes_le (h.trans hp.le)

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
this : p.IsPrime
q : Ideal R
hq : q ∈ I.minimalPrimes
e : q ≤ p
⊢ ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal A
⊢ (under R J).height = J.height

Tactic:
rw [(J.comap _).height_eq_inf_minimalPrimes, J.height_eq_inf_minimalPrimes]
  simp only [IsLocalization.minimalPrimes_comap S A, iInf_image]
  apply iInf_congr (fun p ↦ iInf_congr fun hp ↦ ?_)
  have := hp.isPrime
  exact IsLocalization.height_under_eq_of_isPrime S _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case refine_1
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
⊢ { carrier := Sᶜ, is_open' := ⋯ } ⊓ { carrier := Tᶜ, is_open' := ⋯ } = ⊥

Tactic:
ext x
    constructor
    · rintro ⟨hS, hT⟩
      rcases h₁ (show x ∈ ⊤ by trivial) with h | h
      exacts [hS h, hT h]
    · simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
⊢ height x = coheight x

Tactic:
← Order.coheight_orderIso (specOrderIsoPrimeSpectrum R),

Goal state after:
R : CommRingCat
x : ↥(Spec R)
⊢ height x = coheight ((specOrderIsoPrimeSpectrum R) x)
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case mp
X : Scheme
x y : ↥X
⊢ y ∈ Set.range ⇑(X.fromSpecStalk x) → y ∈ {y | y ⤳ x}

pp: case mpr
X : Scheme
x y : ↥X
⊢ y ∈ {y | y ⤳ x} → y ∈ Set.range ⇑(X.fromSpecStalk x)

Tactic:
· rintro ⟨y, rfl⟩
    exact ((IsLocalRing.specializes_closedPoint y).map (X.fromSpecStalk x).continuous).trans
      (specializes_of_eq fromSpecStalk_closedPoint)

Goal state after:
case mpr
X : Scheme
x y : ↥X
⊢ y ∈ {y | y ⤳ x} → y ∈ Set.range ⇑(X.fromSpecStalk x)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
U : Z.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen U

Tactic:
exact hU

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

Goal state before:
pp: case h₀.h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ ((pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
            pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯) ≫
        pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) =
    (𝟙 (pullback (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
        pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)

Tactic:
rw [← cancel_mono (glueDataObjι _ _), ← cancel_mono (Scheme.Opens.ι _)]
        simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
          glueDataT'Aux_fst, limit.lift_π_assoc, cospan_left, glueDataT_fst, Scheme.homOfLE_ι,
          glueDataT'Aux_snd_ι, glueDataT'Aux_fst_assoc, glueDataT_fst_assoc, Category.id_comp]
        rw [pullback.condition_assoc (f := I.glueDataObjι i)]
        simp

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)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(f ⁻¹ᵁ U)
⊢ ∃ U' ≤ U, f ⁻¹ᵁ U' = V

Tactic:
obtain ⟨U', hU', e⟩ := hf₁.isOpen_iff.mp V.2
      exact ⟨⟨U', hU'⟩ ⊓ U, inf_le_right, Opens.ext (by simpa [e] using hVU)⟩

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.ker f).ideal U ≤
    RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso Γ(Y, ↑U)).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)))

Tactic:
have he : f.app U ≫ e.hom =
      (ΓSpecIso Γ(Y, ↑U)).inv ≫ (pullback.snd f U.1.ι ≫ U.1.toSpecΓ).appTop := by
    rw [← (Iso.inv_comp_eq _).mpr U.2.isoSpec_inv_appTop, Category.assoc, Iso.eq_inv_comp]
    simp only [Opens.topIso_hom, eqToHom_op, Hom.app_eq_appLE, Iso.trans_hom, Functor.mapIso_hom,
      Iso.op_hom, eqToIso.hom, Hom.appIso_hom, Hom.appLE_map, Hom.map_appLE, Hom.appLE_comp_appLE,
      Opens.map_top, e, pullback.condition, IsAffineOpen.toSpecΓ_isoSpec_inv, Category.assoc]
    rw [Hom.comp_appLE, Opens.ι_app]
    exact Hom.map_appLE _ _ (homOfLE le_top).op

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).ι) ⊤
he : Hom.app f ↑U ≫ e.hom = (ΓSpecIso Γ(Y, ↑U)).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)
⊢ (Hom.ker f).ideal U ≤
    RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso Γ(Y, ↑U)).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)))
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)
X Y : Scheme
f : X ⟶ Y
hf : P f
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) →
      ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y), P f → IsAffine Y → IsAffineHom f
hY : ¬IsAffine Y
⊢ IsAffineHom f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsAffineHom) _ (iSup_affineOpens_eq_top _)]
    intro U
    exact this P hA _ (IsZariskiLocalAtTarget.restrict hf _) U.2

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

Goal state before:
pp: X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ (I.comapIso f).hom ≫ pullback.fst f I.subschemeι = (I.comap f).subschemeι

Tactic:
rw [← comapIso_inv_subschemeι, Iso.hom_inv_id_assoc]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
⊢ ∃ a b y, ((diagonalCover f 𝒰 𝒱).f ⟨a, (b, b)⟩) y = x

Tactic:
have H : pullback.fst f f x = pullback.snd f f x :=
    hf (by rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.condition])

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
H : (pullback.fst f f) x = (pullback.snd f f) x
⊢ ∃ a b y, ((diagonalCover f 𝒰 𝒱).f ⟨a, (b, b)⟩) y = x
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ IsClosedImmersion (Scheme.Hom.liftCoborder f)

Tactic:
have : IsPreimmersion (f.liftCoborder ≫ f.coborderRange.ι) := by
    simp only [Scheme.Hom.liftCoborder_ι]; infer_instance
  have : IsPreimmersion f.liftCoborder := .of_comp f.liftCoborder f.coborderRange.ι
  refine .of_isPreimmersion _ ?_
  convert! isClosed_preimage_val_coborder
  apply Set.image_injective.mpr f.coborderRange.ι.isEmbedding.injective
  rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.liftCoborder_ι]
  exact (Set.image_preimage_eq_of_subset (by simpa using! subset_coborder)).symm

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

Goal state before:
pp: case hf
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
U : ↑(↑(Hom.coborderRange f)).affineOpens
⊢ Function.Injective ⇑(CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op))

Tactic:
rw [← ConcreteCategory.mono_iff_injective_of_preservesPullback]

Goal state after:
case hf
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
U : ↑(↑(Hom.coborderRange f)).affineOpens
⊢ Mono (X.presheaf.map (eqToHom ⋯).op)
Module: Mathlib.LinearAlgebra.Charpoly.BaseChange

Goal state before:
pp: R : Type u_1
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✝ : Nontrivial R
⊢ (-1) ^ Fintype.card (Module.Free.ChooseBasisIndex R M) *
      ((toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M)) f).charpoly.coeff 0 =
    (-1) ^ Module.finrank R M * f.charpoly.coeff 0

Tactic:
← Module.finrank_eq_card_chooseBasisIndex,

Goal state after:
R : Type u_1
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✝ : Nontrivial R
⊢ (-1) ^ Module.finrank R M *
      ((toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M)) f).charpoly.coeff 0 =
    (-1) ^ Module.finrank R M * f.charpoly.coeff 0