mathlib-initiative/mathlib-tactics huggingface dataset:
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.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R✝ S✝ : CommRingCat
f✝ : R✝ ⟶ S✝
p✝ : PrimeSpectrum ↑S✝
x : PrimeSpectrum ↑R✝
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).hom ≫
      (Arrow.mk
          (CommRingCat.ofHom
            (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
              (CommRingCat.Hom.hom f) ⋯))).hom =
    (Arrow.mk (Hom.stalkMap (Spec.map f) p)).hom ≫ (Spec.stalkIso S p).hom

Tactic:
rw [← Scheme.localRingHom_comp_stalkIso]
    simp

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : J
⊢ ⇑(ConcreteCategory.hom (ofHom { toFun := fun x ↦ ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ })) = id

Tactic:
by ext; rfl

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 (D.f i j) (D.f i k)).base) ''
      ⇑(ConcreteCategory.hom (pullback.fst (D.f i j) (D.f i k)).base) ⁻¹' S =
    ⇑(ConcreteCategory.hom (D.f i k).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) '' S

Tactic:
rw [← eq₁, ← eq₂, TopCat.coe_comp, Set.image_comp, TopCat.coe_comp, Set.preimage_comp,
    Set.image_preimage_eq]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
S : Set ↑↑(D.V (i, j))
eq₁ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.fst (D.f i j) (D.f i k)).base
eq₂ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.snd (D.f i j) (D.f i k)).base
⊢ ⇑(ConcreteCategory.hom (pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)))) ''
      ⇑(ConcreteCategory.hom (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

case h
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
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ (D.ι i) x = (D.ι j) y ↔
    (ConcreteCategory.hom
          (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i))
        x =
      (ConcreteCategory.hom
          (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι j))
        y

Tactic:
rw [← ((TopCat.mono_iff_injective D.isoCarrier.inv).mp _).eq_iff, ← ConcreteCategory.comp_apply]

Goal state after:
D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ (D.ι i) x = (D.ι j) y ↔
    (ConcreteCategory.hom
          (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom D.isoCarrier.inv)
        ((ConcreteCategory.hom
            (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι j))
          y)

D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ Mono D.isoCarrier.inv
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

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

Tactic:
← (D.V (i, k)).presheaf.map_comp

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

Goal state before:
pp: case w
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))
⊢ ⇑(ConcreteCategory.hom (D.t k i).base) ⁻¹' ⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) '' ↑U =
    ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U

Tactic:
have := (𝖣.t_fac k i j).symm

Goal state after:
case w
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))
this : pullback.fst (D.f k i) (D.f k j) ≫ D.t k i = D.t' k i j ≫ pullback.snd (D.f i j) (D.f i k)
⊢ ⇑(ConcreteCategory.hom (D.t k i).base) ⁻¹' ⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) '' ↑U =
    ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U
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
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 (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g ⟶ v 𝒰 f g j i

Tactic:
refine ?_ ≫ (pullbackAssoc ..).hom ≫ (pullbackSymmetry ..).hom

Goal state after:
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 (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g ⟶ pullback (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥Y
⊢ IsIso f

Tactic:
have : IsEmpty X := f.base.hom.1.isEmpty
  have : Epi f.base := by
    rw [TopCat.epi_iff_surjective]; rintro (x : Y)
    exact isEmptyElim x
  apply IsOpenImmersion.isIso

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case inst
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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst
hlk : l ⟶ k₂.fst
z : (F ⋙ forget).obj l
hy₁ : (F.map k₁.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hli)) z) = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
hy₂ : (F.map k₂.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hlk)) z) = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι := ⋯
⊢ IsOpenImmersion (α ≫ pullback.fst (V F i j).ι (V F i k).ι)

Tactic:
· simp only [limit.lift_π, PullbackCone.mk_π_app, α]
      infer_instance

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
⊢ (gluing 𝒰 f g).glued ⟶ Y

Tactic:
apply Multicoequalizer.desc _ _ fun i ↦ pullback.snd _ _

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
⊢ ∀ (a : (MultispanShape.prod (gluing 𝒰 f g).J).L),
    (gluing 𝒰 f g).diagram.fst a ≫ pullback.snd (𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).fst a) ≫ f) g =
      (gluing 𝒰 f g).diagram.snd a ≫ pullback.snd (𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).snd a) ≫ f) g
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        (pullback.fst (D.f j i) (D.f j k)).c.app
            (op ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
          invApp (pullback.snd (D.f j i) (D.f j k))
              ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).1
                ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              ((TopCat.Presheaf.pushforward C (D.f j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯).op =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)

Tactic:
erw [← (D.V (j, k)).presheaf.map_comp]
      · simp_rw [← Category.assoc]
        erw [← comp_c_app, ← comp_c_app]
        · simp_rw [Category.assoc]
          dsimp only [Functor.op, unop_op, Quiver.Hom.unop_op]
          rw [eqToHom_map (Opens.map _), eqToHom_op, eqToHom_trans]
          congr

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i✝ : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
i j : WalkingPair
hij : WalkingPair.right ≠ WalkingPair.left
⊢ Function.onFun Disjoint (fun x ↦ Scheme.Hom.opensRange (fi x)) WalkingPair.right WalkingPair.left

Tactic:
simpa [fi] using hf.1.symm

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
i j : J
l : (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).I₀
x : ↥((Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).X l)
⊢ (TopCat.Hom.hom (F.map l.snd.2).base) ((TopCat.Hom.hom (Hom.isoOpensRange (F.map l.snd.1)).inv.base) x) ∈
    ⋃ i_1, Set.range ⇑(F.map i_1.snd.1)

Tactic:
exact Set.mem_iUnion.mpr ⟨⟨l.1, l.2.2, l.2.1⟩, ⟨_, rfl⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
by
    suffices IsVanKampenColimit (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) from
      this.of_iso (hc.uniqueUpToIso (coprodIsCoprod _ _)).symm
    refine BinaryCofan.isVanKampen_mk _ _ (fun _ _ ↦ coprodIsCoprod _ _) _
      (fun _ _ ↦ pullbackIsPullback _ _) ?_ ?_
    · intro X' Y' αX αY f h₁ h₂
      have h₁' (x : _) := congr($h₁ x).symm
      have h₂' (x : _) := congr($h₂ x).symm
      dsimp at h₁ h₂ h₁' h₂'
      refine ⟨(IsOpenImmersion.isPullback _ _ _ _ h₁.symm ?_).flip,
        (IsOpenImmersion.isPullback _ _ _ _ h₂.symm ?_).flip⟩ <;>
        ext x <;> obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x <;> simp_all
    · dsimp
      refine fun {Z} f ↦ (nonempty_isColimit_binaryCofanMk_of_isCompl _ _ ?_).some
      rw [Scheme.Hom.opensRange_pullbackFst, Scheme.Hom.opensRange_pullbackFst]
      convert! (isCompl_range_inl_inr X Y).map (CompleteLatticeHom.setPreimage f)
      simp [isCompl_iff, disjoint_iff, codisjoint_iff, ← TopologicalSpace.Opens.coe_inj]

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 : ↑Γ(↑↑U, ⊤)
hr : r ∈ Finset.image (⇑(ConcreteCategory.hom (↑U).topIso.inv)) s
⊢ Q (f ∣_ ↑U ∣_ (↑↑U).basicOpen ↑⟨r, hr⟩)

Tactic:
obtain ⟨r, hr', rfl⟩ := Finset.mem_image.mp hr

Goal state after:
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⟩)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case mp
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : J
ki : k ⟶ ↓(i, j).1
kj : k ⟶ ↓(i, j).2
y : ↥(F.obj ⟨k, (ki, kj)⟩.fst)
hy : (F.map ki) y = ((glueData F).f i j) x
⊢ ∃ k fi fj x_1, (F.map fi) x_1 = ((glueData F).f i j) x ∧ (F.map fj) x_1 = ((glueData F).t i j ≫ (glueData F).f j i) x

Tactic:
refine ⟨k, ki, kj, y, hy, ?_⟩

Goal state after:
case mp
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : J
ki : k ⟶ ↓(i, j).1
kj : k ⟶ ↓(i, j).2
y : ↥(F.obj ⟨k, (ki, kj)⟩.fst)
hy : (F.map ki) y = ((glueData F).f i j) x
⊢ (F.map kj) y = ((glueData F).t i j ≫ (glueData F).f j i) x
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
m : s.pt ⟶ (D.vPullbackCone i j).pt
⊢ m ≫ (D.vPullbackCone i j).fst = s.fst → m ≫ (D.vPullbackCone i j).snd = s.snd → m = lift (D.f i j) s.fst ⋯

Tactic:
e₁

Goal state after:
case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
m : s.pt ⟶ (D.vPullbackCone i j).pt
e₁ : m ≫ (D.vPullbackCone i j).fst = s.fst
⊢ m ≫ (D.vPullbackCone i j).snd = s.snd → m = lift (D.f i j) s.fst ⋯
Module: Mathlib.RingTheory.RingHom.Surjective

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

Tactic:
introv R H x
  obtain ⟨x, ⟨_, s, hs, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (M.map f) x
  obtain ⟨y, rfl⟩ := H x
  use IsLocalization.mk' R' y ⟨s, hs⟩
  rw [IsLocalization.map_mk']

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

Goal state before:
pp: case of_sSup_eq_top.x
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
H : ∀ (i : ι), P.universally (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
hU : ⊤ ≤ iSup U
x : ↥Y'
⊢ x ∈ ⨆ i, i₂ ⁻¹ᵁ U i

Tactic:
simpa using @hU (i₂ x) trivial

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

Goal state before:
pp: 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
f' : Spec A ⟶ Spec R
g' : Spec B ⟶ Spec R
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
⊢ ∀ (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))

Tactic:
e₁

Goal state after:
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
f' : Spec A ⟶ Spec R
g' : Spec B ⟶ Spec R
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
e₁ : f' ≫ iS = iX ≫ f
⊢ ∀ (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
⊢ QuasiSeparatedSpace ↥X ↔ QuasiCompact (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom)

Tactic:
← HasAffineProperty.iff_of_isAffine (f := terminal.from X) (P := @QuasiSeparated),

Goal state after:
X : Scheme
⊢ QuasiSeparated (terminal.from X) ↔ QuasiCompact (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], SpecializingMap ⇑f → (∃ R, Y = Spec R) → IsClosedMap ⇑f
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x✝ : QuasiCompact (Scheme.Cover.pullbackHom Y.affineCover f i)
⊢ topologically (@IsClosedMap) (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
refine this (Y.affineCover.pullbackHom f i) ?_ ⟨_, rfl⟩

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], SpecializingMap ⇑f → (∃ R, Y = Spec R) → IsClosedMap ⇑f
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x✝ : QuasiCompact (Scheme.Cover.pullbackHom Y.affineCover f i)
⊢ SpecializingMap ⇑(Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
this :
  ∀ (i : (X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).I₀),
    IsAffine ((X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).X i)
i : (X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).I₀
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).f i ≫ f)))

Tactic:
simpa [Scheme.Hom.app_eq_appLE] using (f.appLE_congr _ rfl (by simp) (fun f => Q f.hom)).mp (H i)

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

Goal state before:
pp: case ofLocalizationSpanTarget
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)
i : (Scheme.affineOpenCoverOfSpanRangeEqTop (fun i ↦ ↑i) ⋯).openCover.I₀
⊢ P ((Scheme.affineOpenCoverOfSpanRangeEqTop (fun i ↦ ↑i) ⋯).openCover.f i ≫ Spec.map (CommRingCat.ofHom f))

Tactic:
simp only [CommRingCat.coe_of, ← Spec.map_comp,
      Scheme.AffineOpenCover.openCover_f, Scheme.affineOpenCoverOfSpanRangeEqTop_f]

Goal state after:
case ofLocalizationSpanTarget
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)
i : (Scheme.affineOpenCoverOfSpanRangeEqTop (fun i ↦ ↑i) ⋯).openCover.I₀
⊢ P (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap S (Localization.Away ↑i))))
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case inr
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
h : U.carrier.Nonempty
⊢ _root_.IsReduced ↑Γ(X, U)

Tactic:
have : Nonempty U := by simpa

Goal state after:
case inr
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
h : U.carrier.Nonempty
this : Nonempty ↥↑U
⊢ _root_.IsReduced ↑Γ(X, U)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
U : Opens ↥X
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f s : ↑Γ(X, U)
hf : (f |_ X.basicOpen s) ⋯ = 0
h : ∃ n, s ^ n * f = s ^ n * 0
⊢ ∃ n, s ^ n * f = 0

Tactic:
by
    simpa using h

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

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
⊢ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
· intro x
    obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
    rw [← (IsIso.comp_inv_eq _).mpr (Scheme.Hom.stalkMap_comp (𝒰.f i) f x)]
    infer_instance

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

Goal state before:
pp: X : Scheme
I✝ I J K : X.IdealSheafData
x✝¹ : ℕ
x✝ : X.IdealSheafData
⊢ x✝ ^ (x✝¹ + 1) = x✝ ^ x✝¹ * x✝

Tactic:
by ext; rfl

Goal state after: