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

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁶ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f f' : MultilinearMap R M₁ M₂
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
⊢ ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i →ₗ[R] M₁' i) (i : ι) (x y : M₁ i →ₗ[R] M₁' i),
    compLinearMapₗ (update m i (x + y)) = compLinearMapₗ (update m i x) + compLinearMapₗ (update m i y)

Tactic:
intro _ f i f₁ f₂
    ext g x
    change (g fun j ↦ update f i (f₁ + f₂) j <| x j) =
        (g fun j ↦ update f i f₁ j <| x j) + g fun j ↦ update f i f₂ j (x j)
    let c : Π (i : ι), (M₁ i →ₗ[R] M₁' i) → M₁' i := fun i f ↦ f (x i)
    convert! g.map_update_add (fun j ↦ f j (x j)) i (f₁ (x i)) (f₂ (x i)) with j j j
    · exact Function.apply_update c f i (f₁ + f₂) j
    · exact Function.apply_update c f i f₁ j
    · exact Function.apply_update c f i f₂ j

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Finite ι
f g : MultilinearMap R (fun x ↦ R) M₂
h : (f fun x ↦ 1) = g fun x ↦ 1
x : ι → R
val✝ : Fintype ι
hf : (f fun i ↦ x i • 1) = (∏ i, x i) • f fun x ↦ 1
hg : (g fun i ↦ x i • 1) = (∏ i, x i) • g fun x ↦ 1
⊢ f x = g x

Tactic:
simp_all

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : Small.{u, max u v} ↑F.sections
x y : (limitCone F).pt
w : (equivShrink ↑F.sections).symm x = (equivShrink ↑F.sections).symm y
⊢ x = y

Tactic:
simp_all

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : Small.{u, max u v} ↑F.sections
x y : (limitCone F).pt
w : (equivShrink ↑F.sections).symm x = (equivShrink ↑F.sections).symm y
⊢ x = y

Tactic:
by
  simp_all

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
X✝ Y✝ : J ⥤ Type (max u v)
f : X✝ ⟶ Y✝
⊢ lim.map f ≫ (limitEquivSections Y✝).toIso.hom = (limitEquivSections X✝).toIso.hom ≫ (Functor.sectionsFunctor J).map f

Tactic:
ext x; exact Subtype.ext (funext fun j ↦ congr_hom (limMap_π f j) x)

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : HasColimit F
inst✝¹ : HasColimit (F ⋙ G)
inst✝ : IsIso (colimit.post F G)
⊢ IsColimit (G.mapCocone (colimit.cocone F))

Tactic:
convert! IsColimit.ofPointIso (colimit.isColimit (F ⋙ G))

Goal state after:
case convert_2
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : HasColimit F
inst✝¹ : HasColimit (F ⋙ G)
inst✝ : IsIso (colimit.post F G)
⊢ IsIso ((colimit.isColimit (F ⋙ G)).desc (G.mapCocone (colimit.cocone F)))
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case neg.inl
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi hjs : i ∈ s
hji : ¬i < i
⊢ (if i = i then s.piecewise a v i - b i else b i) = if i = i then a i - b i else b i

Tactic:
rw [if_pos rfl, if_pos rfl, s.piecewise_eq_of_mem _ _ hi]

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 Y : C × D} (f : X ⟶ Y),
    ((curry ⋙ uncurry).obj F).map f ≫ (Iso.refl (((curry ⋙ uncurry).obj F).obj Y)).hom =
      (Iso.refl (((curry ⋙ uncurry).obj F).obj X)).hom ≫ ((𝟭 (C × D ⥤ E)).obj F).map f

Tactic:
rintro ⟨X₁, X₂⟩ ⟨Y₁, Y₂⟩ ⟨f₁, f₂⟩
      dsimp at f₁ f₂ ⊢
      simp only [← F.map_comp, prod_comp, Category.comp_id, Category.id_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁷ : Ring R
inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M'
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x✝¹ : M₂
x✝ : x✝¹ ∈ ⇑f '' {v | ∀ (i : ι), v i ∈ p i}
x : (i : ι) → M₁ i
hx : x ∈ {v | ∀ (i : ι), v i ∈ p i}
hf : f x = x✝¹
⊢ c • x✝¹ ∈ ⇑f '' {v | ∀ (i : ι), v i ∈ p i}

Tactic:
by
    let ⟨i⟩ := ‹Nonempty ι›
    let := Classical.decEq ι
    refine ⟨update x i (c • x i), fun j => if hij : j = i then ?_ else ?_, hf ▸ ?_⟩
    · rw [hij, update_self]
      exact (p i).smul_mem _ (hx i)
    · rw [update_of_ne hij]
      exact hx j
    · rw [f.map_update_smul, update_eq_self]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ Cᵒᵖ
c : Cone F
hc : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s : Cone F
j : J
⊢ (Quiver.Hom.op ((hom ((hc (unop s.pt)).lift ((yoneda.obj (unop s.pt)).mapCone s))) (𝟙 (unop s.pt))) ≫
        c.π.app j).unop =
    (s.π.app j).unop

Tactic:
simpa using congr_hom ((hc s.pt.unop).fac ((yoneda.obj s.pt.unop).mapCone s) j) (𝟙 (unop s.pt))

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
⊢ shrinkYonedaEquiv (shrinkYoneda.{w, v, u}.map f) = shrinkYonedaObjObjEquiv.symm f

Tactic:
by
  simp [shrinkYonedaEquiv, shrinkYoneda, shrinkYonedaObjObjEquiv]

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

Goal state before:
pp: case h₁
C : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C
inst✝¹⁵ : MonoidalCategory C
D : Type u₂
inst✝¹⁴ : Category.{v₂, u₂} D
inst✝¹³ : MonoidalCategory D
E : Type u₃
inst✝¹² : Category.{v₃, u₃} E
inst✝¹¹ : MonoidalCategory E
E' : Type u₄
inst✝¹⁰ : Category.{v₄, u₄} E'
inst✝⁹ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁸ : F₁.LaxMonoidal
inst✝⁷ : F₂.LaxMonoidal
inst✝⁶ : F₃.LaxMonoidal
F G : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
X Y : C
⊢ (μ (F.prod' H) X Y ≫ (prod' α β).app (X ⊗ Y)).1 = (((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y).1

Tactic:
simp only [prod_comp_fst, prod'_μ_fst, prod'_app_fst,
        prodMonoidal_tensorHom, IsMonoidal.tensor]

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

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ adj.unit.app (𝟙_ C) = adj.unit.app (𝟙_ C) ≫ 𝟙 (G.obj (F.obj (𝟙_ C)))

Tactic:
rw [comp_id]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory D := induced F fData
⊢ F.CoreMonoidal

Tactic:
exact
    { εIso := fData.εIso
      μIso := fData.μIso
      μIso_hom_natural_left := fun _ ↦ by simp [fData.whiskerRight_eq]
      μIso_hom_natural_right := fun _ ↦ by simp [fData.whiskerLeft_eq]
      associativity := fun _ _ _ ↦ by simp [fData.associator_eq]
      left_unitality := fun _ ↦ by simp [fData.leftUnitor_eq]
      right_unitality := fun _ ↦ by simp [fData.rightUnitor_eq] }

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)
left_unitality : ∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
right_unitality : ∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
X : C
⊢ (ρ_ (F.obj X)).hom = F.obj X ◁ ε ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom

Tactic:
by
    simp_rw [← id_tensorHom, right_unitality]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf : C
η : f ≅ g
θ : g ≅ h
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
η_h : p ⊗ h ≅ pf
ih_η : p ◁ η ≪≫ η_g = η_f
ih_θ : p ◁ θ ≪≫ η_h = η_g
⊢ p ◁ (η ≪≫ θ) ≪≫ η_h = η_f

Tactic:
simp_all

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf : C
η : f ≅ g
θ : g ≅ h
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
η_h : p ⊗ h ≅ pf
ih_η : p ◁ η ≪≫ η_g = η_f
ih_θ : p ◁ θ ≪≫ η_h = η_g
⊢ p ◁ (η ≪≫ θ) ≪≫ η_h = η_f

Tactic:
by
  simp_all

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i j : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
ηs₁ : h ⊗ j ⟶ i ⊗ j
η₁ : g ⊗ j ⟶ h ⊗ j
η₂ : g ⊗ j ⟶ i ⊗ j
η₃ : f ⊗ j ⟶ i ⊗ j
e_ηs₁ : ηs ▷ j = ηs₁
e_η₁ : η ▷ j = η₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (α ▷ᵢ j).hom ≫ η₂ = η₃
⊢ (α.hom ≫ η ≫ ηs) ▷ j = η₃

Tactic:
simp_all

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i j : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
ηs₁ : h ⊗ j ⟶ i ⊗ j
η₁ : g ⊗ j ⟶ h ⊗ j
η₂ : g ⊗ j ⟶ i ⊗ j
η₃ : f ⊗ j ⟶ i ⊗ j
e_ηs₁ : ηs ▷ j = ηs₁
e_η₁ : η ▷ j = η₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (α ▷ᵢ j).hom ≫ η₂ = η₃
⊢ (α.hom ≫ η ≫ ηs) ▷ j = η₃

Tactic:
by
  simp_all

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X : C
⊢ (ρ_ (F.obj X)).hom = F.obj X ◁ εIso.hom ≫ (μIso X (𝟙_ C)).hom ≫ F.map (ρ_ X).hom

Tactic:
rw [← cancel_mono (ρ_ (F.obj X)).inv, Iso.hom_inv_id, oplax_right_unitality]
    simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g h i : C
α : f' ≅ g
η : g ⟶ h
ηs : h ⟶ i
ηs₁ : h ⊗ f ⟶ i ⊗ f
η₁ : g ⊗ f ⟶ h ⊗ f
η₂ : g ⊗ f ⟶ i ⊗ f
η₃ : f' ⊗ f ⟶ i ⊗ f
e_ηs₁ : ηs ▷ f = ηs₁
e_η₁ : η ▷ f = η₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (α ▷ᵢ f).hom ≫ η₂ = η₃
⊢ (α.hom ≫ η ≫ ηs) ▷ f = η₃

Tactic:
simp_all

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (h.μIso X✝ x✝).inv ≫ F.map x✝¹ ▷ F.obj x✝ = F.map (x✝¹ ▷ x✝) ≫ (h.μIso Y✝ x✝).inv

Tactic:
← cancel_epi (h.μIso _ _).hom,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (h.μIso X✝ x✝).hom ≫ (h.μIso X✝ x✝).inv ≫ F.map x✝¹ ▷ F.obj x✝ =
    (h.μIso X✝ x✝).hom ≫ F.map (x✝¹ ▷ x✝) ≫ (h.μIso Y✝ x✝).inv
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g h i : C
α : f' ≅ g
η : g ⟶ h
ηs : h ⟶ i
ηs₁ : h ⊗ f ⟶ i ⊗ f
η₁ : g ⊗ f ⟶ h ⊗ f
η₂ : g ⊗ f ⟶ i ⊗ f
η₃ : f' ⊗ f ⟶ i ⊗ f
e_ηs₁ : ηs ▷ f = ηs₁
e_η₁ : η ▷ f = η₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (α ▷ᵢ f).hom ≫ η₂ = η₃
⊢ (α.hom ≫ η ≫ ηs) ▷ f = η₃

Tactic:
by
  simp_all

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h i : C
η : f ⟶ g
ηs : f' ⟶ g'
θ : h ⟶ i
ηθ : f' ⊗ h ⟶ g' ⊗ i
η₁ : f ⊗ f' ⊗ h ⟶ g ⊗ g' ⊗ i
ηθ₁ : f ⊗ f' ⊗ h ⟶ (g ⊗ g') ⊗ i
ηθ₂ : (f ⊗ f') ⊗ h ⟶ (g ⊗ g') ⊗ i
e_ηθ : ηs ⊗ₘ θ = ηθ
e_η₁ : (Iso.refl f).hom ≫ η ≫ (Iso.refl g).hom ⊗ₘ ηθ = η₁
e_ηθ₁ : η₁ ≫ (α_ g g' i).inv = ηθ₁
e_ηθ₂ : (α_ f f' h).hom ≫ ηθ₁ = ηθ₂
⊢ (η ⊗ₘ ηs) ⊗ₘ θ = ηθ₂

Tactic:
simp_all

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h i : C
η : f ⟶ g
ηs : f' ⟶ g'
θ : h ⟶ i
ηθ : f' ⊗ h ⟶ g' ⊗ i
η₁ : f ⊗ f' ⊗ h ⟶ g ⊗ g' ⊗ i
ηθ₁ : f ⊗ f' ⊗ h ⟶ (g ⊗ g') ⊗ i
ηθ₂ : (f ⊗ f') ⊗ h ⟶ (g ⊗ g') ⊗ i
e_ηθ : ηs ⊗ₘ θ = ηθ
e_η₁ : (Iso.refl f).hom ≫ η ≫ (Iso.refl g).hom ⊗ₘ ηθ = η₁
e_ηθ₁ : η₁ ≫ (α_ g g' i).inv = ηθ₁
e_ηθ₂ : (α_ f f' h).hom ≫ ηθ₁ = ηθ₂
⊢ (η ⊗ₘ ηs) ⊗ₘ θ = ηθ₂

Tactic:
by
  simp_all

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (h.μIso x✝¹ X✝).inv ≫ F.obj x✝¹ ◁ F.map x✝ = F.map (x✝¹ ◁ x✝) ≫ (h.μIso x✝¹ Y✝).inv

Tactic:
← cancel_epi (h.μIso _ _).hom,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (h.μIso x✝¹ X✝).hom ≫ (h.μIso x✝¹ X✝).inv ≫ F.obj x✝¹ ◁ F.map x✝ =
    (h.μIso x✝¹ X✝).hom ≫ F.map (x✝¹ ◁ x✝) ≫ (h.μIso x✝¹ Y✝).inv
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C
⊢ μ (F.prod' G) x✝¹ x✝ ≫ δ (F.prod' G) x✝¹ x✝ = 𝟙 ((F.prod' G).obj x✝¹ ⊗ (F.prod' G).obj x✝)

Tactic:
by
    ext
    · simp only [CategoryTheory.prod_comp_fst, prod'_μ_fst, prod'_δ_fst, μ_δ,
        prod'_obj, prodMonoidal_tensorObj, prod_id]
    · simp only [CategoryTheory.prod_comp_snd, prod'_μ_snd, prod'_δ_snd, μ_δ,
        prod'_obj, prodMonoidal_tensorObj, prod_id]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
⊢ F₁.map e.inv ≫ app X = app Y ≫ F₂.map e.inv

Tactic:
rw [← cancel_epi (F₁.map e.hom)]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
⊢ F₁.map e.hom ≫ F₁.map e.inv ≫ app X = F₁.map e.hom ≫ app Y ≫ F₂.map e.inv
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case comp_of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
g✝ : Y✝ ⟶ Z✝
x✝ y✝ z✝ : C
f' : x✝ ⟶ y✝
g : y✝ ⟶ z✝
hf' : W.multiplicativeClosure f'
hg : W g
h_rec : ∀ (f : X✝ ⟶ x✝), W.multiplicativeClosure f → W.multiplicativeClosure (f ≫ f')
f : X✝ ⟶ x✝
hf : W.multiplicativeClosure f
⊢ W.multiplicativeClosure ((f ≫ f') ≫ g)

Tactic:
exact .comp_of (f ≫ f') g (h_rec f hf) hg

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ (adj.homEquiv (G.obj X ⊗ 𝟙_ C) X).symm (ρ_ (G.obj X)).hom =
    (adj.homEquiv (G.obj X ⊗ 𝟙_ C) X).symm
      (G.obj X ◁ (adj.homEquiv (𝟙_ C) (𝟙_ D)) (η F) ≫
        (adj.homEquiv (G.obj X ⊗ G.obj (𝟙_ D)) (X ⊗ 𝟙_ D))
            (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D))) ≫
          G.map (ρ_ X).hom)

Tactic:
by
    rw [homEquiv_counit, homEquiv_unit, MonoidalCategory.whiskerLeft_comp, homEquiv_unit,
      homEquiv_counit, map_comp, map_comp, map_comp, map_comp, map_comp, map_comp,
      assoc, assoc, assoc, assoc, assoc, counit_naturality, counit_naturality_assoc,
      counit_naturality_assoc, left_triangle_components_assoc, ← δ_natural_right_assoc,
      ← δ_natural_right_assoc, tensorHom_def, assoc, ← whisker_exchange_assoc,
      ← MonoidalCategory.whiskerLeft_comp_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
      assoc, counit_naturality, left_triangle_components_assoc, MonoidalCategory.whiskerRight_id,
      assoc, assoc, Iso.inv_hom_id, comp_id, right_unitality_hom_assoc]

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

Goal state before:
pp: case mpr
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
a✝ : (forget C).PreservesMonomorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
this : Mono f
⊢ MorphismProperty.injective C f

Tactic:
change Function.Injective ((forget C).map f)

Goal state after:
case mpr
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
a✝ : (forget C).PreservesMonomorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
this : Mono f
⊢ Function.Injective ⇑(hom ((forget C).map f))
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ HasPullback f.op g.op ↔ HasPushout f g

Tactic:
HasPullback,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ HasLimit (cospan f.op g.op) ↔ HasPushout f g
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
⊢ HasPullback f.unop g.unop ↔ HasPushout f g

Tactic:
HasPullback,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
⊢ HasLimit (cospan f.unop g.unop) ↔ HasPushout f g
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
f : A →ₗc[R] B
f' : A → B
h : f' = ⇑f
x✝ : A
⊢ (counit ∘ₗ (↑f).copy f' h) x✝ = counit x✝

Tactic:
simp_all

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

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
i : ι
⊢ comul ∘ₗ lapply i = TensorProduct.map (lapply i) (lapply i) ∘ₗ comul

Tactic:
ext j; have := eq_or_ne i j
  aesop (add simp [TensorProduct.map_map, proj_comp_single, diag])

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Semiring B
inst✝⁹ : Semiring C
inst✝⁸ : Semiring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
toCoalgHom✝¹ : A →ₗc[R] B
map_one'✝¹ : toCoalgHom✝¹.toFun 1 = 1
map_mul'✝¹ : ∀ (x y : A), toCoalgHom✝¹.toFun (x * y) = toCoalgHom✝¹.toFun x * toCoalgHom✝¹.toFun y
toCoalgHom✝ : A →ₗc[R] B
map_one'✝ : toCoalgHom✝.toFun 1 = 1
map_mul'✝ : ∀ (x y : A), toCoalgHom✝.toFun (x * y) = toCoalgHom✝.toFun x * toCoalgHom✝.toFun y
h :
  (fun f ↦ f.toFun) { toCoalgHom := toCoalgHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toCoalgHom := toCoalgHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toCoalgHom := toCoalgHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toCoalgHom := toCoalgHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Semiring B
inst✝⁹ : Semiring C
inst✝⁸ : Semiring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
φ f : A →ₐc[R] B
f' : A → B
h : f' = ⇑f
⊢ ((↑f).copy f' h).toFun 1 = 1

Tactic:
simp_all

Goal state after: