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

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
n : ℕ
c : ι →₀ R
hc : ∑ i, c i • b i = f ^ (n + 1)
⊢ (toBasicOpenₗ R M f) (LocalizedModule.mk (∑ i, c i • a i) ⟨f ^ (n + 1), ⋯⟩) = s

Tactic:
refine (structureSheafInType R M).eq_of_locally_eq' (fun i ↦ basicOpen (b i)) _
    (fun i ↦ (ibU _).hom) iU _ _ fun i ↦ (Subtype.ext (funext fun x ↦ ?_)).trans (H _).symm

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
n : ℕ
c : ι →₀ R
hc : ∑ i, c i • b i = f ^ (n + 1)
i : ι
x : ↥(unop (op (basicOpen (b i))))
⊢ ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op))
          ((toBasicOpenₗ R M f) (LocalizedModule.mk (∑ i, c i • a i) ⟨f ^ (n + 1), ⋯⟩)))
      x =
    ↑(const (a i) (b i) (basicOpen (b i)) ⋯) x
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s = ⋂ f ∈ s, (↑(X.toRingedSpace.basicOpen f))ᶜ

Tactic:
erw [Set.iInter₂_congr this]

Goal state after:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⋂ i ∈ s, ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝ : Category.{v_1, u_1} J
F : Discrete J ⥤ Type u_2
i : J
x : F.obj { as := i }
⊢ (ConcreteCategory.hom (F.map (𝟙 { as := i }))) x = x ∧ (ConcreteCategory.hom (F.map (𝟙 { as := i }))) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : WidePushoutShape J
x : F.obj i
⊢ (ConcreteCategory.hom (F.map (𝟙 i))) x = x ∧ (ConcreteCategory.hom (F.map (𝟙 i))) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
j : J
x : F.obj none
⊢ (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init j))) x =
      (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init j))) x ∧
    (ConcreteCategory.hom (F.map (𝟙 none))) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
x : F.obj none
⊢ (ConcreteCategory.hom (F.map (𝟙 none))) x = x ∧
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) x =
      (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) x

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
x : F.obj none
⊢ (ConcreteCategory.hom (F.map (𝟙 none))) x = x ∧ (ConcreteCategory.hom (F.map (𝟙 none))) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
⊢ equalizer.lift s.fst ⋯ ≫ equalizer.ι f g = s.fst

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ coequalizer.π f g ≫ coequalizer.desc s.inl ⋯ = s.inl

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ v ≫ 𝟙 S = 𝟙 T ≫ v

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ v ≫ 𝟙 S = 𝟙 T ≫ v

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
⊢ pullback.fst s v ≫ g = rhs ≫ pullback.fst t v

Tactic:
by simp [rhs]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X✝ Y : Scheme
U✝ : X✝.Opens
hU : IsAffineOpen U✝
f : ↑Γ(X✝, U✝)
X : Scheme
U : X.Opens
⊢ (fun U_1 ↦ ↑U_1 ≤ Scheme.Hom.opensRange U.ι) = fun V ↦ ↑V ≤ U

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯ ≫ equalizer.ι f g =
    pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯ ≫ pullback.fst s v

Tactic:
by simp

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
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ 1 • ↑s • f = ↑s • f

Tactic:
by simp

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
x : ↑(PrimeSpectrum.Top R)
m : M
⊢ x ∈ ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K✝ : Precoverage C
P : MorphismProperty C
K L : Precoverage C
⊢ ∀ {X Y : C} {f : Y ⟶ X} {R : Presieve X} {U : C} {g : U ⟶ X},
    R ∈ K.coverings X → R g → ⊤ f → ∀ [inst : HasPullback f g], ⊤ (pullback.snd f g)

Tactic:
by simp

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
x : ↑(PrimeSpectrum.Top R)
⊢ ∀ (x_1 y : M),
    (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) ((toOpenₗ R M ⊤) (x_1 + y)) =
      (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) ((toOpenₗ R M ⊤) x_1) +
        (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) ((toOpenₗ R M ⊤) y)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K✝ : Precoverage C
P : MorphismProperty C
K L : Precoverage C
⊢ ∀ {X Y : C} {f : Y ⟶ X} {R : Presieve X},
    R ∈ K.coverings X → (∀ {U : C} {g : U ⟶ X} [inst : HasPullback f g], R g → ⊤ (pullback.snd f g)) → ⊤ f

Tactic:
by simp

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
x : ↑(PrimeSpectrum.Top R)
m : M
α : stalk (moduleStructurePresheaf R M).presheaf x ≅
  (forget₂ (ModuleCat R) Ab).obj ((structurePresheafInModuleCat R M).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ (ModuleCat R) Ab).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }
⊢ x ∈ ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K✝ : Precoverage C
P : MorphismProperty C
K L : Precoverage C
⊢ ∀ {X Y : C} {f : X ⟶ Y} {R : Presieve X}, R ∈ K.coverings X → ∀ {U : C} (g : U ⟶ X), R g → ⊤ f → ⊤ (g ≫ f)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K✝ : Precoverage C
P : MorphismProperty C
K L : Precoverage C
⊢ ∀ {X Y : C} {f : X ⟶ Y} {R : Presieve X}, R ∈ K.coverings X → (∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → ⊤ (g ≫ f)) → ⊤ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasEqualizers C
inst✝² : HasPullbacks C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage C
𝒰 : J.ZeroHypercover S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : (MorphismProperty.isomorphisms C).IsLocalAtTarget J
i : 𝒰.I₀
⊢ 𝒰.f i ≫ 𝟙 S = 𝟙 (𝒰.X i) ≫ 𝒰.f i

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X✝ Y✝ : Scheme
U✝ : X✝.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X✝, U✝)
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ f ⁻¹ᵁ Y.basicOpen r = X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCat
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ

Tactic:
have := ΓSpec.adjunction.right_triangle_components (op R)
  dsimp at this
  rwa [← IsIso.eq_comp_inv, Category.id_comp, ← Spec.map_inv, IsIso.Iso.inv_inv, eq_comm] at this

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
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)) }
⊢ x ∈ ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X✝ Y✝ : Scheme
U✝ : X✝.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X✝, U✝)
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r) = f ⁻¹ᵁ Y.basicOpen r

Tactic:
by simp

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
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 ⋯)
⊢ x ∈ ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ (Scheme.ΓSpecIso Γ(X, U)).hom =
    Scheme.Hom.appTop (Spec.map U.topIso.inv) ≫ Scheme.Hom.appTop (↑U).toSpecΓ ≫ U.topIso.hom

Tactic:
by simp

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
inst✝ : HasMulticoequalizer D.diagram
i j : D.J
⊢ D.f i j ≫ D.ι i = (D.t i j ≫ D.f j i) ≫ D.ι j

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCat
⊢ map (preimage (𝟙 (Spec R))) = map (𝟙 R)

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R S T : CommRingCat
f : Spec R ⟶ Spec S
g : Spec S ⟶ Spec T
⊢ map (preimage (f ≫ g)) = map (preimage g ≫ preimage f)

Tactic:
by simp

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
this : j ≠ i
⊢ D.U i = D.U i

Tactic:
by simp

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
this : j ≠ i
⊢ D.U j = D.U j

Tactic:
by simp

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
⊢ (if h : i = i then eqToHom ⋯ else eqToHom ⋯ ≫ D.t i i h ≫ eqToHom ⋯) =
    𝟙 (if h : (i, i).1 = (i, i).2 then D.U (i, i).1 else D.V (i, i).1 (i, i).2 h)

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Gluing

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

Tactic:
← Set.image_univ,

Goal state after:
D : GlueData
i j : D.J
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' Set.univ =
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) '' Set.range ⇑(ConcreteCategory.hom (D.f j i))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
⊢ U.carrier ↓∩ X.zeroLocus ↑(I ⊓ J) = U.carrier ↓∩ (X.zeroLocus ↑I ∪ X.zeroLocus ↑J)

Tactic:
simp only [← U.toSpecΓ_preimage_zeroLocus, PrimeSpectrum.zeroLocus_inf I J,
    Set.preimage_union]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
⊢ X.zeroLocus ↑(⨅ i ∈ ∅, I i) = (⋃ i ∈ ∅, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : J
⊢ (Opens.map (U i).inclusion').obj (U i) = ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X : C
R S T : Over X
f : S ⟶ T
⊢ R.hom ≫ 𝟙 X = 𝟙 R.left ≫ R.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X : C
R S T : Over X
f : S ⟶ T
⊢ S.hom ≫ 𝟙 X = Hom.left f ≫ T.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X : C
R S T U : Over X
f : R ⟶ S
g : T ⟶ U
⊢ R.hom ≫ 𝟙 X = Hom.left f ≫ S.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X : C
R S T U : Over X
f : R ⟶ S
g : T ⟶ U
⊢ T.hom ≫ 𝟙 X = Hom.left g ≫ U.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X A B R S Y Z : C
f✝ : R ⟶ X
g : S ⟶ X
f : R ⟶ S
⊢ (asIso (pullback.snd (𝟙 S) f)).hom ≫ (𝟙_ (Over R)).hom = ((pullback f).obj (𝟙_ (Over S))).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasPullbacks C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst✝ : MonObj (mk f)
⊢ pullback.snd f (𝟙 X) ≫ 𝟙 X = (mk (pullback.snd f (𝟙 X))).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
⊢ D.f i j ≫ D.ι i = (D.t i j ≫ D.f j i) ≫ D.ι j

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryFan 0 X), s.snd ≫ 𝟙 X = s.snd

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryFan X 0), s.fst ≫ 𝟙 X = s.fst

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryCofan 0 X), 𝟙 X ≫ s.inr = s.inr

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryCofan X 0), 𝟙 X ≫ s.inl = s.inl

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x : 𝒰.I₀
⊢ (pullbackSymmetry (𝒰.f x) (𝒰.f x)).hom =
    𝟙
      (match (x, x) with
      | (x, y) => pullback (𝒰.f x) (𝒰.f y))

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ (fst f (𝒰.f i) ≫ f) ≫ 𝟙 Y = snd f (𝒰.f i) ≫ 𝒰.f i

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ 𝒰.f j ≫ 𝟙 Y = 𝟙 (𝒰.X j) ≫ 𝒰.f j

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
e :
  ∀ {Z : C}
    (h :
      (D.V (k, i)).presheaf.obj
          (op ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).obj ((Opens.map (D.t' k i j).base).1 U))) ⟶
        Z),
    invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
        (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
          (D.V (k, i)).presheaf.map (eqToHom ⋯) ≫ h =
      (D.t' k i j).c.app (op U) ≫ invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U) ≫ h
⊢ invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
      (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) =
    invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
      (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
        (D.V (k, i)).presheaf.map (eqToHom ⋯) ≫ (D.V (k, i)).presheaf.map (eqToHom ⋯)

Tactic:
simp [eqToHom_map]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (snd f (𝒰.f i))
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫
      f ≫ Cover.glueMorphisms 𝒰 (fun i ↦ inv (snd f (𝒰.f i)) ≫ fst f (𝒰.f i)) ⋯ =
    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ 𝟙 X

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (snd f (𝒰.f i))
i : 𝒰.I₀
⊢ 𝒰.f i ≫ Cover.glueMorphisms 𝒰 (fun i ↦ inv (snd f (𝒰.f i)) ≫ fst f (𝒰.f i)) ⋯ ≫ f = 𝒰.f i ≫ 𝟙 Y

Tactic:
by simp

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

Tactic:
by simp

Goal state after: