mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor

Goal state before:
pp: case refine_1
⊢ ∀ {b₀ b₁ b₂ b₃ : CommRingCat} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    (Cat.Hom.isoMk (extendScalarsComp (Hom.hom (f ≫ g)) (Hom.hom h))).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom g))).hom
            (extendScalars (Hom.hom h)).toCatHom ≫
          (Bicategory.associator (extendScalars (Hom.hom f)).toCatHom (extendScalars (Hom.hom g)).toCatHom
                (extendScalars (Hom.hom h)).toCatHom).hom ≫
            Bicategory.whiskerLeft (extendScalars (Hom.hom f)).toCatHom
                (Cat.Hom.isoMk (extendScalarsComp (Hom.hom g) (Hom.hom h))).inv ≫
              (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom (g ≫ h)))).inv =
      eqToHom ⋯

pp: case refine_2
⊢ ∀ {b₀ b₁ : CommRingCat} (f : b₀ ⟶ b₁),
    (Cat.Hom.isoMk (extendScalarsComp (Hom.hom (𝟙 b₀)) (Hom.hom f))).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsId ↑b₀)).hom (extendScalars (Hom.hom f)).toCatHom ≫
          (Bicategory.leftUnitor (extendScalars (Hom.hom f)).toCatHom).hom =
      eqToHom ⋯

pp: case refine_3
⊢ ∀ {b₀ b₁ : CommRingCat} (f : b₀ ⟶ b₁),
    (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom (𝟙 b₁)))).hom ≫
        Bicategory.whiskerLeft (extendScalars (Hom.hom f)).toCatHom (Cat.Hom.isoMk (extendScalarsId ↑b₁)).hom ≫
          (Bicategory.rightUnitor (extendScalars (Hom.hom f)).toCatHom).hom =
      eqToHom ⋯

Tactic:
·

Goal state after:
case refine_1
⊢ ∀ {b₀ b₁ b₂ b₃ : CommRingCat} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    (Cat.Hom.isoMk (extendScalarsComp (Hom.hom (f ≫ g)) (Hom.hom h))).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom g))).hom
            (extendScalars (Hom.hom h)).toCatHom ≫
          (Bicategory.associator (extendScalars (Hom.hom f)).toCatHom (extendScalars (Hom.hom g)).toCatHom
                (extendScalars (Hom.hom h)).toCatHom).hom ≫
            Bicategory.whiskerLeft (extendScalars (Hom.hom f)).toCatHom
                (Cat.Hom.isoMk (extendScalarsComp (Hom.hom g) (Hom.hom h))).inv ≫
              (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom (g ≫ h)))).inv =
      eqToHom ⋯
Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor

Goal state before:
pp: case refine_2
⊢ ∀ {b₀ b₁ : CommRingCat} (f : b₀ ⟶ b₁),
    (Cat.Hom.isoMk (extendScalarsComp (Hom.hom (𝟙 b₀)) (Hom.hom f))).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsId ↑b₀)).hom (extendScalars (Hom.hom f)).toCatHom ≫
          (Bicategory.leftUnitor (extendScalars (Hom.hom f)).toCatHom).hom =
      eqToHom ⋯

pp: case refine_3
⊢ ∀ {b₀ b₁ : CommRingCat} (f : b₀ ⟶ b₁),
    (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom (𝟙 b₁)))).hom ≫
        Bicategory.whiskerLeft (extendScalars (Hom.hom f)).toCatHom (Cat.Hom.isoMk (extendScalarsId ↑b₁)).hom ≫
          (Bicategory.rightUnitor (extendScalars (Hom.hom f)).toCatHom).hom =
      eqToHom ⋯

Tactic:
·

Goal state after:
case refine_2
⊢ ∀ {b₀ b₁ : CommRingCat} (f : b₀ ⟶ b₁),
    (Cat.Hom.isoMk (extendScalarsComp (Hom.hom (𝟙 b₀)) (Hom.hom f))).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsId ↑b₀)).hom (extendScalars (Hom.hom f)).toCatHom ≫
          (Bicategory.leftUnitor (extendScalars (Hom.hom f)).toCatHom).hom =
      eqToHom ⋯
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: case refine_2
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 Y✝ : Cᵒᵖ
π : X ⟶ Y✝
r r' : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X)
hS : S ∈ J (Opposite.unop X)
r₀ : Presieve.FamilyOfElements (R₀ ⋙ forget RingCat) S.arrows
m₀ : Presieve.FamilyOfElements (M₀.presheaf ⋙ forget Ab) S.arrows
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
a : ↑(A.obj.obj X)
ha : ((r₀.smul m₀).map (whiskerRight φ (forget Ab))).IsAmalgamation a
Y : Cᵒᵖ
f : X ⟶ Y
a₀ : ↑(R₀.obj Y)
ha₀ : (ConcreteCategory.hom (α.app Y)) a₀ = (ConcreteCategory.hom (R.obj.map f)) r
b₀ : ↑(M₀.obj Y)
hb₀ : (ConcreteCategory.hom (φ.app Y)) b₀ = (ConcreteCategory.hom (A.obj.map f)) m
Z : C
g : Z ⟶ Opposite.unop Y
hg : S.arrows (g ≫ f.unop)
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Z))) (m₀ (g ≫ f.unop) hg) =
    (ConcreteCategory.hom (φ.app (Opposite.op Z))) ((ConcreteCategory.hom (M₀.map g.op)) b₀)

Tactic:
·

Goal state after:
case refine_2
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 Y✝ : Cᵒᵖ
π : X ⟶ Y✝
r r' : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X)
hS : S ∈ J (Opposite.unop X)
r₀ : Presieve.FamilyOfElements (R₀ ⋙ forget RingCat) S.arrows
m₀ : Presieve.FamilyOfElements (M₀.presheaf ⋙ forget Ab) S.arrows
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
a : ↑(A.obj.obj X)
ha : ((r₀.smul m₀).map (whiskerRight φ (forget Ab))).IsAmalgamation a
Y : Cᵒᵖ
f : X ⟶ Y
a₀ : ↑(R₀.obj Y)
ha₀ : (ConcreteCategory.hom (α.app Y)) a₀ = (ConcreteCategory.hom (R.obj.map f)) r
b₀ : ↑(M₀.obj Y)
hb₀ : (ConcreteCategory.hom (φ.app Y)) b₀ = (ConcreteCategory.hom (A.obj.map f)) m
Z : C
g : Z ⟶ Opposite.unop Y
hg : S.arrows (g ≫ f.unop)
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Z))) (m₀ (g ≫ f.unop) hg) =
    (ConcreteCategory.hom (φ.app (Opposite.op Z))) ((ConcreteCategory.hom (M₀.map g.op)) b₀)
Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor

Goal state before:
pp: case refine_3
⊢ ∀ {b₀ b₁ : CommRingCat} (f : b₀ ⟶ b₁),
    (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom (𝟙 b₁)))).hom ≫
        Bicategory.whiskerLeft (extendScalars (Hom.hom f)).toCatHom (Cat.Hom.isoMk (extendScalarsId ↑b₁)).hom ≫
          (Bicategory.rightUnitor (extendScalars (Hom.hom f)).toCatHom).hom =
      eqToHom ⋯

Tactic:
·

Goal state after:
case refine_3
⊢ ∀ {b₀ b₁ : CommRingCat} (f : b₀ ⟶ b₁),
    (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom (𝟙 b₁)))).hom ≫
        Bicategory.whiskerLeft (extendScalars (Hom.hom f)).toCatHom (Cat.Hom.isoMk (extendScalarsId ↑b₁)).hom ≫
          (Bicategory.rightUnitor (extendScalars (Hom.hom f)).toCatHom).hom =
      eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
s : Cofork (Sigma.map' f fun x ↦ 𝟙 R) 0
b : β
hb : b ∈ Set.range f
⊢ (Sigma.ι (fun x ↦ R) b ≫
      Cofork.π (sigmaConstCokernelCofork R f) ≫
        Sigma.desc fun x ↦
          match x with
          | ⟨b, property⟩ => Sigma.ι (fun x ↦ R) b ≫ s.π) =
    Sigma.ι (fun x ↦ R) b ≫ s.π

pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
s : Cofork (Sigma.map' f fun x ↦ 𝟙 R) 0
b : β
hb : b ∉ Set.range f
⊢ (Sigma.ι (fun x ↦ R) b ≫
      Cofork.π (sigmaConstCokernelCofork R f) ≫
        Sigma.desc fun x ↦
          match x with
          | ⟨b, property⟩ => Sigma.ι (fun x ↦ R) b ≫ s.π) =
    Sigma.ι (fun x ↦ R) b ≫ s.π

Tactic:
·

Goal state after:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
s : Cofork (Sigma.map' f fun x ↦ 𝟙 R) 0
b : β
hb : b ∈ Set.range f
⊢ (Sigma.ι (fun x ↦ R) b ≫
      Cofork.π (sigmaConstCokernelCofork R f) ≫
        Sigma.desc fun x ↦
          match x with
          | ⟨b, property⟩ => Sigma.ι (fun x ↦ R) b ≫ s.π) =
    Sigma.ι (fun x ↦ R) b ≫ s.π
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
s : Cofork (Sigma.map' f fun x ↦ 𝟙 R) 0
b : β
hb : b ∉ Set.range f
⊢ (Sigma.ι (fun x ↦ R) b ≫
      Cofork.π (sigmaConstCokernelCofork R f) ≫
        Sigma.desc fun x ↦
          match x with
          | ⟨b, property⟩ => Sigma.ι (fun x ↦ R) b ≫ s.π) =
    Sigma.ι (fun x ↦ R) b ≫ s.π

Tactic:
·

Goal state after:
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
s : Cofork (Sigma.map' f fun x ↦ 𝟙 R) 0
b : β
hb : b ∉ Set.range f
⊢ (Sigma.ι (fun x ↦ R) b ≫
      Cofork.π (sigmaConstCokernelCofork R f) ≫
        Sigma.desc fun x ↦
          match x with
          | ⟨b, property⟩ => Sigma.ι (fun x ↦ R) b ≫ s.π) =
    Sigma.ι (fun x ↦ R) b ≫ s.π
Module: Mathlib.CategoryTheory.Limits.Bicones

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

pp: case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
g : BiconeHom J Bicone.right Z✝
⊢ BiconeHom J Bicone.right Z✝

pp: case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.left Z✝

pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.right Z✝

pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram k✝) Z✝
⊢ BiconeHom J (Bicone.diagram j✝) Z✝

Tactic:
·

Goal state after:
case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
g : BiconeHom J Bicone.left Z✝
⊢ BiconeHom J Bicone.left Z✝
Module: Mathlib.CategoryTheory.Limits.Bicones

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

pp: case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.left Z✝

pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.right Z✝

pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram k✝) Z✝
⊢ BiconeHom J (Bicone.diagram j✝) Z✝

Tactic:
·

Goal state after:
case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
g : BiconeHom J Bicone.right Z✝
⊢ BiconeHom J Bicone.right Z✝
Module: Mathlib.CategoryTheory.Limits.Bicones

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

pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.right Z✝

pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram k✝) Z✝
⊢ BiconeHom J (Bicone.diagram j✝) Z✝

Tactic:
·

Goal state after:
case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.left Z✝
Module: Mathlib.CategoryTheory.Limits.Bicones

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

pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram k✝) Z✝
⊢ BiconeHom J (Bicone.diagram j✝) Z✝

Tactic:
·

Goal state after:
case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.right Z✝
Module: Mathlib.CategoryTheory.Limits.Bicones

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

Tactic:
·

Goal state after:
case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram k✝) Z✝
⊢ BiconeHom J (Bicone.diagram j✝) Z✝
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j

pp: case right_id
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j

pp: case left
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

pp: case right
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

pp: case diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ k✝ : J
f : j✝ ⟶ k✝
⊢ (Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram k✝) c₁.pt c₂.pt fun j ↦ F.obj j

Tactic:
·

Goal state after:
case left_id
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right_id
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j

pp: case left
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

pp: case right
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

pp: case diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ k✝ : J
f : j✝ ⟶ k✝
⊢ (Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram k✝) c₁.pt c₂.pt fun j ↦ F.obj j

Tactic:
·

Goal state after:
case right_id
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
⊢ (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

pp: case right
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

pp: case diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ k✝ : J
f : j✝ ⟶ k✝
⊢ (Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram k✝) c₁.pt c₂.pt fun j ↦ F.obj j

Tactic:
·

Goal state after:
case left
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.left c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

Tactic:
exact c₁.π.app _

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

Goal state before:
pp: case right
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j

pp: case diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ k✝ : J
f : j✝ ⟶ k✝
⊢ (Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram k✝) c₁.pt c₂.pt fun j ↦ F.obj j

Tactic:
·

Goal state after:
case right
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ : J
⊢ (Bicone.casesOn Bicone.right c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ k✝ : J
f : j✝ ⟶ k✝
⊢ (Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram k✝) c₁.pt c₂.pt fun j ↦ F.obj j

Tactic:
·

Goal state after:
case diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ k✝ : J
f : j✝ ⟶ k✝
⊢ (Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram k✝) c₁.pt c₂.pt fun j ↦ F.obj j
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✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) F.unop

Tactic:
apply +allowSynthFailures preservesColimitsOfShape_unop
    exact preservesLimitsOfShape_of_equiv (Discrete.opposite _).symm _

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyCoflat F.op
X : D
⊢ IsCofiltered (StructuredArrow X F)

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyFlat F
x✝ : Dᵒᵖ
X : D
⊢ IsFiltered (CostructuredArrow F.op (op X))

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyCoflat F.op
X : D
⊢ IsCofiltered (StructuredArrow X F)
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyFlat F
x✝ : Dᵒᵖ
X : D
⊢ IsFiltered (CostructuredArrow F.op (op X))

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyFlat F
x✝ : Dᵒᵖ
X : D
⊢ IsFiltered (CostructuredArrow F.op (op X))
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyFlat F.op
X : D
⊢ IsFiltered (CostructuredArrow F X)

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyCoflat F
x✝ : Dᵒᵖ
X : D
⊢ IsCofiltered (StructuredArrow (op X) F.op)

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyFlat F.op
X : D
⊢ IsFiltered (CostructuredArrow F X)
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyCoflat F
x✝ : Dᵒᵖ
X : D
⊢ IsCofiltered (StructuredArrow (op X) F.op)

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyCoflat F
x✝ : Dᵒᵖ
X : D
⊢ IsCofiltered (StructuredArrow (op X) F.op)
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ J₁.close (Sieve.pullback f S) ≤ Sieve.pullback f (J₁.close S)

pp: case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ Sieve.pullback f (J₁.close S) ≤ J₁.close (Sieve.pullback f S)

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ J₁.close (Sieve.pullback f S) ≤ Sieve.pullback f (J₁.close S)
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ Sieve.pullback f (J₁.close S) ≤ J₁.close (Sieve.pullback f S)

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ Sieve.pullback f (J₁.close S) ≤ J₁.close (Sieve.pullback f S)
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
⊢ J₁.close S = ⊤ → S ∈ J₁ X

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ J₁ X → J₁.close S = ⊤

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ J₁.close S = ⊤ → S ∈ J₁ X
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ J₁ X → J₁.close S = ⊤

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ J₁ X → J₁.close S = ⊤
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ Presieve.IsSeparatedFor (Functor.closedSieves J₁).toFunctor S.arrows

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), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ Presieve.IsSeparatedFor (Functor.closedSieves J₁).toFunctor S.arrows