mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
W X Y Z : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (f : W ⟶ X) (g : Y ⟶ Z),
    Quotient.map₂ Hom.tensor ⋯ f g =
      Quot.map (fun f ↦ f.whiskerRight Y) ⋯ f ≫ Quot.map (fun f ↦ Hom.whiskerLeft X f) ⋯ g

Tactic:
by
    rintro ⟨f⟩ ⟨g⟩
    exact Quotient.sound (tensorHom_def _ _)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case id_whiskerRight
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝ ((Hom.id X✝).whiskerRight Y✝) = projectMapAux f✝ (Hom.id (X✝.tensor Y✝))

Tactic:
| id_whiskerRight =>

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
c₁ c₂ c₃ c₄ : C
d₁ d₂ : D
f : c₁ ⟶ c₂
g : c₃ ⟶ c₄
h : d₁ ⟶ d₂
⊢ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ (αₗ c₂ c₄ d₂).hom = (αₗ c₁ c₃ d₁).hom ≫ (f ⊙ₗₘ g ⊙ₗₘ h)

Tactic:
actionAssocIso_hom_naturality

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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
c₁ c₂ c₃ c₄ : C
d₁ d₂ : D
f : c₁ ⟶ c₂
g : c₃ ⟶ c₄
h : d₁ ⟶ d₂
⊢ (αₗ c₁ c₃ d₁).hom ≫ (f ⊙ₗₘ g ⊙ₗₘ h) = (αₗ c₁ c₃ d₁).hom ≫ (f ⊙ₗₘ g ⊙ₗₘ h)
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalRightAction C D
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
⊢ (f ⊙ᵣₘ g ⊗ₘ h) ≫ (αᵣ d₂ c₂ c₄).hom = (αᵣ d₁ c₁ c₃).hom ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h)

Tactic:
actionAssocIso_hom_naturality

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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalRightAction C D
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
⊢ (αᵣ d₁ c₁ c₃).hom ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h) = (αᵣ d₁ c₁ c₃).hom ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ R.X P.X Q.X).inv ▷ T.X ≫
      (((α_ (R.X ⊗ P.X) Q.X T.X).hom ≫ P.actLeft ▷ (Q.X ⊗ T.X)) ≫ P.X ◁ Q.actRight) ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (α_ R.X (P.X ⊗ Q.X) T.X).hom ≫
      R.X ◁ (α_ P.X Q.X T.X).hom ≫
        R.X ◁ P.X ◁ Q.actRight ≫
          (α_ R.X P.X Q.X).inv ≫
            P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

Tactic:
slice_rhs 3 4 => rw [associator_inv_naturality_right]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ R.X P.X Q.X).inv ▷ T.X ≫
      (((α_ (R.X ⊗ P.X) Q.X T.X).hom ≫ P.actLeft ▷ (Q.X ⊗ T.X)) ≫ P.X ◁ Q.actRight) ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (α_ R.X (P.X ⊗ Q.X) T.X).hom ≫
      R.X ◁ (α_ P.X Q.X T.X).hom ≫
        (((α_ R.X P.X (Q.X ⊗ T.X)).inv ≫ (R.X ⊗ P.X) ◁ Q.actRight) ≫ P.actLeft ▷ Q.X) ≫
          coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : Reflective i
⊢ IsLimit (asEmptyCone ((reflector i).obj (𝟙_ C)))

Tactic:
apply isLimitOfReflects i
         apply isLimitChangeEmptyCone _ isTerminalTensorUnit
         letI : IsIso ((reflectorAdjunction i).unit.app (𝟙_ C)) := by
           have := reflective_products i
           refine Functor.essImage.unit_isIso ⟨terminal D, ⟨PreservesTerminal.iso i |>.trans ?_⟩⟩
           exact IsLimit.conePointUniqueUpToIso (limit.isLimit _) isTerminalTensorUnit
         exact asIso ((reflectorAdjunction i).unit.app (𝟙_ C))

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : Reflective i
inst✝² : MonoidalClosed C
inst✝¹ : CartesianMonoidalCategory D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : C ⥤ D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))) ≫
        (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B))))
⊢ (ir.homEquiv (A ⊗ (A ⟹ i.obj B)) B)
      ((reflector i).map (A ◁ η.app (A ⟹ i.obj B)) ≫
        (prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
            L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))) ≫
          (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B))) =
    (ihom.ev A).app (i.obj B)

Tactic:
ir.homEquiv_apply_eq,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : Reflective i
inst✝² : MonoidalClosed C
inst✝¹ : CartesianMonoidalCategory D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : C ⥤ D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))) ≫
        (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B))))
⊢ (reflector i).map (A ◁ η.app (A ⟹ i.obj B)) ≫
      (prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))) ≫
        (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B)) =
    (ir.homEquiv (A ⊗ (A ⟹ i.obj B)) B).symm ((ihom.ev A).app (i.obj B))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalClosed V
F G✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' c'' : C
f : c' ⟶ c''
this :
  F.map f ▷ G.obj c ≫ (DayConvolution.unit F G).app (c'', c) =
    (DayConvolution.unit F G).app (c', c) ≫ (F ⊛ G).map (f ▷ c)
⊢ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c)) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (F ⊛ G)).obj c).obj (op c')).map f =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c'', c)) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (F ⊛ G)).obj c).map f.op).app c''

Tactic:
replace this := congrArg MonoidalClosed.curry this

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalClosed V
F G✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' c'' : C
f : c' ⟶ c''
this :
  MonoidalClosed.curry (F.map f ▷ G.obj c ≫ (DayConvolution.unit F G).app (c'', c)) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c) ≫ (F ⊛ G).map (f ▷ c))
⊢ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c)) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (F ⊛ G)).obj c).obj (op c')).map f =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c'', c)) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (F ⊛ G)).obj c).map f.op).app c''
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalClosed V
F G✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
j : C
this :
  F.obj j ◁ G.map f ≫ (DayConvolution.unit F G).app (j, c') = (DayConvolution.unit F G).app (j, c) ≫ (F ⊛ G).map (j ◁ f)
⊢ G.map f ≫ MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c')) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c)) ≫ (ihom (F.obj j)).map ((F ⊛ G).map (j ◁ f))

Tactic:
replace this := congrArg MonoidalClosed.curry this

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalClosed V
F G✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
j : C
this :
  MonoidalClosed.curry (F.obj j ◁ G.map f ≫ (DayConvolution.unit F G).app (j, c')) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c) ≫ (F ⊛ G).map (j ◁ f))
⊢ G.map f ≫ MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c')) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c)) ≫ (ihom (F.obj j)).map ((F ⊛ G).map (j ◁ f))
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x : ↑A
⊢ 1 * x = x

Tactic:
convert! LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (one_mul A)) ((1 : R) ⊗ₜ x)
      rw [MonoidalCategory.leftUnitor_hom_apply, one_smul]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
U : C ⥤ V
inst✝ : DayConvolutionUnit U
c : C
v : V
g h : U.obj c ⟶ v
e : ∀ (f : 𝟙_ C ⟶ c), can ≫ U.map f ≫ g = can ≫ U.map f ≫ h
j : CostructuredArrow (fromPUnit (𝟙_ C)) c
⊢ ((LeftExtension.mk U { app := fun x ↦ can, naturality := ⋯ }).coconeAt c).ι.app j ≫ g =
    ((LeftExtension.mk U { app := fun x ↦ can, naturality := ⋯ }).coconeAt c).ι.app j ≫ h

Tactic:
simpa using e j.hom

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X✝ Y✝ : C ⥤ Comon D
α : X✝ ⟶ Y✝
x : C
⊢ (α.app x).hom ≫ ε = ε

Tactic:
IsComonHom.hom_counit (α.app x).hom

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X✝ Y✝ : C ⥤ Comon D
α : X✝ ⟶ Y✝
x : C
⊢ ε = ε
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
⊢ ∀ x ∉ g ⁻¹' {h c},
    eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            ((biproduct.π (fun b ↦ s (g b)) x ≫ biproduct.ι (fun b ↦ s (g b)) x) ≫ w) ≫
              biproduct.π (fun b ↦ s (h b)) c =
      0

Tactic:
· intro b nm
    simp only [Set.mem_preimage, Set.mem_singleton_iff] at nm
    simp only [Category.assoc]
    convert! comp_zero
    convert! comp_zero
    convert! comp_zero
    convert! comp_zero
    simp only [o.eq_zero nm]

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:
cases M

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
ι✝ : Type
fintype✝ : Fintype ι✝
X✝ : ι✝ → C
⊢ (𝟭 C).mapMat_.obj { ι := ι✝, fintype := fintype✝, X := X✝ } =
    (𝟭 (Mat_ C)).obj { ι := ι✝, fintype := fintype✝, X := X✝ }
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
i✝ : ((𝟭 C).mapMat_.obj M).ι
j✝ : ((𝟭 (Mat_ C)).obj N).ι
⊢ ((𝟭 C).mapMat_.map f ≫ (eqToIso ⋯).hom) i✝ j✝ = ((eqToIso ⋯).hom ≫ (𝟭 (Mat_ C)).map f) i✝ j✝

Tactic:
cases M

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
N : Mat_ C
j✝ : ((𝟭 (Mat_ C)).obj N).ι
ι✝ : Type
fintype✝ : Fintype ι✝
X✝ : ι✝ → C
f : { ι := ι✝, fintype := fintype✝, X := X✝ } ⟶ N
i✝ : ((𝟭 C).mapMat_.obj { ι := ι✝, fintype := fintype✝, X := X✝ }).ι
⊢ ((𝟭 C).mapMat_.map f ≫ (eqToIso ⋯).hom) i✝ j✝ = ((eqToIso ⋯).hom ≫ (𝟭 (Mat_ C)).map f) i✝ j✝
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:
cases M

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: 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
i✝ : ((F ⋙ G).mapMat_.obj M).ι
j✝ : ((F.mapMat_ ⋙ G.mapMat_).obj N).ι
⊢ ((F ⋙ G).mapMat_.map f ≫ (eqToIso ⋯).hom) i✝ j✝ = ((eqToIso ⋯).hom ≫ (F.mapMat_ ⋙ G.mapMat_).map f) i✝ j✝

Tactic:
cases M

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
M : Mat_ C
⊢ ((biproduct.desc fun i x k ↦ if h : i = k then eqToHom ⋯ else 0) ≫
      biproduct.lift fun i j x ↦ if h : j = i then eqToHom ⋯ else 0) =
    𝟙 (⨁ fun i ↦ (embedding C).obj (M.X i))

Tactic:
apply biproduct.hom_ext
    intro i
    apply biproduct.hom_ext'
    intro j
    simp only [Category.id_comp, Category.assoc, biproduct.lift_π, biproduct.ι_desc_assoc,
      biproduct.ι_π]
    ext ⟨⟩ ⟨⟩
    simp only [embedding, comp_apply, comp_dite, dite_comp, comp_zero, zero_comp,
      Finset.sum_dite_eq', Finset.mem_univ, ite_true, eqToHom_refl, Category.comp_id]
    split_ifs with h
    · subst h
      simp
    · rfl

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)
j : A
f g : J ⟶ F.obj j
h : f ≫ c.ι.app j = g ≫ c.ι.app j
k : ↑J.obj → A
a : (x : ↑J.obj) → j ⟶ k x
hk :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (F.map (a x))) (f.hom.hom' x) = (ConcreteCategory.hom (F.map (a x))) (g.hom.hom' x)
⊢ ∃ l c b, ∀ (x : ↑J.obj), a x ≫ b x = c

Tactic:
let φ (x : J.obj) : j ⟶ IsCardinalFiltered.max k hJ :=
          a x ≫ IsCardinalFiltered.toMax k hJ x
        exact ⟨IsCardinalFiltered.coeq φ hJ,
          IsCardinalFiltered.toCoeq φ hJ,
          fun x ↦ IsCardinalFiltered.toMax k hJ x ≫ IsCardinalFiltered.coeqHom φ hJ,
          fun x ↦ by simpa [φ] using IsCardinalFiltered.coeq_condition φ hJ x⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
X : Type w
inst✝ : PartialOrder X
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
hm : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : SetCardinalLT κ₁ ↑B) (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC
B : Set X
hB : HasCardinalLT (↑B) κ₂
T : Type w
f : T → ↑B
hT : HasCardinalLT T κ₁
C₀ : SetCardinalLT κ₁ ↑B := ⟨Set.range f, ⋯⟩
⊢ ∃ a, ∀ (t : T), ↑(f t) ≤ ↑a

Tactic:
obtain ⟨C, hC, hC'⟩ := hY' B hB C₀

Goal state after:
κ₁ κ₂ : Cardinal.{w}
X : Type w
inst✝ : PartialOrder X
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
hm : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : SetCardinalLT κ₁ ↑B) (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC
B : Set X
hB : HasCardinalLT (↑B) κ₂
T : Type w
f : T → ↑B
hT : HasCardinalLT T κ₁
C₀ : SetCardinalLT κ₁ ↑B := ⟨Set.range f, ⋯⟩
C : SetCardinalLT κ₁ ↑B
hC : C ∈ Y B hB
hC' : C₀ ≤ C
⊢ ∃ a, ∀ (t : T), ↑(f t) ≤ ↑a
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: case refine_1
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
f : X ⟶ c.pt
j : X → J
g : (x : X) → (fun X ↦ X) (F.obj (j x))
hg : ∀ (x : X), (hom (c.ι.app (j x))) (g x) = (hom f) x
⊢ ∃ i xi, f = (hom (((coyoneda.obj (op X)).mapCocone c).ι.app i)) xi

Tactic:
refine ⟨IsCardinalFiltered.max j hX,
          ↾fun x ↦ F.map (IsCardinalFiltered.toMax j hX x) (g x), ?_⟩

Goal state after:
case refine_1
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
f : X ⟶ c.pt
j : X → J
g : (x : X) → (fun X ↦ X) (F.obj (j x))
hg : ∀ (x : X), (hom (c.ι.app (j x))) (g x) = (hom f) x
⊢ f =
    (hom (((coyoneda.obj (op X)).mapCocone c).ι.app (IsCardinalFiltered.max j hX)))
      (↾fun x ↦ (hom (F.map (IsCardinalFiltered.toMax j hX x))) (g x))
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)
φ : X → (j ⟶ IsCardinalFiltered.max k hX) := fun x ↦ a x ≫ IsCardinalFiltered.toMax k hX x
⊢ ∃ l c b, ∀ (x : ToType X), a x ≫ b x = c

Tactic:
exact ⟨IsCardinalFiltered.coeq φ hX,
            IsCardinalFiltered.toCoeq φ hX,
            fun x ↦ IsCardinalFiltered.toMax k hX x ≫ IsCardinalFiltered.coeqHom φ hX,
            fun x ↦ by simpa [φ] using IsCardinalFiltered.coeq_condition φ hX x⟩

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
⊢ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck = coherentTopology C

Tactic:
by
  ext B S
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · induction h with
    | of Y T hT =>
      apply Coverage.Saturate.of
      simp only [Coverage.sup_covering, Set.mem_union] at hT
      exact Or.elim hT
        (fun ⟨α, x, X, π, ⟨h, _⟩⟩ ↦ ⟨α, x, X, π, ⟨h, inferInstance⟩⟩)
        (fun ⟨Z, f, ⟨h, _⟩⟩ ↦ ⟨Unit, inferInstance, fun _ ↦ Z, fun _ ↦ f, ⟨h, inferInstance⟩⟩)
    | top => apply Coverage.Saturate.top
    | transitive Y T => apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]
  · induction h with
    | of Y T hT =>
      obtain ⟨I, _, X, f, rfl, hT⟩ := hT
      apply Coverage.Saturate.transitive Y (generate (Presieve.ofArrows
        (fun (_ : Unit) ↦ (∐ fun (i : I) => X i)) (fun (_ : Unit) ↦ Sigma.desc f)))
      · 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⟩⟩
      · rintro R g ⟨W, ψ, σ, ⟨⟩, rfl⟩
        change _ ∈ ((extensiveCoverage C) ⊔ (regularCoverage C)).toGrothendieck R
        rw [Sieve.pullback_comp]
        apply pullback_stable
        have : generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i) ≤
            (generate (Presieve.ofArrows X f)).pullback (Sigma.desc f) := by
          rintro Q q ⟨E, e, r, ⟨hq, rfl⟩⟩
          exact ⟨E, e, r ≫ (Sigma.desc f), by cases hq; simpa using Presieve.ofArrows.mk _, by simp⟩
        apply Coverage.saturate_of_superset _ this
        apply Coverage.Saturate.of
        refine Or.inl ⟨I, inferInstance, _, _, ⟨rfl, ?_⟩⟩
        convert! IsIso.id _
        aesop
    | top => apply Coverage.Saturate.top
    | transitive Y T => apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]

Goal state after: