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

Goal state before:
pp: case some.none.term.right
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.right) ≫
      (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.right = t →
            ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some WalkingPair.right) ≅
              (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj (some WalkingPair.right)))
          (some WalkingPair.right) (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.right)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

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

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
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
    dsimp
    change _ = (comapₗ f.toSemilinearMap U V hUV r).1 p * (comapₗ f.toSemilinearMap U V hUV s).1 p
    simp only [comapₗ_eq_localRingHom, PrimeSpectrum.comap_asIdeal]
    exact (Localization.localRingHom ..).map_mul _ _

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))
⊢ ((Localization.localRingHom (PrimeSpectrum.comap g ↑p).asIdeal (↑p).asIdeal g ?hJK).comp
        (Localization.localRingHom (PrimeSpectrum.comap (g.comp f) ↑p).asIdeal (PrimeSpectrum.comap g ↑p).asIdeal f
          ?hIJ))
      (↑s ⟨PrimeSpectrum.comap (g.comp f) ↑p, ⋯⟩) =
    ↑(((comap g V W hVW).comp (comap f U V hUV)) s) p

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case hIJ
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))
⊢ (PrimeSpectrum.comap (g.comp f) ↑p).asIdeal = Ideal.comap f (PrimeSpectrum.comap g ↑p).asIdeal

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case hJK
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))
⊢ (PrimeSpectrum.comap g ↑p).asIdeal = Ideal.comap g (↑p).asIdeal

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
i j k : D.J
hij : ¬i = j
hik : ¬i = k
Y Z : C
f : Z ⟶ Y
⊢ eqToHom ⋯ ≫ f ≍ f

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
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.U i = D.U i

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
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.U j = D.U j

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

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case inl
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i k : D.J
⊢ (if hij : i = i then
        (pullbackSymmetry (D.f' i i) (D.f' i k)).hom ≫
          pullback.map (D.f' i k) (D.f' i i) (D.f' i k) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
      else
        if hik : i = k then
          have this := ⋯;
          pullback.fst (D.f' i i) (D.f' i k) ≫
            eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i k) (D.f' i i))
        else
          if hjk : i = k then
            have this := ⋯;
            pullback.fst (D.f' i i) (D.f' i k) ≫
              eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i k) (D.f' i i))
          else
            pullback.map (D.f' i i) (D.f' i k) (D.f i i hij) (D.f i k hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
              D.t' i i k hij hik hjk ≫
                pullback.map (D.f i k hjk) (D.f i i ⋯) (D.f' i k) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯) ≫
      pullback.snd (D.f' i k) (D.f' i i) =
    pullback.fst (D.f' i i) (D.f' i k) ≫ if h : i = i then eqToHom ⋯ else eqToHom ⋯ ≫ D.t i i h ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
⊢ ∀ {x y z : (i : D.J) × ↑(D.U i)}, D.Rel x y → D.Rel y z → D.Rel x z

Tactic:
by
    rintro ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ ⟨x, e₁, e₂⟩
    rintro ⟨y, e₃, e₄⟩
    let z := (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv ⟨⟨_, _⟩, e₂.trans e₃.symm⟩
    have eq₁ : (D.t j i) ((pullback.fst _ _ : _ /-(D.f j k)-/ ⟶ D.V (j, i)) z) = x := by
      dsimp only [coe_of, z]
      rw [pullbackIsoProdSubtype_inv_fst_apply, D.t_inv_apply]
    have eq₂ : (pullback.snd _ _ : _ ⟶ D.V _) z = y := pullbackIsoProdSubtype_inv_snd_apply _ _ _
    clear_value z
    use (pullback.fst _ _ : _ ⟶ D.V (i, k)) (D.t' _ _ _ z)
    dsimp +instances only at *
    subst eq₁ eq₂ e₁ e₃ e₄
    have h₁ : D.t' j i k ≫ pullback.fst _ _ ≫ D.f i k = pullback.fst _ _ ≫ D.t j i ≫ D.f i j := by
      rw [← 𝖣.t_fac_assoc]; congr 1; exact pullback.condition
    have h₂ : D.t' j i k ≫ pullback.fst _ _ ≫ D.t i k ≫ D.f k i =
        pullback.snd _ _ ≫ D.t j k ≫ D.f k j := by
      rw [← 𝖣.t_fac_assoc]
      apply @Epi.left_cancellation _ _ _ _ (D.t' k j i)
      rw [𝖣.cocycle_assoc, 𝖣.t_fac_assoc, 𝖣.t_inv_assoc]
      exact pullback.condition.symm
    exact ⟨CategoryTheory.congr_fun h₁ z, CategoryTheory.congr_fun h₂ z⟩

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
x✝² x✝¹ : Discrete ι
j : ι
x✝ : { as := j } ⟶ { as := j }
⊢ F.map { down := { down := ⋯ } } ≫ homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j }) ⋯ =
    homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j }) ⋯ ≫
      ((Functor.const (Discrete ι)).obj (coproduct F)).map { down := { down := ⋯ } }

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
⊢ (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y → D.Rel ⟨i, x⟩ ⟨j, y⟩

pp: case mpr
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
⊢ D.Rel ⟨i, x⟩ ⟨j, y⟩ → (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y

Tactic:
· delta GlueData.ι
    simp_rw [← Multicoequalizer.ι_sigmaπ]
    intro h
    rw [←
      show _ = Sigma.mk i x from ConcreteCategory.congr_hom (sigmaIsoSigma.{_, u} D.U).inv_hom_id _]
    rw [←
      show _ = Sigma.mk j y from ConcreteCategory.congr_hom (sigmaIsoSigma.{_, u} D.U).inv_hom_id _]
    change InvImage D.Rel (sigmaIsoSigma.{_, u} D.U).hom _ _
    rw [← (InvImage.equivalence _ _ D.rel_equiv).eqvGen_iff]
    refine Relation.EqvGen.mono ?_ _ _ (D.eqvGen_of_π_eq h :)
    rintro _ _ ⟨x⟩
    obtain ⟨⟨⟨i, j⟩, y⟩, rfl⟩ :=
      (ConcreteCategory.bijective_of_isIso (sigmaIsoSigma.{u, u} _).inv).2 x
    unfold InvImage MultispanIndex.fstSigmaMap MultispanIndex.sndSigmaMap
    rw [sigmaIsoSigma_inv_apply]
    -- `rw [← ConcreteCategory.comp_apply]` succeeds but rewrites the wrong expression
    erw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, colimit.ι_desc_assoc,
      ← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, colimit.ι_desc_assoc]
      -- previous line now `erw` after https://github.com/leanprover-community/mathlib4/pull/13170
    erw [sigmaIsoSigma_hom_ι_apply, sigmaIsoSigma_hom_ι_apply]
    exact ⟨y, ⟨rfl, rfl⟩⟩

Goal state after:
case mpr
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
⊢ D.Rel ⟨i, x⟩ ⟨j, y⟩ → (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
x y : ↑(D.U i)
h : (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) y
w✝ : ↑(D.V (⟨i, x⟩.fst, ⟨i, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f i i)) w✝ = x
e₂ : (ConcreteCategory.hom (D.f i i)) ((ConcreteCategory.hom (D.t i i)) w✝) = y
⊢ (ConcreteCategory.hom (D.f i i)) w✝ = (ConcreteCategory.hom (D.f i i)) ((ConcreteCategory.hom (D.t i i)) w✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Gluing

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

Tactic:
simp

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

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
i : ι
t : Set ι
hit : i ∉ t
ht : t.Finite
IH : X.zeroLocus ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ
⊢ ↑(⨅ i_1, ⨅ (_ : i_1 = i ∨ i_1 ∈ t), I i_1) = ↑(I i) ∩ ↑(⨅ i ∈ t, I i)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal ↑A
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
⊢ f ≫ Spec.map (ΓSpecIso A).hom ≫ Spec.map (ΓSpecIso A).inv = f

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R✝ S✝ : CommRingCat
f✝ : R✝ ⟶ S✝
p✝ : PrimeSpectrum ↑S✝
x : PrimeSpectrum ↑R✝
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).hom ≫
      (Arrow.mk
          (CommRingCat.ofHom
            (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
              (CommRingCat.Hom.hom f) ⋯))).hom =
    (Arrow.mk
          ((Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).hom ≫
            CommRingCat.ofHom
                (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
                  (CommRingCat.Hom.hom f) ⋯) ≫
              (Spec.stalkIso S p).inv)).hom ≫
      (Spec.stalkIso S p).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Gluing

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

Tactic:
intro j

Goal state after:
D : GlueData
i : D.J
U : Opens ↑(D.U i)
j : D.J
⊢ IsOpen (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' ↑U)
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:
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:
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:
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:
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:
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:
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:
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:
simp

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

Goal state before:
pp: case e_a.h₀
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)
⊢ (Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f)) ≫ pullback.fst (pullback.fst f f ≫ f) (𝟙 X)) ≫
      pullback.fst f f =
    Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯) ≫ pullback.fst f f

Tactic:
simp

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

Goal state before:
pp: case h₁
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)
⊢ (Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f)) ≫ pullback.fst (pullback.fst f f ≫ f) (𝟙 X)) ≫
      pullback.snd f f =
    Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯) ≫ pullback.snd f f

Tactic:
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:
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
⊢ (limit.isoLimitCone { cone := BinaryFan.mk 0 (𝟙 X), isLimit := binaryFanZeroLeftIsLimit X }).inv ≫ prod.snd = 𝟙 X

Tactic:
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:
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
⊢ (limit.isoLimitCone { cone := BinaryFan.mk (𝟙 X) 0, isLimit := binaryFanZeroRightIsLimit X }).inv ≫ prod.fst = 𝟙 X

Tactic:
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:
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
⊢ coprod.inr ≫
      (colimit.isoColimitCocone { cocone := BinaryCofan.mk 0 (𝟙 X), isColimit := binaryCofanZeroLeftIsColimit X }).hom =
    𝟙 X

Tactic:
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:
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
⊢ coprod.inl ≫
      (colimit.isoColimitCocone
          { cocone := BinaryCofan.mk (𝟙 X) 0, isColimit := binaryCofanZeroRightIsColimit X }).hom =
    𝟙 X

Tactic:
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 Y : C
inst✝ : HasBinaryProduct X Y
⊢ (limit.isoLimitCone
          { cone := PullbackCone.mk prod.fst prod.snd ⋯,
            isLimit :=
              isPullbackOfIsTerminalIsProduct 0 0 prod.fst prod.snd HasZeroObject.zeroIsTerminal
                (prodIsProd X Y) }).inv ≫
      pullback.fst 0 0 =
    prod.fst

Tactic:
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 Y : C
inst✝ : HasBinaryProduct X Y
⊢ (limit.isoLimitCone
          { cone := PullbackCone.mk prod.fst prod.snd ⋯,
            isLimit :=
              isPullbackOfIsTerminalIsProduct 0 0 prod.fst prod.snd HasZeroObject.zeroIsTerminal
                (prodIsProd X Y) }).inv ≫
      pullback.snd 0 0 =
    prod.snd

Tactic:
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 Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inl 0 0 ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk coprod.inl coprod.inr ⋯,
            isColimit :=
              isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                (coprodIsCoprod X Y) }).hom =
    coprod.inl

Tactic:
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 Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inr 0 0 ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk coprod.inl coprod.inr ⋯,
            isColimit :=
              isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                (coprodIsCoprod X Y) }).hom =
    coprod.inr

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D✝ : GlueData
D : GlueData
⊢ { I₀ := D.J, X := D.U, f := D.ι }.presieve₀ ∈ (precoverage IsOpenImmersion).coverings D.glued

Tactic:
rw [presieve₀_mem_precoverage_iff]
    exact ⟨D.ι_jointly_surjective, inferInstance⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case refine_2
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ 𝒰.f z ≫ 𝟙 X = 𝟙 (𝒰.X z) ≫ 𝒰.f z

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.fst (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.fst (𝒰.f y) (𝒰.f z) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)

Tactic:
simp

Goal state after: