mathlib-initiative/mathlib-tactics huggingface dataset:
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
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(colimit F)
j k : Jᵒᵖ
f : j ⟶ k
⊢ (Opens.map (F.map f.unop).base).op.obj (op ((Opens.map (colimit.ι F (unop j)).base).obj U)) =
    op ((Opens.map (colimit.ι F (unop k)).base).obj U)

Tactic:
← colimit.w F f.unop,

Goal state after:
J : Type u'
inst✝² : Category.{v', u'} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(colimit F)
j k : Jᵒᵖ
f : j ⟶ k
⊢ (Opens.map (F.map f.unop).base).op.obj (op ((Opens.map (colimit.ι F (unop j)).base).obj U)) =
    op ((Opens.map (F.map f.unop ≫ colimit.ι F (unop j)).base).obj U)
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
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U V : (Opens ↑↑s.pt)ᵒᵖ
i : U ⟶ V
⊢ s.pt.presheaf.map i ≫ descCApp F s V =
    descCApp F s U ≫
      ((pushforward C (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (colimitCocone F).pt.presheaf).map i

Tactic:
by
  dsimp [descCApp]
  refine limit_obj_ext (fun j => ?_)
  have w := Functor.congr_hom (congr_arg Opens.map
    (colimit.ι_desc ((PresheafedSpace.forget C).mapCocone s) (unop j))) i.unop
  simp only [Opens.map_comp_map] at w
  simp [congr_arg Quiver.Hom.op w]

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

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
⊢ (Opens.map f.base).obj (Y.toRingedSpace.basicOpen s) =
    X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s)

Tactic:
ext x
  constructor
  · rintro ⟨hxU, hx⟩
    rw [SetLike.mem_coe, X.toRingedSpace.mem_basicOpen _ _ hxU]
    delta toRingedSpace
    rw [← stalkMap_germ_apply]
    exact (f.stalkMap _).hom.isUnit_map hx
  · rintro ⟨hxU, hx⟩
    simp only [Opens.map_coe, Set.mem_preimage, SetLike.mem_coe, toRingedSpace] at hx ⊢
    rw [RingedSpace.mem_basicOpen _ s (f.base x) hxU]
    rw [← stalkMap_germ_apply] at hx
    exact (isUnit_map_iff (f.stalkMap x).hom _).mp hx

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

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
⊢ (Opens.map f.base).obj (Y.toRingedSpace.basicOpen s) =
    X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s)

Tactic:
by
  ext x
  constructor
  · rintro ⟨hxU, hx⟩
    rw [SetLike.mem_coe, X.toRingedSpace.mem_basicOpen _ _ hxU]
    delta toRingedSpace
    rw [← stalkMap_germ_apply]
    exact (f.stalkMap _).hom.isUnit_map hx
  · rintro ⟨hxU, hx⟩
    simp only [Opens.map_coe, Set.mem_preimage, SetLike.mem_coe, toRingedSpace] at hx ⊢
    rw [RingedSpace.mem_basicOpen _ s (f.base x) hxU]
    rw [← stalkMap_germ_apply] at hx
    exact (isUnit_map_iff (f.stalkMap x).hom _).mp hx

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

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
k : ℕ
h : 0 < k + Nat.succ 0
⊢ X.basicOpen (f ^ (k + Nat.succ 0)) = X.basicOpen f
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1.refine_1
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : (ConcreteCategory.hom ((P.cocone x).ι.app U)) ⟨fU, hU⟩ = (ConcreteCategory.hom ((P.cocone x).ι.app V)) ⟨fV, hV⟩
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w : ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
⊢ ↑(unop (op W)) ⟶ ↑(unop U)

Tactic:
rcases W with ⟨W, m⟩

Goal state after:
case refine_1.refine_1
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : (ConcreteCategory.hom ((P.cocone x).ι.app U)) ⟨fU, hU⟩ = (ConcreteCategory.hom ((P.cocone x).ι.app V)) ⟨fV, hV⟩
W : Opens ↑X
m : x ∈ W
iU : ⟨W, m⟩ ⟶ unop U
iV : ⟨W, m⟩ ⟶ unop V
w : ∀ (w : ↥↑⟨W, m⟩), fU (iU w) = fV (iV w)
⊢ ↑(unop (op ⟨W, m⟩)) ⟶ ↑(unop U)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Function.Injective fun x ↦ f ''ᵁ x

Tactic:
intro U V hUV

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U V : X.Opens
hUV : (fun x ↦ f ''ᵁ x) U = (fun x ↦ f ''ᵁ x) V
⊢ U = V
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
f : R
inst✝ : IsLocalization.Away f S
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap R S)))

Tactic:
have e := (IsLocalization.algEquiv (.powers f) S
    (Localization.Away f)).symm.toAlgHom.comp_algebraMap
  rw [← e, CommRingCat.ofHom_comp, Spec.map_comp]
  have H : IsIso (CommRingCat.ofHom (IsLocalization.algEquiv
    (Submonoid.powers f) S (Localization.Away f)).symm.toAlgHom.toRingHom) := by
    exact inferInstanceAs (IsIso <| (IsLocalization.algEquiv
      (Submonoid.powers f) S (Localization.Away f)).toRingEquiv.toCommRingCatIso.inv)
  simp only [AlgHom.toRingHom_eq_coe, AlgEquiv.toAlgHom_toRingHom] at H ⊢
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P✝ P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.IsStableUnderBaseChange
ι : Type (u + 1)
S : Scheme
X : ι → Scheme
f : (i : ι) → X i ⟶ S
hf : (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑(f i)) ∧ ∀ (i : ι), P (f i)
Y : Scheme
g : Y ⟶ S
T : ι → Scheme
p₁ : (i : ι) → T i ⟶ Y
p₂ : (i : ι) → T i ⟶ X i
H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : ↥Y
⊢ ∃ i, x ∈ Set.range ⇑(p₁ i)

Tactic:
obtain ⟨i, y, hy⟩ := hf.1 (g x)

Goal state after:
P✝ P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.IsStableUnderBaseChange
ι : Type (u + 1)
S : Scheme
X : ι → Scheme
f : (i : ι) → X i ⟶ S
hf : (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑(f i)) ∧ ∀ (i : ι), P (f i)
Y : Scheme
g : Y ⟶ S
T : ι → Scheme
p₁ : (i : ι) → T i ⟶ Y
p₂ : (i : ι) → T i ⟶ X i
H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : ↥Y
i : ι
y : ↥(X i)
hy : (f i) y = g x
⊢ ∃ i, x ∈ Set.range ⇑(p₁ i)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case neg.mpr
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
y : ↥V
hy : y ∈ ↑W
x : ↥(pullback iV f)
hx : (pullback.snd iV f) x ∉ Set.range ⇑iU
e : iV y = f ((pullback.snd iV f) x)
⊢ (pullback.snd iV f) x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)

Tactic:
← H.isoPullback_inv_snd

Goal state after:
case neg.mpr
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
y : ↥V
hy : y ∈ ↑W
x : ↥(pullback iV f)
hx : (H.isoPullback.inv ≫ iU) x ∉ Set.range ⇑iU
e : iV y = f ((pullback.snd iV f) x)
⊢ (pullback.snd iV f) x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
fg : Y ⟶ X
H : fg = f ≫ g
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V = (Scheme.Hom.appIso g V).inv ≫ Scheme.Hom.app fg (g ''ᵁ V) ≫ Y.presheaf.map (eqToHom ⋯).op

Tactic:
by
  subst H
  rw [Scheme.Hom.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
    ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
    eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case e'_2
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀
e_1✝ :
  (pullback (pullback.fst (𝒰.f i.fst) f) ((𝒰.X i.fst).affineCover.f i.snd) ⟶ X) =
    (pullback (pullback.fst (𝒰.f i.fst) f) ((𝒰.X i.fst).affineCover.f i.snd) ⟶ X)
⊢ (pullbackRightPullbackFstIso (𝒰.f i.fst) f ((𝒰.X i.fst).affineCover.f i.snd)).hom ≫
      pullback.snd (𝒰.affineRefinement.f i) f =
    pullback.snd ((𝒰.X i.fst).affineCover.f i.snd) (pullback.fst (𝒰.f i.fst) f) ≫ pullback.snd (𝒰.f i.fst) f

Tactic:
exact pullbackRightPullbackFstIso_hom_snd _ _ _

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

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (isoRestrict f).hom ≫ Y.ofRestrict ⋯ = f

Tactic:
apply LocallyRingedSpace.forgetToSheafedSpace.map_injective
  exact SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict f.toShHom

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_2
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ W.ι ''ᵁ W.ι ⁻¹ᵁ U = U

Tactic:
exact (W.functor_map_eq_inf U).trans (by simpa)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
r : ↑Γ(Y, U)
⊢ Arrow.mk (f ∣_ U ∣_ (↑U).basicOpen ((ConcreteCategory.hom (Y.presheaf.map (eqToHom ⋯).op)) r)) ≅
    Arrow.mk (f ∣_ Y.basicOpen r)

Tactic:
by
  refine morphismRestrictRestrict _ _ _ ≪≫ morphismRestrictEq _ ?_
  simp [Scheme.Opens.ι_image_basicOpen]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : V' ≤ V
⊢ resLE (𝟙 X) V V' i ≫ resLE f U V e = resLE f U V' ⋯

Tactic:
resLE_comp_resLE,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : V' ≤ V
⊢ resLE (𝟙 X ≫ f) U V' ⋯ = resLE f U V' ⋯
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : U ≤ U'
⊢ resLE f U V e ≫ resLE (𝟙 Y) U' U i = resLE f U' V ⋯

Tactic:
resLE_comp_resLE,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : U ≤ U'
⊢ resLE (f ≫ 𝟙 Y) U' V ⋯ = resLE f U' V ⋯
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ toStalk (↑(unop (op (Γ.obj (op X))))) ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ≫
      PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x =
    X.presheaf.Γgerm x

Tactic:
rw [PresheafedSpace.Hom.stalkMap,
    ← algebraMap_germ (basicOpen (1 : Γ.obj (op X))) _ (by rw [basicOpen_one]; trivial),
    ← Category.assoc, Category.assoc (CommRingCat.ofHom _), stalkFunctor_map_germ, ← Category.assoc,
    X.toΓSpecSheafedSpace_app_eq, X.toΓSpecCApp_spec, Γgerm,
    ← dsimp% stalkPushforward_germ _ _ X.presheaf ⊤]

Goal state after:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (X.toToΓSpecMapBasicOpen 1 ≫
        ((pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base).obj X.presheaf).germ (basicOpen 1)
          ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x =
    ((pushforward CommRingCat ?m.124).obj X.presheaf).germ ⊤ ((ConcreteCategory.hom ?m.124) x) True.intro ≫
      stalkPushforward CommRingCat ?m.124 X.presheaf x

X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ TopCat

X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ ↑X.toPresheafedSpace ⟶ ?m.123
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
⊢ ↑⊤ = ↑(Scheme.Hom.opensRange (𝟙 X))

Tactic:
exact Set.range_id.symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map (homOfLE ⋯).op ≫ Scheme.Hom.app hU.isoSpec.inv (U.ι ⁻¹ᵁ V) =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Tactic:
Scheme.Hom.app_eq _ this,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map (homOfLE ⋯).op ≫
      (↑U).presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.app hU.isoSpec.inv ⊤ ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ X.basicOpen (f * x) =
    X.basicOpen
      (x • ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x ↦ f ^ x) n, ⋯⟩))

Tactic:
rw [Algebra.smul_def, Scheme.basicOpen_mul, Scheme.basicOpen_mul, RingHom.algebraMap_toAlgebra,
    Scheme.basicOpen_res]

Goal state after:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ X.basicOpen f ⊓ X.basicOpen x =
    X.basicOpen f ⊓ X.basicOpen x ⊓
      X.basicOpen ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x ↦ f ^ x) n, ⋯⟩)
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
⊢ _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U

Tactic:
aesop (add safe constructors _root_.Equivalence)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
⊢ ↑D.glued.toPresheafedSpace ≅
    D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued

Tactic:
refine (PresheafedSpace.forget _).mapIso ?_ ≪≫
    GlueData.gluedIso _ (PresheafedSpace.forget.{_, _, u} _)
  refine SheafedSpace.forgetToPresheafedSpace.mapIso ?_ ≪≫
    SheafedSpace.GlueData.isoPresheafedSpace _
  refine LocallyRingedSpace.forgetToSheafedSpace.mapIso ?_ ≪≫
    LocallyRingedSpace.GlueData.isoSheafedSpace _
  exact Scheme.GlueData.isoLocallyRingedSpace _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
U : Set ↥D.glued
i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J
⊢ IsOpen
      (⇑(ConcreteCategory.hom
            (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)) ⁻¹'
        ⇑(TopCat.homeoOfIso D.isoCarrier.symm) ⁻¹' U) ↔
    IsOpen (⇑(D.ι i) ⁻¹' U)

Tactic:
rw [← Set.preimage_comp, ← ι_isoCarrier_inv]

Goal state after:
D : GlueData
U : Set ↥D.glued
i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J
⊢ IsOpen
      (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ∘
          ⇑(ConcreteCategory.hom
              (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)) ⁻¹'
        U) ↔
    IsOpen
      (⇑(ConcreteCategory.hom
            (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
              D.isoCarrier.inv)) ⁻¹'
        U)
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))
⊢ invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫
      invApp (pullback.snd (D.f i j) (D.f i k))
          (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).1 (unop (op U))))) ≫
        (D.V (i, k)).presheaf.map (eqToHom ⋯)

Tactic:
have := PresheafedSpace.congr_app (@pullback.condition _ _ _ _ _ (D.f i j) (D.f i k) _)
  dsimp only [comp_c_app] at this
  rw [← cancel_epi (inv ((D.f_open i j).invApp _ U)), IsIso.inv_hom_id_assoc,
    IsOpenImmersion.inv_invApp]
  simp_rw [Category.assoc]
  erw [(π₁ i, j, k).c.naturality_assoc, reassoc_of% this, ← Functor.map_comp_assoc,
    IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.app_invApp_assoc, ←
    (D.V (i, k)).presheaf.map_comp, ← (D.V (i, k)).presheaf.map_comp]
  convert! (Category.comp_id _).symm
  erw [(D.V (i, k)).presheaf.map_id]
  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
i j k : 𝒰.I₀
⊢ t' 𝒰 f g i j k ≫
      t' 𝒰 f g j k i ≫
        t' 𝒰 f g k i j ≫
          pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)

Tactic:
by
  simp only [t'_snd_snd, t'_fst_fst_fst, t'_fst_snd]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case a.inl
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥X
hxy : coprod.inl y = (coprod.map f g) ((coprodMk X Y) (Sum.inl x))
⊢ (coprodMk X Y) (Sum.inl x) ∈ Scheme.Hom.opensRange coprod.inl

Tactic:
← SetLike.mem_coe

Goal state after:
case a.inl
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥X
hxy : coprod.inl y = (coprod.map f g) ((coprodMk X Y) (Sum.inl x))
⊢ (coprodMk X Y) (Sum.inl x) ∈ ↑(Scheme.Hom.opensRange coprod.inl)
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 : 𝒰.I₀
⊢ pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫ (gluing 𝒰 f g).ι i =
    pullback.fst (p1 𝒰 f g) (𝒰.f i)

Tactic:
apply Cover.hom_ext ((gluing 𝒰 f g).openCover.pullback₁ (pullback.fst _ _))

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ ∀ (x : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀),
    (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).f x ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
          (gluing 𝒰 f g).ι i =
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).f x ≫
        pullback.fst (p1 𝒰 f g) (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := (Pi.evalRingHom R i).toAlgebra
⊢ IsLocalization.Away (Function.update 0 i 1) (R i)

Tactic:
apply IsLocalization.away_of_isIdempotentElem_of_mul

Goal state after:
case he
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := ⋯
⊢ IsIdempotentElem (Function.update 0 i 1)

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

case H'
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := ⋯
⊢ Function.Surjective ⇑(algebraMap ((a : ι) → R a) (R i))
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:
let := isLocal_affineProperty P
  rw [eq_targetAffineLocally P]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
s : Cocone F
i j : (glueData F).J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
dsimp [glueData, GlueData.diagram]

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

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
dsimp [glueData, GlueData.diagram]

Goal state after:
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g
s : PullbackCone f✝ g
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
i : (openCoverOfBase 𝒰 f f).I₀
j : (𝒱 i).I₀
H :
  pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      pullback.snd ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) =
    pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      pullback.fst ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))
⊢ ((pullback.map (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) (pullback.diagonal f)
            (pullback.map ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) f f
              ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯)
            (𝟙 X) (𝟙 ((diagonalCover f 𝒰 𝒱).X ⟨i, (j, j)⟩)) (𝟙 (pullback.diagonalObj f)) ⋯ ⋯ ≫
          (pullbackDiagonalMapIso f (𝒰.f i) ((𝒱 i).f j) ((𝒱 i).f j)).hom ≫
            CategoryTheory.inv (pullback.diagonal ((𝒱 i).f j))) ≫
        pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))) ≫
      pullback.snd ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) =
    (pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
        𝟙 ((diagonalCover f 𝒰 𝒱).X ⟨i, (j, j)⟩)) ≫
      pullback.snd ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))

Tactic:
· simp only [Category.assoc, pullback.diagonal_snd, Category.comp_id]
    simp only [← Category.assoc, IsIso.comp_inv_eq]
    apply pullback.hom_ext <;> simp [H]

Goal state after: