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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Fintype (κ i)
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : DecidableEq ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
p : (i : ι) → κ i
j : ι'
this : ∀ (l : ι), (x l) (p l) = 0 → 0 = ∏ i, (x i) (p i)
⊢ ((freeDFinsuppEquiv (DFinsupp.single (p, j) 1)) x) j = (DFinsupp.single (p, j).2 (∏ i, (x i) ((p, j).1 i))) j

Tactic:
simpa [freeDFinsuppEquiv_def, MultilinearMap.piRingEquiv, DFinsupp.sigmaCurryEquiv,
        fromDFinsuppEquiv_apply]

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 : Fin n.succ) → AddCommMonoid (M i)
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
f✝ f' f g : MultilinearMap R M₁ M₂
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
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 : Fin n.succ) → AddCommMonoid (M i)
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
f f' g : MultilinearMap R M₁ M₂
toFun✝ : ((i : ι) → M₁ i) → M₂
map_update_add'✝ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    toFun✝ (update m i (x + y)) = toFun✝ (update m i x) + toFun✝ (update m i y)
map_update_smul'✝ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    toFun✝ (update m i (c • x)) = c • toFun✝ (update m i x)
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_update_add' := map_update_add'✝, map_update_smul' := map_update_smul'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_update_add' := map_update_add'✝, map_update_smul' := map_update_smul'✝ } = g
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type u_6
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
f✝ f' : M [⋀^ι]→ₗ[R] N
g✝ g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v✝ : ι → M
v' : ι → M'
f g : M [⋀^ι]→ₗ[R] N'
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (↑f - ↑g).toFun v = 0

Tactic:
by
        simp [f.map_eq_zero_of_eq v h hij, g.map_eq_zero_of_eq v h hij]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
s : ℤˣ
inst✝ : Nonempty n
⊢ detp s 0 = 0

Tactic:
simp [detp]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
s : ℤˣ
A : Matrix n n R
S : Type u_4
inst✝ : CommSemiring S
f : R →+* S
⊢ detp s (A.map ⇑f) = f (detp s A)

Tactic:
simp [detp]

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

Goal state before:
pp: case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
j : ι
h : j = i
⊢ update (t.piecewise (m + m') m') i (m i) j = t.piecewise (m + m'') m'' j

pp: case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
j : ι
h : ¬j = i
⊢ update (t.piecewise (m + m') m') i (m i) j = t.piecewise (m + m'') m'' j

Tactic:
· rw [h]
      simp [m'', hit]

Goal state after:
case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
j : ι
h : ¬j = i
⊢ update (t.piecewise (m + m') m') i (m i) j = t.piecewise (m + m'') m'' j
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ ((reindex e e') M).det = ↑↑(sign (e'.trans e.symm)) * M.det

Tactic:
by
  trans ((M.reindex (e.trans e'.symm) (.refl _)).reindex e' e').det
  · congr 1; ext; simp
  · simp_rw [det_reindex_self, reindex_apply, Equiv.refl_symm, Equiv.coe_refl, det_permute]
    rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
v : n → R
A : Matrix n n R
⊢ (A * diagonal v).det = (∏ i, v i) * A.det

Tactic:
rw [det_mul, det_diagonal, mul_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ⊇ x2) ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨i, ij⟩)
        ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) z) ∧
      (fun x1 x2 ↦ x1 ⊇ x2) ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨k, kj⟩)
        ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) z)

Tactic:
refine ⟨⟨l, lk ≫ kj⟩, e ▸ ?_, ?_⟩ <;>
    simp_rw [F.map_comp]

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ Set.range ⇑(ConcreteCategory.hom (F.map ij)) ⊇ Set.range ⇑(ConcreteCategory.hom (F.map li ≫ F.map ij))

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ Set.range ⇑(ConcreteCategory.hom (F.map kj)) ⊇ Set.range ⇑(ConcreteCategory.hom (F.map lk ≫ F.map kj))
Module: Mathlib.Algebra.Category.Grp.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget GrpCat) x y
⊢ colimitInvAux F x = colimitInvAux F y

Tactic:
apply G.mk_eq

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget GrpCat) x y
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) ⟨x.fst, x.snd⁻¹⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, y.snd⁻¹⟩.snd
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:
by
    intro h m i c x
    classical
    ext v
    simp [domDomRestrict_aux_right]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
⊢ f = g

Tactic:
by
  apply (cancel_epi (colimitObjIsoColimitCompEvaluation H k).inv).1
  ext j
  simpa using w j

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 : Cᵒᵖ
P Q : C ⥤ Type w
α : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
β : P ⟶ Q
⊢ shrinkCoyonedaEquiv (α ≫ β) = (ConcreteCategory.hom (β.app (unop X))) (shrinkCoyonedaEquiv α)

Tactic:
by
  simp [shrinkCoyonedaEquiv]

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
⊢ IsLimit (limitCone F)

Tactic:
refine IsLimit.ofFaithful (forget (ModuleCat R)) (Types.Small.limitConeIsLimit.{v, w} _)
    (fun s => ofHom ⟨⟨(Types.Small.limitConeIsLimit.{v, w} _).lift
                ((forget (ModuleCat R)).mapCone s), ?_⟩, ?_⟩)
    (fun s => rfl)
  · intro x y
    simp [← equivShrink_add]
    rfl
  · intro r x
    simp [← equivShrink_smul]
    rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ V ◁ g ≫ (f ⊗ₘ h) = f ⊗ₘ g ≫ h

Tactic:
by
  simp [tensorHom_def']

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 : C
f : Y = Z
⊢ X ◁ eqToHom f = eqToHom ⋯

Tactic:
cases f

Goal state after:
case refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ X ◁ eqToHom ⋯ = eqToHom ⋯
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X = Y
Z : C
⊢ eqToHom f ▷ Z = eqToHom ⋯

Tactic:
cases f

Goal state after:
case refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Z : C
⊢ eqToHom ⋯ ▷ Z = eqToHom ⋯
Module: Mathlib.CategoryTheory.Monoidal.Category

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

Tactic:
rw [← cancel_epi (W ◁ (α_ X Y Z).inv), ← cancel_mono (α_ (W ⊗ X) Y Z).inv]

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

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

Tactic:
by
  simp [tensorHom_def']

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

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
⊢ ∀ {X Y Z : D}, X ◁ 0 = 0

Tactic:
by
      intros
      apply F.map_injective
      simp [Functor.Monoidal.map_whiskerLeft]

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

Goal state before:
pp: 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
⊢ (leftDistributor X f ⊗ᵢ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j ↦ X ⊗ f j) Y =
    α_ X (⨁ f) Y ≪≫
      (asIso (𝟙 X) ⊗ᵢ rightDistributor f Y) ≪≫
        (leftDistributor X fun j ↦ f j ⊗ Y) ≪≫ biproduct.mapIso fun x ↦ (α_ X (f x) Y).symm

Tactic:
by
  classical
  cases nonempty_fintype J
  ext
  simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.symm_hom, Iso.trans_hom,
    asIso_hom, comp_zero, comp_dite, Preadditive.sum_comp, Preadditive.comp_sum, sum_tensor,
    tensor_sum, comp_tensor_id, tensorIso_hom, leftDistributor_hom, rightDistributor_hom,
    biproduct.mapIso_hom, biproduct.ι_map, biproduct.ι_π, Finset.sum_dite_irrel,
    Finset.sum_dite_eq', Finset.sum_const_zero, Finset.mem_univ, if_true]
  simp_rw [← tensorHom_id, ← id_tensorHom]
  simp only [← comp_tensor_id, ← id_tensor_comp_assoc, Category.assoc, biproduct.ι_π, comp_dite,
    dite_comp, tensor_dite, dite_tensor]
  simp

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
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
Y : D
f : Y ⟶ F.obj X
⊢ (ε F ⊗ₘ f) ≫ μ F (𝟙_ C) X = 𝟙_ D ◁ f ≫ (λ_ (F.obj X)).hom ≫ F.map (λ_ X).inv

Tactic:
by
  simp [tensorHom_def']

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
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
Y : D
f : Y ⟶ F.obj X
⊢ 𝟙_ D ◁ f ≫ (λ_ (F.obj X)).hom = (ε F ⊗ₘ f) ≫ μ F (𝟙_ C) X ≫ F.map (λ_ X).hom

Tactic:
by
  simp [tensorHom_def']

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
Y : D
f : F.obj X ⟶ Y
⊢ δ F X (𝟙_ C) ≫ (f ⊗ₘ η F) = F.map (ρ_ X).hom ≫ (ρ_ (F.obj X)).inv ≫ f ▷ 𝟙_ D

Tactic:
by
  simp [tensorHom_def']

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

Goal state before:
pp: case none.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ none
⊢ (span f✝.op g.op).map f ≫
      (match none with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f

Tactic:
cases f

Goal state after:
case none.none.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).map (WidePushoutShape.Hom.id none) ≫
      (match none with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.id none)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case none.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ some WalkingPair.left
⊢ (span f✝.op g.op).map f ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f

Tactic:
cases f

Goal state after:
case none.some.left.init
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).map (WidePushoutShape.Hom.init WalkingPair.left) ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.init WalkingPair.left)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case none.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ some WalkingPair.right
⊢ (span f✝.op g.op).map f ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f

Tactic:
cases f

Goal state after:
case none.some.right.init
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).map (WidePushoutShape.Hom.init WalkingPair.right) ≫
      (match some WalkingPair.right with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom =
    (match none with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.init WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case some.left.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ none
⊢ (span f✝.op g.op).map f ≫
      (match none with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f

Tactic:
cases f

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

Goal state before:
pp: case some.left.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ (span f✝.op g.op).map f ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((span f✝.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f✝.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f✝.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f

Tactic:
cases f

Goal state after:
case some.left.some.left.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
      (match some WalkingPair.left with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom =
    (match some WalkingPair.left with
        | none => Iso.refl ((span f.op g.op).obj none)
        | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
        | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.id (some WalkingPair.left))