mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B₀ : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} B₀
inst✝ : Bicategory C
obj : B₀ → C
map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B₀) → map (𝟙 b) ≅ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ≅ map f ≫ map g
map₂_associator :
  autoParam
    (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
      (mapComp (f ≫ g) h).hom ≫
          (mapComp f g).hom ▷ map h ≫
            (α_ (map f) (map g) (map h)).hom ≫ map f ◁ (mapComp g h).inv ≫ (mapComp f (g ≫ h)).inv =
        eqToHom ⋯)
    mkPseudofunctor._auto_1
b₀ b₁ : B₀
f : b₀ ⟶ b₁
⊢ map (𝟙 b₀ ≫ f) = map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B₀ : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} B₀
inst✝ : Bicategory C
obj : B₀ → C
map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B₀) → map (𝟙 b) ≅ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ≅ map f ≫ map g
map₂_associator :
  autoParam
    (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
      (mapComp (f ≫ g) h).hom ≫
          (mapComp f g).hom ▷ map h ≫
            (α_ (map f) (map g) (map h)).hom ≫ map f ◁ (mapComp g h).inv ≫ (mapComp f (g ≫ h)).inv =
        eqToHom ⋯)
    mkPseudofunctor._auto_1
map₂_left_unitor :
  autoParam
    (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), (mapComp (𝟙 b₀) f).hom ≫ (mapId b₀).hom ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯)
    mkPseudofunctor._auto_3
b₀ b₁ : B₀
f : b₀ ⟶ b₁
⊢ map (f ≫ 𝟙 b₁) = map f

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r : ↑(R.obj.obj X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Y))) 0 = (ConcreteCategory.hom (A.obj.map f.op)) 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ 𝟙 Bicone.left ≫ BiconeHom.left_id = BiconeHom.left_id

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ 𝟙 Bicone.right ≫ BiconeHom.right_id = BiconeHom.right_id

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ 𝟙 Bicone.left ≫ BiconeHom.left j✝ = BiconeHom.left j✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ 𝟙 Bicone.right ≫ BiconeHom.right j✝ = BiconeHom.right j✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ 𝟙 (Bicone.diagram j✝) ≫ BiconeHom.diagram f✝ = BiconeHom.diagram f✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ BiconeHom.left_id ≫ 𝟙 Bicone.left = BiconeHom.left_id

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ BiconeHom.right_id ≫ 𝟙 Bicone.right = BiconeHom.right_id

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ BiconeHom.left j✝ ≫ 𝟙 (Bicone.diagram j✝) = BiconeHom.left j✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ BiconeHom.right j✝ ≫ 𝟙 (Bicone.diagram j✝) = BiconeHom.right j✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ BiconeHom.diagram f✝ ≫ 𝟙 (Bicone.diagram k✝) = BiconeHom.diagram f✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id.left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ (BiconeHom.left_id ≫ BiconeHom.left_id) ≫ BiconeHom.left_id =
    BiconeHom.left_id ≫ BiconeHom.left_id ≫ BiconeHom.left_id

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id.left_id.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ (BiconeHom.left_id ≫ BiconeHom.left_id) ≫ BiconeHom.left j✝ =
    BiconeHom.left_id ≫ BiconeHom.left_id ≫ BiconeHom.left j✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id.left.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ (BiconeHom.left_id ≫ BiconeHom.left j✝) ≫ BiconeHom.diagram f✝ =
    BiconeHom.left_id ≫ BiconeHom.left j✝ ≫ BiconeHom.diagram f✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right_id.right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ (BiconeHom.right_id ≫ BiconeHom.right_id) ≫ BiconeHom.right_id =
    BiconeHom.right_id ≫ BiconeHom.right_id ≫ BiconeHom.right_id

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right_id.right_id.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ (BiconeHom.right_id ≫ BiconeHom.right_id) ≫ BiconeHom.right j✝ =
    BiconeHom.right_id ≫ BiconeHom.right_id ≫ BiconeHom.right j✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right_id.right.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ (BiconeHom.right_id ≫ BiconeHom.right j✝) ≫ BiconeHom.diagram f✝ =
    BiconeHom.right_id ≫ BiconeHom.right j✝ ≫ BiconeHom.diagram f✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left.diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝¹ : J
f✝¹ : j✝ ⟶ k✝¹
k✝ : J
f✝ : k✝¹ ⟶ k✝
⊢ (BiconeHom.left j✝ ≫ BiconeHom.diagram f✝¹) ≫ BiconeHom.diagram f✝ =
    BiconeHom.left j✝ ≫ BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right.diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝¹ : J
f✝¹ : j✝ ⟶ k✝¹
k✝ : J
f✝ : k✝¹ ⟶ k✝
⊢ (BiconeHom.right j✝ ≫ BiconeHom.diagram f✝¹) ≫ BiconeHom.diagram f✝ =
    BiconeHom.right j✝ ≫ BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case diagram.diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝² : J
f✝² : j✝ ⟶ k✝²
k✝¹ : J
f✝¹ : k✝² ⟶ k✝¹
k✝ : J
f✝ : k✝¹ ⟶ k✝
⊢ (BiconeHom.diagram f✝² ≫ BiconeHom.diagram f✝¹) ≫ BiconeHom.diagram f✝ =
    BiconeHom.diagram f✝² ≫ BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
R : Sheaf J✝ RingCat
inst✝¹ : HasWeakSheafify J✝ AddCommGrpCat
inst✝ : J✝.WEqualsLocallyBijective AddCommGrpCat
I J : Type u
f : I → J
⊢ (free J).freeHomEquiv.symm ((free J).freeHomEquiv (freeMap f)) = (free J).freeHomEquiv.symm (freeSection ∘ f)

Tactic:
simp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
R : Sheaf J✝ RingCat
inst✝¹ : HasWeakSheafify J✝ AddCommGrpCat
inst✝ : J✝.WEqualsLocallyBijective AddCommGrpCat
I J : Type u
f : I → J
⊢ freeMap f = (free J).freeHomEquiv.symm (freeSection ∘ f)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
R : Sheaf J✝ RingCat
inst✝¹ : HasWeakSheafify J✝ AddCommGrpCat
inst✝ : J✝.WEqualsLocallyBijective AddCommGrpCat
I J : Type u
⊢ coprod.inl ≫ (freeSumIso I J).hom = freeMap Sum.inl

Tactic:
rw [← dsimp% freeFunctor_map (↾(Sum.inl : I → I ⊕ J))]
  exact IsColimit.comp_coconePointUniqueUpToIso_hom
    (coprodIsCoprod (free (R := R) I) (free J)) _ (.mk .left)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesFiniteCoproducts F
n : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin n))ᵒᵖ F

Tactic:
exact preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝))ᵒᵖ F

Tactic:
exact preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝))ᵒᵖ F

Tactic:
exact preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝))ᵒᵖ F

Tactic:
exact preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r₀ : ↑(R₀.obj X)
m₀ : ↑(M₀.obj X)
⊢ (ConcreteCategory.hom (α.app X)) r₀ = (ConcreteCategory.hom (R.obj.map (𝟙 X))) ((ConcreteCategory.hom (α.app X)) r₀)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r₀ : ↑(R₀.obj X)
m₀ : ↑(M₀.obj X)
⊢ (ConcreteCategory.hom (φ.app X)) m₀ = (ConcreteCategory.hom (A.obj.map (𝟙 X))) ((ConcreteCategory.hom (φ.app X)) m₀)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
⊢ ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j

Tactic:
intro j

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
j : J
⊢ Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
h : J₁.close S = ⊤
Y : C
f : Y ⟶ X
⊢ ⊤.arrows f → Sieve.pullback f S ∈ J₁ Y

Tactic:
hf

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
h : J₁.close S = ⊤
Y : C
f : Y ⟶ X
hf : ⊤.arrows f
⊢ Sieve.pullback f S ∈ J₁ Y
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := ⋯
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := ⋯
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₀ : Cone (biconeMk J c₁ c₂) := ⋯
g₁ : c₀.pt ⟶ c₁.pt := ⋯
g₂ : c₀.pt ⟶ c₂.pt := ⋯
this✝ : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
⊢ ∀ (j : J), Hom.right g₁ ≫ c.π.app j = (c.extend (Hom.right g₁)).π.app j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ BiconeHom.left_id ∈ {BiconeHom.left_id}

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ BiconeHom.left val✝ ∈ {BiconeHom.left val✝}

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := ⋯
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := ⋯
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₀ : Cone (biconeMk J c₁ c₂) := ⋯
g₁ : c₀.pt ⟶ c₁.pt := ⋯
g₂ : c₀.pt ⟶ c₂.pt := ⋯
this✝ : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
⊢ ∀ (j : J), Hom.right g₂ ≫ c.π.app j = (c.extend (Hom.right g₂)).π.app j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right_id
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ BiconeHom.right_id ∈ {BiconeHom.right_id}

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ BiconeHom.right val✝ ∈ {BiconeHom.right val✝}

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
Y : C
f : Y ⟶ X
⊢ ∀ (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)

Tactic:
hf

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f M = ↑(x f hf)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
i : E.I₀
⊢ 𝟙 (E.X i) ≫ E.f i = E.f i

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S T : C
E✝ : PreZeroHypercover S
F : PreZeroHypercover S
X : C
E : PreZeroHypercover X
Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i ≫ f) g
i : E.I₀
⊢ (E.f i ≫ f) ≫ 𝟙 Z = E.f i ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S T : C
E✝ : PreZeroHypercover S
F : PreZeroHypercover S
X : C
E : PreZeroHypercover X
Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i ≫ f) g
i : E.I₀
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S T : C
E✝ : PreZeroHypercover S
F : PreZeroHypercover S
Y : C
E : PreZeroHypercover Y
X Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : ∀ (i : E.I₀), HasPullback f (E.f i ≫ g)
i : E.I₀
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S T : C
E✝ : PreZeroHypercover S
F : PreZeroHypercover S
Y : C
E : PreZeroHypercover Y
X Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : ∀ (i : E.I₀), HasPullback f (E.f i ≫ g)
i : E.I₀
⊢ (E.f i ≫ g) ≫ 𝟙 Z = E.f i ≫ g

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
f : Y ⟶ X
⊢ ∀ (h : S.arrows f), (ConcreteCategory.hom ((Functor.closedSieves J₁).toFunctor.map f.op)) ⟨J₁.close M, ⋯⟩ = x f h

Tactic:
hf

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (ConcreteCategory.hom ((Functor.closedSieves J₁).toFunctor.map f.op)) ⟨J₁.close M, ⋯⟩ = x f hf
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
f g : E.Hom F
h : f = g
⊢ ∃ (hs : f.s₀ = f.s₀), ∀ (i : E.I₀), f.h₀ i = f.h₀ i ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
i : F.I₀
⊢ F.X i = F.X (s₀ (s₀.symm i))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
i : E.I₀
⊢ i = s₀.symm (s₀ i)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
i : E.I₀
⊢ E.f i ≫ eqToHom ⋯ = E.f i

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
x✝ : E.I₀
⊢ ({ s₀ := ⇑s₀, h₀ := fun i ↦ (h₀ i).hom, w₀ := ⋯ } ≫
          { s₀ := ⇑s₀.symm, h₀ := fun i ↦ eqToHom ⋯ ≫ (h₀ (s₀.symm i)).inv, w₀ := ⋯ }).s₀
      x✝ =
    (𝟙 E).s₀ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
i : E.I₀
⊢ ({ s₀ := ⇑s₀, h₀ := fun i ↦ (h₀ i).hom, w₀ := ⋯ } ≫
          { s₀ := ⇑s₀.symm, h₀ := fun i ↦ eqToHom ⋯ ≫ (h₀ (s₀.symm i)).inv, w₀ := ⋯ }).h₀
      i =
    (𝟙 E).h₀ i ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
x✝ : F.I₀
⊢ ({ s₀ := ⇑s₀.symm, h₀ := fun i ↦ eqToHom ⋯ ≫ (h₀ (s₀.symm i)).inv, w₀ := ⋯ } ≫
          { s₀ := ⇑s₀, h₀ := fun i ↦ (h₀ i).hom, w₀ := ⋯ }).s₀
      x✝ =
    (𝟙 F).s₀ x✝

Tactic:
simp

Goal state after: