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

Goal state before:
pp: case mk
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Preadditive C
D : Type u_1
inst✝⁵ : Category.{v₁, u_1} D
inst✝⁴ : Preadditive D
E : Type u_2
inst✝³ : Category.{v₁, u_2} E
inst✝² : Preadditive E
F : C ⥤ D
inst✝¹ : F.Additive
G : D ⥤ E
inst✝ : G.Additive
ι✝ : Type
fintype✝ : Fintype ι✝
X✝ : ι✝ → C
⊢ (F ⋙ G).mapMat_.obj { ι := ι✝, fintype := fintype✝, X := X✝ } =
    (F.mapMat_ ⋙ G.mapMat_).obj { ι := ι✝, fintype := fintype✝, X := X✝ }

Tactic:
;

Goal state after:
case mk
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Preadditive C
D : Type u_1
inst✝⁵ : Category.{v₁, u_1} D
inst✝⁴ : Preadditive D
E : Type u_2
inst✝³ : Category.{v₁, u_2} E
inst✝² : Preadditive E
F : C ⥤ D
inst✝¹ : F.Additive
G : D ⥤ E
inst✝ : G.Additive
ι✝ : Type
fintype✝ : Fintype ι✝
X✝ : ι✝ → C
⊢ (F ⋙ G).mapMat_.obj { ι := ι✝, fintype := fintype✝, X := X✝ } =
    (F.mapMat_ ⋙ G.mapMat_).obj { ι := ι✝, fintype := fintype✝, X := X✝ }
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case mk
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Preadditive C
D : Type u_1
inst✝⁵ : Category.{v₁, u_1} D
inst✝⁴ : Preadditive D
E : Type u_2
inst✝³ : Category.{v₁, u_2} E
inst✝² : Preadditive E
F : C ⥤ D
inst✝¹ : F.Additive
G : D ⥤ E
inst✝ : G.Additive
N : Mat_ C
j✝ : ((F.mapMat_ ⋙ G.mapMat_).obj N).ι
ι✝ : Type
fintype✝ : Fintype ι✝
X✝ : ι✝ → C
f : { ι := ι✝, fintype := fintype✝, X := X✝ } ⟶ N
i✝ : ((F ⋙ G).mapMat_.obj { ι := ι✝, fintype := fintype✝, X := X✝ }).ι
⊢ ((F ⋙ G).mapMat_.map f ≫ (eqToIso ⋯).hom) i✝ j✝ = ((eqToIso ⋯).hom ≫ (F.mapMat_ ⋙ G.mapMat_).map f) i✝ j✝

Tactic:
;

Goal state after:
case mk
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Preadditive C
D : Type u_1
inst✝⁵ : Category.{v₁, u_1} D
inst✝⁴ : Preadditive D
E : Type u_2
inst✝³ : Category.{v₁, u_2} E
inst✝² : Preadditive E
F : C ⥤ D
inst✝¹ : F.Additive
G : D ⥤ E
inst✝ : G.Additive
N : Mat_ C
j✝ : ((F.mapMat_ ⋙ G.mapMat_).obj N).ι
ι✝ : Type
fintype✝ : Fintype ι✝
X✝ : ι✝ → C
f : { ι := ι✝, fintype := fintype✝, X := X✝ } ⟶ N
i✝ : ((F ⋙ G).mapMat_.obj { ι := ι✝, fintype := fintype✝, X := X✝ }).ι
⊢ ((F ⋙ G).mapMat_.map f ≫ (eqToIso ⋯).hom) i✝ j✝ = ((eqToIso ⋯).hom ≫ (F.mapMat_ ⋙ G.mapMat_).map f) i✝ j✝
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
x✝ : C
j✝ : { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun x ↦ x✝ }.ι
⊢ 𝟙 x✝ = 𝟙 { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun x ↦ x✝ } PUnit.unit j✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
x✝ : C
j✝ : { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun x ↦ x✝ }.ι
⊢ 𝟙 x✝ = 𝟙 { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun x ↦ x✝ } PUnit.unit j✝
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
j✝ : { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun x ↦ Z✝ }.ι
⊢ x✝¹ ≫ x✝ = ((fun x x_1 ↦ x✝¹) ≫ fun x x_1 ↦ x✝) PUnit.unit j✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
j✝ : { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun x ↦ Z✝ }.ι
⊢ x✝¹ ≫ x✝ = ((fun x x_1 ↦ x✝¹) ≫ fun x x_1 ↦ x✝) PUnit.unit j✝
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ((fun j x ↦ if h : j = i then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : i = k then eqToHom ⋯ else 0) i j =
    if h : i = j then eqToHom ⋯ else 0

pp: case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ∀ b ∈ Finset.univ,
    b ≠ i → ((fun j x ↦ if h : j = b then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : b = k then eqToHom ⋯ else 0) i j = 0

pp: case h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ i ∉ Finset.univ →
    ((fun j x ↦ if h : j = i then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : i = k then eqToHom ⋯ else 0) i j = 0

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ((fun j x ↦ if h : j = i then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : i = k then eqToHom ⋯ else 0) i j =
    if h : i = j then eqToHom ⋯ else 0

case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ∀ b ∈ Finset.univ,
    b ≠ i → ((fun j x ↦ if h : j = b then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : b = k then eqToHom ⋯ else 0) i j = 0

case h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ i ∉ Finset.univ →
    ((fun j x ↦ if h : j = i then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : i = k then eqToHom ⋯ else 0) i j = 0
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
x : ↑(F.obj x✝¹)
⊢ (Hom.hom (F.map f ≫ ofHom { toFun := ⇑(ConcreteCategory.hom (c.ι.app x✝)), inj' := ⋯, map_rel_iff' := ⋯ })) x =
    (Hom.hom
        (ofHom { toFun := ⇑(ConcreteCategory.hom (c.ι.app x✝¹)), inj' := ⋯, map_rel_iff' := ⋯ } ≫
          ((Functor.const J).obj { carrier := CoconePt hc, str := instPartialOrderCoconePt hc }).map f))
      x

Tactic:
;

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
x : ↑(F.obj x✝¹)
⊢ (Hom.hom (F.map f ≫ ofHom { toFun := ⇑(ConcreteCategory.hom (c.ι.app x✝)), inj' := ⋯, map_rel_iff' := ⋯ })) x =
    (Hom.hom
        (ofHom { toFun := ⇑(ConcreteCategory.hom (c.ι.app x✝¹)), inj' := ⋯, map_rel_iff' := ⋯ } ≫
          ((Functor.const J).obj { carrier := CoconePt hc, str := instPartialOrderCoconePt hc }).map f))
      x
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case pos
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : C ⥤ D
inst✝ : F.Additive
X : Mat_ C
j : X.ι
⊢ biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫
      (biproduct.matrix fun i j ↦ F.map (𝟙 X i j)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) j =
    biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫ 𝟙 (⨁ fun i ↦ F.obj (X.X i)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) j

Tactic:
;

Goal state after:
case pos
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : C ⥤ D
inst✝ : F.Additive
X : Mat_ C
j : X.ι
⊢ biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫
      (biproduct.matrix fun i j ↦ F.map (𝟙 X i j)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) j =
    biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫ 𝟙 (⨁ fun i ↦ F.obj (X.X i)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) j
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type u
inst✝ : Semiring R
W✝ X✝ Y✝ Z✝ : Mat R
f✝ : Matrix W✝.obj X✝.obj R
g✝ : Matrix X✝.obj Y✝.obj R
h✝ : Matrix Y✝.obj Z✝.obj R
⊢ ((have this :=
        (have this := f✝;
          this) *
          have this := g✝;
          this;
      this) *
      have this := h✝;
      this) =
    (have this := f✝;
      this) *
      have this :=
        (have this := g✝;
          this) *
          have this := h✝;
          this;
      this

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type u
inst✝ : Semiring R
W✝ X✝ Y✝ Z✝ : Mat R
f✝ : Matrix W✝.obj X✝.obj R
g✝ : Matrix X✝.obj Y✝.obj R
h✝ : Matrix Y✝.obj Z✝.obj R
⊢ ((have this :=
        (have this := f✝;
          this) *
          have this := g✝;
          this;
      this) *
      have this := h✝;
      this) =
    (have this := f✝;
      this) *
      have this :=
        (have this := g✝;
          this) *
          have this := h✝;
          this;
      this
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
S : Subtype (J.PropSetWithTop κ')
x✝ : ↑↑S
⊢ ↑x✝ ≤ ⊤

Tactic:
;

Goal state after:
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
S : Subtype (J.PropSetWithTop κ')
x✝ : ↑↑S
⊢ ↑x✝ ≤ ⊤
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
obj✝ : Type
property✝ : Finite obj✝
⊢ (equivalenceSingleObjInverse R).obj
      { ι := { obj := obj✝, property := property✝ }.obj, fintype := FintypeCat.fintype, X := fun x ↦ PUnit.unit } =
    { obj := obj✝, property := property✝ }

Tactic:
;

Goal state after:
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
obj✝ : Type
property✝ : Finite obj✝
⊢ (equivalenceSingleObjInverse R).obj
      { ι := { obj := obj✝, property := property✝ }.obj, fintype := FintypeCat.fintype, X := fun x ↦ PUnit.unit } =
    { obj := obj✝, property := property✝ }
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j X Y : J
i✝ : Unit
⊢ ObjectProperty.ofObj (fun x ↦ j) j

Tactic:
;

Goal state after:
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j X Y : J
i✝ : Unit
⊢ ObjectProperty.ofObj (fun x ↦ j) j
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
i✝ : Unit
⊢ ∃ a, (fun x ↦ ⟨j, ⋯⟩) a = ⟨j, ⋯⟩

Tactic:
;

Goal state after:
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
i✝ : Unit
⊢ ∃ a, (fun x ↦ ⟨j, ⋯⟩) a = ⟨j, ⋯⟩
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j X Y : J
i✝ : Unit
lift✝ : {j_1 : J} → (Diagram.single j).P j_1 → (j_1 ⟶ j)
hlift✝ : ∀ {j_1 : J} (hj : (Diagram.single j).P j_1), (Diagram.single j).W (lift✝ hj)
uniq✝ : ∀ {j_1 : J} (hj : (Diagram.single j).P j_1) {φ : j_1 ⟶ j}, (Diagram.single j).W φ → lift✝ hj = φ
comm✝ : ∀ {i j_1 : J} (f : i ⟶ j_1) (hf : (Diagram.single j).W f), f ≫ lift✝ ⋯ = lift✝ ⋯
⊢ j = j

Tactic:
;

Goal state after:
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j X Y : J
i✝ : Unit
lift✝ : {j_1 : J} → (Diagram.single j).P j_1 → (j_1 ⟶ j)
hlift✝ : ∀ {j_1 : J} (hj : (Diagram.single j).P j_1), (Diagram.single j).W (lift✝ hj)
uniq✝ : ∀ {j_1 : J} (hj : (Diagram.single j).P j_1) {φ : j_1 ⟶ j}, (Diagram.single j).W φ → lift✝ hj = φ
comm✝ : ∀ {i j_1 : J} (f : i ⟶ j_1) (hf : (Diagram.single j).W f), f ≫ lift✝ ⋯ = lift✝ ⋯
⊢ j = j
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁴ : HasCoproduct D₁.obj₁
inst✝³ : HasCoproduct D₁.obj₂
inst✝² : HasPushouts C
inst✝¹ : MorphismProperty.IsSmall.{w, v, u} W
inst✝ : LocallySmall.{w, v, u} C
⊢ Small.{w, max u v} (D₂ W Z)

Tactic:
;

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁴ : HasCoproduct D₁.obj₁
inst✝³ : HasCoproduct D₁.obj₂
inst✝² : HasPushouts C
inst✝¹ : MorphismProperty.IsSmall.{w, v, u} W
inst✝ : LocallySmall.{w, v, u} C
⊢ Small.{w, max u v} (D₂ W Z)
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c✝ : Cocone F
hc : IsColimit c✝
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c✝.ι.app j = g ≫ c✝.ι.app j
k : ToType X → J
a : (x : ToType X) → j ⟶ k x
hk : ∀ (x : ToType X), (hom (F.map (a x))) ((hom f) x) = (hom (F.map (a x))) ((hom g) x)
l : J
b : j ⟶ l
c : (x : ToType X) → k x ⟶ l
hl : ∀ (x : ToType X), a x ≫ c x = b
x : X
⊢ (hom (f ≫ F.map b)).toFun x = (hom (g ≫ F.map b)).toFun x

Tactic:
;

Goal state after:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c✝ : Cocone F
hc : IsColimit c✝
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c✝.ι.app j = g ≫ c✝.ι.app j
k : ToType X → J
a : (x : ToType X) → j ⟶ k x
hk : ∀ (x : ToType X), (hom (F.map (a x))) ((hom f) x) = (hom (F.map (a x))) ((hom g) x)
l : J
b : j ⟶ l
c : (x : ToType X) → k x ⟶ l
hl : ∀ (x : ToType X), a x ≫ c x = b
x : X
⊢ (hom (f ≫ F.map b)).toFun x = (hom (g ≫ F.map b)).toFun x
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case refine_3.inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
l₁ l₂ : m ⟶ m
hl₁ : (D₂ D hι u).W l₁
hl₂ : (D₂ D hι u).W l₂
⊢ l₁ = l₂

Tactic:
eq_id_of_D₂_W D hι u hD hl₁,

Goal state after:
case refine_3.inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
l₁ l₂ : m ⟶ m
hl₁ : (D₂ D hι u).W l₁
hl₂ : (D₂ D hι u).W l₂
⊢ 𝟙 m = l₂
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
j k : J
f : j ⟶ k
i : ι
hf : (D i).W f
⊢ f ≫ φ ⟨i, ⟨k, ⋯⟩⟩ = φ ⟨i, ⟨j, ⋯⟩⟩

Tactic:
simp [φ, (D i).isTerminal.comm_assoc _ hf]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case refine_1
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
he : (D₂ D hι u).IsTerminal m :=
  have H := ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
D₂' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₂ D hι u;
  { toDiagram := __Diagram, top := m, isTerminal := he, uniq_terminal := ⋯ }
i : ι
⊢ (D i).W ≤ D₂'.W

pp: case refine_2
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
he : (D₂ D hι u).IsTerminal m :=
  have H := ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
D₂' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₂ D hι u;
  { toDiagram := __Diagram, top := m, isTerminal := he, uniq_terminal := ⋯ }
i : ι
⊢ (D i).P ≤ D₂'.P

Tactic:
· exact le_trans (le_trans (le_trans (by rfl) (le_iSup _ i)) le_sup_left) le_sup_left

Goal state after:
case refine_2
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
he : (D₂ D hι u).IsTerminal m :=
  have H := ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
D₂' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₂ D hι u;
  { toDiagram := __Diagram, top := m, isTerminal := he, uniq_terminal := ⋯ }
i : ι
⊢ (D i).P ≤ D₂'.P
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: case mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
i✝ : α
⊢ S.arrows (π i✝)

Tactic:
;

Goal state after:
case mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
i✝ : α
⊢ S.arrows (π i✝)
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : Preregular C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w✝ : EffectiveEpi g
g' : Y ⟶ ∐ X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : α → C := fun a ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun a ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun a ↦ pullback.fst g' (Sigma.ι X₁ a)
x✝ : IsIso (Sigma.desc fun x ↦ pullback.fst g' (Sigma.ι X₁ x))
b✝ : α
⊢ Sigma.ι (fun b ↦ Limits.pullback g' (Sigma.ι X₁ b)) b✝ ≫ Sigma.desc π' ≫ g =
    Sigma.ι (fun b ↦ Limits.pullback g' (Sigma.ι X₁ b)) b✝ ≫ Sigma.desc π₂

Tactic:
;

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : Preregular C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w✝ : EffectiveEpi g
g' : Y ⟶ ∐ X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : α → C := fun a ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun a ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun a ↦ pullback.fst g' (Sigma.ι X₁ a)
x✝ : IsIso (Sigma.desc fun x ↦ pullback.fst g' (Sigma.ι X₁ x))
b✝ : α
⊢ Sigma.ι (fun b ↦ Limits.pullback g' (Sigma.ι X₁ b)) b✝ ≫ Sigma.desc π' ≫ g =
    Sigma.ι (fun b ↦ Limits.pullback g' (Sigma.ι X₁ b)) b✝ ≫ Sigma.desc π₂
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: case refine_2.of.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
⊢ (extensiveCoverage C ⊔ regularCoverage C).Saturate Y
    (generate (Presieve.ofArrows (fun x ↦ ∐ fun i ↦ X i) fun x ↦ Sigma.desc f))

Tactic:
apply Coverage.Saturate.of
        simp only [Coverage.sup_covering, extensiveCoverage, regularCoverage, Set.mem_union,
          Set.mem_ofPred_eq]
        exact Or.inr ⟨_, Sigma.desc f, ⟨rfl, inferInstance⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: case mk
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝¹ : Unit
ψ : R ⟶ ∐ fun i ↦ X i
Q : C
i✝ : I
e : Q ⟶ X i✝
⊢ Presieve.ofArrows X f (Sigma.ι X i✝ ≫ Sigma.desc f)

Tactic:
;

Goal state after:
case mk
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝¹ : Unit
ψ : R ⟶ ∐ fun i ↦ X i
Q : C
i✝ : I
e : Q ⟶ X i✝
⊢ Presieve.ofArrows X f (Sigma.ι X i✝ ≫ Sigma.desc f)
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
i✝ : α
⊢ S.arrows (π i✝)

Tactic:
;

Goal state after:
case mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
i✝ : α
⊢ S.arrows (π i✝)
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B x✝¹ : D
x✝ : x✝¹ ⟶ B
⊢ Presieve.singleton (F.effectiveEpiOver B) x✝ =
    Presieve.ofArrows (fun x ↦ F.effectiveEpiOverObj B) (fun x ↦ F.effectiveEpiOver B) x✝

Tactic:
;

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B x✝¹ : D
x✝ : x✝¹ ⟶ B
⊢ Presieve.singleton (F.effectiveEpiOver B) x✝ =
    Presieve.ofArrows (fun x ↦ F.effectiveEpiOverObj B) (fun x ↦ F.effectiveEpiOver B) x✝
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
B x✝¹ : D
x✝ : x✝¹ ⟶ B
⊢ Presieve.singleton (F.effectiveEpiOver B) x✝ =
    Presieve.ofArrows (fun x ↦ F.effectiveEpiOverObj B) (fun x ↦ F.effectiveEpiOver B) x✝

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
B x✝¹ : D
x✝ : x✝¹ ⟶ B
⊢ Presieve.singleton (F.effectiveEpiOver B) x✝ =
    Presieve.ofArrows (fun x ↦ F.effectiveEpiOverObj B) (fun x ↦ F.effectiveEpiOver B) x✝