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✝¹³ : Semiring R
inst✝¹² : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹¹ : (i : ι) → Module R (M₁ i)
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R M₂
inst✝⁸ : Semiring S
inst✝⁷ : Module S M₂
inst✝⁶ : SMulCommClass R S M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module S M₃
inst✝³ : Module R M₃
inst✝² : SMulCommClass R S M₃
inst✝¹ : LinearMap.CompatibleSMul M₂ M₃ S R
inst✝ : LinearMap.CompatibleSMul M₃ M₂ S R
g : M₂ ≃ₗ[R] M₃
x✝ : MultilinearMap R M₁ M₂
⊢ (LinearMap.compMultilinearMapₗ S ↑g.symm) ((LinearMap.compMultilinearMapₗ S ↑g).toFun x✝) = x✝

Tactic:
ext; simp

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✝¹³ : Semiring R
inst✝¹² : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹¹ : (i : ι) → Module R (M₁ i)
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R M₂
inst✝⁸ : Semiring S
inst✝⁷ : Module S M₂
inst✝⁶ : SMulCommClass R S M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module S M₃
inst✝³ : Module R M₃
inst✝² : SMulCommClass R S M₃
inst✝¹ : LinearMap.CompatibleSMul M₂ M₃ S R
inst✝ : LinearMap.CompatibleSMul M₃ M₂ S R
g : M₂ ≃ₗ[R] M₃
x✝ : MultilinearMap R M₁ M₃
⊢ (LinearMap.compMultilinearMapₗ S ↑g).toFun ((LinearMap.compMultilinearMapₗ S ↑g.symm) x✝) = x✝

Tactic:
ext; simp

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✝⁹ : 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)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
⊢ ∀ [inst : DecidableEq { a // ¬P a }] (m : (i : { a // ¬P a }) → M₁ ↑i) (i : { a // ¬P a }) (c : R) (x : M₁ ↑i),
    f.domDomRestrict P (update m i (c • x)) = c • f.domDomRestrict P (update m i x)

Tactic:
intro h m i c x

Goal state after:
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)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
h : DecidableEq { a // ¬P a }
m : (i : { a // ¬P a }) → M₁ ↑i
i : { a // ¬P a }
c : R
x : M₁ ↑i
⊢ f.domDomRestrict P (update m i (c • x)) = c • f.domDomRestrict P (update m i x)
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case inr
ι : Type u_3
M₁ : ι → Type u_1
α : Type u_2
inst✝¹ : DecidableEq α
s : Set ι
inst✝ : DecidableEq { x // x ∈ s }
e : α ≃ ↑s
m : α → (i : ι) → M₁ i
a : α
z : (i : ι) → M₁ i
i : ↑s
hne : a ≠ e.symm i
⊢ m (e.symm i) ↑i = update (fun j ↦ m (e.symm j) ↑j) (e a) (z ↑(e a)) i

Tactic:
update_of_ne fun h ↦ (Equiv.symm_apply_apply .. ▸ h ▸ hne) rfl

Goal state after:
case inr
ι : Type u_3
M₁ : ι → Type u_1
α : Type u_2
inst✝¹ : DecidableEq α
s : Set ι
inst✝ : DecidableEq { x // x ∈ s }
e : α ≃ ↑s
m : α → (i : ι) → M₁ i
a : α
z : (i : ι) → M₁ i
i : ↑s
hne : a ≠ e.symm i
⊢ m (e.symm i) ↑i = m (e.symm i) ↑i
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)
e : (i : ι) → M₁ i ≃ₗ[R] M₁' i
x✝ : MultilinearMap R M₁' M₂
⊢ (compLinearMapₗ fun x ↦ ↑(e x).symm) ((compLinearMapₗ fun x ↦ ↑(e x)).toFun x✝) = x✝

Tactic:
ext; simp

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✝⁸ : 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)
e : (i : ι) → M₁ i ≃ₗ[R] M₁' i
x✝ : MultilinearMap R M₁ M₂
⊢ (compLinearMapₗ fun x ↦ ↑(e x)).toFun ((compLinearMapₗ fun x ↦ ↑(e x).symm) x✝) = x✝

Tactic:
ext; simp

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

Goal state before:
pp: 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✝ : DecidableEq ι
x : (i : ι) → M₁ i
i : ι
v : M₁ i
⊢ f (update x i v) = f x - f (update x i (x i - v))

Tactic:
map_update_sub,

Goal state after:
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✝ : DecidableEq ι
x : (i : ι) → M₁ i
i : ι
v : M₁ i
⊢ f (update x i v) = f x - (f (update x i (x i)) - f (update x i v))
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
Y : D
⊢ F.map (𝟙 (X, Y)) = 𝟙 (F.obj (X, Y))

Tactic:
exact F.map_id ⟨X,Y⟩

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
F₁ F₂ : B ⥤ C ⥤ D
h : F₁.flip = F₂.flip
⊢ F₁.flip.flip = F₂

Tactic:
← flip_flip 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
F₁ F₂ : B ⥤ C ⥤ D
h : F₁.flip = F₂.flip
⊢ F₁.flip.flip = F₂.flip.flip
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
X : Cᵒᵖ
c : Cone F
hc : IsLimit c
⊢ Nonempty (IsLimit ((coyoneda.obj X).mapCone c))

Tactic:
rw [Types.isLimit_iff]
    intro s hs
    exact ⟨hc.lift (Limits.coneOfSectionCompCoyoneda F X ⟨s, hs⟩), hc.fac _,
      hc.uniq (Limits.coneOfSectionCompCoyoneda F X ⟨s, hs⟩)⟩

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone (F ⋙ forget₂ CommGrpCat GrpCat)
hc : IsLimit c
this✝² : HasLimit (F ⋙ forget₂ CommGrpCat GrpCat)
this✝¹ : Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections
this✝ : Small.{u, max u v} ↑((F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).sections
this : Small.{u, max u v} ↑((F ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget GrpCat).sections
⊢ (forget₂ CommGrpCat GrpCat).mapCone
      { pt := of (Types.Small.limitCone (F ⋙ forget CommGrpCat)).pt,
        π :=
          { app := fun j ↦ ofHom (MonCat.limitπMonoidHom (F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) j),
            naturality := ⋯ } } ≅
    c

Tactic:
apply IsLimit.uniqueUpToIso (GrpCat.limitConeIsLimit _) hc

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ L.map (section_ (h.unit.app Y)) ≫ 𝟙 (L.obj ((𝟭 C).obj Y)) = h.counit.app (L.obj Y)

Tactic:
simp only [Functor.id_obj, ← h.left_triangle_components Y,
      ← assoc, ← Functor.map_comp, IsSplitEpi.id, Functor.map_id, id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Full
inst✝ : R.Faithful
this : R.whiskerLeft h.unit ≫ (R.associator L R).inv ≫ whiskerRight h.counit R = R.rightUnitor.hom ≫ R.leftUnitor.inv
⊢ IsIso (R.whiskerLeft h.unit)

Tactic:
rw [← IsIso.eq_comp_inv] at this

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Full
inst✝ : R.Faithful
this :
  R.whiskerLeft h.unit = (R.rightUnitor.hom ≫ R.leftUnitor.inv) ≫ inv ((R.associator L R).inv ≫ whiskerRight h.counit R)
⊢ IsIso (R.whiskerLeft h.unit)
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Full
inst✝ : R.Faithful
this : whiskerRight h.unit L ≫ (L.associator R L).hom ≫ L.whiskerLeft h.counit = L.leftUnitor.hom ≫ L.rightUnitor.inv
⊢ IsIso (whiskerRight h.unit L)

Tactic:
rw [← IsIso.eq_comp_inv] at this

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Full
inst✝ : R.Faithful
this :
  whiskerRight h.unit L = (L.leftUnitor.hom ≫ L.rightUnitor.inv) ≫ inv ((L.associator R L).hom ≫ L.whiskerLeft h.counit)
⊢ IsIso (whiskerRight h.unit L)
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: 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
inst✝⁶ : Linear R F
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
inst✝⁴ : Preadditive E
inst✝³ : CategoryTheory.Linear R E
G : D ⥤ E
inst✝² : F.Full
inst✝¹ : F.EssSurj
inst✝ : Linear R (F ⋙ G)
X Y : D
f : X ⟶ Y
r : R
⊢ ∃ X' Y' eX eY f', f = eX.inv ≫ F.map f' ≫ eY.hom

Tactic:
by
    obtain ⟨f', hf'⟩ :=
      F.map_surjective ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)
    exact ⟨_, _, F.objObjPreimageIso X, F.objObjPreimageIso Y, f', by cat_disch⟩

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

Goal state before:
pp: case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
Y : C
val✝ : Fintype J
j✝ : J
⊢ ∑ x,
      ((𝟙 X ⊗ₘ biproduct.π f x) ⊗ₘ 𝟙 Y) ≫
        (biproduct.ι (fun j ↦ X ⊗ f j) x ⊗ₘ 𝟙 Y) ≫ (biproduct.π (fun j ↦ X ⊗ f j) j✝ ⊗ₘ 𝟙 Y) =
    ∑ x,
      (α_ X (⨁ f) Y).hom ≫
        (𝟙 X ⊗ₘ (biproduct.π f x ⊗ₘ 𝟙 Y) ≫ biproduct.ι (fun j ↦ f j ⊗ Y) x) ≫
          (𝟙 X ⊗ₘ biproduct.π (fun j ↦ f j ⊗ Y) j✝) ≫ (α_ X (f j✝) Y).inv

Tactic:
simp only [← comp_tensor_id, ← id_tensor_comp_assoc, Category.assoc, biproduct.ι_π, comp_dite,
    dite_comp, tensor_dite, dite_tensor]

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
Y : C
val✝ : Fintype J
j✝ : J
⊢ (∑ x, if h : x = j✝ then (𝟙 X ⊗ₘ biproduct.π f x) ≫ eqToHom ⋯ ⊗ₘ 𝟙 Y else (𝟙 X ⊗ₘ biproduct.π f x) ≫ 0 ⊗ₘ 𝟙 Y) =
    ∑ x,
      if h : x = j✝ then (α_ X (⨁ f) Y).hom ≫ (𝟙 X ⊗ₘ (biproduct.π f x ⊗ₘ 𝟙 Y) ≫ eqToHom ⋯) ≫ (α_ X (f j✝) Y).inv
      else (α_ X (⨁ f) Y).hom ≫ (𝟙 X ⊗ₘ (biproduct.π f x ⊗ₘ 𝟙 Y) ≫ 0) ≫ (α_ X (f j✝) 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
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ T ◁ 𝟙 (𝟙_ D) = 𝟙 (T ⊗ 𝟙_ D)

Tactic:
MonoidalCategory.whiskerLeft_id

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
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ 𝟙 (T ⊗ 𝟙_ D) = 𝟙 (T ⊗ 𝟙_ D)
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
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ T ◁ 𝟙 (F.obj (𝟙_ C)) = 𝟙 (T ⊗ F.obj (𝟙_ C))

Tactic:
MonoidalCategory.whiskerLeft_id

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
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ 𝟙 (T ⊗ F.obj (𝟙_ C)) = 𝟙 (T ⊗ F.obj (𝟙_ C))
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
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
T : D
⊢ T ◁ 𝟙 (F.obj X ⊗ F.obj Y) = 𝟙 (T ⊗ F.obj X ⊗ F.obj Y)

Tactic:
MonoidalCategory.whiskerLeft_id

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
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
T : D
⊢ 𝟙 (T ⊗ F.obj X ⊗ F.obj Y) = 𝟙 (T ⊗ F.obj X ⊗ F.obj Y)
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
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
T : D
⊢ T ◁ 𝟙 (F.obj (X ⊗ Y)) = 𝟙 (T ⊗ F.obj (X ⊗ Y))

Tactic:
MonoidalCategory.whiskerLeft_id

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
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
T : D
⊢ 𝟙 (T ⊗ F.obj (X ⊗ Y)) = 𝟙 (T ⊗ F.obj (X ⊗ Y))
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: case refine_1
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
⊢ inl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt).hom =
    (c.map G).inl

Tactic:
dsimp only [inl]

Goal state after:
case refine_1
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
⊢ ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).ι.app WalkingSpan.left ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt).hom =
    (c.map G).ι.app WalkingSpan.left
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
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit (G.mapCocone (PushoutCocone.mk (c.ι.app WalkingSpan.right) (c.ι.app WalkingSpan.left) ?m.112))

Tactic:
exact isColimitOfPreserves _ (PushoutCocone.flipIsColimit hc)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom

Tactic:
← cancel_mono (α_ Z Y X).inv

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ ((β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom) ≫ (α_ Z Y X).inv =
    (X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom) ≫ (α_ Z Y X).inv
Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsLimit (cospan f f) F
inst✝ : Mono (F.map f)
⊢ Mono f

Tactic:
by
  have := PullbackCone.isLimitMkIdId (F.map f)
  simp_rw [← F.map_id] at this
  apply PullbackCone.mono_of_isLimitMkIdId _ (isLimitOfIsLimitPullbackConeMap F _ this)

Goal state after:
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 ⟶ Z
g : Y ⟶ Z
⊢ HasColimit (cospan f g).leftOp ↔ HasPullback f g

Tactic:
hasColimit_leftOp_iff_hasLimit

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasLimit (cospan f g) ↔ HasPullback f g
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
this : ∀ (X Y : C), μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)
⊢ ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)) ≫ G.map (β_ X Y).hom =
    (i.inv.app X ⊗ₘ i.inv.app Y) ≫ (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X ≫ i.hom.app (Y ⊗ X)

Tactic:
← Functor.LaxBraided.braided_assoc

Goal state after:
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
this : ∀ (X Y : C), μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)
⊢ ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)) ≫ G.map (β_ X Y).hom =
    (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ F.map (β_ X Y).hom ≫ i.hom.app (Y ⊗ X)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
⊢ (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom = tensorμ (𝟙_ C) X₁ (𝟙_ C) X₂ ≫ (λ_ (𝟙_ C)).hom ▷ (X₁ ⊗ X₂) ≫ (λ_ (X₁ ⊗ X₂)).hom

Tactic:
dsimp only [tensorμ]
  have :
    (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom =
      (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).hom ≫
        (𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).inv) ≫ (λ_ ((X₁ ⊗ 𝟙_ C) ⊗ X₂)).hom ≫ ((ρ_ X₁).hom ▷ X₂) := by
    monoidal
  simp [this]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
L R : C ⥤ C
adj : L ⊣ R
α : 𝟭 C ⟶ L
c : C
⊢ ((conjugateEquiv adj Adjunction.id) α).app c = α.app (R.obj c) ≫ adj.counit.app c

Tactic:
by
  simp [conjugateEquiv, mateEquiv, Adjunction.id]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
L R : C ⥤ C
adj : L ⊣ R
α : R ⟶ 𝟭 C
c : C
⊢ ((conjugateEquiv adj Adjunction.id).symm α).app c = adj.unit.app c ≫ α.app (L.obj c)

Tactic:
by
  simp [conjugateEquiv, mateEquiv, Adjunction.id]

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

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
κ : ι → Type u_2
Λ : ι → Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_4
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_5
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f g h : F
a : A
repr : Repr R a ι
a₁ : (i : ι) → Repr R (repr.left i) (κ i)
a₂ : (i : ι) → Repr R (repr.right i) (Λ i)
this :
  ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] ((a₁ i).right j ⊗ₜ[R] repr.right i) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] ((a₂ i).left j ⊗ₜ[R] (a₂ i).right j)
⊢ ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, f (repr.left i) ⊗ₜ[R] (g ((a₂ i).left j) ⊗ₜ[R] h ((a₂ i).right j)) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, f ((a₁ i).left j) ⊗ₜ[R] (g ((a₁ i).right j) ⊗ₜ[R] h (repr.right i))

Tactic:
apply_fun TensorProduct.map (f : A →ₗ[R] B)
    (TensorProduct.map (g : A →ₗ[R] B) (h : A →ₗ[R] B)) at this

Goal state after:
R : Type u
A : Type v
ι : Type u_1
κ : ι → Type u_2
Λ : ι → Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_4
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_5
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f g h : F
a : A
repr : Repr R a ι
a₁ : (i : ι) → Repr R (repr.left i) (κ i)
a₂ : (i : ι) → Repr R (repr.right i) (Λ i)
this :
  (TensorProduct.map (↑f) (TensorProduct.map ↑g ↑h))
      (∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] ((a₁ i).right j ⊗ₜ[R] repr.right i)) =
    (TensorProduct.map (↑f) (TensorProduct.map ↑g ↑h))
      (∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] ((a₂ i).left j ⊗ₜ[R] (a₂ i).right j))
⊢ ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, f (repr.left i) ⊗ₜ[R] (g ((a₂ i).left j) ⊗ₜ[R] h ((a₂ i).right j)) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, f ((a₁ i).left j) ⊗ₜ[R] (g ((a₁ i).right j) ⊗ₜ[R] h (repr.right i))
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ ↑(TensorProduct.comm R R R) ∘ₗ comul = comul

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul ∘ₗ inl R A B = TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul ∘ₗ inr R A B = TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ counit ∘ₗ inr R A B = counit

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ counit ∘ₗ inl R A B = counit

Tactic:
ext; simp

Goal state after: