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

Goal state before:
pp: R : CommRingCat
x : PrimeSpectrum ↑R
⊢ CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal)) ≫ (stalkIso R x).inv =
    (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial

Tactic:
by
  ext s : 2
  exact (IsLocalization.algEquiv _ ((structureSheaf R).presheaf.stalk _) _).symm.commutes s

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : IsOpen s
⊢ IsOpen[inst✝] (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s)

Tactic:
rw [(ofOpenSubsets U).isOpen_iff] at hs

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
⊢ IsOpen[inst✝] (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
S : Set ↑↑(D.V (i, j))
eq₁ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.fst (D.f i j) (D.f i k)).base
eq₂ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.snd (D.f i j) (D.f i k)).base
⊢ ⇑(ConcreteCategory.hom (pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)))) ''
      ⇑(ConcreteCategory.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom) ''
        ⇑(ConcreteCategory.hom (pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)))) ∘
            ⇑(ConcreteCategory.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom) ⁻¹'
          S =
    ⇑(ConcreteCategory.hom (D.f i k).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) '' S

Tactic:
Set.preimage_comp,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
S : Set ↑↑(D.V (i, j))
eq₁ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.fst (D.f i j) (D.f i k)).base
eq₂ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.snd (D.f i j) (D.f i k)).base
⊢ ⇑(ConcreteCategory.hom (pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)))) ''
      ⇑(ConcreteCategory.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom) ''
        ⇑(ConcreteCategory.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom) ⁻¹'
          ⇑(ConcreteCategory.hom (pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)))) ⁻¹' S =
    ⇑(ConcreteCategory.hom (D.f i k).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) '' S
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫
      invApp (pullback.snd (D.f i j) (D.f i k))
          (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).1 (unop (op U))))) ≫
        (D.V (i, k)).presheaf.map (eqToHom ⋯)

Tactic:
← cancel_epi (inv ((D.f_open i j).invApp _ U)),

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ inv (invApp (D.f i j) U) ≫ invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    inv (invApp (D.f i j) U) ≫
      (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫
        invApp (pullback.snd (D.f i j) (D.f i k))
            (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).1 (unop (op U))))) ≫
          (D.V (i, k)).presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h₀
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))

pp: case h₁
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))

Tactic:
· apply glued_cover_cocycle_fst

Goal state after:
case h₁
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ ∃ (eq :
    (Opens.map (D.t k i).base).op.obj (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) =
      op
        ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).obj
          (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))),
    invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
        (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
          (D.V (k, i)).presheaf.map (eqToHom eq) =
      (D.t' k i j).c.app (op U) ≫
        invApp (pullback.fst (D.f k i) (D.f k j)) (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U)))))

Tactic:
fconstructor
  -- Porting note: I don't know what the magic was in Lean3 proof, it just skipped the proof of `eq`
  · delta IsOpenImmersion.opensFunctor IsOpenEmbedding.functor
    dsimp only [Functor.op, Opens.map_def, IsOpenMap.functor, unop_op, Opens.coe_mk]
    congr 2
    have := (𝖣.t_fac k i j).symm
    rw [← IsIso.inv_comp_eq] at this
    replace this := (congr_arg ((PresheafedSpace.Hom.base ·)) this).symm
    replace this := congr_arg (TopCat.Hom.hom ·) this
    replace this := congr_arg (ContinuousMap.toFun ·) this
    dsimp at this
    rw [this, Set.image_comp, Set.image_comp, Set.preimage_image_eq]
    swap
    · refine Function.HasLeftInverse.injective ⟨(D.t i k).base, fun x => ?_⟩
      rw [← ConcreteCategory.comp_apply, ← comp_base, D.t_inv, id_base, ConcreteCategory.id_apply]
    refine congr_arg (_ '' ·) ?_
    refine congr_fun ?_ _
    refine Set.image_eq_preimage_of_inverse ?_ ?_
    · intro x
      rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.inv_hom_id, id_base,
        ConcreteCategory.id_apply]
    · intro x
      rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.hom_inv_id, id_base,
        ConcreteCategory.id_apply]
  · rw [← IsIso.eq_inv_comp, IsOpenImmersion.inv_invApp, Category.assoc,
      (D.t' k i j).c.naturality_assoc]
    simp_rw [← Category.assoc]
    dsimp
    rw [← comp_c_app, congr_app (D.t_fac k i j), comp_c_app]
    dsimp
    simp_rw [Category.assoc]
    rw [IsOpenImmersion.inv_naturality, IsOpenImmersion.inv_naturality_assoc,
      IsOpenImmersion.app_inv_app'_assoc]
    · simp_rw [← (𝖣.V (k, i)).presheaf.map_comp]; rfl
    rintro x ⟨y, -, eq⟩
    replace eq := ConcreteCategory.congr_arg (𝖣.t i k).base eq
    change ((π₂ i, j, k) ≫ D.t i k).base y = (D.t k i ≫ D.t i k).base x at eq
    rw [𝖣.t_inv, id_base, TopCat.id_app] at eq
    subst eq
    use (inv (D.t' k i j)).base y
    change (inv (D.t' k i j) ≫ π₁ k, i, j).base y = _
    congr 3
    rw [IsIso.inv_comp_eq, 𝖣.t_fac_assoc, 𝖣.t_inv, Category.comp_id]

Goal state after:
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 j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv) ∘ ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι j)) ⁻¹'
      ⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv) ''
        ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)) '' ↑U =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      ⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

Tactic:
Set.preimage_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι j)) ⁻¹'
      ⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv) ⁻¹'
        ⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv) ''
          ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)) '' ↑U =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      ⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case a
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ Scheme.Hom.opensRange coprod.inl ≤ coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
case a
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
x : ↥X
⊢ coprod.inl x ∈ coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
⊢ Set.range ⇑(tAux F i j) ⊆ Set.range ⇑(V F j i).ι

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
x : ↥↑(V F i j)
⊢ (tAux F i j) x ∈ Set.range ⇑(V F j i).ι
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: ⊢ IsStableUnderBaseChange fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f

Tactic:
by
  refine IsStableUnderBaseChange.mk surjective_respectsIso ?_
  introv h x
  induction x with
  | zero => exact ⟨0, map_zero _⟩
  | tmul x y =>
    obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
    rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
  | add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩

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

Goal state before:
pp: X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
⊢ QuasiSeparatedSpace ↥X

Tactic:
let := HasAffineProperty.isLocal_affineProperty @QuasiCompact
  rw [← quasiCompact_affineProperty_iff_quasiSeparatedSpace X.toSpecΓ]
  have : ∀ i, IsAffine ((X.openCoverOfIsOpenCover U hU).X i) := hU₁
  refine AffineTargetMorphismProperty.diagonal_of_openCover_source _
    (Scheme.openCoverOfIsOpenCover _ _ hU) fun i j ↦ ?_
  rw [← isCompact_univ_iff, (pullback.fst ((X.openCoverOfIsOpenCover U hU).f i)
    ((X.openCoverOfIsOpenCover U hU).f j) ≫
    (X.openCoverOfIsOpenCover U hU).f i).isOpenEmbedding.isCompact_iff, Set.image_univ,
    IsOpenImmersion.range_pullback_to_base_of_left]
  simpa using hU₂ i j

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ @QuasiSeparated ≤ MorphismProperty.diagonal @QuasiCompact

Tactic:
quasiSeparated_eq_diagonal_is_quasiCompact

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
⊢ MorphismProperty.diagonal @QuasiCompact ≤ MorphismProperty.diagonal @QuasiCompact
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 : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
⊢ P f

Tactic:
have (i : _) : IsAffine ((X.openCoverOfIsOpenCover _ hU).X i) := (U i).2

Goal state after:
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
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
this :
  ∀ (i : (X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).I₀),
    IsAffine ((X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).X i)
⊢ P f
Module: Mathlib.RingTheory.Ideal.Height

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

Tactic:
rw [Ideal.height_eq_primeHeight, Ideal.primeHeight]
  exact Order.height_top_eq_krullDim

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

Goal state before:
pp: case refine_2
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 : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
⊢ ∀ i ∈ hS.toFinset, ¬I ≤ i

Tactic:
intro K hK e

Goal state after:
case refine_2
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 : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
K : Ideal R
hK : K ∈ hS.toFinset
e : I ≤ K
⊢ False
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case neg.x
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 : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := ⋯
hS : S.Finite
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this✝¹ : p.IsPrime
h : ¬p.height = ⊤
this✝ : p.FiniteHeight
this : J.height ≤ p.height
e : ↑r = p.height
⊢ p ∈ S

pp: case neg.a
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 : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := ⋯
hS : S.Finite
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this✝¹ : p.IsPrime
h : ¬p.height = ⊤
this✝ : p.FiniteHeight
this : J.height ≤ p.height
e : ↑r = p.height
⊢ x ∈ ↑p

Tactic:
· refine ⟨mem_minimalPrimes_of_height_le (le_sup_left.trans hp.le) (e.symm.trans_le h₃),
          e.symm⟩

Goal state after:
case neg.a
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 : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := ⋯
hS : S.Finite
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this✝¹ : p.IsPrime
h : ¬p.height = ⊤
this✝ : p.FiniteHeight
this : J.height ≤ p.height
e : ↑r = p.height
⊢ x ∈ ↑p
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↥(I.glueDataObj U)
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((I.glueDataObjι U) p) ∈ X.basicOpen f
this : IsIso (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f))
⊢ ⊤ ≤ (X.basicOpen f).ι ⁻¹ᵁ ↑V

Tactic:
exact fun x _ ↦ (hfg.trans_le (X.basicOpen_le g)) x.2

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

Goal state before:
pp: case refine_1.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)) (RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) ≤
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))

Tactic:
refine Ideal.map_le_iff_le_comap.mpr fun x hx ↦ ?_

Goal state after:
case refine_1.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s x : ↑Γ(Y, ↑U)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))
⊢ x ∈
    Ideal.comap (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      (RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s))))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ Set.range ⇑f ⊆ ↑(ker f).support

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ f x ∈ ↑(ker f).support
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X✝ : Scheme
U : X✝.Opens
X Y : Scheme
f✝ f g : X ⟶ Y
e : f = g
x : ↥X
⊢ f x = g x

Tactic:
by subst e; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : Triplet f g
e : T₁ = T₂
⊢ T₁.tensor = T₂.tensor

Tactic:
by subst e; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
K : Type u
inst✝ : Field K
g : Spec (CommRingCat.of K) ⟶ X
⊢ descResidueField (stalkClosedPointTo (g ≫ f)) =
    Hom.residueFieldMap f (g (closedPoint K)) ≫ descResidueField (stalkClosedPointTo g)

Tactic:
simp [← cancel_epi (Y.residue _), stalkClosedPointTo_comp, residue_residueFieldMap_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case refine_2
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥Y
x✝ : x ∈ ⇑g ⁻¹' Set.range ⇑f
y : ↥X
hy : f y = g x
⊢ x ∈ Set.range ⇑(pullback.snd f g)

Tactic:
obtain ⟨a, ha⟩ := Triplet.exists_preimage (Triplet.mk' y x hy)
    use a, ha.right

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
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝¹ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : (fun {R S} [CommRing R] [CommRing S] ↦ Q) (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) (f ∣_ Y.basicOpen r)

Tactic:
simp only at hf

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝¹ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) (f ∣_ Y.basicOpen r)
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case right
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝¹ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)))

Tactic:
rw [(isAffineOpen_top Y).app_basicOpen_eq_away_map f (isAffineOpen_top X),
        CommRingCat.hom_comp, hPi.cancel_right_isIso, ← Scheme.Hom.appTop]

Goal state after:
case right
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝¹ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ Q
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
          (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) r)))
          (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) r)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case respectsIso.h₁
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [IsAffine Z], IsAffine Y → IsAffine X

Tactic:
rintro X Y Z e _ _ H
        have : IsAffine _ := H
        exact .of_isIso e.hom

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↥Y → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ IsAffineHom f

Tactic:
rw [HasAffineProperty.iff_of_iSup_eq_top (P := @IsAffineHom) fun i ↦ ⟨U i, hU i⟩]

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↥Y → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ ∀ (i : ↥Y), IsAffine ↑(f ⁻¹ᵁ ↑⟨U i, ⋯⟩)

X Y : Scheme
f : X ⟶ Y
U : ↥Y → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ ⨆ i, ↑⟨U i, ⋯⟩ = ⊤