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

Goal state before:
pp: X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ (Γ.rightOp.map ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f) ≫
          locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))).unop ≫
      ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
            X.presheaf).map
        (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
erw [← Adjunction.homEquiv_counit, Equiv.symm_apply_apply]

Goal state after:
X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ f.unop ≫
      ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
            X.presheaf).map
        (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : Scheme
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom

Tactic:
have := ΓSpec.adjunction.left_triangle_components X
  dsimp at this
  rw [← IsIso.eq_comp_inv] at this
  simp only [Category.id_comp] at this
  rw [← Quiver.Hom.op_inj.eq_iff, this, ← op_inv, IsIso.Iso.inv_inv]

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
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
e : cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅ cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) := ⋯
⊢ IsLimit ((Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯))

Tactic:
apply hc.ofIsoLimit

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
e : cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅ cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) := ⋯
⊢ (D.mapGlueData F).vPullbackCone i j ≅
    (Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
⊢ CommRingCat.Hom.hom ((structureSheaf R).obj.map (eqToHom ⋯)) = CommRingCat.Hom.hom (eqToHom ⋯)

Tactic:
eqToHom_map

Goal state after:
R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
⊢ CommRingCat.Hom.hom (eqToHom ⋯) = CommRingCat.Hom.hom (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
⊢ P V

Tactic:
by
  have : ∀ (x : V.1), ∃ f : Γ(X, V), ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f) := by
    intro x
    obtain ⟨i, hi⟩ := Opens.mem_iSup.mp (iSup_U.ge (Set.mem_univ x))
    obtain ⟨f, g, e, hf⟩ := exists_basicOpen_le_affine_inter V.prop (U i).prop x ⟨x.prop, hi⟩
    refine ⟨f, hf, ?_⟩
    convert! basicOpen _ g (hU i) using 1
    ext1
    exact e
  choose f hf₁ hf₂ using this
  suffices Ideal.span (Set.range f) = ⊤ by
    obtain ⟨t, ht₁, ht₂⟩ := (Ideal.span_eq_top_iff_finite _).mp this
    apply openCover V t ht₂
    rintro ⟨i, hi⟩
    obtain ⟨x, rfl⟩ := ht₁ hi
    exact hf₂ x
  rw [← V.prop.self_le_iSup_basicOpen_iff]
  intro x hx
  rw [iSup_range', Opens.mem_iSup]
  exact ⟨_, hf₁ ⟨x, hx⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
ht' : t.Nonempty
⊢ X.zeroLocus ↑(⨅ i ∈ t, I i) = ⋃ i ∈ t, X.zeroLocus ↑(I i)

Tactic:
by
  rw [zeroLocus_biInf I ht, Set.union_eq_left]
  obtain ⟨i, hi⟩ := ht'
  exact fun x hx ↦ Set.mem_iUnion₂_of_mem hi
    (codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) (I i)) hx)

Goal state after:
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 (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

Tactic:
simp only [forget_obj, forget_map, TopCat.pullback_snd_image_fst_preimage]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫
      t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.snd (𝒰.f j ≫ f) g =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f j)).hom ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.snd (𝒰.f j ≫ f) g

Tactic:
t_fst_snd,

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
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f j)).hom ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.snd (𝒰.f j ≫ f) g
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.snd (𝒰.f i ≫ f) g =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g

Tactic:
t_fst_snd,

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 : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.snd (𝒰.f i ≫ f) g =
    pullbackFstιToV 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.snd (𝒰.f j ≫ f) g
Module: Mathlib.AlgebraicGeometry.Limits

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

Tactic:
intro x y

Goal state after:
case H
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := (Pi.evalRingHom R i).toAlgebra
x y : (a : ι) → R a
⊢ (algebraMap ((a : ι) → R a) (R i)) x = (algebraMap ((a : ι) → R a) (R i)) y ↔
    Function.update 0 i 1 * x = Function.update 0 i 1 * y
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
i : ι
⊢ g ⁻¹ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = f ⁻¹ᵁ U i

Tactic:
change (g ≫ (⨆ i, U i).ι) ⁻¹ᵁ U i = _

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
i : ι
⊢ (g ≫ (⨆ i, U i).ι) ⁻¹ᵁ U i = f ⁻¹ᵁ U i
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case inr
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (Scheme.Cover.pullbackHom (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit))

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso P
      (isPullback_inr_inr_coprodMap f g).flip.isoPullback.hom]

Goal state after:
case inr
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (⋯.isoPullback.hom ≫ Scheme.Cover.pullbackHom (coprodOpenCover X' Y') (coprod.map f g) (Sum.inr PUnit.unit))
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✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (Iso.refl (pullback ((Cover.ulift 𝒰).f i ≫ f) g)).hom ≫
      (Cover.pushforwardIso (gluing (Cover.ulift 𝒰) f g).openCover
            (limit.isoLimitCone
                { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
                  isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv).f
        ((Equiv.refl (Cover.ulift 𝒰).I₀) i)

Tactic:
simp_rw [Cover.pushforwardIso_I₀, Cover.pushforwardIso_f, GlueData.openCover_f,
          GlueData.openCover_I₀, gluing_J]
        exact pullback.hom_ext (by simp [p1]) (by simp [p2])

Goal state after:
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
s : Cocone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rintro ⟨i, j⟩
    dsimp [glueData, GlueData.diagram]
    simp only [t, IsOpenImmersion.lift_fac]
    apply (Scheme.Opens.iSupOpenCover _).hom_ext _ _ fun k ↦ ?_
    simp only [Opens.iSupOpenCover, V, Scheme.homOfLE_ι_assoc]
    rw [homOfLE_tAux_assoc F ↓i ↓j k.2.1 k.2.2, Iso.eq_inv_comp]
    simp

Goal state after:
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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
m : (forgetToLocallyRingedSpace.mapCocone (cocone F)).pt ⟶ s.pt
hm : ∀ (j : J), (forgetToLocallyRingedSpace.mapCocone (cocone F)).ι.app j ≫ m = s.ι.app j
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine Multicoequalizer.hom_ext _ _ _ fun i ↦ ?_

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
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
m : (forgetToLocallyRingedSpace.mapCocone (cocone F)).pt ⟶ s.pt
hm : ∀ (j : J), (forgetToLocallyRingedSpace.mapCocone (cocone F)).ι.app j ≫ m = s.ι.app j
i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ SurjectiveOnStalks f ↔ (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤)).SurjectiveOnStalks

Tactic:
rw [← Spec_iff, MorphismProperty.arrow_mk_iso_iff @SurjectiveOnStalks (arrowIsoSpecΓOfIsAffine f)]

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
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
Mₐ : (a : ↑s) → Submonoid (Localization.Away ↑a) :=
  fun a ↦ Submonoid.map (algebraMap S (Localization.Away ↑a)) (Submonoid.map f M)
Sₐ : ↑s → Type u := fun a ↦ Localization (Mₐ a)
hM : ∀ (a : ↑s), Submonoid.map ((algebraMap S (Localization.Away ↑a)).comp f) M = Mₐ a
this : ∀ (a : ↑s), IsLocalization (Submonoid.map ((algebraMap S (Localization.Away ↑a)).comp f) M) (Sₐ a)
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
          ∀ (i : ι), P ((algebraMap S' (Sₜ i)).comp (IsLocalization.map S' f ⋯))

Tactic:
have (a : s) :
      IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away a.val) (M.map f)) (Sₐ a) :=
    inferInstanceAs <| IsLocalization (Mₐ a) (Sₐ a)

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
Mₐ : (a : ↑s) → Submonoid (Localization.Away ↑a) :=
  fun a ↦ Submonoid.map (algebraMap S (Localization.Away ↑a)) (Submonoid.map f M)
Sₐ : ↑s → Type u := fun a ↦ Localization (Mₐ a)
hM : ∀ (a : ↑s), Submonoid.map ((algebraMap S (Localization.Away ↑a)).comp f) M = Mₐ a
this✝ : ∀ (a : ↑s), IsLocalization (Submonoid.map ((algebraMap S (Localization.Away ↑a)).comp f) M) (Sₐ a)
this : ∀ (a : ↑s), IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f M)) (Sₐ a)
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
          ∀ (i : ι), P ((algebraMap S' (Sₜ i)).comp (IsLocalization.map S' f ⋯))
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
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
⊢ Q = Q'

Tactic:
ext R S _ _ f

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
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
R S : Type u
x✝¹ : CommRing R
x✝ : CommRing S
f : R →+* S
⊢ Q f ↔ Q' f
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
inst✝ : J.IsPrime
h : I < J
⊢ I.height + 1 ≤ J.height

Tactic:
simp only [Ideal.height_eq_primeHeight, Ideal.primeHeight]
  exact Order.height_add_one_le h

Goal state after:
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
⊢ ↑(f ⁻¹ᵁ ⊥) = ↑⊥

Tactic:
simp [Opens.map]

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

Goal state before:
pp: case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ {x y : ↑Γ(X, U)},
    (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) y → ∃ c, ↑c * x = ↑c * y

Tactic:
intro x y

Goal state after:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) y → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) y → ∃ c, ↑c * x = ↑c * y

Tactic:
rw [← sub_eq_zero, ← map_sub, RingHom.algebraMap_toAlgebra]

Goal state after:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (x - y) = 0 → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : Subsingleton ↥X
⊢ T1Space (PrimeSpectrum ↑Γ(X, ⊤))

Tactic:
apply X.isoSpec.hom.homeomorph.t1Space

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ I.glueDataObjMap h ≫ I.glueDataObjι V = I.glueDataObjι U ≫ X.homOfLE h

Tactic:
by
  rw [glueDataObjMap, glueDataObjι, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp,
    Ideal.quotientMap_comp_mk, CommRingCat.ofHom_comp, Spec.map_comp_assoc, glueDataObjι,
    Category.assoc]
  congr 1
  rw [Iso.eq_inv_comp, IsAffineOpen.isoSpec_hom, CommRingCat.ofHom_hom]
  erw [Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc U.1 V.1 h]
  rw [← IsAffineOpen.isoSpec_hom V.2, Iso.hom_inv_id, Category.comp_id]

Goal state after:
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)))
⊢ (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ f.app (Y.basicOpen s))) x = 0

Tactic:
trans (f.app (Y.basicOpen s)).hom (algebraMap Γ(Y, U) _ x)

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)))
⊢ (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ f.app (Y.basicOpen s))) x =
    (CommRingCat.Hom.hom (f.app (Y.basicOpen s))) ((algebraMap ↑Γ(Y, ↑U) ↑Γ(Y, Y.basicOpen s)) x)

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)))
⊢ (CommRingCat.Hom.hom (f.app (Y.basicOpen s))) ((algebraMap ↑Γ(Y, ↑U) ↑Γ(Y, Y.basicOpen s)) x) = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case a.inl
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥U
hx : (coprodMk U V) (Sum.inl x) ∈ coprod.desc f g ⁻¹ᵁ W
⊢ (coprodMk U V) (Sum.inl x) ∈ Scheme.Hom.opensRange i

Tactic:
replace hx : f x ∈ W := by simpa [← Scheme.Hom.comp_apply] using hx
      exact ⟨coprodMk _ _ (.inl ⟨x, hx⟩), by simp [i, ← Scheme.Hom.comp_apply]⟩

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Set.range ⇑(I.glueData.ι U) = ↑(I.gluedTo ⁻¹ᵁ ↑U)

Tactic:
simp only [TopologicalSpace.Opens.map_coe]

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Set.range ⇑(I.glueData.ι U) = ⇑I.gluedTo ⁻¹' ↑↑U
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
ι : Type u_3
inst✝³ : Finite ι
S : ι → Type u_4
inst✝² : (i : ι) → CommRing (S i)
inst✝¹ : (i : ι) → Algebra R (S i)
inst✝ : ∀ (i : ι), FinitePresentation R (S i)
⊢ FinitePresentation R ((a : ι) → S a)

Tactic:
by
  classical
  let (i : ι) : Algebra (Π a, S a) (S i) := (Pi.evalAlgHom R S i).toAlgebra
  have (i : ι) : IsLocalization.Away (Pi.single i 1 : ∀ a, S a) (S i) := by
    refine IsLocalization.away_of_isIdempotentElem ?_ (RingHom.ker_evalRingHom _ _)
      ((Pi.evalRingHom S i).surjective)
    simp [IsIdempotentElem, ← Pi.single_mul_left]
  exact Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway
    _ (Ideal.span_single_eq_top S) (fun i ↦ S i)

Goal state after: