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

Goal state before:
pp: case of_sSup_eq_top
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) {ι : Type u} (U : ι → X.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)) →
        stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
· intro X Y f ι U hU hf x
    have hy : x ∈ iSup U := by rw [hU]; trivial
    obtain ⟨i, hi⟩ := Opens.mem_iSup.mp hy
    rw [← hP.cancel_right_isIso _ ((U i).ι.stalkMap ⟨x, hi⟩)]
    simpa [Scheme.Hom.stalkMap_comp] using hf i ⟨x, hi⟩

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↥Y
⊢ CompactSpace ↥(pullback f g)

Tactic:
let 𝒰 := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
⊢ CompactSpace ↥(pullback f g)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ I.height = I.primeHeight

Tactic:
by
  simp [height, primeHeight, Ideal.minimalPrimes_eq_subsingleton_self]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
⊢ (∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n) →
    ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n

pp: case mpr
R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
⊢ (∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n) →
    ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n

Tactic:
· intro H q hq e _
    exact H q hq e

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
⊢ (∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n) →
    ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case StableUnderCompositionWithLocalizationAwayTarget
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 T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
r : S
inst✝ : IsLocalization.Away r T
f : R →+* S
hf : P (Spec.map (CommRingCat.ofHom f))
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap S T)))
⊢ P (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap S T)))

Tactic:
rw [Spec.map_comp]

Goal state after:
case StableUnderCompositionWithLocalizationAwayTarget
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 T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
r : S
inst✝ : IsLocalization.Away r T
f : R →+* S
hf : P (Spec.map (CommRingCat.ofHom f))
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap S T)))
⊢ P (Spec.map (CommRingCat.ofHom (algebraMap S T)) ≫ Spec.map (CommRingCat.ofHom f))
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : ↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f)),
    X.basicOpen s = ⊥ →
      ∀ (x : ↥X) (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
        (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx)) s = 0
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) = ⊥

Tactic:
rw [← Scheme.preimage_basicOpen, hs]

Goal state after:
case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : ↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f)),
    X.basicOpen s = ⊥ →
      ∀ (x : ↥X) (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
        (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx)) s = 0
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
⊢ f ⁻¹ᵁ ⊥ = ⊥
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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ ∀ (i : ↑Us), P ((V i).ι ≫ f ≫ U.ι)

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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ iSup V = ⊤

Tactic:
· intro s
      let f' : (V s).toScheme ⟶ U.ι ⁻¹ᵁ s := f ∣_ U.ι ⁻¹ᵁ s
      have hf' : P f' := IsZariskiLocalAtTarget.restrict hf _
      let e : (U.ι ⁻¹ᵁ s).toScheme ≅ s := IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ s).ι ≫ U.ι) s.1.ι
        (by simpa only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, Scheme.Opens.range_ι,
          Opens.map_coe, Set.image_preimage_eq_iff, heq, Opens.coe_sSup] using! le_sSup s.2)
      have heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ s.1.ι := by
        simp only [V, IsOpenImmersion.isoOfRangeEq_hom_fac, f', e, morphismRestrict_ι_assoc]
      rw [heq, ← Category.assoc]
      refine this _ ?_ ?_
      · rwa [P.cancel_right_of_respectsIso]
      · obtain ⟨a, ha⟩ := hUs s.2
        use a, ha.symm

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ iSup V = ⊤
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I✝ : X.IdealSheafData
I : Ideal ↑Γ(X, ⊤)
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) I) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) I

Tactic:
rw [Ideal.map_map, ← CommRingCat.hom_comp, ← Functor.map_comp]; rfl

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
f : ↑Γ(X, ↑V)
hU : U = X.affineBasicOpen f
⊢ IsLocalization.Away ((Ideal.Quotient.mk (I.ideal V)) f) (↑Γ(X, ↑U) ⧸ I.ideal U)

Tactic:
by
  let := (Ideal.quotientMap _ _ (I.ideal_le_comap_ideal h)).toAlgebra
  let := (X.presheaf.map (homOfLE (X := X.Opens) h).op).hom.toAlgebra
  have : IsLocalization.Away f Γ(X, U) := by
    subst hU; exact V.2.isLocalization_of_eq_basicOpen _ _ rfl
  simp only [IsLocalization.Away, ← Submonoid.map_powers]
  refine IsLocalization.of_surjective _ _ _ Ideal.Quotient.mk_surjective _
    Ideal.Quotient.mk_surjective ?_ ?_
  · simp [RingHom.algebraMap_toAlgebra, Ideal.quotientMap_comp_mk]; rfl
  · simp only [Ideal.mk_ker, RingHom.algebraMap_toAlgebra, I.map_ideal', le_refl]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

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

Tactic:
Iso.trans_hom

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
s : ↑Γ(Y, U)
hs : s ∈ (ker f).ideal ⟨U, hU⟩
hxs : f x ∈ Y.basicOpen s
this : x ∈ f ⁻¹ᵁ Y.basicOpen s
⊢ False

Tactic:
rwa [Scheme.preimage_basicOpen, RingHom.mem_ker.mp (f.ideal_ker_le _ hs),
    Scheme.basicOpen_zero] at this

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

Goal state before:
pp: X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑U ∩ ↑↑V ∩ ↑(X.basicOpen ↑i))

Tactic:
rw [Set.inter_inter_distrib_right]

Goal state after:
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑U ∩ ↑(X.basicOpen ↑i) ∩ (↑↑V ∩ ↑(X.basicOpen ↑i)))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I✝ I J : X.IdealSheafData
h : I ≤ J
U V : J.subschemeCover.openCover.I₀
⊢ pullback.snd (J.subschemeCover.f U) (J.subschemeCover.f V) ≫ J.subschemeCover.f V ≫ J.subschemeι =
    pullback.snd (J.subschemeCover.f U) (J.subschemeCover.f V) ≫ J.glueDataObjι V ≫ (↑V).ι

Tactic:
subschemeCover_map_subschemeι

Goal state after:
X : Scheme
I✝ I J : X.IdealSheafData
h : I ≤ J
U V : J.subschemeCover.openCover.I₀
⊢ pullback.snd (J.subschemeCover.f U) (J.subschemeCover.f V) ≫ J.glueDataObjι V ≫ (↑V).ι =
    pullback.snd (J.subschemeCover.f U) (J.subschemeCover.f V) ≫ J.glueDataObjι V ≫ (↑V).ι
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₀
⊢ (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

Tactic:
simp [IdealSheafData.glueDataObjι, Scheme.Hom.liftQuotient_comp_assoc, pullback.condition]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine ↑U
⊢ IsIso (Scheme.Hom.appTop (f ∣_ U)) ↔ IsIso (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯)

Tactic:
simp only [morphismRestrict_app', TopologicalSpace.Opens.map_top]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine ↑U
⊢ IsIso (Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ⊤) ⋯) ↔ IsIso (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯)
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: ⊢ OfLocalizationSpan @Finite

Tactic:
rw [RingHom.ofLocalizationSpan_iff_finite]
  introv R hs H
  -- We first setup the instances
  let := f.toAlgebra
  let := fun r : s => (Localization.awayMap f r).toAlgebra
  have (r : s) : IsLocalization ((Submonoid.powers (r : R)).map (algebraMap R S))
      (Localization.Away (f r)) := by
    rw [Submonoid.map_powers]; exact Localization.isLocalization
  have : ∀ r : s, IsScalarTower R (Localization.Away (r : R)) (Localization.Away (f r)) :=
    fun r => IsScalarTower.of_algebraMap_eq'
      (IsLocalization.map_comp (Submonoid.powers (r : R)).le_comap_map).symm
  -- By the hypothesis, we may find a finite generating set for each `Sᵣ`. This set can then be
  -- lifted into `R` by multiplying a sufficiently large power of `r`. I claim that the union of
  -- these generates `S`.
  constructor
  replace H := fun r => (H r).1
  choose s₁ s₂ using H
  let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f x)) (s₁ x)
  use s.attach.biUnion sf
  rw [Submodule.span_attach_biUnion, eq_top_iff]
  -- It suffices to show that `r ^ n • x ∈ span T` for each `r : s`, since `{ r ^ n }` spans `R`.
  -- This then follows from the fact that each `x : R` is a linear combination of the generating set
  -- of `Sᵣ`. By multiplying a sufficiently large power of `r`, we can cancel out the `r`s in the
  -- denominators of both the generating set and the coefficients.
  rintro x -
  apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set R) hs _ _
  intro r
  obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
    multiple_mem_span_of_mem_localization_span (Submonoid.powers (r : R))
      (Localization.Away (r : R)) (s₁ r : Set (Localization.Away (f r))) (algebraMap S _ x)
      (by rw [s₂ r]; trivial)
  dsimp only at hn₁
  rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁
  obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
    IsLocalization.smul_mem_finsetIntegerMultiple_span (Submonoid.powers (r : R))
      (Localization.Away (f r)) _ (s₁ r) hn₁
  rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂
  simp_rw [Submonoid.map_powers] at hn₂
  use n₂ + n₁
  exact le_iSup (fun x : s => Submodule.span R (sf x : Set S)) r hn₂

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ IsNoetherian X ↔ ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)

Tactic:
by
  constructor
  · intro h i
    apply (isLocallyNoetherian_iff_of_affine_openCover _).mp
    exact h.toIsLocallyNoetherian
  · intro hNoeth
    convert! IsNoetherian.mk
    · exact (isLocallyNoetherian_iff_of_affine_openCover _).mpr hNoeth
    · exact Scheme.OpenCover.compactSpace 𝒰

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case neg
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
i : Fin n
hi : (e.val i).Monic
i_min : ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
j : Fin n
hj : j ≠ i
hj' : e.val j ≠ 0
⊢ P R e

Tactic:
replace i_min := i_min j hj'

Goal state after:
case neg
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
i : Fin n
hi : (e.val i).Monic
j : Fin n
hj : j ≠ i
hj' : e.val j ≠ 0
i_min : (e.val i).degree ≤ (e.val j).degree
⊢ P R e
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝¹ : Subsingleton ↥Y
inst✝ : IsIntegral Y
⊢ Flat f

Tactic:
refine (MorphismProperty.cancel_right_of_respectsIso @Flat _ Y.isoSpec.hom).mp ?_
  refine (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ ?_
  rw [← Spec.map_preimage (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom),
    HasRingHomProperty.Spec_iff (P := @Flat)]
  exact .of_isField (isField_of_isIntegral_of_subsingleton _) _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp.trans
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x✝ y✝ x y z : (j : J) × F.obj j
a✝¹ : Relation.EqvGen F.ColimitTypeRel x y
a✝ : Relation.EqvGen F.ColimitTypeRel y z
h : ∃ k f g, (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd
h' : ∃ k f g, (ConcreteCategory.hom (F.map f)) y.snd = (ConcreteCategory.hom (F.map g)) z.snd
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) z.snd

Tactic:
obtain ⟨k, f, g, h⟩ := h
      obtain ⟨k', f', g', h'⟩ := h'
      obtain ⟨l, a, b, h''⟩ := span g f'
      refine ⟨l, f ≫ a, g' ≫ b, ?_⟩
      simp only [map_comp, comp_apply, h, ← h']
      simp [← comp_apply, ← map_comp, h'']

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ Scheme.Hom.appTop (isoOfIsAffine n S).hom =
    (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).hom ≫
      CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S))

Tactic:
simp [isoOfIsAffine_hom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inl
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : IsEmpty I
⊢ Nonempty ↥c.pt

Tactic:
have e := (isLimitEquivIsTerminalOfIsEmpty _ _ hc).uniqueUpToIso specULiftZIsTerminal
    exact Nonempty.map e.inv inferInstance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case h
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
x : ↥↑f.domain
⊢ x ∈
    Set.range
      ⇑({ I₀ := ↑{x | ∃ g, ∃ (_ : g.toRationalMap = f), g.domain = x}, X := fun U ↦ ↑↑U, f := fun U ↦ X.homOfLE ⋯ }.f
          ⟨⋯.choose, ⋯⟩)

Tactic:
exact ⟨⟨x.1, (TopologicalSpace.Opens.mem_sSup.mp x.2).choose_spec.2⟩, Subtype.ext (by simp)⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  { obj := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subscheme,
    map := fun {X Y} f ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
x✝² x✝¹ : I
x✝ : x✝² ⟶ x✝¹
⊢ D'.map x✝ ≫ (vanishingIdeal { carrier := Z x✝¹, isClosed' := ⋯ }).subschemeι =
    (vanishingIdeal { carrier := Z x✝², isClosed' := ⋯ }).subschemeι ≫ D.map x✝

Tactic:
by simp [D']

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case e
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
x✝ : ↥X₁
⊢ x✝ ∈ ↑((f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).ι ''ᵁ (f.comp g).hom ⁻¹ᵁ h.domain) ↔
    x✝ ∈ ↑(f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)

Tactic:
comp_hom,

Goal state after:
case e
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
x✝ : ↥X₁
⊢ x✝ ∈
      ↑((f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).ι ''ᵁ
          ((Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv ≫ f.hom ∣_ g.domain ≫ g.hom) ⁻¹ᵁ h.domain) ↔
    x✝ ∈ ↑(f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case H
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y ⟶ Z
⊢ (f.comp (Hom.toPartialMap g)).hom = (X.isoOfEq ⋯).hom ≫ (f.compHom g).hom

Tactic:
comp_hom,

Goal state after:
case H
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y ⟶ Z
⊢ (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ (Hom.toPartialMap g).domain)).inv ≫
      f.hom ∣_ (Hom.toPartialMap g).domain ≫ (Hom.toPartialMap g).hom =
    (X.isoOfEq ⋯).hom ≫ (f.compHom g).hom
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case H
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ ((PartialMap.id X).comp f).hom = (X.isoOfEq ⋯).hom ≫ f.hom

Tactic:
comp_hom,

Goal state after:
case H
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ (Hom.isoImage (PartialMap.id X).domain.ι ((PartialMap.id X).hom ⁻¹ᵁ f.domain)).inv ≫
      (PartialMap.id X).hom ∣_ f.domain ≫ f.hom =
    (X.isoOfEq ⋯).hom ≫ f.hom
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ UniversallyInjective f ↔ Surjective (pullback.diagonal f)

Tactic:
rw [universallyInjective_eq_diagonal]; rfl

Goal state after: