mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝³ : AddMonoid k
inst✝² : SMulZeroClass S k
inst✝¹ : SMulZeroClass Sᵐᵒᵖ k
inst✝ : IsCentralScalar S k
x✝¹ : S
x✝ : SkewMonoidAlgebra k G
coeff✝ : G →₀ k
⊢ { coeff := MulOpposite.op x✝¹ • coeff✝ } = { coeff := x✝¹ • coeff✝ }

Tactic:
op_smul_eq_smul

Goal state after:
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := f, c := gc } }.hom x
U : Opens ↑↑Y.toPresheafedSpace
s : CC (Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ (Opens.map f).obj (unop (op U))
⊢ (ConcreteCategory.hom (X.presheaf.germ ((Opens.map f).obj (unop (op U))) x hx))
      ((ConcreteCategory.hom (fc.app (op U))) s) =
    (ConcreteCategory.hom (X.presheaf.germ ((Opens.map f).obj (unop (op U))) x hx))
      ((ConcreteCategory.hom (gc.app (op U))) s)

Tactic:
← PresheafedSpace.stalkMap_germ_apply ⟨f, fc⟩,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := f, c := gc } }.hom x
U : Opens ↑↑Y.toPresheafedSpace
s : CC (Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ (Opens.map f).obj (unop (op U))
⊢ (ConcreteCategory.hom ({ base := f, c := fc }.stalkMap x))
      ((ConcreteCategory.hom (Y.presheaf.germ (unop (op U)) ((ConcreteCategory.hom { base := f, c := fc }.base) x) hx))
        s) =
    (ConcreteCategory.hom (X.presheaf.germ ((Opens.map f).obj (unop (op U))) x hx))
      ((ConcreteCategory.hom (gc.app (op U))) s)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝² : Category.{v', u'} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape J TopCat
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens ↑(colimit (F ⋙ forget C)))ᵒᵖ
this :
  op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) =
    op ((Opens.map (colimit.ι (F ⋙ forget C) j₂)).obj (unop U))
⊢ (F.map (f ≫ g)).c.app (op ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) ≫
      𝟙
          ((F.obj j₁).presheaf.obj
            (op ((Opens.map (F.map (f ≫ g)).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))))) ≫
        (pushforwardEq ⋯ (F.obj j₁).presheaf).hom.app U =
    ((F.map g).c.app (op ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) ≫
        𝟙
            ((F.obj j₂).presheaf.obj
              (op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))))) ≫
          (pushforwardEq ⋯ (F.obj j₂).presheaf).hom.app U) ≫
      (F.map f).c.app (op ((Opens.map (colimit.ι (F ⋙ forget C) j₂)).obj (unop U))) ≫
        𝟙
            ((F.obj j₁).presheaf.obj
              (op ((Opens.map (F.map f).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₂)).obj (unop U))))) ≫
          (pushforwardEq ⋯ (F.obj j₁).presheaf).hom.app U

Tactic:
simp only [map_comp_c_app, pushforward_obj_obj, pushforward_map_app, comp_base,
      pushforwardEq_hom_app, op_obj, Opens.map_comp_obj, id_comp, assoc, eqToHom_map_comp,
      NatTrans.naturality_assoc, pushforward_obj_map, eqToHom_unop]

Goal state after:
J : Type u'
inst✝² : Category.{v', u'} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape J TopCat
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens ↑(colimit (F ⋙ forget C)))ᵒᵖ
this :
  op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) =
    op ((Opens.map (colimit.ι (F ⋙ forget C) j₂)).obj (unop U))
⊢ (F.map g).c.app (op ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) ≫
      (F.map f).c.app (op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U)))) ≫
        (F.obj j₁).presheaf.map (eqToHom ⋯) =
    (F.map g).c.app (op ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) ≫
      (F.map f).c.app (op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U)))) ≫
        (F.obj j₁).presheaf.map ((Opens.map (F.map f).base).map (eqToHom ⋯)).op ≫ (F.obj j₁).presheaf.map (eqToHom ⋯)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case inl
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : f ^ n = 0
h : n = 0
⊢ X.toRingedSpace.basicOpen f = ⊥

Tactic:
| inl h =>

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
h : 0 < n
⊢ X.basicOpen (f ^ n) = X.basicOpen f

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' h
  induction k with
  | zero => simp
  | succ n hn => rw [pow_add]; simp_all

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
x : ↥X
hx : IsClosed {x}
⊢ height x = 0

Tactic:
simp only [height_eq_zero]

Goal state after:
X : Scheme
x : ↥X
hx : IsClosed {x}
⊢ IsMin x
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

Tactic:
by
  obtain ⟨U, hp, s, e⟩ := TopCat.Presheaf.exists_germ_eq _ y
  obtain ⟨_, ⟨r, rfl⟩, hpr : p ∈ PrimeSpectrum.basicOpen r, hrU : PrimeSpectrum.basicOpen r ≤ U⟩ :=
    PrimeSpectrum.isTopologicalBasis_basic_opens.exists_subset_of_mem_open (show p ∈ U from hp) U.2
  change PrimeSpectrum.basicOpen r ≤ U at hrU
  replace e :=
    ((Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).germ_res_apply
      (homOfLE hrU) p hpr _).trans e
  set s' := (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).map
      (homOfLE hrU).op s with h
  replace e : ((Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).obj).germ _
      p hpr) s' = y := by
    rw [h]; exact e
  clear_value s'; clear! U
  obtain ⟨⟨s, ⟨_, n, rfl⟩⟩, hsn⟩ :=
    @IsLocalization.surj _ _ _ _ _ _
      (StructureSheaf.IsLocalization.to_basicOpen S <| algebraMap R S r) s'
  refine ⟨⟨s, ⟨r, hpr⟩ ^ n⟩, ?_⟩
  rw [Submonoid.smul_def, Algebra.smul_def, algebraMap_pushforward_stalk, toPushforwardStalk,
    CommRingCat.comp_apply, CommRingCat.comp_apply]
  iterate 2
    erw [← (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).germ_res_apply
      (homOfLE le_top) p hpr]
  rw [← e]
  let f := TopCat.Presheaf.germ (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _*
      (structureSheaf S).obj) _ p hpr
  rw [← map_mul, mul_comm]
  dsimp only [Subtype.coe_mk] at hsn
  rw [← map_pow (algebraMap R S)] at hsn
  congr 1

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasLimits C
ι✝ : Type v
F✝ : Discrete ι✝ ⥤ SheafedSpace C
inst✝³ : HasColimit F✝
i✝ : Discrete ι✝
ι : Type w
inst✝² : Small.{v, w} ι
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
⊢ IsOpenImmersion (colimit.ι F i)

Tactic:
by
  obtain ⟨ι', ⟨e⟩⟩ := Small.equiv_small (α := ι)
  let f : Discrete ι' ≌ Discrete ι := Discrete.equivalence e.symm
  have : colimit.ι F i = (colimit.ι F i ≫ (HasColimit.isoOfEquivalence f (Iso.refl _)).inv) ≫
      (HasColimit.isoOfEquivalence f (Iso.refl _)).hom := by
    simp
  rw [this, HasColimit.ι_isoOfEquivalence_inv]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ unop (op (basicOpen (g' * g)))
⊢ ↑(const (g' • f) (g' * g) (basicOpen (g' * g)) ⋯) ⟨y, hy⟩ =
    ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s) ⟨y, hy⟩

Tactic:
· rw [PrimeSpectrum.basicOpen_mul] at hy
    obtain ⟨hgy, H⟩ := hfg ⟨y, hg'U hy.1⟩
    refine (LocalizedModule.mk_eq.mpr ⟨1, ?_⟩).trans H.symm
    simp [Submonoid.smul_def, ← smul_assoc]; ring_nf

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ U : X.Opens
⊢ Over.homMk (X.homOfLE ⋯) ⋯ = 𝟙 (Over.mk U.ι)

Tactic:
ext1
    exact Scheme.homOfLE_rfl _ _

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
x : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
⊢ (structurePresheafInModuleCat R M).germ U x hxU ≫ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x =
    (structurePresheafInModuleCat R M).germ U x hxU ≫ 𝟙 ((structurePresheafInModuleCat R M).stalk x)

Tactic:
ext s

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ↑((structurePresheafInModuleCat R M).obj (op U))
⊢ (ModuleCat.Hom.hom
        ((structurePresheafInModuleCat R M).germ U x hxU ≫ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x))
      s =
    (ModuleCat.Hom.hom
        ((structurePresheafInModuleCat R M).germ U x hxU ≫ 𝟙 ((structurePresheafInModuleCat R M).stalk x)))
      s
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case h
X Y : LocallyRingedSpace
f : X ⟶ Y
⊢ ∀ (r : ↑(unop (Γ.rightOp.obj Y))),
    (Γ.rightOp.map f).unop ≫ ((𝟭 LocallyRingedSpace).obj X).presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom
          (algebraMap (↑(unop (Γ.rightOp.obj Y)))
            ((structureSheafInType ↑(unop (Γ.rightOp.obj Y)) ↑(unop (Γ.rightOp.obj Y))).obj.obj (op (basicOpen r)))) ≫
        ((𝟭 LocallyRingedSpace).map f ≫ Y.toΓSpec).c.app (op (basicOpen r))

Tactic:
· intro r
      rw [LocallyRingedSpace.comp_c_app, ← Category.assoc]
      erw [Y.toΓSpecSheafedSpace_app_spec, f.c.naturality]
      rfl

Goal state after:
Module: Mathlib.Topology.Gluing

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

Tactic:
delta GlueData.ι

Goal state after:
case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
⊢ (ConcreteCategory.hom (Multicoequalizer.π D.diagram i)) x =
      (ConcreteCategory.hom (Multicoequalizer.π D.diagram j)) y →
    D.Rel ⟨i, x⟩ ⟨j, y⟩
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inl
X : Scheme
inst✝ : Subsingleton ↥X
h : IsEmpty ↥X
⊢ IsAffine X

Tactic:
| inl h =>

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X : Scheme
inst✝ : Subsingleton ↥X
⊢ IsAffine X

Tactic:
by
  cases isEmpty_or_nonempty X with
  | inl h => infer_instance
  | inr h =>
  obtain ⟨x⟩ := h
  obtain ⟨_, ⟨U, hU : IsAffine _, rfl⟩, hxU, -⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open (a := x) (by trivial) isOpen_univ
  obtain rfl : U = ⊤ := by ext y; simpa [Subsingleton.elim y x]
  exact .of_isIso (Scheme.topIso X).inv

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : P.RespectsRight IsOpenImmersion
⊢ P f ↔ ∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)

Tactic:
by
  refine ⟨fun hf x ↦ ⟨⊤, ⊤, trivial, by simp, resLE _ hf⟩, fun hf ↦ ?_⟩
  choose U V hxU e hf using hf
  rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (fun x : X ↦ V x) (P := P)]
  · intro x
    rw [← Scheme.Hom.resLE_comp_ι _ (e x)]
    exact MorphismProperty.RespectsRight.postcomp (Q := @IsOpenImmersion) _ inferInstance _ (hf x)
  · rw [eq_top_iff]
    rintro x -
    simp only [Opens.mem_iSup]
    use x, hxU x

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

Goal state before:
pp: case openCover
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U✝ : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U✝ i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U✝ i))
this : Q.IsLocal := isLocal_affineProperty P
U : ↑Y.affineOpens
s : Finset ↑Γ(Y, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : ↥s), Q (f ∣_ ↑(Y.affineBasicOpen ↑f_1))
r : ↑Γ(Y, ↑U)
hr' : r ∈ s
hr : (ConcreteCategory.hom (↑U).topIso.inv) r ∈ Finset.image (⇑(ConcreteCategory.hom (↑U).topIso.inv)) s
⊢ Q (f ∣_ ↑U ∣_ (↑↑U).basicOpen ↑⟨(ConcreteCategory.hom (↑U).topIso.inv) r, hr⟩)

Tactic:
exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r).symm).mp (H ⟨r, hr'⟩)

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
inst✝ : IsAffine Y
⊢ P f ↔ Q f

Tactic:
by
  let := isLocal_affineProperty P
  rw [iff_of_openCover (P := P) (Scheme.coverOfIsIso.{0} (𝟙 Y))]
  trans Q (pullback.snd f (𝟙 _))
  · exact ⟨fun H => H PUnit.unit, fun H _ => H⟩
  rw [← Category.comp_id (pullback.snd _ _), ← pullback.condition,
    Q.cancel_left_of_respectsIso]

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:
exact H ⟨_, V.2.image_of_isOpenImmersion (Y.ofRestrict _)⟩

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.f j i).c.app
      (op
        ((Opens.map
              (colimit.ι D.diagram.multispan
                  (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
          (⋯.functor.obj U))))

Tactic:
D.ι_image_preimage_eq i j U

Goal state after:
case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.f j i).c.app
      (op ((opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U)))))
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
⊢ IsZariskiLocalAtTarget (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective)

Tactic:
refine topologically_isZariskiLocalAtTarget _ (fun _ s _ _ h ↦ h.restrictPreimage s) ?_

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1}
    (U : ι → Opens β),
    IsOpenCover U →
      Continuous f → (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: A B C : CommRingCat
f : A ⟶ B
g : A ⟶ C
⊢ IsPullback (Spec.map (pushout.inl f g)) (Spec.map (pushout.inr f g)) (Spec.map f) (Spec.map g)

Tactic:
by
  apply isPullback_SpecMap_of_isPushout
  exact IsPushout.of_hasPushout f g

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
f : R →+* S
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hs : Ideal.span s = ⊤
h : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
⊢ s ⊆ ↑(Ideal.span {g | P ((algebraMap S (Localization.Away g)).comp f)})

Tactic:
intro g

Goal state after:
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
f : R →+* S
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hs : Ideal.span s = ⊤
h : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
g : S
⊢ g ∈ s → g ∈ ↑(Ideal.span {g | P ((algebraMap S (Localization.Away g)).comp f)})
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: 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
hPb : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
hf : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
⊢ {g | P ((algebraMap T (Localization.Away g)).comp (algebraMap R T))} ⊆
    ↑(Ideal.comap Algebra.TensorProduct.includeRight
        (Ideal.span {g | P ((algebraMap (S ⊗[R] T) (Localization.Away g)).comp (algebraMap S (S ⊗[R] T)))}))

Tactic:
intro g

Goal state after:
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
hPb : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
hf : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
g : T
⊢ g ∈ {g | P ((algebraMap T (Localization.Away g)).comp (algebraMap R T))} →
    g ∈
      ↑(Ideal.comap Algebra.TensorProduct.includeRight
          (Ideal.span {g | P ((algebraMap (S ⊗[R] T) (Localization.Away g)).comp (algebraMap S (S ⊗[R] T)))}))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
⊢ QuasiSeparatedSpace ↥X ↔ ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Tactic:
rw [quasiSeparatedSpace_iff]

Goal state after:
X : Scheme
⊢ (∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) ↔
    ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: case e'_5.snd
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := ⋯
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := ⋯
algInst✝ : Algebra ↑R ↑B := ⋯
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))
⊢ (L ((pullback.map (Spec.map φ) (Spec.map ψ) f g iX iY iS e₁ e₂) ((pullbackSpecIso ↑R ↑A ↑B).symm.hom x))).2 =
    (Prod.map (⇑iX) (⇑iY)
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B)
          ((pullbackSpecIso ↑R ↑A ↑B).hom ((pullbackSpecIso ↑R ↑A ↑B).symm.hom x)))).2

Tactic:
simp only [L, ← Scheme.Hom.comp_apply, pullback.lift_snd, Iso.symm_hom,
        Iso.inv_hom_id]

Goal state after:
case e'_5.snd
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑B := (CommRingCat.Hom.hom ψ).toAlgebra
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))
⊢ (pullback.snd (Spec.map φ) (Spec.map ψ) ≫ iY) ((pullbackSpecIso ↑R ↑A ↑B).inv x) =
    (Prod.map (⇑iX) (⇑iY)
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B) ((𝟙 (Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))) x))).2
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: case e'_5.snd
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑B := (CommRingCat.Hom.hom ψ).toAlgebra
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))
⊢ ((pullbackSpecIso ↑R ↑A ↑B).inv ≫ pullback.snd (Spec.map φ) (Spec.map ψ) ≫ iY) x =
    (Prod.map (⇑iX) (⇑iY)
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B) ((𝟙 (Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))) x))).2

Tactic:
pullbackSpecIso_inv_snd_assoc

Goal state after:
case e'_5.snd
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑B := (CommRingCat.Hom.hom ψ).toAlgebra
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))
⊢ (Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight) ≫ iY) x =
    (Prod.map (⇑iX) (⇑iY)
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B) ((𝟙 (Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))) x))).2