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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y Z✝ : Scheme
f✝ : X ⟶ Z✝
g✝ : Y ⟶ Z✝
H : IsOpenImmersion f✝
Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
H' : Set.range ⇑g ⊆ Set.range ⇑f
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (lift f g H' ≫ f)

Tactic:
by simpa

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥↑U
⊢ ∀ (hxU : x ∈ W),
    (↑U).presheaf.germ W x hxU ≫ 𝟙 ((↑U).presheaf.stalk x) =
      (↑U).presheaf.germ W x hxU ≫ (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x

Tactic:
hxW

Goal state after:
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥↑U
hxW : x ∈ W
⊢ (↑U).presheaf.germ W x hxW ≫ 𝟙 ((↑U).presheaf.stalk x) =
    (↑U).presheaf.germ W x hxW ≫ (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
U : Opens ↑(PrimeSpectrum.Top R)
⊢ const 1 1 U ⋯ = 1

Tactic:
simpa using const_algebraMap 1 (A := A) U

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
this : V.ι ''ᵁ ?m.39 ≤ U.ι ''ᵁ W
⊢ ⋯.functor.obj (unop (op (X.homOfLE h ''ᵁ W))) ≤ ⋯.functor.obj (unop (op W))

Tactic:
by simpa

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ U ⊓ W = U

Tactic:
by simpa

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
rw [Category.comp_id, Category.id_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case w.e_f
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ f.c.app (op ⊤) ≫ X.presheaf.Γgerm x = Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x) ≫ Hom.stalkMap f x

Tactic:
exact (PresheafedSpace.stalkMap_germ f.1 ⊤ x trivial).symm

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
        (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯ ≫
      equalizer.lift (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯)
        ⋯ =
    𝟙 (equalizer lhs rhs)

Tactic:
by ext <;> simp

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)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) :=
  isLocalization_basicOpen hV ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
⊢ (CommRingCat.Hom.hom
          (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r))
            ⋯)).comp
      (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)) =
    (IsLocalization.map (↑(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)) ⋯).comp
      (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r))

Tactic:
IsLocalization.map_comp,

Goal state after:
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)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) :=
  isLocalization_basicOpen hV ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
⊢ (CommRingCat.Hom.hom
          (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r))
            ⋯)).comp
      (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)) =
    (algebraMap ↑Γ(X, V) ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r))).comp
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))
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 (X.presheaf.map (eqToHom ⋯).op)).comp
      ((IsLocalization.map (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
            (CommRingCat.Hom.hom (Scheme.Hom.app f U)) ⋯).comp
        (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)))

Tactic:
IsLocalization.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 (Scheme.Hom.app f (Y.basicOpen r))).comp (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)) =
    (CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op)).comp
      ((algebraMap ↑Γ(X, f ⁻¹ᵁ U)
            ↑(CommRingCat.of ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))).comp
        (CommRingCat.Hom.hom (Scheme.Hom.app f U)))
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs : (isLocallyFraction R M).pred s
⊢ (isLocallyFraction S N).pred (comapFun f U V hUV s)

Tactic:
let := Module.compHom N σ
  let := σ.toAlgebra
  have : IsScalarTower R S N := .of_algebraMap_smul fun _ _ ↦ rfl
  rintro ⟨p, hpV⟩
  obtain ⟨W, m, iWU, a, b, h_frac⟩ := hs ⟨PrimeSpectrum.comap σ p, hUV hpV⟩
  refine ⟨⟨_, (PrimeSpectrum.continuous_comap σ).isOpen_preimage _ W.2⟩ ⊓ V,
    ⟨m, hpV⟩, Opens.infLERight _ _, f a, σ b, ?_⟩
  rintro ⟨q, ⟨hqW, hqV⟩⟩
  obtain ⟨hs, H⟩ := h_frac ⟨PrimeSpectrum.comap σ q, hqW⟩
  refine ⟨hs, ?_⟩
  dsimp [comapFun] at H ⊢
  rw [H]
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U : Opens ↑(PrimeSpectrum.Top R)
p : ↑(PrimeSpectrum.Top R)
hpU : p ∈ U.carrier
⊢ p ∈ PrimeSpectrum.comap (RingHom.id R) ⁻¹' U.carrier

Tactic:
by rwa [PrimeSpectrum.comap_id]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
⊢ D.Rel ⟨i, x⟩ ⟨j, y⟩ → (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y

Tactic:
rintro ⟨z, e₁, e₂⟩

Goal state after:
case mpr
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
z : ↑(D.V (⟨i, x⟩.fst, ⟨j, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, x⟩.fst ⟨j, y⟩.fst)) z = ⟨i, x⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, y⟩.fst ⟨i, x⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, x⟩.fst ⟨j, y⟩.fst)) z) = ⟨j, y⟩.snd
⊢ (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
x₁ : ↑(D.U i)
x₂ : ↑(D.U j)
y : ↑(D.V (⟨i, x₁⟩.fst, ⟨j, x₂⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, x₁⟩.fst ⟨j, x₂⟩.fst)) y = ⟨i, x₁⟩.snd
eq₂ : (ConcreteCategory.hom (D.ι j)) x₂ = (ConcreteCategory.hom (D.ι i)) x₁
⊢ (ConcreteCategory.hom (D.f i j ≫ D.ι i)) y = (ConcreteCategory.hom (D.ι i)) x₁

Tactic:
by simp [e₁]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case h.left
D : GlueData
h : MkCore
i j : h.J
x✝ : ↑((Opens.toTopCat (h.U i)).obj (h.V i j))
⊢ (ConcreteCategory.hom (h.t i j ≫ h.t j i)) x✝ = (ConcreteCategory.hom (𝟙 ((Opens.toTopCat (h.U i)).obj (h.V i j)))) x✝

pp: case h.right
D : GlueData
h : MkCore
i j : h.J
x✝ : ↑((Opens.toTopCat (h.U j)).obj (h.V j i))
⊢ (ConcreteCategory.hom (h.t j i ≫ h.t i j)) x✝ = (ConcreteCategory.hom (𝟙 ((Opens.toTopCat (h.U j)).obj (h.V j i)))) x✝

Tactic:
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 : 𝒰.I₀
this✝ : HasPullback (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) ≫ 𝟙 Z =
    (pullbackSymmetry (𝒰.f j) (𝒰.f i)).hom ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f

pp: case refine_2
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this✝ : HasPullback (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

Tactic:
· rw [pullbackSymmetry_hom_comp_snd_assoc, pullback.condition_assoc, Category.comp_id]

Goal state after:
case refine_2
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this✝ : HasPullback (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_2
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this✝ : HasPullback (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

Tactic:
rw [Category.comp_id, Category.id_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

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

Tactic:
rw [Category.comp_id, Category.id_comp]

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
⊢ ∀ (b : (MultispanShape.prod (gluing 𝒰 f g).J).R),
    Multicoequalizer.π (gluing 𝒰 f g).diagram b ≫ p1 𝒰 f g ≫ f =
      Multicoequalizer.π (gluing 𝒰 f g).diagram b ≫ p2 𝒰 f g ≫ g

Tactic:
simp [p1, p2, pullback.condition]

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 ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).fst = s.fst
h₂ : m ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).snd = s.snd
⊢ m = gluedLift 𝒰 f g s

Tactic:
PullbackCone.mk_pt,

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 ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).fst = s.fst
h₂ : m ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).snd = s.snd
⊢ m = gluedLift 𝒰 f g s
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
X : Scheme
s : Set σ
hs : s.Finite
U : σ → X.Opens
hU : ∀ i ∈ s, IsAffineOpen (U i)
hU' : s.Pairwise (Disjoint on U)
this : Finite ↑s
⊢ ∀ (i : ↑s), IsAffineOpen (U ↑i)

Tactic:
by simpa

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

Goal state before:
pp: case restrict
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
U : Y.Opens
H : targetAffineLocally Q f
V : ↑(↑U).affineOpens
⊢ Q (f ∣_ U ∣_ ↑V)

Tactic:
Q.arrow_mk_iso_iff (morphismRestrictRestrict f _ _)

Goal state after:
case restrict
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
U : Y.Opens
H : targetAffineLocally Q f
V : ↑(↑U).affineOpens
⊢ Q (f ∣_ U.ι ''ᵁ ↑V)
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
s : PullbackCone (D.ι i) (D.ι j)
⊢ s.fst.base ≫ D.toTopGlueData.ι i = s.snd.base ≫ D.toTopGlueData.ι j

Tactic:
← 𝖣.ι_gluedIso_hom (PresheafedSpace.forget _) _,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ s.fst.base ≫ (forget C).map (D.ι i) ≫ (D.gluedIso (forget C)).hom = s.snd.base ≫ D.toTopGlueData.ι j
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
x✝¹ : Continuous[inst✝¹, inst✝] f
x✝ : IsOpen[inst✝] s
hf : ∀ (x : α), closure[inst✝] {f x} ⊆ f '' closure[inst✝¹] {x}
x : α
hx : x ∈ f ⁻¹' s
y : β
hy : y ∈ s
hcl : f x ⤳ y
a : α
ha : a ∈ closure[inst✝¹] {x}
hay : f a = y
⊢ s.restrictPreimage f ⟨a, ⋯⟩ = ⟨y, hy⟩

Tactic:
by simpa

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
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
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)
⊢ Ideal.span (Set.range fun t ↦ ↑t) = ⊤

Tactic:
by simpa

Goal state after:
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
a : Localization.Away ↑r
e' : (Localization.awayMap f ↑r) a = (algebraMap S (Localization.Away (f ↑r))) x
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range

Tactic:
obtain ⟨b, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (Submonoid.powers (r : R)) a

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' :
  (Localization.awayMap f ↑r) (IsLocalization.mk' (Localization.Away ↑r) b ⟨(fun x ↦ ↑r ^ x) n, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) x
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
t : T
ht : t ∈ ↑sg
⊢ t ∈
    ↑(Ideal.span
        (Set.range fun x ↦
          match x with
          | (a, b) => g ↑a * ↑b))

Tactic:
have : 1 ∈ Ideal.span (Set.range <| fun a : sf ↦ a.val) := by simp [hsfone]

Goal state after:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
t : T
ht : t ∈ ↑sg
this : 1 ∈ Ideal.span (Set.range fun a ↦ ↑a)
⊢ t ∈
    ↑(Ideal.span
        (Set.range fun x ↦
          match x with
          | (a, b) => g ↑a * ↑b))
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)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (IsLocalization.map S' f ⋯)

Tactic:
locally_iff_exists hPl.away.respectsIso

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)
⊢ ∃ ι 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 : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst f g)))

Tactic:
erw [← PreservesPullback.iso_inv_fst AffineScheme.forgetToScheme (AffineScheme.ofHom f)
      (AffineScheme.ofHom g)]
  rw [Scheme.Hom.comp_appTop, CommRingCat.hom_comp, hP'.cancel_right_isIso,
    AffineScheme.forgetToScheme_map]
  have := congr_arg Quiver.Hom.unop
      (PreservesPullback.iso_hom_fst AffineScheme.Γ.rightOp (AffineScheme.ofHom f)
        (AffineScheme.ofHom g))
  simp only [AffineScheme.Γ, Functor.rightOp_obj, Functor.comp_obj, Functor.op_obj, unop_comp,
    AffineScheme.forgetToScheme_obj, Scheme.Γ_obj, Functor.rightOp_map, Functor.comp_map,
    Functor.op_map, Quiver.Hom.unop_op, AffineScheme.forgetToScheme_map, Scheme.Γ_map] at this
  rw [← this, CommRingCat.hom_comp, hP'.cancel_right_isIso, ← pushoutIsoUnopPullback_inl_hom,
    CommRingCat.hom_comp, hP'.cancel_right_isIso]
  exact hP.pushout_inl hP' _ _ H

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

Goal state before:
pp: 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 : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f)))
      ((algebraMap S (Localization.Away ↑r)).comp f)
⊢ Ideal.span (Set.range fun i ↦ ↑i) = ⊤

Tactic:
by simpa

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

Goal state before:
pp: 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 : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (Localization.awayMap f ↑r)
⊢ Ideal.span (Set.range fun i ↦ ↑i) = ⊤

Tactic:
by simpa

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

Goal state before:
pp: case ofLocalizationSpan
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))
⊢ RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))

Tactic:
intro R S _ _ f s hs H
    apply IsZariskiLocalAtTarget.of_iSup_eq_top _ (PrimeSpectrum.iSup_basicOpen_eq_top_iff
      (f := fun i : s ↦ (i : R)).mpr (by simpa))
    intro i
    exact (MorphismProperty.arrow_mk_iso_iff P (SpecMapRestrictBasicOpenIso
      (CommRingCat.ofHom f) i.1)).mpr (H i)

Goal state after: