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

pp: case refine_3
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ∣_ W.ι ⁻¹ᵁ U ≫ (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ?refine_2).hom =
    (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

pp: case refine_4
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑V).hom =
    (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

pp: case refine_5
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (W.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑W).hom = (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ?refine_2).hom ≫ X.homOfLE hU

pp: case refine_6
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ≫ (Iso.refl ↑W).hom = (Iso.refl ↑V).hom ≫ X.homOfLE hV

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

Goal state after:
case refine_3
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ∣_ W.ι ⁻¹ᵁ U ≫ (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom =
    (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

case refine_4
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑V).hom =
    (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

case refine_5
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (W.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑W).hom = (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE hU

case refine_6
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ≫ (Iso.refl ↑W).hom = (Iso.refl ↑V).hom ≫ X.homOfLE hV
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : ↑U ⊆ ⋃ i ∈ t, ↑(basicOpen (g i))
N : ℕ := (t ×ˢ t).sup fun x ↦ n x.1 x.2 + 1
i j : ↥t
⊢ (g ↑i * g ↑j) ^ N • g ↑j • f ↑i = (g ↑i * g ↑j) ^ N • g ↑i • f ↑j

Tactic:
have : n i j + 1 ≤ N := (t ×ˢ t).le_sup (f := fun x ↦ n x.1 x.2 + 1) (b := ⟨_, _⟩) (by simp)

Goal state after:
case refine_1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : ↑U ⊆ ⋃ i ∈ t, ↑(basicOpen (g i))
N : ℕ := (t ×ˢ t).sup fun x ↦ n x.1 x.2 + 1
i j : ↥t
this : n ↑i ↑j + 1 ≤ N
⊢ (g ↑i * g ↑j) ^ N • g ↑j • f ↑i = (g ↑i * g ↑j) ^ N • g ↑i • f ↑j
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
simp [← cancel_mono W.ι]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: I : Type w
inst✝¹ : Category.{v, w} I
D : I ⥤ Scheme
inst✝ : ∀ (i : I), IsAffine (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this : ∀ (i : I), IsIso (α.app i)
⊢ PreservesLimit D Scheme.Γ.rightOp

Tactic:
have : IsIso α := NatIso.isIso_of_isIso_app α

Goal state after:
I : Type w
inst✝¹ : Category.{v, w} I
D : I ⥤ Scheme
inst✝ : ∀ (i : I), IsAffine (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this✝ : ∀ (i : I), IsIso (α.app i)
this : IsIso α
⊢ PreservesLimit D Scheme.Γ.rightOp
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq :
  (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))
this :
  (pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ inv (pullback.snd (D.f j i) (D.f j i))) ≫
      (pullback.fst (D.f j i) (D.f j i) ≫ D.t j i ≫ inv (pullback.snd (D.f i i) (D.f i j))) ≫
        (pullbackSymmetry (D.f i i) (D.f i j)).hom =
    𝟙 (pullback (D.f i j) (D.f i i))
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))

Tactic:
fst_eq_snd_of_mono_eq,

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq :
  (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))
this :
  (pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ inv (pullback.snd (D.f j i) (D.f j i))) ≫
      (pullback.snd (D.f j i) (D.f j i) ≫ D.t j i ≫ inv (pullback.snd (D.f i i) (D.f i j))) ≫
        (pullbackSymmetry (D.f i i) (D.f i j)).hom =
    𝟙 (pullback (D.f i j) (D.f i i))
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case e'_10
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)
e_5✝ : CommRing.toCommSemiring.toAddCommMonoid = inst✝⁴.toAddCommGroup.toAddCommMonoid
e_7✝ : Semiring.toModule ≍ Semiring.toModule
α : stalk (moduleStructurePresheaf R R).presheaf x ≅
  (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).obj ((structurePresheafInCommRingCat R).stalk x) := ⋯
this :
  germ (moduleStructurePresheaf R R).presheaf ⊤ x ⋯ ≫ α.hom =
    (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).map ((structurePresheafInCommRingCat R).germ ⊤ x ⋯)
⊢ (Algebra.linearMap R ↑((structurePresheafInCommRingCat R).stalk x)) 1 =
    (↑(commRingCatStalkEquivModuleStalk R x) ∘ₗ toStalkₗ R R x) 1

Tactic:
dsimp [toStalkₗ]

Goal state after:
case e'_10
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)
e_5✝ : CommRing.toCommSemiring.toAddCommMonoid = inst✝⁴.toAddCommGroup.toAddCommMonoid
e_7✝ : Semiring.toModule ≍ Semiring.toModule
α : stalk (moduleStructurePresheaf R R).presheaf x ≅
  (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).obj ((structurePresheafInCommRingCat R).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)) }
this :
  germ (moduleStructurePresheaf R R).presheaf ⊤ x ⋯ ≫ α.hom =
    (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).map ((structurePresheafInCommRingCat R).germ ⊤ x ⋯)
⊢ (algebraMap R ↑((structurePresheafInCommRingCat R).stalk x)) 1 =
    (commRingCatStalkEquivModuleStalk R x)
      ((ConcreteCategory.hom (germ (moduleStructurePresheaf R R).presheaf ⊤ x ⋯)) ((toOpenₗ R R ⊤) 1))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
U✝ : X.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X, U✝)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
⊢ Arrow.mk (Scheme.Hom.stalkMap f x) ≅
    Arrow.mk
      (CommRingCat.ofHom
        (Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯))

Tactic:
let := Y.presheaf.algebra_section_stalk ⟨f x, hVU hx⟩

Goal state after:
X Y : Scheme
U✝ : X.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X, U✝)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩) := Y.presheaf.algebra_section_stalk ⟨f x, ⋯⟩
⊢ Arrow.mk (Scheme.Hom.stalkMap f x) ≅
    Arrow.mk
      (CommRingCat.ofHom
        (Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⋃ i, ⇑hU.fromSpec ⁻¹' ↑(X.basicOpen ↑i) = ⇑hU.fromSpec ⁻¹' U.carrier ↔
    ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ

Tactic:
congr! 1

Goal state after:
case e'_2
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum ↑Γ(X, U))
⊢ ⋃ i, ⇑hU.fromSpec ⁻¹' ↑(X.basicOpen ↑i) = ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier

case e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum ↑Γ(X, U))
⊢ ⇑hU.fromSpec ⁻¹' U.carrier = Set.univ
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ IsOpen
    (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ''
      (imageBasicOpen f g U s).carrier)

Tactic:
rw [← (TopCat.homeoOfIso (PreservesCoequalizer.iso (SheafedSpace.forget _) f.toShHom
    g.toShHom)).isOpen_preimage, TopCat.coequalizer_isOpen_iff, ← Set.preimage_comp]
  erw [← TopCat.coe_comp]
  rw [PreservesCoequalizer.iso_hom, ι_comp_coequalizerComparison]
  dsimp only [SheafedSpace.forget]
  rw [imageBasicOpen_image_preimage]
  exact (imageBasicOpen f g U s).2

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: 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.zeroLocus ↑(I ⊓ J) = X.zeroLocus ↑I ∪ X.zeroLocus ↑J

Tactic:
by
    ext x
    by_cases hxU : x ∈ U
    · simpa [hxU] using congr(⟨x, hxU⟩ ∈ $this)
    · simp only [Submodule.coe_inf, Set.mem_union,
        codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) (I ∩ J)) hxU,
        codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) I) hxU, true_or]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.t i j ≫ D.f j i)) '' ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U

Tactic:
convert! D.preimage_image_eq_image i j U using 1

Goal state after:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.t i j ≫ D.f j i)) '' ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U =
    ⇑(ConcreteCategory.hom (D.f j i)) '' ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.f j i)) '' ⇑(ConcreteCategory.hom (D.t i j)) '' ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U =
    ⇑(ConcreteCategory.hom (D.f j i)) '' ⇑(ConcreteCategory.hom (D.f i j)) ∘ ⇑(ConcreteCategory.hom (D.t j i)) ⁻¹' U

Tactic:
congr! 1

Goal state after:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.t i j)) '' ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U =
    ⇑(ConcreteCategory.hom (D.f i j)) ∘ ⇑(ConcreteCategory.hom (D.t j i)) ⁻¹' U
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
U : Opens ↑(D.U i)
⊢ IsOpen (⇑(ConcreteCategory.hom (D.ι i)) '' ↑U)

Tactic:
isOpen_iff

Goal state after:
D : GlueData
i : D.J
U : Opens ↑(D.U i)
⊢ ∀ (i_1 : D.J), IsOpen (⇑(ConcreteCategory.hom (D.ι i_1)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' ↑U)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case e'_3
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
e_1✝ : ↑((Opens.toTopCat (of α)).obj (U i)) = ↑((ofOpenSubsets U).U i)
⊢ ⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹'
      ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) ⁻¹' ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s =
    ⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s

Tactic:
congr! 1

Goal state after:
case e'_3.e'_4
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
e_1✝ : ↑((Opens.toTopCat (of α)).obj (U i)) = ↑((ofOpenSubsets U).U i)
⊢ ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) ⁻¹' ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s = s
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case e'_3
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
e_1✝ : ↥(𝒰.X (idx 𝒰 x)) = ↥((gluedCover 𝒰).U (idx 𝒰 x))
⊢ ⇑(TopCat.Hom.hom ((gluedCover 𝒰).ι (idx 𝒰 x)).base) ⁻¹'
      ⇑(TopCat.Hom.hom (fromGlued 𝒰).base) ⁻¹' (fun a ↦ (fromGlued 𝒰) a) '' U =
    ⇑((gluedCover 𝒰).ι (idx 𝒰 x)) ⁻¹' U

Tactic:
congr! 1

Goal state after:
case e'_3.e'_4
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
e_1✝ : ↥(𝒰.X (idx 𝒰 x)) = ↥((gluedCover 𝒰).U (idx 𝒰 x))
⊢ ⇑(TopCat.Hom.hom (fromGlued 𝒰).base) ⁻¹' (fun a ↦ (fromGlued 𝒰) a) '' U = U
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀.h₀
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 ≫
          pullback.snd (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k))
            (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.fst (𝒰.f j ≫ f) g =
    ((pullback.fst (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
            (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
          t 𝒰 f g i j) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.fst (𝒰.f j ≫ f) g

Tactic:
simp only [t'_snd_fst_fst, t'_snd_fst_snd, t'_snd_snd, t_fst_fst, t_fst_snd, t_snd,
        Category.assoc]

Goal state after:
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
i j k : 𝒰.I₀
⊢ ((t' 𝒰 f g i j k ≫
          pullback.snd (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k))
            (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.snd (𝒰.f j ≫ f) g =
    ((pullback.fst (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
            (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
          t 𝒰 f g i j) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.snd (𝒰.f j ≫ f) g

Tactic:
simp only [t'_snd_fst_fst, t'_snd_fst_snd, t'_snd_snd, t_fst_fst, t_fst_snd, t_snd,
        Category.assoc]

Goal state after:
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
i j k : 𝒰.I₀
⊢ (t' 𝒰 f g i j k ≫
        pullback.snd (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k))
          (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))) ≫
      pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) =
    (pullback.fst (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
          (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
        t 𝒰 f g i j) ≫
      pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)

Tactic:
simp only [t'_snd_fst_fst, t'_snd_fst_snd, t'_snd_snd, t_fst_fst, t_fst_snd, t_snd,
        Category.assoc]

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

Goal state before:
pp: case op.op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X Y : WalkingMultispan (MultispanShape.prod D.J)
f : Y ⟶ X
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f.op ≫
      D.ιInvAppπApp U (unop (op Y)) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map f.op

Tactic:
rcases f with (_ | ⟨j, k⟩ | ⟨j, k⟩)

Goal state after:
case op.op.id
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X : WalkingMultispan (MultispanShape.prod D.J)
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map
        (Quiver.Hom.op (WalkingMultispan.Hom.id X)) ≫
      D.ιInvAppπApp U (unop (op X)) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map (Quiver.Hom.op (WalkingMultispan.Hom.id X))

case op.op.fst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))) ≫
      D.ιInvAppπApp U (unop (op (WalkingMultispan.left (j, k)))) =
    D.ιInvAppπApp U (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))) ≫
      (D.diagramOverOpen U).map (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k)))

case op.op.snd
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map
        (Quiver.Hom.op (WalkingMultispan.Hom.snd (j, k))) ≫
      D.ιInvAppπApp U (unop (op (WalkingMultispan.left (j, k)))) =
    D.ιInvAppπApp U (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (j, k))))) ≫
      (D.diagramOverOpen U).map (Quiver.Hom.op (WalkingMultispan.Hom.snd (j, k)))
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
k₁ k₂ : (Opens.iSupOpenCover fun k ↦ Hom.opensRange (F.map k.snd.1)).I₀
⊢ pullback.fst ((Opens.iSupOpenCover fun k ↦ Hom.opensRange (F.map k.snd.1)).f k₁)
        ((Opens.iSupOpenCover fun k ↦ Hom.opensRange (F.map k.snd.1)).f k₂) ≫
      (Hom.isoOpensRange (F.map k₁.snd.1)).inv ≫ F.map k₁.snd.2 =
    pullback.snd ((Opens.iSupOpenCover fun k ↦ Hom.opensRange (F.map k.snd.1)).f k₁)
        ((Opens.iSupOpenCover fun k ↦ Hom.opensRange (F.map k.snd.1)).f k₂) ≫
      (Hom.isoOpensRange (F.map k₂.snd.1)).inv ≫ F.map k₂.snd.2

Tactic:
by
      dsimp [Scheme.Opens.iSupOpenCover]
      apply fst_inv_eq_snd_inv F

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case right
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ Function.Injective
    ⇑(ConcreteCategory.hom ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init WalkingPair.right)))

Tactic:
simpa using! g.isOpenEmbedding.injective

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: I : Type u_1
inst✝¹ : Category.{v_1, u_1} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝ : ∀ (i : I), IsAffine (D.obj i)
α : D ⟶ (D ⋙ Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this : ∀ (i : I), IsIso (α.app i)
⊢ IsAffine c.pt

Tactic:
have : IsIso α := NatIso.isIso_of_isIso_app α

Goal state after:
I : Type u_1
inst✝¹ : Category.{v_1, u_1} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝ : ∀ (i : I), IsAffine (D.obj i)
α : D ⟶ (D ⋙ Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this✝ : ∀ (i : I), IsIso (α.app i)
this : IsIso α
⊢ IsAffine c.pt
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case H
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
X Y : Scheme
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : P.HasOfPostcompProperty IsOpenImmersion
f : X ⟶ Y
U : ↥X → Y.Opens
h₁ : ∀ (x : ↥X), f x ∈ U x
h₂ : ∀ (x : ↥X), P ((f ⁻¹ᵁ U x).ι ≫ f)
⊢ Set.range ⇑f ⊆ ↑(⨆ i, U i)

Tactic:
rintro y ⟨x, rfl⟩
    simp only [Opens.coe_iSup, Set.mem_iUnion, SetLike.mem_coe]
    exact ⟨x, h₁ x⟩

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

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
hf : P f
i : 𝒰.I₀
⊢ P (pullback.snd f (𝒰.f i))

Tactic:
apply hP _ (𝒰.f i)
    rw [← pullback.condition]
    exact IsZariskiLocalAtSource.comp hf _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_2.h₀.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) ≫
      pullback.fst ((𝒱 i).f j) ((𝒱 i).f j) =
    ((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.diagonal ((𝒱 i).f j)) ≫
      pullback.fst ((𝒱 i).f j) ((𝒱 i).f j)

Tactic:
simp [H]

Goal state after: