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

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W =
    X.presheaf.map ((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
      X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)
⊢ X.presheaf.map
      (((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
        inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op) =
    X.presheaf.map (homOfLE ⋯).op

Tactic:
]

Goal state after:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W =
    X.presheaf.map ((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
      X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)
⊢ X.presheaf.map
      (((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
        inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op) =
    X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: case mpr.refine_1
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ W ≤ (U ⊔ V) ⊓ W

Tactic:
]

Goal state after:
case mpr.refine_1
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ W ≤ (U ⊔ V) ⊓ W
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
⊢ (appIso (X.homOfLE h) W).hom ≫ X.presheaf.map (homOfLE ⋯).op =
    𝟙 (X.presheaf.obj (op (⋯.functor.obj (unop (op (X.homOfLE h ''ᵁ W))))))

Tactic:
]

Goal state after:
X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
⊢ (appIso (X.homOfLE h) W).hom ≫ X.presheaf.map (homOfLE ⋯).op =
    𝟙 (X.presheaf.obj (op (⋯.functor.obj (unop (op (X.homOfLE h ''ᵁ W))))))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
⊢ (∀ (x : ↥↑(⨆ i, U i)), ∃ i, x ∈ Set.range ⇑({ I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.f i)) ∧
    ∀ (i : { I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.I₀),
      IsOpenImmersion ({ I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.f i)

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
⊢ (∀ (x : ↥↑(⨆ i, U i)), ∃ i, x ∈ Set.range ⇑({ I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.f i)) ∧
    ∀ (i : { I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.I₀),
      IsOpenImmersion ({ I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.f i)
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: case mpr.refine_2
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
    (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x))

Tactic:
]

Goal state after:
case mpr.refine_2
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
    (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op) = X.presheaf.map ((eqToHom ⋯).op ≫ i)

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op) = X.presheaf.map ((eqToHom ⋯).op ≫ i)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
e : U = V
⊢ Set.range ⇑V.ι = Set.range ⇑V.ι

Tactic:
]

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
inst✝ : IsIso f
U : Y.Opens
⊢ ⇑(TopCat.Hom.hom f.base) '' ↑(f ⁻¹ᵁ U) = ↑U

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Y.Opens
⊢ ⇑(TopCat.Hom.hom f.base) '' ↑(f ⁻¹ᵁ U) = ↑U
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: case mpr.refine_3
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
    (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x))

Tactic:
]

Goal state after:
case mpr.refine_3
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
    (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
⊢ ⇑V.ι '' Set.range ⇑(V.ι ⁻¹ᵁ V.ι ''ᵁ V.ι ⁻¹ᵁ U).ι = ↑(V.ι ''ᵁ V.ι ⁻¹ᵁ U)

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
⊢ ⇑V.ι '' Set.range ⇑(V.ι ⁻¹ᵁ V.ι ''ᵁ V.ι ⁻¹ᵁ U).ι = ↑(V.ι ''ᵁ V.ι ⁻¹ᵁ U)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
hUV : U ≤ V
⊢ (isoOfLE hUV).hom ≫ U.ι = (V.ι ⁻¹ᵁ U).ι ≫ V.ι

Tactic:
by
  simp [isoOfLE]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
hUV : U ≤ V
⊢ (isoOfLE hUV).inv ≫ (V.ι ⁻¹ᵁ U).ι ≫ V.ι = U.ι

Tactic:
by
  simp [isoOfLE]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
R : CommRingCat
f g x : ↑R
hx : x = f * g
⊢ IsLocalization.Away (f * g) (Localization.Away (f * g))

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
R : CommRingCat
f g x : ↑R
hx : x = f * g
⊢ IsLocalization.Away (f * g) (Localization.Away (f * g))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: R : CommRingCat
f g : ↑R
⊢ ((basicOpenIsoSpecAway (f * g)).inv ≫ (Spec R).homOfLE ⋯) ≫ Scheme.Opens.ι (PrimeSpectrum.basicOpen f) =
    (Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv) ≫
      Scheme.Opens.ι (PrimeSpectrum.basicOpen f)

Tactic:
]

Goal state after:
R : CommRingCat
f g : ↑R
⊢ ((basicOpenIsoSpecAway (f * g)).inv ≫ (Spec R).homOfLE ⋯) ≫ Scheme.Opens.ι (PrimeSpectrum.basicOpen f) =
    (Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv) ≫
      Scheme.Opens.ι (PrimeSpectrum.basicOpen f)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (f ⁻¹ᵁ U).ι ≫ f = (f ⁻¹ᵁ U).ι ≫ f

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_1
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ V.ι ''ᵁ (Opens.map V.ι.base).obj U = U ⊓ V

Tactic:
]

Goal state after:
case refine_1
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ V.ι ''ᵁ (Opens.map V.ι.base).obj U = U ⊓ V
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ (𝟙 X ⁻¹ᵁ U).ι = U.ι

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
⊢ (𝟙 X ⁻¹ᵁ U).ι = U.ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.snd g (Scheme.Opens.ι U) =
    ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.snd g (Scheme.Opens.ι U) =
    ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv) ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U))) ≫
      pullback.fst g (Scheme.Opens.ι U) =
    (((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
        (pullbackRestrictIsoRestrict g U).inv) ≫
      pullback.fst g (Scheme.Opens.ι U)

Tactic:
]

Goal state after:
case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv) ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U))) ≫
      pullback.fst g (Scheme.Opens.ι U) =
    (((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
        (pullbackRestrictIsoRestrict g U).inv) ≫
      pullback.fst g (Scheme.Opens.ι U)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ ((f ≫ g) ⁻¹ᵁ U).ι ≫ f = (f ⁻¹ᵁ g ⁻¹ᵁ U).ι ≫ f

Tactic:
]

Goal state after:
case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ ((f ≫ g) ⁻¹ᵁ U).ι ≫ f = (f ⁻¹ᵁ g ⁻¹ᵁ U).ι ≫ f
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
W : (↑(f ⁻¹ᵁ U)).Opens
e : W ≤ (f ∣_ U) ⁻¹ᵁ V
⊢ Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ unop (op W)) ⋯ = Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ (Arrow.mk (f ∣_ Scheme.Hom.opensRange g)).hom) ≫ e.inv) ≫ g =
    (Arrow.mk (pullback.snd f g)).hom ≫ g

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ (Arrow.mk (f ∣_ Scheme.Hom.opensRange g)).hom) ≫ e.inv) ≫ g =
    (Arrow.mk (pullback.snd f g)).hom ≫ g
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
]

Goal state after:
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
this : n ↑i ↑j + 1 ≤ N
⊢ (g ↑i * g ↑j) ^ (N - (n ↑i ↑j + 1)) • (g ↑i * g ↑j) ^ (n ↑i ↑j + 1) • g ↑j • f ↑i =
    (g ↑i * g ↑j) ^ (N - (n ↑i ↑j + 1)) • (g ↑i * g ↑j) ^ (n ↑i ↑j + 1) • g ↑i • f ↑j

Tactic:
]

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 - (n ↑i ↑j + 1)) • (g ↑i * g ↑j) ^ (n ↑i ↑j + 1) • g ↑j • f ↑i =
    (g ↑i * g ↑j) ^ (N - (n ↑i ↑j + 1)) • (g ↑i * g ↑j) ^ (n ↑i ↑j + 1) • g ↑i • f ↑j
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x✝ : ↑X.toTopCat
⊢ X.toΓSpecFun x✝ ∈ basicOpen r ↔ IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.Γgerm x✝)) r)

Tactic:
]

Goal state after:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x✝ : ↑X.toTopCat
⊢ X.toΓSpecFun x✝ ∈ basicOpen r ↔ IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.Γgerm x✝)) r)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
⊢ ∀ s ∈ Set.range fun r ↦ ↑(basicOpen r), IsOpen (X.toΓSpecFun ⁻¹' s)

Tactic:
]

Goal state after:
X : LocallyRingedSpace
⊢ ∀ s ∈ Set.range fun r ↦ ↑(basicOpen r), IsOpen (X.toΓSpecFun ⁻¹' s)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ IsOpen ↑(X.toRingedSpace.basicOpen r)

Tactic:
]

Goal state after:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ IsOpen ↑(X.toRingedSpace.basicOpen r)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
⊢ resLE f U V e ⁻¹ᵁ O = resLE f U V e ⁻¹ᵁ O

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ (ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r =
    (ConcreteCategory.hom (X.toRingedSpace.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op))) r

Tactic:
]

Goal state after:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ (ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r =
    (ConcreteCategory.hom (X.toRingedSpace.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op))) r
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case e'_3
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 : ↥t
⊢ const ((fun i ↦ g ↑i ^ N • f ↑i) i) ((fun i ↦ g ↑i ^ (N + 1)) i) (basicOpen ((fun i ↦ g ↑i ^ (N + 1)) i)) ⋯ =
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map (homOfLE ?refine_2.convert_1).op))
      (const (f ↑i) (g ↑i) (basicOpen (g ↑i)) ⋯)

Tactic:
refine Subtype.ext <| funext fun x ↦ LocalizedModule.mk_eq.mpr ⟨1, ?_⟩

Goal state after:
case e'_3
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 : ↥t
x : ↥(unop (op (basicOpen ((fun i ↦ g ↑i ^ (N + 1)) i))))
⊢ 1 • ⟨g ↑i, ⋯⟩ • (fun i ↦ g ↑i ^ N • f ↑i) i = 1 • ⟨(fun i ↦ g ↑i ^ (N + 1)) i, ⋯⟩ • f ↑i
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
W : (↑V).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ (app (f ∣_ U) O ≫ app (X.homOfLE e) ((f ∣_ U) ⁻¹ᵁ O)) ≫ X.presheaf.map (homOfLE ⋯).op =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [morphismRestrict_app', appLE, homOfLE_leOfHom, homOfLE_app, Category.assoc]

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
W : (↑V).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (homOfLE ⋯).op =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))
⊢ ConcreteCategory.hom
        (CommRingCat.ofHom
            (algebraMap (↑(Γ.obj (op X)))
              ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))) ≫
          f) =
      (IsLocalization.Away.lift r ⋯).comp
        (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))) ↔
    f = X.toΓSpecCApp r

Tactic:
]

Goal state after:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))
⊢ ConcreteCategory.hom
        (CommRingCat.ofHom
            (algebraMap (↑(Γ.obj (op X)))
              ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))) ≫
          f) =
      (IsLocalization.Away.lift r ⋯).comp
        (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))) ↔
    f = X.toΓSpecCApp r