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

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 0 ↔ IsEmpty (X ≅ Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = if Nonempty (X ≅ Y) then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
| M.X ◁ g.hom ≫ f.hom ▷ Q.X

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
| colimit.ι (parallelPair (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one

Tactic:
whisker_exchange

Goal state after:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
| f.hom ▷ P.X ≫ N.X ◁ g.hom

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
| colimit.ι (parallelPair (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ M.whiskerLeft g ≫ whiskerRight f Q = whiskerRight f P ≫ N.whiskerLeft g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: X : PartOrdEmb
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: X Y Z : PartOrdEmb
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: X Y : PartOrdEmb
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: X Y : PartOrdEmb
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: α β : PartOrdEmb
f : α ⟶ β
hf : Function.Bijective ⇑(ConcreteCategory.hom ((forget PartOrdEmb).map f))
⊢ ∀ {a b : ↑α},
    (Equiv.ofBijective (⇑(ConcreteCategory.hom ((forget PartOrdEmb).map f))) hf) a ≤
        (Equiv.ofBijective (⇑(ConcreteCategory.hom ((forget PartOrdEmb).map f))) hf) b ↔
      a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: α β : PartOrdEmb
f : α ⟶ β
hf : IsIso ((forget PartOrdEmb).map f)
⊢ IsIso f

Tactic:
by

Goal state after:
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 : CoconePt hc
⊢ ∃ j x' y', ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = x) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = x), x' ≤ y'

Tactic:
by

Goal state after:
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
⊢ ∀ (a b c_1 : CoconePt hc),
    (∃ j x' y',
        ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = a) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = b), x' ≤ y') →
      (∃ j x' y',
          ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = b) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = c_1),
            x' ≤ y') →
        ∃ j x' y',
          ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = a) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = c_1), x' ≤ y'

Tactic:
by

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
hF : ∀ (j : J), IsCardinalFiltered (↑(F.obj j)) κ
⊢ IsCardinalFiltered (CoconePt hc) κ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X✝ Y✝ : Mat_ C
f : X✝.Hom Y✝
⊢ (Hom.id X✝).comp f = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X✝ Y✝ : Mat_ C
f : X✝.Hom Y✝
⊢ f.comp (Hom.id Y✝) = f

Tactic:
by

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
⊢ (isCardinalFiltered κ).colimitsOfShape J ≤ isCardinalFiltered κ

Tactic:
by

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
⊢ HasColimitsOfShape J (CardinalDirectedPoset κ)

Tactic:
by

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
A : Type u
inst✝¹ : SmallCategory A
inst✝ : IsCardinalFiltered A κ
⊢ PreservesColimitsOfShape A (forget (CardinalDirectedPoset κ))

Tactic:
by

Goal state after:
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 y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l₁ : J
a : j ⟶ l₁
b : k ⟶ l₁
h₃ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a)) x₁ = (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b)) x₂
l₂ : J
a' : j ⟶ l₂
b' : k ⟶ l₂
h₄ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a')) y₁ =
    (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b')) y₂
l : J
d : l₁ ⟶ l
d' : l₂ ⟶ l
h₅ : a ≫ d = a' ≫ d'
h₆ : b ≫ d = b' ≫ d'
⊢ (ConcreteCategory.hom (F.map (a ≫ d))) x₁ = (ConcreteCategory.hom (F.map (b ≫ d))) x₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
W✝ X✝ Y✝ Z✝ : Mat_ C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i : M.ι
⊢ 𝟙 M i i = 𝟙 (M.X i)

Tactic:
by

Goal state after:
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.ι
h : i ≠ j
⊢ 𝟙 M i j = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M N K : Mat_ C
f f' : M ⟶ N
g : N ⟶ K
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g

Tactic:
by

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝³ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
P : Set ↑J.obj → Prop
inst✝² : IsDirectedOrder (Subtype P)
inst✝¹ : Nonempty (Subtype P)
inst✝ : ∀ (S : Subtype P), IsCardinalFiltered (↑↑S) κ
S : Subtype P
⊢ PartOrdEmb.isCardinalFiltered κ ((PartOrdEmb.functorOfPredicateSet P).obj S)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M N K : Mat_ C
f : M ⟶ N
g g' : N ⟶ K
⊢ f ≫ (g + g') = f ≫ g + f ≫ g'

Tactic:
by

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
⊢ Cardinal.mk κ.ord.ToType = κ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.ι
y : (f j).ι
⊢ (fun i j_1 ↦
      { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.X i ⟶ (f j).X j_1)
    x y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : (f j).ι
y : { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.ι
⊢ (fun i j_1 ↦
      (f j).X i ⟶ { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.X j_1)
    x y

Tactic:
by

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
α : Type u := (S : Set X) × (x : PartialOrder ↑S) × ULift.{u, 0} (PLift (IsCardinalFiltered (↑S) κ))
this : (a : α) → PartialOrder ↑a.fst := fun a ↦ a.snd.fst
ι : α → CardinalDirectedPoset κ := fun a ↦ { obj := { carrier := ↑a.fst, str := this a }, property := ⋯ }
J : CardinalDirectedPoset κ
x✝ : hasCardinalLTWithTerminal κ J
hJ : HasCardinalLT (↑J.obj) κ
right✝ : HasTerminal ↑J.obj
⊢ Cardinal.mk ↑J.obj ≤ Cardinal.mk X

Tactic:
by

Goal state after:
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 y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l₁ : J
a : j ⟶ l₁
b : k ⟶ l₁
h₃ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a)) x₁ = (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b)) x₂
l₂ : J
a' : j ⟶ l₂
b' : k ⟶ l₂
h₄ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a')) y₁ =
    (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b')) y₂
l : J
d : l₁ ⟶ l
d' : l₂ ⟶ l
h₅ : a ≫ d = a' ≫ d'
h₆ : b ≫ d = b' ≫ d'
⊢ (ConcreteCategory.hom (F.map (a' ≫ d'))) y₁ = (ConcreteCategory.hom (F.map (a ≫ d))) y₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
⊢ ((fun x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0) ≫ fun x y ↦
      if h : x.fst = j' then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0) =
    if h : j = j' then eqToHom ⋯ else 0

Tactic:
by

Goal state after:
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 y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l₁ : J
a : j ⟶ l₁
b : k ⟶ l₁
h₃ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a)) x₁ = (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b)) x₂
l₂ : J
a' : j ⟶ l₂
b' : k ⟶ l₂
h₄ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a')) y₁ =
    (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b')) y₂
l : J
d : l₁ ⟶ l
d' : l₂ ⟶ l
h₅ : a ≫ d = a' ≫ d'
h₆ : b ≫ d = b' ≫ d'
⊢ (ConcreteCategory.hom (F.map (a' ≫ d'))) y₁ = (ConcreteCategory.hom (F.map (b ≫ d))) y₂

Tactic:
by

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
α : Type u := (S : Set X) × (x : PartialOrder ↑S) × ULift.{u, 0} (PLift (IsCardinalFiltered (↑S) κ))
this✝ : (a : α) → PartialOrder ↑a.fst := fun a ↦ a.snd.fst
ι : α → CardinalDirectedPoset κ := fun a ↦ { obj := { carrier := ↑a.fst, str := this✝ a }, property := ⋯ }
J : CardinalDirectedPoset κ
x✝ : hasCardinalLTWithTerminal κ J
hJ : HasCardinalLT (↑J.obj) κ
right✝ : HasTerminal ↑J.obj
f : ↑J.obj ↪ X
e : ↑J.obj ≃ ↑(Set.range ⇑f) := Equiv.ofInjective ⇑f ⋯
this : PartialOrder ↑(Set.range ⇑f) := PartialOrder.lift ⇑e.symm ⋯
⊢ ∀ {a b : ↑(Set.range ⇑f)}, e.symm a ≤ e.symm b ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
α : Type u := (S : Set X) × (x : PartialOrder ↑S) × ULift.{u, 0} (PLift (IsCardinalFiltered (↑S) κ))
this✝ : (a : α) → PartialOrder ↑a.fst := fun a ↦ a.snd.fst
ι : α → CardinalDirectedPoset κ := fun a ↦ { obj := { carrier := ↑a.fst, str := this✝ a }, property := ⋯ }
J : CardinalDirectedPoset κ
x✝ : hasCardinalLTWithTerminal κ J
hJ : HasCardinalLT (↑J.obj) κ
right✝ : HasTerminal ↑J.obj
f : ↑J.obj ↪ X
e : ↑J.obj ≃ ↑(Set.range ⇑f) := Equiv.ofInjective ⇑f ⋯
this : PartialOrder ↑(Set.range ⇑f) := PartialOrder.lift ⇑e.symm ⋯
e' : ↑(Set.range ⇑f) ≃o ↑J.obj :=
  let __Equiv := e.symm;
  { toEquiv := __Equiv, map_rel_iff' := ⋯ }
⊢ ↑(CardinalDirectedPoset.ι.obj J) ≃o
    ↑(CardinalDirectedPoset.ι.obj (ι ⟨Set.range ⇑f, ⟨inferInstance, { down := { down := ⋯ } }⟩⟩))

Tactic:
by

Goal state after:
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 y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
⊢ ∃ l a b x₃ y₃,
    x₃ = (ConcreteCategory.hom (F.map a)) x₁ ∧
      x₃ = (ConcreteCategory.hom (F.map b)) x₂ ∧
        y₃ = (ConcreteCategory.hom (F.map a)) y₁ ∧ y₃ = (ConcreteCategory.hom (F.map b)) y₂

Tactic:
by

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{u, u, u + 1} Q), hasCardinalLTWithTerminal κ ≤ Q.isoClosure

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case h₀.hnc
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : (f i).ι
a✝ : b ∈ Finset.univ
hb : b ≠ j
⊢ ¬⋯ ▸ j = b

Tactic:
simp only

Goal state after:
case h₀.hnc
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : (f i).ι
a✝ : b ∈ Finset.univ
hb : b ≠ j
⊢ ¬j = b
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 y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l : J
a : j ⟶ l
b : k ⟶ l
x₃ y₃ : ↑(F.obj l)
h₃ : x₃ = (ConcreteCategory.hom (F.map a)) x₁
h₄ : x₃ = (ConcreteCategory.hom (F.map b)) x₂
h₅ : y₃ = (ConcreteCategory.hom (F.map a)) y₁
h₆ : y₃ = (ConcreteCategory.hom (F.map b)) y₂
⊢ x₃ ≤ y₃

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
⊢ ∑ j,
      { pt := { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd },
              π := fun j x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0,
              ι := fun j x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0, ι_π := ⋯ }.π
          j ≫
        { pt := { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd },
              π := fun j x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0,
              ι := fun j x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0, ι_π := ⋯ }.ι
          j =
    𝟙
      { pt := { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd },
          π := fun j x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0,
          ι := fun j x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0, ι_π := ⋯ }.pt

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
D : Type u_1
inst✝¹ : Category.{v₁, u_1} D
inst✝ : Preadditive D
M : Mat_ C
⊢ (𝟭 C).mapMat_.obj M = (𝟭 (Mat_ C)).obj M

Tactic:
by

Goal state after:
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 y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l : J
a : j ⟶ l
b : k ⟶ l
x₃ y₃ : ↑(F.obj l)
h₃ : x₃ = (ConcreteCategory.hom (F.map a)) x₁
h₄ : x₃ = (ConcreteCategory.hom (F.map b)) x₂
h₅ : y₃ = (ConcreteCategory.hom (F.map a)) y₁
h₆ : y₃ = (ConcreteCategory.hom (F.map b)) y₂
⊢ y₃ ≤ x₃

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
D : Type u_1
inst✝¹ : Category.{v₁, u_1} D
inst✝ : Preadditive D
M N : Mat_ C
f : M ⟶ N
⊢ (𝟭 C).mapMat_.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (𝟭 (Mat_ C)).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: 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
M : Mat_ C
⊢ (F ⋙ G).mapMat_.obj M = (F.mapMat_ ⋙ G.mapMat_).obj M

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: 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
M N : Mat_ C
f : M ⟶ N
⊢ (F ⋙ G).mapMat_.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (F.mapMat_ ⋙ G.mapMat_).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

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

Tactic:
by

Goal state after:
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✝
⊢ (fun x x_1 ↦ x✝¹ ≫ x✝) = (fun x x_1 ↦ x✝¹) ≫ fun x x_1 ↦ x✝

Tactic:
by

Goal state after:
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
⊢ ∀ (a b : CoconePt hc),
    (∃ j x' y',
        ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = a) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = b), x' ≤ y') →
      (∃ j x' y',
          ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = b) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = a), x' ≤ y') →
        a = b

Tactic:
by

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
f : J ⟶ c.pt
j : ↑J.obj → A
g : (x : ↑J.obj) → (fun X ↦ X) ((F ⋙ forget (CardinalDirectedPoset κ)).obj (j x))
hg :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
      (ConcreteCategory.hom f) x
m : A := IsCardinalFiltered.max j hJ
φ : ↑J.obj → ↑(F.obj m).obj := fun x ↦ (ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x)
x : ↑J.obj
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom (c.ι.app m)) (φ x)

Tactic:
by

Goal state after:
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
j : J
x y : ↑(F.1 j)
h : (ConcreteCategory.hom (c.ι.app j)) x = (ConcreteCategory.hom (c.ι.app j)) y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

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

Tactic:
by

Goal state after: