mathlib-initiative/mathlib-tactics huggingface dataset:
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.ι lhs rhs ≫ pullback.fst s v) ≫ f = (equalizer.ι lhs rhs ≫ pullback.fst s v) ≫ g

Tactic:
simp [hl, hr, equalizer.condition_assoc lhs rhs]

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:
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 : Scheme
U : X.Opens
⊢ (fun U_1 ↦ ↑U_1 ≤ Scheme.Hom.opensRange U.ι) = fun V ↦ ↑V ≤ U

Tactic:
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:
simp

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

Goal state before:
pp: case h₀
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 := ⋯
rhs : pullback s v ⟶ pullback t v := ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ ((pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
            (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯ ≫
          equalizer.lift
            (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯) ⋯) ≫
        equalizer.ι lhs rhs) ≫
      pullback.fst s v =
    (𝟙 (equalizer lhs rhs) ≫ equalizer.ι lhs rhs) ≫ pullback.fst s v

Tactic:
simp

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

Goal state before:
pp: case h₁
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 := ⋯
rhs : pullback s v ⟶ pullback t v := ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ ((pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
            (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯ ≫
          equalizer.lift
            (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯) ⋯) ≫
        equalizer.ι lhs rhs) ≫
      pullback.snd s v =
    (𝟙 (equalizer lhs rhs) ≫ equalizer.ι lhs rhs) ≫ pullback.snd s v

Tactic:
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✝ : M
⊢ (ConcreteCategory.hom (ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M))) x✝ =
    (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) x✝

Tactic:
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:
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:
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:
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:
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:
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:
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:
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:
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:
simp

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

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

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

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

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ (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))

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

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: 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))
⊢ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ Scheme.Hom.app f (Y.basicOpen r)) =
    (CommRingCat.Hom.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op))).comp
      (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
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:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : Scheme
B : CommRingCat
φ : B ⟶ Γ(X, ⊤)
⊢ (Scheme.ΓSpecIso B).inv ≫ Scheme.Hom.app (Spec.map φ.op.unop) ⊤ ≫ Scheme.Hom.app (ΓSpec.adjunction.unit.app X) ⊤ = φ

Tactic:
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:
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:
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:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case h
R S : CommRingCat
f : Spec S ⟶ Spec R
⊢ map (preimage f) = f

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

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

Tactic:
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:
simp

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: D : GlueData (Type v)
x' : D.sigmaOpens
i : D.J
y : D.U i
⊢ (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) y =
    (ConcreteCategory.hom D.π)
      ((ConcreteCategory.hom (colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv) ⟨i, y⟩)

Tactic:
simp

Goal state after:
D : GlueData (Type v)
x' : D.sigmaOpens
i : D.J
y : D.U i
⊢ (ConcreteCategory.hom (Sigma.ι D.U i ≫ Multicoequalizer.sigmaπ D.diagram)) y =
    (ConcreteCategory.hom D.π)
      ((ConcreteCategory.hom (colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv) ⟨i, y⟩)
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 : D.J
⊢ F.map (D.t i i) = 𝟙 (F.obj (D.V (i, i)))

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e_6
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
⊢ ↑((Scheme.Hom.resLE f U V hVU) ⟨x, hx⟩) = ↑⟨f x, ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case left.id
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
fst✝ snd✝ : D.J
⊢ (D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.id (WalkingMultispan.left (fst✝, snd✝))) ≫
      (match WalkingMultispan.left (fst✝, snd✝) 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 WalkingMultispan.left (fst✝, snd✝) 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 (WalkingMultispan.Hom.id (WalkingMultispan.left (fst✝, snd✝)))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case left.fst
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
fst✝ snd✝ : D.J
⊢ (D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.fst (fst✝, snd✝)) ≫
      (match WalkingMultispan.right ((MultispanShape.prod D.J).fst (fst✝, snd✝)) 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 WalkingMultispan.left (fst✝, snd✝) 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 (WalkingMultispan.Hom.fst (fst✝, snd✝))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case left.snd
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
fst✝ snd✝ : D.J
⊢ (D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.snd (fst✝, snd✝)) ≫
      (match WalkingMultispan.right ((MultispanShape.prod D.J).snd (fst✝, snd✝)) 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 WalkingMultispan.left (fst✝, snd✝) 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 (WalkingMultispan.Hom.snd (fst✝, snd✝))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case right.id
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
a✝ : (MultispanShape.prod D.J).R
⊢ (D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝)) ≫
      (match WalkingMultispan.right a✝ 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 WalkingMultispan.right a✝ 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 (WalkingMultispan.Hom.id (WalkingMultispan.right a✝))

Tactic:
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
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
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
W : Opens ↑(PrimeSpectrum.Top R)
m : ↑⟨PrimeSpectrum.comap σ p, ⋯⟩ ∈ W
iWU : W ⟶ U
a : M
b : R
h_frac : ∀ (x : ↥W), ∃ (hs : b ∉ (↑x).asIdeal), (fun x ↦ s (iWU x)) x = LocalizedModule.mk a ⟨b, hs⟩
q : ↑(PrimeSpectrum.Top S)
hqW : q ∈ ↑{ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ }
hqV : q ∈ ↑V
hs : b ∉ (↑⟨PrimeSpectrum.comap σ q, hqW⟩).asIdeal
H : s ⟨PrimeSpectrum.comap σ q, ⋯⟩ = LocalizedModule.mk a ⟨b, hs⟩
⊢ (Localizations.comapFun f q) (LocalizedModule.mk a ⟨b, hs⟩) = LocalizedModule.mk (f a) ⟨σ b, hs⟩

Tactic:
simp

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
m : R
s : ↥(PrimeSpectrum.comap f ↑p).asIdeal.primeCompl
⊢ (Localizations.comapFun f.toSemilinearMap ↑p) (LocalizedModule.mk m s) = LocalizedModule.mk (f m) ⟨f ↑s, ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case none.none.id
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)
⊢ (cospan (F.map (D.ι i)) (F.map (D.ι j))).map (WidePullbackShape.Hom.id none) ≫
      (Option.casesOn (motive := fun t ↦
          none = t →
            ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj none ≅
              (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj none))
          none (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 ↦
          none = t →
            ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj none ≅
              (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj none))
          none (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 (WidePullbackShape.Hom.id none)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case some.none.term.left
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)
⊢ (cospan (F.map (D.ι i)) (F.map (D.ι j))).map (WidePullbackShape.Hom.term WalkingPair.left) ≫
      (Option.casesOn (motive := fun t ↦
          none = t →
            ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj none ≅
              (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj none))
          none (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 ↦
          some WalkingPair.left = t →
            ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some WalkingPair.left) ≅
              (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj (some WalkingPair.left)))
          (some WalkingPair.left) (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 (WidePullbackShape.Hom.term WalkingPair.left)

Tactic:
simp

Goal state after: