mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case mpr
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
⊢ z₁ = z₂ → ∀ (x : ι → R), (∏ i, x i) • z₁ = (∏ i, x i) • z₂

Tactic:
intro h

Goal state after:
case mpr
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
h : z₁ = z₂
⊢ ∀ (x : ι → R), (∏ i, x i) • z₁ = (∏ i, x i) • z₂
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c✝ : Cone F
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c✝.π.app j)) x = s j
this : ∀ (c : Cone F) (y : c.pt), ∃! x, ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j
x : (c : Cone F) → c.pt → c✝.pt
hx :
  ∀ (c : Cone F) (y : c.pt),
    (fun x ↦ ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j) (x c y) ∧
      ∀ (y_1 : c✝.pt), (fun x ↦ ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j) y_1 → y_1 = x c y
c : Cone F
j : J
⊢ ↾x c ≫ c✝.π.app j = c.π.app j

Tactic:
by ext y; exact (hx c y).1 j

Goal state after:
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
t : Cocone F
j : J
x : ↑(F.obj j)
⊢ (Hom.hom
        ((colimitCocone F).ι.app j ≫
          ofHom
            (let __src := descAddMonoidHom t;
            { toFun := (↑__src).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })))
      x =
    (Hom.hom (t.ι.app j)) x

Tactic:
exact descAddMonoidHom_quotMk t x

Goal state after:
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ RingCat
x✝² x✝¹ : J
f : x✝² ⟶ x✝¹
x✝ : ↑(F.obj x✝²)
⊢ (Hom.hom
        (F.map f ≫
          ofHom
            (SemiRingCat.Hom.hom
              ((SemiRingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ RingCat SemiRingCat)).ι.app x✝¹))))
      x✝ =
    (Hom.hom
        (ofHom
            (SemiRingCat.Hom.hom
              ((SemiRingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ RingCat SemiRingCat)).ι.app x✝²)) ≫
          ((Functor.const J).obj (colimit F)).map f))
      x✝

Tactic:
simpa using! (Types.TypeMax.colimitCocone (F ⋙ forget RingCat)).ι.naturality_apply f _

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

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F : C × D ⥤ E
X₁ : C
X₂ : D
Y₁ : C
Y₂ : D
f₁ : (X₁, X₂).1 ⟶ (Y₁, Y₂).1
f₂ : (X₁, X₂).2 ⟶ (Y₁, Y₂).2
⊢ ((curry ⋙ uncurry).obj F).map (f₁, f₂) ≫ (Iso.refl (((curry ⋙ uncurry).obj F).obj (Y₁, Y₂))).hom =
    (Iso.refl (((curry ⋙ uncurry).obj F).obj (X₁, X₂))).hom ≫ ((𝟭 (C × D ⥤ E)).obj F).map (f₁, f₂)

Tactic:
dsimp at f₁ f₂ ⊢

Goal state after:
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F : C × D ⥤ E
X₁ : C
X₂ : D
Y₁ : C
Y₂ : D
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
⊢ (F.map (f₁ ×ₘ 𝟙 X₂) ≫ F.map (𝟙 Y₁ ×ₘ f₂)) ≫ 𝟙 (F.obj (Y₁, Y₂)) = 𝟙 (F.obj (X₁, X₂)) ≫ F.map (f₁, f₂)
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ Type u_1
inst✝ : F.IsCorepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max u_1 v, u, max (u_1 + 1) (v + 1)}
    (uliftCoyoneda.{u_1, v, u}.obj (op (F ⋙ uliftFunctor.{v, u_1}).coreprX))

Tactic:
exact inferInstanceAs <| PreservesLimitsOfSize (coyoneda.obj _ ⋙ uliftFunctor)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z X' : C
f : X ⟶ X'
⊢ (f ⊗ₘ 𝟙 Y ⊗ₘ 𝟙 Z) ≫ (α_ X' Y Z).inv = (α_ X Y Z).inv ≫ ((f ⊗ₘ 𝟙 Y) ⊗ₘ 𝟙 Z)

Tactic:
associator_inv_naturality

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z X' : C
f : X ⟶ X'
⊢ (α_ X Y Z).inv ≫ ((f ⊗ₘ 𝟙 Y) ⊗ₘ 𝟙 Z) = (α_ X Y Z).inv ≫ ((f ⊗ₘ 𝟙 Y) ⊗ₘ 𝟙 Z)
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_2
inst✝¹ : Category.{v_2, u_2} C
inst✝ : MonoidalCategory C
F G F' G' : J ⥤ C
α : F ⟶ F'
β : G ⟶ G'
X Y : J
f : X ⟶ Y
X' : J
⊢ F.map f ▷ G.obj X' ≫ (α.app Y ⊗ₘ β.app X') = (α.app X ⊗ₘ β.app X') ≫ F'.map f ▷ G'.obj X'

Tactic:
simpa using tensor_naturality α β f (𝟙 X')

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: case mp
R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
⊢ Linear R F → ∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)

Tactic:
intro h

Goal state after:
case mp
R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
h : Linear R F
⊢ ∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
⊢ (∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)) → Linear R F

Tactic:
refine fun h => ⟨fun {X Y} f r => ?_⟩
    have : r • f = (r • 𝟙 X) ≫ f := by simp
    rw [this, F.map_comp, h, Linear.smul_comp, Category.id_comp]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ F.map (X ◁ (r • f)) = F.map (r • X ◁ f)

Tactic:
rw [Functor.Monoidal.map_whiskerLeft]

Goal state after:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ Functor.OplaxMonoidal.δ F X Y ≫ F.obj X ◁ F.map (r • f) ≫ Functor.LaxMonoidal.μ F X Z = F.map (r • X ◁ f)
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : C ⥤ D
⊢ G.map c.fst ≫ G.map f = G.map c.snd ≫ G.map g

Tactic:
by simpa using G.congr_map c.condition

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : C ⥤ D
⊢ G.map f ≫ G.map c.inl = G.map g ≫ G.map c.inr

Tactic:
by simpa using G.congr_map c.condition

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.surjective C f
hg : MorphismProperty.surjective C g
⊢ MorphismProperty.surjective C (f ≫ g)

Tactic:
by
    delta MorphismProperty.surjective
    rw [hom_comp]
    exact hg.comp hf

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
⊢ MorphismProperty.surjective C = epimorphisms C → (forget C).PreservesEpimorphisms

Tactic:
intro h

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
⊢ (forget C).PreservesEpimorphisms
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
⊢ MorphismProperty.injective C = monomorphisms C → (forget C).PreservesMonomorphisms

Tactic:
intro h

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.injective C = monomorphisms C
⊢ (forget C).PreservesMonomorphisms
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
⊢ MorphismProperty.injective C = monomorphisms C ↔ (forget C).PreservesMonomorphisms

Tactic:
constructor
  · intro h
    constructor
    rintro _ _ f (hf : monomorphisms C f)
    rw [mono_iff_injective]
    rw [← h] at hf
    exact hf
  · intro
    apply le_antisymm (injective_le_monomorphisms C)
    intro _ _ f hf
    have : Mono f := hf
    change Function.Injective ((forget C).map f)
    rw [← mono_iff_injective]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsColimit c → IsLimit c.op

Tactic:
intro h

Goal state after:
case f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
h : IsColimit c
⊢ IsLimit c.op
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsLimit c.op → IsColimit c

Tactic:
intro h

Goal state after:
case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
h : IsLimit c.op
⊢ IsColimit c
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsColimit c → IsLimit c.unop

Tactic:
intro h

Goal state after:
case f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
h : IsColimit c
⊢ IsLimit c.unop
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsLimit c.unop → IsColimit c

Tactic:
intro h

Goal state after:
case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
h : IsLimit c.unop
⊢ IsColimit c
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (f₁ ⊗ₘ g₁ ⊗ₘ f₂ ⊗ₘ g₂) ≫ (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ X₁ X₂ (U₁ ⊗ U₂)).hom

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv

pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (β_ X₂ U₁).hom ⊗ₘ 𝟙 U₂

pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (α_ U₁ X₂ U₂).hom

Tactic:
associator_inv_naturality

Goal state after:
case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ X₁ U₁ (X₂ ⊗ U₂)).inv ≫ ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂)

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ X₁ X₂ (U₁ ⊗ U₂)).hom

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv

case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (β_ X₂ U₁).hom ⊗ₘ 𝟙 U₂

case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (α_ U₁ X₂ U₂).hom
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
inst✝ : Small.{w, max u w} (Quot F)
⊢ Function.Bijective ⇑(Quot.desc F (colimitCocone F))

Tactic:
rw [Quot.desc_colimitCocone]

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
inst✝ : Small.{w, max u w} (Quot F)
⊢ Function.Bijective ⇑Shrink.addEquiv.symm.toAddMonoidHom
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ (inl r + inr (-(r •> x.snd <• r))) * x = 1

Tactic:
by
  ext <;> dsimp
  · rw [add_zero, h]
  · rw [add_zero, zero_add, smul_neg, op_smul_op_smul, h, op_one, one_smul,
      add_neg_cancel]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹³ : CommSemiring R✝
inst✝¹² : CommSemiring S
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : AddCommMonoid B
inst✝⁹ : Algebra R✝ S
inst✝⁸ : Module R✝ A
inst✝⁷ : Module S A
inst✝⁶ : Module R✝ B
inst✝⁵ : IsScalarTower R✝ S A
R : Type u_5
C : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
inst✝ : IsCocomm R C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by simp [comul_def, coassoc_simps]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: X : Type ?u.36
Y : Pointed
f : typeToPointed.obj X ⟶ Y
x : (typeToPointed.obj X).X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.point ⇑(ConcreteCategory.hom f), map_point := ⋯ })
          ((fun f ↦ ↾(f.toFun ∘ some)) f)).toFun
      x =
    f.toFun x

Tactic:
cases x

Goal state after:
case none
X : Type ?u.36
Y : Pointed
f : typeToPointed.obj X ⟶ Y
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.point ⇑(ConcreteCategory.hom f), map_point := ⋯ })
          ((fun f ↦ ↾(f.toFun ∘ some)) f)).toFun
      none =
    f.toFun none

case some
X : Type ?u.36
Y : Pointed
f : typeToPointed.obj X ⟶ Y
val✝ : X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.point ⇑(ConcreteCategory.hom f), map_point := ⋯ })
          ((fun f ↦ ↾(f.toFun ∘ some)) f)).toFun
      (some val✝) =
    f.toFun (some val✝)
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: X'✝ X✝ : Type ?u.36
Y✝ : Pointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget Pointed).obj Y✝
x : (typeToPointed.obj X'✝).X
⊢ ({ toFun := fun f ↦ ↾(f.toFun ∘ some),
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      x =
    (typeToPointed.map f ≫
          { toFun := fun f ↦ ↾(f.toFun ∘ some),
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      x

Tactic:
cases x

Goal state after:
case none
X'✝ X✝ : Type ?u.36
Y✝ : Pointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget Pointed).obj Y✝
⊢ ({ toFun := fun f ↦ ↾(f.toFun ∘ some),
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      none =
    (typeToPointed.map f ≫
          { toFun := fun f ↦ ↾(f.toFun ∘ some),
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      none

case some
X'✝ X✝ : Type ?u.36
Y✝ : Pointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget Pointed).obj Y✝
val✝ : X'✝
⊢ ({ toFun := fun f ↦ ↾(f.toFun ∘ some),
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      (some val✝) =
    (typeToPointed.map f ≫
          { toFun := fun f ↦ ↾(f.toFun ∘ some),
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      (some val✝)
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
x : (pointedToBipointedFst.obj X).X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      x =
    f.toFun x

Tactic:
cases x

Goal state after:
case none
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      none =
    f.toFun none

case some
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
val✝ : X.X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      (some val✝) =
    f.toFun (some val✝)
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
x : (pointedToBipointedFst.obj X'✝).X
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      x =
    (pointedToBipointedFst.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      x

Tactic:
cases x

Goal state after:
case none
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      none =
    (pointedToBipointedFst.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      none

case some
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
val✝ : X'✝.X
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      (some val✝) =
    (pointedToBipointedFst.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      (some val✝)
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
x : (pointedToBipointedSnd.obj X).X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      x =
    f.toFun x

Tactic:
cases x

Goal state after:
case none
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      none =
    f.toFun none

case some
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
val✝ : X.X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      (some val✝) =
    f.toFun (some val✝)