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

Goal state before:
pp: ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst✝⁶ : Ring K
inst✝⁵ : IsDomain K
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
j : ι
hj : j ∈ s.erase i
⊢ f (update v i (g j • v j)) = 0

Tactic:
obtain ⟨hij, _⟩ := Finset.mem_erase.mp hj

Goal state after:
ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst✝⁶ : Ring K
inst✝⁵ : IsDomain K
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
right✝ : j ∈ s
⊢ f (update v i (g j • v j)) = 0
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: case neg
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i ↦ e (v i)) = g fun i ↦ e (v i)
v : ι → ι₁
hi : ¬Function.Injective v
this : ¬Function.Injective fun i ↦ e (v i)
⊢ 0 = g fun i ↦ e (v i)

Tactic:
g.map_eq_zero_of_not_injective _ this

Goal state after:
case neg
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i ↦ e (v i)) = g fun i ↦ e (v i)
v : ι → ι₁
hi : ¬Function.Injective v
this : ¬Function.Injective fun i ↦ e (v i)
⊢ 0 = 0
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
i : n
key : ∑ j, ∑ i ∈ ofSign s with i i = j, ∏ k, A k (i k) = ∑ i ∈ ofSign s, ∏ k, A k (i k)
x : n
hx : x ∈ univ
σ : Perm n
hσ : σ ∈ {i_1 ∈ ofSign s | i_1 i = x}
⊢ A i x * ∏ k ∈ {i}ᶜ, A k (σ k) = A i (σ i) * ∏ i ∈ {i}ᶜ, A i (σ i)

Tactic:
(mem_filter.mp hσ).2

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
key : ∑ j, ∑ i ∈ ofSign s with i i = j, ∏ k, A k (i k) = ∑ i ∈ ofSign s, ∏ k, A k (i k)
x : n
hx : x ∈ univ
σ : Perm n
hσ : σ ∈ {i_1 ∈ ofSign s | i_1 i = x}
⊢ A i x * ∏ k ∈ {i}ᶜ, A k (σ k) = A i x * ∏ i ∈ {i}ᶜ, A i (σ i)
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
inst✝ : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
⊢ vecMulVec u v = vecMulVec (update u i (u i)) v

Tactic:
update_eq_self

Goal state after:
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
⊢ vecMulVec u v = vecMulVec u v
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∉ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → T' mX ≫ f = T' mY
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
mf' : ⟨X, ⟨Y, ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H'
⊢ eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f' = (fun {X_1} mZ ↦ eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY'

Tactic:
grind [eq_condition]

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

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : IsCofilteredOrEmpty C
inst✝ : IsCofilteredOrEmpty D
k l : C × D
f g : k ⟶ l
⊢ (eqHom f.1 g.1, eqHom f.2 g.2) ≫ f = (eqHom f.1 g.1, eqHom f.2 g.2) ≫ g

Tactic:
simp [eq_condition]

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

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
⊢ (M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)).det = N.det

Tactic:
M_k,

Goal state after:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
⊢ (M'.updateRow k.succ (M' k.succ + c k • M' k.castSucc)).det = N.det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case pos
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : i = k
⊢ M' i.succ j = N i.succ j + 0 * M' i.castSucc j

Tactic:
rw [zero_mul, add_zero, hM', hik, updateRow_self]

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

Goal state before:
pp: R : Type uR
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : AddCommMonoid M'
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
ι₁ : Type u_1
ι₂ : Type u_2
σ : ι₁ ≃ ι₂
g : M₂ →ₗ[R] M₃
f : MultilinearMap R (fun x ↦ M') M₂
⊢ MultilinearMap.domDomCongr σ (g.compMultilinearMap f) = g.compMultilinearMap (MultilinearMap.domDomCongr σ f)

Tactic:
ext
  simp [MultilinearMap.domDomCongr]

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✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f✝ g f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ -f (update m i (x + y)) = -f (update m i x) + -f (update m i y)

Tactic:
simp [add_comm]

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

Goal state before:
pp: F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
a : F.obj (Opposite.op 0)
n : ℕ
⊢ ∀ {j' : ℕᵒᵖ} (f : Opposite.op n ⟶ j'),
    (ConcreteCategory.hom (F.map f))
        ((fun x ↦
            match x with
            | Opposite.op n => preimage hF a n)
          (Opposite.op n)) =
      (fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        j'

Tactic:
⟨m⟩

Goal state after:
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
a : F.obj (Opposite.op 0)
n m : ℕ
⊢ ∀ (f : Opposite.op n ⟶ Opposite.op m),
    (ConcreteCategory.hom (F.map f))
        ((fun x ↦
            match x with
            | Opposite.op n => preimage hF a n)
          (Opposite.op n)) =
      (fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op m)
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✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ (colim ⋙ G).map f ≫ (preservesColimitIso G Y✝).hom =
    (preservesColimitIso G X✝).hom ≫ ((Functor.whiskeringRight J C D).obj G ⋙ colim).map f

Tactic:
rw [← Iso.inv_comp_eq, ← Category.assoc, ← Iso.eq_comp_inv]

Goal state after:
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✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ (preservesColimitIso G X✝).inv ≫ (colim ⋙ G).map f =
    ((Functor.whiskeringRight J C D).obj G ⋙ colim).map f ≫ (preservesColimitIso G Y✝).inv
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case refine_3
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✝¹
i : ι
this : DecidableEq ι := Classical.decEq ι
⊢ c • f (update x i (x i)) = c • f x

Tactic:
update_eq_self

Goal state after:
case refine_3
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✝¹
i : ι
this : DecidableEq ι := Classical.decEq ι
⊢ c • f x = c • f x
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, u_1, u, u_1 + 1} F

Tactic:
suffices PreservesLimitsOfSize (F ⋙ uliftFunctor.{v}) from
    preservesLimits_of_reflects_of_preserves _ (uliftFunctor.{v})
  rw [preservesLimitsOfSize_iff_of_natIso (F ⋙ uliftFunctor.{v}).uliftCoyonedaCoreprXIso.symm]
  exact inferInstanceAs <| PreservesLimitsOfSize (coyoneda.obj _ ⋙ uliftFunctor)

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
P : Cᵒᵖ ⥤ Type w
f : shrinkYoneda.{w, v, u}.obj X ⟶ P
g : Y ⟶ X
⊢ (ConcreteCategory.hom (P.map g.op)) (shrinkYonedaEquiv f) = shrinkYonedaEquiv (shrinkYoneda.{w, v, u}.map g ≫ f)

Tactic:
by
  simpa [shrinkYonedaEquiv, shrinkYoneda]
    using (f.naturality_apply g.op ((equivShrink _) (𝟙 _))).symm

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✝
⊢ shrinkYonedaObjObjEquiv (shrinkYonedaEquiv (shrinkYoneda.{w, v, u}.map f)) = f

Tactic:
by simp [shrinkYonedaEquiv_shrinkYoneda_map]

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
P : C ⥤ Type w
t : P.obj X
⊢ shrinkCoyonedaEquiv (shrinkCoyonedaEquiv.symm ((ConcreteCategory.hom (P.map f)) t)) =
    shrinkCoyonedaEquiv (shrinkCoyoneda.{w, v, u}.map f.op ≫ shrinkCoyonedaEquiv.symm t)

Tactic:
obtain ⟨t, rfl⟩ := shrinkCoyonedaEquiv.surjective t

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
P : C ⥤ Type w
t : shrinkCoyoneda.{w, v, u}.obj (op X) ⟶ P
⊢ shrinkCoyonedaEquiv (shrinkCoyonedaEquiv.symm ((ConcreteCategory.hom (P.map f)) (shrinkCoyonedaEquiv t))) =
    shrinkCoyonedaEquiv (shrinkCoyoneda.{w, v, u}.map f.op ≫ shrinkCoyonedaEquiv.symm (shrinkCoyonedaEquiv t))
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
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
i j : ι
h : i ≤ j
x : G i
⊢ (Hom.hom (s.ι.app j)) ((f i j h) x) = (Hom.hom (s.ι.app i)) x

Tactic:
← s.w (homOfLE h)

Goal state after:
R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
i j : ι
h : i ≤ j
x : G i
⊢ (Hom.hom (s.ι.app j)) ((f i j h) x) = (Hom.hom ((directLimitDiagram G f).map (homOfLE h) ≫ s.ι.app j)) x
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) Z).inv ≫ (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom =
    W ◁ (α_ X Y Z).inv ≫ W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv

Tactic:
← 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.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
X₁ X₂ : D
⊢ F.map (𝟙 X₁ ⊗ₘ 𝟙 X₂) = F.map (𝟙 (X₁ ⊗ X₂))

Tactic:
cases fData

Goal state after:
case mk
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
X₁ X₂ : D
μIso✝ : (X Y : D) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
whiskerLeft_eq✝ :
  ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso✝ X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso✝ X Y₂).hom
whiskerRight_eq✝ :
  ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso✝ X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso✝ X₂ Y).hom
tensorHom_eq✝ :
  ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    F.map (f ⊗ₘ g) = (μIso✝ X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso✝ Y₁ Y₂).hom
εIso✝ : 𝟙_ C ≅ F.obj (𝟙_ D)
associator_eq✝ :
  ∀ (X Y Z : D),
    F.map (α_ X Y Z).hom =
      (((μIso✝ (X ⊗ Y) Z).symm ≪≫ ((μIso✝ X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
          α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ μIso✝ Y Z) ≪≫ μIso✝ X (Y ⊗ Z)).hom
leftUnitor_eq✝ :
  ∀ (X : D), F.map (λ_ X).hom = (((μIso✝ (𝟙_ D) X).symm ≪≫ (εIso✝.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫ λ_ (F.obj X)).hom
rightUnitor_eq✝ :
  ∀ (X : D), F.map (ρ_ X).hom = (((μIso✝ X (𝟙_ D)).symm ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso✝.symm)) ≪≫ ρ_ (F.obj X)).hom
⊢ F.map (𝟙 X₁ ⊗ₘ 𝟙 X₂) = F.map (𝟙 (X₁ ⊗ X₂))
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
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : D
f₁ : X₁✝ ⟶ Y₁✝
f₂ : X₂✝ ⟶ Y₂✝
g₁ : Y₁✝ ⟶ Z₁✝
g₂ : Y₂✝ ⟶ Z₂✝
⊢ F.map ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) = F.map (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

Tactic:
cases fData

Goal state after:
case mk
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
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : D
f₁ : X₁✝ ⟶ Y₁✝
f₂ : X₂✝ ⟶ Y₂✝
g₁ : Y₁✝ ⟶ Z₁✝
g₂ : Y₂✝ ⟶ Z₂✝
μIso✝ : (X Y : D) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
whiskerLeft_eq✝ :
  ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso✝ X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso✝ X Y₂).hom
whiskerRight_eq✝ :
  ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso✝ X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso✝ X₂ Y).hom
tensorHom_eq✝ :
  ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    F.map (f ⊗ₘ g) = (μIso✝ X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso✝ Y₁ Y₂).hom
εIso✝ : 𝟙_ C ≅ F.obj (𝟙_ D)
associator_eq✝ :
  ∀ (X Y Z : D),
    F.map (α_ X Y Z).hom =
      (((μIso✝ (X ⊗ Y) Z).symm ≪≫ ((μIso✝ X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
          α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ μIso✝ Y Z) ≪≫ μIso✝ X (Y ⊗ Z)).hom
leftUnitor_eq✝ :
  ∀ (X : D), F.map (λ_ X).hom = (((μIso✝ (𝟙_ D) X).symm ≪≫ (εIso✝.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫ λ_ (F.obj X)).hom
rightUnitor_eq✝ :
  ∀ (X : D), F.map (ρ_ X).hom = (((μIso✝ X (𝟙_ D)).symm ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso✝.symm)) ≪≫ ρ_ (F.obj X)).hom
⊢ F.map ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) = F.map (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)
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
X Y : D
⊢ F.map ((α_ X (𝟙_ D) Y).hom ≫ X ◁ (λ_ Y).hom) = F.map ((ρ_ X).hom ▷ Y)

Tactic:
cases fData

Goal state after:
case mk
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
X Y : D
μIso✝ : (X Y : D) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
whiskerLeft_eq✝ :
  ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso✝ X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso✝ X Y₂).hom
whiskerRight_eq✝ :
  ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso✝ X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso✝ X₂ Y).hom
tensorHom_eq✝ :
  ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    F.map (f ⊗ₘ g) = (μIso✝ X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso✝ Y₁ Y₂).hom
εIso✝ : 𝟙_ C ≅ F.obj (𝟙_ D)
associator_eq✝ :
  ∀ (X Y Z : D),
    F.map (α_ X Y Z).hom =
      (((μIso✝ (X ⊗ Y) Z).symm ≪≫ ((μIso✝ X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
          α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ μIso✝ Y Z) ≪≫ μIso✝ X (Y ⊗ Z)).hom
leftUnitor_eq✝ :
  ∀ (X : D), F.map (λ_ X).hom = (((μIso✝ (𝟙_ D) X).symm ≪≫ (εIso✝.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫ λ_ (F.obj X)).hom
rightUnitor_eq✝ :
  ∀ (X : D), F.map (ρ_ X).hom = (((μIso✝ X (𝟙_ D)).symm ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso✝.symm)) ≪≫ ρ_ (F.obj X)).hom
⊢ F.map ((α_ X (𝟙_ D) Y).hom ≫ X ◁ (λ_ Y).hom) = F.map ((ρ_ X).hom ▷ Y)
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
f g h i : C
η η' : f ⟶ g
α : g ≅ h
θ θ' : h ⟶ i
αθ : g ⟶ i
ηαθ : f ⟶ i
e_η : η = η'
e_θ : θ = θ'
e_αθ : α.hom ≫ θ' = αθ
e_ηαθ : η' ≫ αθ = ηαθ
⊢ η ≫ α.hom ≫ θ = ηαθ

Tactic:
by
  simp [e_η, e_θ, e_αθ, e_ηαθ]

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
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ ∀ (j : WalkingSpan),
    ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι.app
          j ≫
        (Iso.refl
            ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
                (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
      (PushoutCocone.mk (G.map h) (G.map k) ⋯).ι.app j

Tactic:
rintro (_ | _ | _) <;> dsimp <;>
          simp only [Category.comp_id, Category.id_comp, ← G.map_comp]

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
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 (PushoutCocone.mk ((G.mapCocone c).ι.app WalkingSpan.left) ((G.mapCocone c).ι.app WalkingSpan.right) ⋯).flip

Tactic:
apply (isColimitMapCoconePushoutCoconeEquiv _ _).toFun

Goal state after:
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))

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
⊢ (span g f).map WalkingSpan.Hom.snd ≫ c.ι.app WalkingSpan.right =
    (span g f).map WalkingSpan.Hom.fst ≫ c.ι.app WalkingSpan.left
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).inv ≫
      (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv ≫ (β_ 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:
by
  rw [← braiding_tensor_right_hom_assoc X Y Z, ← cancel_mono (α_ Z Y X).inv]
  repeat rw [assoc]
  rw [Iso.hom_inv_id, comp_id, ← braiding_naturality_right, braiding_tensor_right_hom]

Goal state after: