mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
H₁ : s.fst ≫ f = s.snd
H₂ : s.fst ≫ g = s.snd
⊢ s.fst ≫ f = s.fst ≫ g

Tactic:
exact H₁.trans H₂.symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
H₁ : f ≫ s.inl = s.inr
H₂ : g ≫ s.inl = s.inr
⊢ f ≫ s.inl = g ≫ s.inl

Tactic:
exact H₁.trans H₂.symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
⊢ Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯ =
    CommRingCat.ofHom
      (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))))
        (↑(X.presheaf.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)))))
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r)

Tactic:
by
  let := hU.isLocalization_basicOpen r
  let := hV.isLocalization_basicOpen (f.appLE U V e r)
  ext : 1
  apply IsLocalization.ringHom_ext (.powers r)
  rw [IsLocalization.Away.map, CommRingCat.hom_ofHom, IsLocalization.map_comp,
    RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp,
    ← CommRingCat.hom_comp, Scheme.Hom.appLE_map, Scheme.Hom.map_appLE]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r))).comp (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)) =
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom
              (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
                (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
                (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
            X.presheaf.map (eqToHom ⋯).op)).comp
      (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r))

Tactic:
rw [IsLocalization.Away.map, CommRingCat.hom_comp, RingHom.comp_assoc, CommRingCat.hom_ofHom,
    IsLocalization.map_comp, RingHom.algebraMap_toAlgebra,
    RingHom.algebraMap_toAlgebra, ← RingHom.comp_assoc, ← CommRingCat.hom_comp,
    ← CommRingCat.hom_comp, ← X.presheaf.map_comp]

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ Scheme.Hom.app f (Y.basicOpen r)) =
    (CommRingCat.Hom.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op))).comp
      (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R S : CommRingCat
f : Spec S ⟶ Spec R
⊢ ∃ a, map a = f

Tactic:
use Spec.preimage f

Goal state after:
case h
R S : CommRingCat
f : Spec S ⟶ Spec R
⊢ map (preimage f) = f
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ X.zeroLocus s ∩ Set.range ⇑hU.fromSpec = X.zeroLocus s ∩ ↑U

Tactic:
range_fromSpec

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ X.zeroLocus s ∩ ↑U = X.zeroLocus s ∩ ↑U
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case neg
X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
this : U.carrier ↓∩ X.zeroLocus ↑(I ⊓ J) = U.carrier ↓∩ (X.zeroLocus ↑I ∪ X.zeroLocus ↑J)
x : ↥X
hxU : x ∉ U
⊢ x ∈ X.zeroLocus ↑(I ⊓ J) ↔ x ∈ X.zeroLocus ↑I ∪ X.zeroLocus ↑J

Tactic:
simp only [Submodule.coe_inf, Set.mem_union,
        codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) (I ∩ J)) hxU,
        codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) I) hxU, true_or]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j : h.J
⊢ IsIso (h.t i j)

Tactic:
use h.t j i; constructor <;> ext1; exacts [h.t_inv _ _ _, h.t_inv _ _ _]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

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

Tactic:
t_fst_fst_assoc,

Goal state after:
case refine_1
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i = pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ 𝒰.f j
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h.hU
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))
x : ↑↑(D.V (k, i))
y : ↑↑(pullback (D.f i j) (D.f i k))
eq : (ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k) ≫ D.t i k).base) y = x
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base)

Tactic:
subst eq

Goal state after:
case h.hU
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))
y : ↑↑(pullback (D.f i j) (D.f i k))
⊢ (ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k) ≫ D.t i k).base) y ∈
    Set.range ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base)
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:
rw [coprodComparison_inl_assoc, coprodSpec, coprod.inl_desc, Scheme.Spec_map,
        ← Spec.map_comp, Category.assoc, Iso.unop_inv, opProdIsoCoprod_inv_inl,
        limit.isoLimitCone_inv_π]
      rfl

Goal state after:
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✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
      (pullback.congrHom h₁ ⋯).hom ≫ pullback.fst s.fst (𝒰.f i) ≫ m =
    ((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫ (pullback.congrHom h₁ ⋯).hom) ≫
      (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i

Tactic:
pullback.congrHom_hom,

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
      pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯ ≫
        pullback.fst s.fst (𝒰.f i) ≫ m =
    ((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
        pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯) ≫
      (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

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

Tactic:
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
X Y : Scheme
f : X ⟶ Y
⊢ P.RespectsIso

Tactic:
by
  let := isLocal_affineProperty P
  rw [eq_targetAffineLocally P]
  infer_instance

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

Goal state before:
pp: case of_sSup_eq_top
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u_1} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f

Tactic:
rintro X Y f ι U hU H

Goal state after:
case of_sSup_eq_top
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this : Q.IsLocal := isLocal_affineProperty P
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
⊢ P f
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
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
conv_lhs => enter [2]; tactic => exact Multicoequalizer.π_desc _ _ _ _ _

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
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

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

Tactic:
refine pullbackSymmetry _ _ ≪≫ pullbackRightPullbackFstIso f g _ ≪≫ ?_ ≪≫
          (pullbackRightPullbackFstIso (S.affineCover.f i) g
            (pullback.snd f (S.affineCover.f i))).symm

Goal state after:
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 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g ≅
    pullback (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: case h
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
x : Rₜ ⟨a, ha⟩
hx : x ∈ p ⟨a, ha⟩
⊢ x = mk' (Rₜ ⟨a, ha⟩) (a * (sec a x).1) ⟨a ^ ((sec a x).2 + 1), ⋯⟩

Tactic:
IsLocalization.eq_mk'_iff_mul_eq,

Goal state after:
case h
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
x : Rₜ ⟨a, ha⟩
hx : x ∈ p ⟨a, ha⟩
⊢ x * (algebraMap R (Rₜ ⟨a, ha⟩)) ↑⟨a ^ ((sec a x).2 + 1), ⋯⟩ = (algebraMap R (Rₜ ⟨a, ha⟩)) (a * (sec a x).1)
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
h₂ : mk' (Rₜ ⟨a, ha⟩) 1 1 ∈ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical

Tactic:
rw [IsLocalization.mem_span_map (Submonoid.powers a)] at h₂

Goal state after:
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
h₂ : ∃ y ∈ Ideal.span (Set.range (mulNumerator s p)), ∃ z, mk' (Rₜ ⟨a, ha⟩) 1 1 = mk' (Rₜ ⟨a, ha⟩) y z
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
ι : Type u_1
s : ι → S
hsone : Ideal.span (Set.range s) = ⊤
Sₜ : ι → Type u
inst✝² : (i : ι) → CommRing (Sₜ i)
inst✝¹ : (i : ι) → Algebra S (Sₜ i)
inst✝ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)
hf : ∀ (i : ι), P ((algebraMap S (Sₜ i)).comp f)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
use Set.range s, hsone

Goal state after:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
ι : Type u_1
s : ι → S
hsone : Ideal.span (Set.range s) = ⊤
Sₜ : ι → Type u
inst✝² : (i : ι) → CommRing (Sₜ i)
inst✝¹ : (i : ι) → Algebra S (Sₜ i)
inst✝ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)
hf : ∀ (i : ι), P ((algebraMap S (Sₜ i)).comp f)
⊢ ∀ t ∈ Set.range s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) x =
    IsLocalization.mk' (Localization.Away (f ↑r)) (f b) ⟨f ↑⟨(fun x ↦ ↑r ^ x) n, ⋯⟩, ⋯⟩
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range

Tactic:
IsLocalization.eq_mk'_iff_mul_eq,

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) x *
      (algebraMap S (Localization.Away (f ↑r))) ↑⟨f ↑⟨(fun x ↦ ↑r ^ x) n, ⋯⟩, ⋯⟩ =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
intro R S T _ _ _ _ t _ f hf
  obtain ⟨s, hsone, hs⟩ := hf
  refine ⟨algebraMap S T '' s, ?_, ?_⟩
  · rw [← Ideal.map_span, hsone, Ideal.map_top]
  · rintro - ⟨a, ha, rfl⟩
    let : Algebra (Localization.Away a) (Localization.Away (algebraMap S T a)) :=
      (IsLocalization.Away.map _ _ (algebraMap S T) a).toAlgebra
    have : (algebraMap (Localization.Away a) (Localization.Away (algebraMap S T a))).comp
        (algebraMap S (Localization.Away a)) =
        (algebraMap T (Localization.Away (algebraMap S T a))).comp (algebraMap S T) := by
      simp [algebraMap_toAlgebra, IsLocalization.Away.map]
    rw [← comp_assoc, ← this, comp_assoc]
    have : IsScalarTower S (Localization.Away a) (Localization.Away ((algebraMap S T) a)) := by
      apply IsScalarTower.of_algebraMap_eq
      intro x
      simp [algebraMap_toAlgebra, IsLocalization.Away.map, ← IsScalarTower.algebraMap_apply]
    have : IsLocalization.Away (algebraMap S (Localization.Away a) t)
        (Localization.Away (algebraMap S T a)) :=
      IsLocalization.Away.commutes _ T ((Localization.Away (algebraMap S T a))) a t
    apply hPa _ (algebraMap S (Localization.Away a) t)
    apply hs a ha

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ P).toProperty.RespectsIso

Tactic:
by
  apply AffineTargetMorphismProperty.respectsIso_mk
  · introv H U
    have : IsIso (e.hom.appLE (e.hom ''ᵁ U) U.1 (e.hom.preimage_image_eq _).ge) :=
      inferInstanceAs (IsIso (e.hom.app _ ≫
        X.presheaf.map (eqToHom (e.hom.preimage_image_eq _).symm).op))
    rw [← Scheme.Hom.appLE_comp_appLE _ _ ⊤ (e.hom ''ᵁ U) U.1 le_top (e.hom.preimage_image_eq _).ge,
      CommRingCat.hom_comp, h₁.cancel_right_isIso]
    exact H ⟨_, U.prop.image_of_isOpenImmersion e.hom⟩
  · introv H U
    rw [Scheme.Hom.comp_appLE, CommRingCat.hom_comp, h₁.cancel_left_isIso]
    exact H U

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

Goal state before:
pp: case h₇₆
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
⊢ X.basicOpen ((f |_ ↑S) ⋯) ≤ X.basicOpen ((f |_ U₂) ⋯)

Tactic:
change X.basicOpen _ ≤ _
      simp only [TopCat.Presheaf.restrictOpenCommRingCat_apply, Scheme.basicOpen_res]
      exact inf_le_inf h₂ le_rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
hI : I.height = ↑n
⊢ ∃ p, ∃ (_ : p.IsPrime) (_ : I ≤ p), p.height = ↑n

Tactic:
by
  simp only [Ideal.height, ENat.iInf_eq_natCast_iff] at hI
  rcases hI with ⟨⟨p, ⟨⟨⟨hpp, hIp⟩, _⟩, h⟩, -⟩, -⟩
  exact ⟨p, hpp, hIp, h ▸ p.height_eq_primeHeight⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
e : R ≃+* S
I : Ideal R
⊢ (map e I).height = I.height

Tactic:
← Ideal.comap_symm e,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
e : R ≃+* S
I : Ideal R
⊢ (comap e.symm I).height = I.height
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₁
X✝ X : Scheme
U : X.Opens
H✝ :
  ∀ (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V),
        ∃ x,
          ∀ [hX : IsReduced X] (s : ↑Γ(X, V)),
            X.basicOpen s = ⊥ → ∀ (x : ↥X) (hx : x ∈ V), (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) s = 0
hX : IsReduced X
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↥X
hx✝ : x ∈ U
V : X.Opens
hx : ↑⟨x, hx✝⟩ ∈ V
i : V ⟶ U
H : (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) ((ConcreteCategory.hom (X.presheaf.map i.op)) s) = 0
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx✝)) s = 0

Tactic:
rw [← X.sheaf.presheaf.germ_res_apply i x hx s]

Goal state after:
case h₁
X✝ X : Scheme
U : X.Opens
H✝ :
  ∀ (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V),
        ∃ x,
          ∀ [hX : IsReduced X] (s : ↑Γ(X, V)),
            X.basicOpen s = ⊥ → ∀ (x : ↥X) (hx : x ∈ V), (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) s = 0
hX : IsReduced X
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↥X
hx✝ : x ∈ U
V : X.Opens
hx : ↑⟨x, hx✝⟩ ∈ V
i : V ⟶ U
H : (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) ((ConcreteCategory.hom (X.presheaf.map i.op)) s) = 0
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) ((ConcreteCategory.hom (X.sheaf.presheaf.map i.op)) s) = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ IsLocalization.Away f ↑Γ(X, X.basicOpen f)

Tactic:
constructor; constructor
  · rintro ⟨_, n, rfl⟩
    simp only [map_pow, RingHom.algebraMap_toAlgebra]
    exact IsUnit.pow _ (RingedSpace.isUnit_res_basicOpen _ f)
  · intro z
    obtain ⟨n, y, e⟩ := exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated X U hU hU' f z
    refine ⟨⟨y, _, n, rfl⟩, ?_⟩
    simpa only [map_pow, Subtype.coe_mk, RingHom.algebraMap_toAlgebra, mul_comm z] using! e.symm
  · intro x y
    rw [← sub_eq_zero, ← map_sub, RingHom.algebraMap_toAlgebra]
    simp_rw [← @sub_eq_zero _ _ (_ * x) (_ * y), ← mul_sub]
    generalize x - y = z
    intro H
    obtain ⟨n, e⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact X hU _ _ H
    refine ⟨⟨_, n, rfl⟩, ?_⟩
    simpa [mul_comm z] using! e

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 =
    (CommRingCat.Hom.hom (f.app (Y.basicOpen s))) ((algebraMap ↑Γ(Y, ↑U) ↑Γ(Y, Y.basicOpen s)) x)

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 (f.app (Y.basicOpen s))) ((algebraMap ↑Γ(Y, ↑U) ↑Γ(Y, Y.basicOpen s)) x) = 0

Tactic:
· simp [-NatTrans.naturality, RingHom.algebraMap_toAlgebra]

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 (f.app (Y.basicOpen s))) ((algebraMap ↑Γ(Y, ↑U) ↑Γ(Y, Y.basicOpen s)) x) = 0