mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
⊢ 𝟙 (φ.obj c) ∈ (map φ hφ S).arrows (φ.obj c) (φ.obj c)

Tactic:
change Map.Arrows φ hφ S _ _ (𝟙 _)

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
⊢ Map.Arrows φ hφ S (φ.obj c) (φ.obj c) (𝟙 (φ.obj c))
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ (∀ (c d : C), (S.arrows c d).Nonempty → c = d) → S.IsTotallyDisconnected

Tactic:
rintro h ⟨c, hc⟩ ⟨d, hd⟩ ⟨f, fS⟩
    simp only [Subtype.mk_eq_mk]
    exact h c d ⟨f, fS⟩

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
A B K L X Y : C
f : A ⟶ B
i : IsInitial K
t : IsTerminal Y
⊢ HasLiftingProperty f ((ihom L).map (t.from X)) ↔ HasLiftingProperty f (t.from (L ⟹ X))

Tactic:
exact HasLiftingProperty.iff_of_arrow_iso_right f
    (Arrow.isoMk' _ _ (Iso.refl _) ((IsTerminal.isTerminalObj (ihom L) _ t).uniqueUpToIso t)
      (t.hom_ext _ _))

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
m : T ⟶ (pullbackCone f g pb).pt
i : T.I
⊢ ((fun s ↦
              { f := fun i ↦ ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩,
                φ := fun i ↦ (hpb ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).lift (PullbackCone.mk ((↑s).1.φ i) ((↑s).2.φ i) ⋯) })
            ((fun m ↦ ⟨(m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd), ⋯⟩) m)).φ
        i ≫
      eqToHom ⋯ =
    m.φ i

Tactic:
by
    simp only [eqToHom_refl, Category.comp_id]
    exact (hpb _).hom_ext ((pb _).equalizer_ext (by aesop) (by aesop))

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₁ = g₁

Tactic:
← w₁,

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₁ = φ₁₂ ≫ h₁₂.p₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
⊢ ∀ {X Y : WithTerminal J} (f : X ⟶ Y),
    (WithTerminal.liftFromOver.obj c).map f ≫
        (WithTerminal.casesOn Y (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom =
      (WithTerminal.casesOn X (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom ≫
        (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map f

Tactic:
by
          rintro (i | _) (j | _) <;> (try rintro ⟨⟩) <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
f : c'.pt ⟶ P
X X' : J
g : X ⟶ X'
⊢ (ConcreteCategory.hom (P.map (F.map g))) (shrinkYonedaEquiv (c'.ι.app (op X) ≫ f)) =
    (ConcreteCategory.hom ((c'.ι.app (op X) ≫ f).app (op (unop (F.1 X')))))
      (shrinkYonedaEquiv (shrinkYoneda.{w, v, u}.map (F.map g).unop))

Tactic:
shrinkYonedaEquiv_shrinkYoneda_map

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
f : c'.pt ⟶ P
X X' : J
g : X ⟶ X'
⊢ (ConcreteCategory.hom (P.map (F.map g))) (shrinkYonedaEquiv (c'.ι.app (op X) ≫ f)) =
    (ConcreteCategory.hom ((c'.ι.app (op X) ≫ f).app (op (unop (F.1 X')))))
      (shrinkYonedaObjObjEquiv.symm (F.map g).unop)
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
s : ↑(F ⋙ P).sections
j₁ j₂ : Jᵒᵖ
f : j₁ ⟶ j₂
⊢ (F.leftOp ⋙ shrinkYoneda.{w, v, u}).map f ≫ shrinkYonedaEquiv.symm (↑s (unop j₂)) =
    shrinkYonedaEquiv.symm (↑s (unop j₁)) ≫ ((Functor.const Jᵒᵖ).obj P).map f

Tactic:
rw [← s.property f.unop]
        dsimp
        rw [shrinkYonedaEquiv_symm_map, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_empty
⊢ ∀ {C : PEmpty.{w + 1} → Type u₁} {D : PEmpty.{w + 1} → Type u₂}
    [inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)] [inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)]
    (L : (j : PEmpty.{w + 1}) → C j ⥤ D j) (W : (j : PEmpty.{w + 1}) → MorphismProperty (C j))
    [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities] [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
intro C

Goal state after:
case h_empty
C : PEmpty.{w + 1} → Type u₁
⊢ ∀ {D : PEmpty.{w + 1} → Type u₂} [inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)] (L : (j : PEmpty.{w + 1}) → C j ⥤ D j)
    (W : (j : PEmpty.{w + 1}) → MorphismProperty (C j)) [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities]
    [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A' : C
⊢ ∀ {X : C} {Y : Over I} (f : A' ⟶ X) (g : X ⟶ (sections I).obj Y),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm (f ≫ g) =
      (toOver I).map f ≫ { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm g

Tactic:
A

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A' A : C
⊢ ∀ {Y : Over I} (f : A' ⟶ A) (g : A ⟶ (sections I).obj Y),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm (f ≫ g) =
      (toOver I).map f ≫ { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm g
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
x y : D
f : x ⟶ y
⊢ 𝟙_ C ⊴ₗ f = ((λₗ x).hom ≫ f) ≫ (λₗ y).inv

Tactic:
actionUnitIso_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
x y : D
f : x ⟶ y
⊢ 𝟙_ C ⊴ₗ f = (𝟙_ C ⊴ₗ f ≫ (λₗ y).hom) ≫ (λₗ y).inv
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
d d' : D
f : d ⟶ d'
⊢ (λₗ d).hom ≫ f = 𝟙_ C ⊴ₗ f ≫ (λₗ d').hom

Tactic:
actionUnitIso_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
d d' : D
f : d ⟶ d'
⊢ 𝟙_ C ⊴ₗ f ≫ (λₗ d').hom = 𝟙_ C ⊴ₗ f ≫ (λₗ d').hom
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
x y : D
f : x ⟶ y
⊢ f ⊵ᵣ 𝟙_ C = ((ρᵣ x).hom ≫ f) ≫ (ρᵣ y).inv

Tactic:
actionUnitIso_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
x y : D
f : x ⟶ y
⊢ f ⊵ᵣ 𝟙_ C = (f ⊵ᵣ 𝟙_ C ≫ (ρᵣ y).hom) ≫ (ρᵣ y).inv
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
f : d ⟶ d'
⊢ (ρᵣ d).hom ≫ f = f ⊵ᵣ 𝟙_ C ≫ (ρᵣ d').hom

Tactic:
actionUnitIso_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
f : d ⟶ d'
⊢ f ⊵ᵣ 𝟙_ C ≫ (ρᵣ d').hom = f ⊵ᵣ 𝟙_ C ≫ (ρᵣ d').hom
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ F₂.map k₁.hom ≫ curry (f.app k₁.right) ≫ (ihom (F₁.obj k₁.right)).map (F₃.map (Under.Hom.right φ)) =
    F₂.map k₂.hom ≫ curry (f.app k₂.right) ≫ (pre (F₁.map (Under.Hom.right φ))).app (F₃.obj k₂.right)

Tactic:
← curry_natural_left_assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right) ≫ (ihom (F₁.obj k₁.right)).map (F₃.map (Under.Hom.right φ)) =
    F₂.map k₂.hom ≫ curry (f.app k₂.right) ≫ (pre (F₁.map (Under.Hom.right φ))).app (F₃.obj k₂.right)
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right) ≫ (ihom (F₁.obj k₁.right)).map (F₃.map (Under.Hom.right φ)) =
    F₂.map k₂.hom ≫ curry (f.app k₂.right) ≫ (pre (F₁.map (Under.Hom.right φ))).app (F₃.obj k₂.right)

Tactic:
← curry_natural_left_assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right) ≫ (ihom (F₁.obj k₁.right)).map (F₃.map (Under.Hom.right φ)) =
    curry (F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right) ≫ (pre (F₁.map (Under.Hom.right φ))).app (F₃.obj k₂.right)
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✝ : MonoidalClosed C
B : Subterminals C
⊢ ∀ (A : C), (subterminalInclusion C).essImage (A ⟹ (subterminalInclusion C).obj B)

Tactic:
A

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✝ : MonoidalClosed C
B : Subterminals C
A : C
⊢ (subterminalInclusion C).essImage (A ⟹ (subterminalInclusion C).obj B)
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✝¹ : MonoidalClosed C
inst✝ : Reflective i
h : (A : C) → i ⋙ ihom A ⋙ reflector i ⋙ i ≅ i ⋙ ihom A
B : D
⊢ ∀ (A : C), i.essImage (A ⟹ i.obj B)

Tactic:
A

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✝¹ : MonoidalClosed C
inst✝ : Reflective i
h : (A : C) → i ⋙ ihom A ⋙ reflector i ⋙ i ≅ i ⋙ ihom A
B : D
A : C
⊢ i.essImage (A ⟹ i.obj B)
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), i.essImage (A ⟹ i.obj B)

Tactic:
A

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
⊢ i.essImage (A ⟹ i.obj B)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom ≫ A ◁ ε ▷ A

pp: case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (λ_ A).hom

pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ A

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).hom

pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ 𝒮 ▷ A

Tactic:
simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.braiding_naturality_right]
    simp only [whiskerLeft_comp]

Goal state after:
case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ ε ≫ A ◁ (β_ A (𝟙_ C)).hom

case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (λ_ A).hom

case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ A

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).hom

case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ 𝒮 ▷ A
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
F G : C ⥤ V
inst✝⁹ : DayConvolution F G
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
⊢ map (map f g) h ≫ (associator F' G' H').hom = (associator F G H).hom ≫ map f (map g h)

Tactic:
apply (corepresentableBy₂' F G H) |>.homEquiv.injective

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
F G : C ⥤ V
inst✝⁹ : DayConvolution F G
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
⊢ (corepresentableBy₂' F G H).homEquiv (map (map f g) h ≫ (associator F' G' H').hom) =
    (corepresentableBy₂' F G H).homEquiv ((associator F G H).hom ≫ map f (map g h))
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✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
x y : D
fst✝ snd✝ : C
⊢ (unit ((ι C V D).obj x) ((ι C V D).obj y)).app (fst✝, snd✝) =
    (unit ((ι C V D).obj x) ((ι C V D).obj y)).app (fst✝, snd✝) ≫ 𝟙 (((ι C V D).obj (x ⊗ y)).obj (fst✝ ⊗ snd✝))

Tactic:
dsimp [DayConvolution.convolution]

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✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
x y : D
fst✝ snd✝ : C
⊢ (unit ((ι C V D).obj x) ((ι C V D).obj y)).app (fst✝, snd✝) =
    (unit ((ι C V D).obj x) ((ι C V D).obj y)).app (fst✝, snd✝) ≫ 𝟙 (((ι C V D).obj (x ⊗ y)).obj (fst✝ ⊗ snd✝))
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✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

Tactic:
obtain (h | h) := subsingleton_or_nontrivial (X ⟶ Y)

Goal state after:
case inl
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✝¹ : Simple X
inst✝ : Simple Y
h : Subsingleton (X ⟶ Y)
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

case inr
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✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1
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 : J
x' : (F ⋙ forget PartOrdEmb).obj j
hx : (ConcreteCategory.hom (c.ι.app j)) x' = x
⊢ ∃ j x' y', ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = x) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = x), x' ≤ y'

Tactic:
exact ⟨j, x', x', hx, hx, le_rfl⟩

Goal state after: