mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v, u₁} C
C' : Type u₂
inst✝¹ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j k : D.J
⊢ ((PreservesPullback.iso F (D.f i j) (D.f i k)).inv ≫
        F.map (D.t' i j k) ≫ (PreservesPullback.iso F (D.f j k) (D.f j i)).hom) ≫
      pullback.snd (F.map (D.f j k)) (F.map (D.f j i)) =
    pullback.fst (F.map (D.f i j)) (F.map (D.f i k)) ≫ F.map (D.t i j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v, u₁} C
C' : Type u₂
inst✝¹ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j k : D.J
⊢ ((PreservesPullback.iso F (D.f i j) (D.f i k)).inv ≫
        F.map (D.t' i j k) ≫ (PreservesPullback.iso F (D.f j k) (D.f j i)).hom) ≫
      ((PreservesPullback.iso F (D.f j k) (D.f j i)).inv ≫
          F.map (D.t' j k i) ≫ (PreservesPullback.iso F (D.f k i) (D.f k j)).hom) ≫
        (PreservesPullback.iso F (D.f k i) (D.f k j)).inv ≫
          F.map (D.t' k i j) ≫ (PreservesPullback.iso F (D.f i j) (D.f i k)).hom =
    𝟙 (pullback (F.map (D.f i j)) (F.map (D.f i k)))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↥X
hx : x ∈ U ⊓ V
⊢ ∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
⊢ f ≫ ↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g) = g ≫ ↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
s : Cofork f g
⊢ ⇑(hom s.π) ∘ ⇑(hom f) = ⇑(hom s.π) ∘ ⇑(hom g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
x✝¹ : Cofork f g
x✝ : (Cofork.ofπ (↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g)) ⋯).pt ⟶ x✝¹.pt
hm : (Cofork.ofπ (↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g)) ⋯).π ≫ x✝ = x✝¹.π
⊢ x✝ = ↾Function.Coequalizer.desc ⇑(hom f) ⇑(hom g) ⇑(hom x✝¹.π) ⋯

Tactic:
by

Goal state after:
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
⊢ ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ hU.fromSpec (hU.primeIdealOf x) = ↑x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
⊢ (comapFun f y) (LocalizedModule.mk a b) = LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
⊢ PrimeSpectrum.comap (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) (hV.primeIdealOf ⟨x, hx⟩) =
    hU.primeIdealOf ⟨f x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed {↑x}
⊢ IsClosed {x}

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed {↑x}
⊢ (hU.primeIdealOf x).asIdeal.IsMaximal

Tactic:
by

Goal state after:
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
⊢ ⇑(hom π) ⁻¹' ⇑(hom π) '' U = U

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v, u₁} C
C' : Type u₂
inst✝¹ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
⊢ ∀ {X Y : WalkingMultispan (MultispanShape.prod D.J)} (f : X ⟶ Y),
    (D.diagram.multispan ⋙ F).map f ≫
        (match Y with
          | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
          | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom =
      (match X with
          | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
          | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom ≫
        (D.mapGlueData F).diagram.multispan.map f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs : (isLocallyFraction R M).pred s
⊢ (isLocallyFraction S N).pred (comapFun f U V hUV s)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝² : HasMulticoequalizer D.diagram
inst✝¹ : PreservesColimit D.diagram.multispan F
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i : D.J
⊢ F.map (D.ι i) ≫ (D.gluedIso F).hom = (D.mapGlueData F).ι i

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s t : (structureSheafInType R M).obj.obj (op U)
x✝ : ↥(unop (op V))
⊢ ↑⟨comapFun f U V hUV ↑(s + t), ⋯⟩ x✝ = ↑(⟨comapFun f U V hUV ↑s, ⋯⟩ + ⟨comapFun f U V hUV ↑t, ⋯⟩) x✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
r : R
m : (structureSheafInType R M).obj.obj (op U)
x✝ : ↥(unop (op V))
⊢ ↑⟨comapFun f U V hUV ↑(r • m), ⋯⟩ x✝ = ↑(σ r • ⟨comapFun f U V hUV ↑m, ⋯⟩) x✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
a : M
b : R
hb : U ≤ basicOpen b
x✝ : ↥(unop (op V))
⊢ ↑((comapₗ f U V hUV) (const a b U hb)) x✝ = ↑(const (f a) (σ b) V ⋯) x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝² : HasMulticoequalizer D.diagram
inst✝¹ : PreservesColimit D.diagram.multispan F
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i : D.J
⊢ (D.mapGlueData F).ι i ≫ (D.gluedIso F).inv = F.map (D.ι i)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : hU.fromSpec y ∈ U
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec y))) y.asIdeal

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑x)) (hU.primeIdealOf x).asIdeal

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
x : WalkingCospan
⊢ (cospan (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅ (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Opens ↥Y
hU : IsAffineOpen U
x : ↥X
hx : f x ∈ U
h :
  ∀ (g : ↑(Y.presheaf.obj (op U))),
    (ConcreteCategory.hom (Scheme.Hom.stalkMap f x)) ((ConcreteCategory.hom (Y.presheaf.germ U (f x) hx)) g) = 0 →
      (ConcreteCategory.hom (Y.presheaf.germ U (f x) hx)) g = 0
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥V
⊢ ↑((comapₗ f.toSemilinearMap U V hUV) s) p =
    (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) (↑s ⟨PrimeSpectrum.comap f ↑p, ⋯⟩)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f✝ : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
x✝ : ↥(unop (op V))
⊢ ↑((comapₗ f.toSemilinearMap U V hUV).toFun 1) x✝ = ↑1 x✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f✝ : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
r s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op V))
⊢ ↑((comapₗ f.toSemilinearMap U V hUV) (r * s)) p =
    ↑((comapₗ f.toSemilinearMap U V hUV) r * (comapₗ f.toSemilinearMap U V hUV) s) p

Tactic:
change _ = (comapₗ f.toSemilinearMap U V hUV r).1 p * (comapₗ f.toSemilinearMap U V hUV s).1 p

Goal state after:
R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f✝ : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
r s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op V))
⊢ ↑((comapₗ f.toSemilinearMap U V hUV) (r * s)) p =
    ↑((comapₗ f.toSemilinearMap U V hUV) r) p * ↑((comapₗ f.toSemilinearMap U V hUV) s) p
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f✝ : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
r s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op V))
⊢ ↑((comapₗ f.toSemilinearMap U V hUV).toFun (r * s)) p =
    ↑((comapₗ f.toSemilinearMap U V hUV).toFun r * (comapₗ f.toSemilinearMap U V hUV).toFun s) p

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f✝ : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
x✝ : ↥(unop (op V))
⊢ ↑((comapₗ f.toSemilinearMap U V hUV).toFun 0) x✝ = ↑0 x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
⊢ ∀ {X Y : WalkingCospan} (f : X ⟶ Y),
    (cospan (F.map (D.ι i)) (F.map (D.ι j))).map f ≫
        (Option.casesOn (motive := fun t ↦
            Y = t →
              ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj Y ≅
                (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj Y))
            Y (fun h ↦ ⋯ ▸ D.gluedIso F)
            (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯).hom =
      (Option.casesOn (motive := fun t ↦
            X = t →
              ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj X ≅
                (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj X))
            X (fun h ↦ ⋯ ▸ D.gluedIso F)
            (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯).hom ≫
        (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).map f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
⊢ s ∈ I ↔
    ∀ (x : ↥X) (h : x ∈ U),
      (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
a b : R
hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl
p : ↥(unop (op V))
⊢ ↑((comap f U V hUV) (const a b U hb)) p = ↑(const (f a) (f b) V ⋯) p

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
I J : Ideal ↑Γ(X, U)
⊢ I = J ↔
    ∀ (x : ↥X) (h : x ∈ U),
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I =
        Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
iVU : V ⟶ U
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op V))
⊢ ↑((comap (RingHom.id R) U V ⋯) s) p = ↑((CommRingCat.Hom.hom ((structureSheaf R).obj.map iVU.op)) s) p

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
p : ↑(PrimeSpectrum.Top R)
hpV : p ∈ V.carrier
⊢ p ∈ PrimeSpectrum.comap (RingHom.id R) ⁻¹' U.carrier

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
⊢ comap (RingHom.id R) U V ⋯ = CommRingCat.Hom.hom (eqToHom ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U : Opens ↑(PrimeSpectrum.Top R)
p : ↑(PrimeSpectrum.Top R)
hpU : p ∈ U.carrier
⊢ p ∈ PrimeSpectrum.comap (RingHom.id R) ⁻¹' U.carrier

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
⊢ comap (RingHom.id R) U U ⋯ = RingHom.id ↑((structureSheaf R).obj.obj (op U))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
g : S →+* P
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
W : Opens ↑(PrimeSpectrum.Top P)
hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U
hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op W))
⊢ ↑((comap (g.comp f) U W ⋯) s) p = ↑(((comap g V W hVW).comp (comap f U V hUV)) s) p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
⊢ IsLimit (D.vPullbackCone i j)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
x✝ : ↑(CommRingCat.of R)
x : ↥(unop (op ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U)))
⊢ ↑((CommRingCat.Hom.hom
            (CommRingCat.ofHom (algebraMap R ↑((structureSheaf R).obj.obj (op U))) ≫
              CommRingCat.ofHom
                (comap f U ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U) ⋯)))
          x✝)
      x =
    ↑((CommRingCat.Hom.hom
            (CommRingCat.ofHom f ≫
              CommRingCat.ofHom
                (algebraMap S
                  ↑((structureSheaf S).obj.obj
                      (op ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U))))))
          x✝)
      x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
x : R
⊢ (comap f (basicOpen x) (basicOpen (f x)) ⋯).comp (algebraMap R ↑((structureSheaf R).obj.obj (op (basicOpen x)))) =
    (IsLocalization.map (↑((structureSheaf S).obj.obj (op (basicOpen (f x))))) f ⋯).comp
      (algebraMap R ↑((structureSheaf R).obj.obj (op (basicOpen x))))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v, u₁} C
D : GlueData C
inst✝² : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst✝¹ : PreservesColimit D.diagram.multispan F
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
⊢ ∃ i y, (ConcreteCategory.hom (F.map (D.ι i))) y = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j : D.J
⊢ Mono (D.f' i j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i : D.J
⊢ IsIso (D.f' i i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
X Y Z : C
f : X ⟶ Y
e : Z = X
⊢ eqToHom e ≫ f ≍ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
⊢ HasPullback (D.f' i j) (D.f' i k)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : i = j
⊢ (if h : i = k then D.U i else D.V i k h) = if h : j = k then D.U j else D.V j k h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : i = j
⊢ (if h : i = j then D.U i else D.V i j h) = if h : j = i then D.U j else D.V j i h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : i = j
⊢ D.U i = D.U j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : i = j
⊢ D.f' i k ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f' j k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : i = j
⊢ D.f' i j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f' j i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : i = k
⊢ IsIso (pullback.snd (D.f' j k) (D.f' j i))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : j = k
⊢ IsIso (pullback.snd (D.f' j k) (D.f' j i))

Tactic:
by

Goal state after: