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 : 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 : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
a b : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) (a + b)) =
    f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) a) +
      f fun j ↦ if h : P j then update x i b ⟨j, h⟩ else z ⟨j, h⟩

Tactic:
(rw [domDomRestrict_aux])

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✝¹² : 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 : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
a b : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) (a + b)) =
    f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) a) +
      f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) b)
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 : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
a b : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) (a + b)) =
    f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) a) +
      f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) b)

Tactic:
(rw [domDomRestrict_aux])

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✝¹² : 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 : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
a b : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) (a + b)) =
    f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) a) +
      f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) b)
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 : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z✝ : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
z : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
c : R
a : M₁ ↑i
⊢ (f fun j ↦ if h : P j then update z i (c • a) ⟨j, h⟩ else z✝ ⟨j, h⟩) =
    c • f fun j ↦ if h : P j then update z i a ⟨j, h⟩ else z✝ ⟨j, h⟩

Tactic:
(rw [domDomRestrict_aux])

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✝¹² : 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 : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z✝ : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
z : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
c : R
a : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) (c • a)) =
    c • f fun j ↦ if h : P j then update z i a ⟨j, h⟩ else z✝ ⟨j, h⟩
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 : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z✝ : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
z : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
c : R
a : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) (c • a)) =
    c • f fun j ↦ if h : P j then update z i a ⟨j, h⟩ else z✝ ⟨j, h⟩

Tactic:
(rw [domDomRestrict_aux])

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✝¹² : 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 : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z✝ : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
z : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
c : R
a : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) (c • a)) =
    c • f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) a)
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 : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z✝ : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
z : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
c : R
a : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) (c • a)) =
    c • f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) a)

Tactic:
(rw [domDomRestrict_aux])

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✝¹² : 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 : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z✝ : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
z : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
c : R
a : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) (c • a)) =
    c • f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) a)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_3.refine_2
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
mk_apply_eq : ∀ (k : o) (x : n), ((σ (x, k)).1, k) = σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((σ.symm (x, k)).1, k) = σ.symm (x, k)
k : o
x✝ : k ∈ univ
x : n
⊢ (fun x ↦ (σ (x, k)).1) ((fun x ↦ (σ.symm (x, k)).1) x) = x

Tactic:
simp [mk_inv_apply_eq]

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

Goal state before:
pp: case convert_2
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
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ ∀ x ∈ univ, x ∉ (↑(sumCongrHom m n).range).toFinset → ↑↑(sign x) * ∏ i, fromBlocks A B 0 D (x i) i = 0

Tactic:
rintro σ - hσn

Goal state after:
case convert_2
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
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range).toFinset
⊢ ↑↑(sign σ) * ∏ i, fromBlocks A B 0 D (σ i) i = 0
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 ι
m : (i : ι) → M₁ i
i : ι
x : M₁ i
⊢ f (update m i 0) = 0

Tactic:
f.map_coord_zero i (update_self i 0 m)

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 ι
m : (i : ι) → M₁ i
i : ι
x : M₁ i
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F : C × D ⥤ E
X : C
X✝ Y✝ Z✝ : D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ F.map (𝟙 X ×ₘ f ≫ g) = F.map (𝟙 X ×ₘ f) ≫ F.map (𝟙 X ×ₘ g)

Tactic:
simp [← F.map_comp]

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
f : X✝ ⟶ Y✝
Y Y' : D
g : Y ⟶ Y'
⊢ { obj := fun Y ↦ F.obj (X✝, Y), map := fun {X Y} g ↦ F.map (𝟙 X✝ ×ₘ g), map_id := ⋯, map_comp := ⋯ }.map g ≫
      F.map (f ×ₘ 𝟙 Y') =
    F.map (f ×ₘ 𝟙 Y) ≫
      { obj := fun Y ↦ F.obj (Y✝, Y), map := fun {X Y} g ↦ F.map (𝟙 Y✝ ×ₘ g), map_id := ⋯, map_comp := ⋯ }.map g

Tactic:
simp [← F.map_comp]

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 ι
inst✝ : Fintype ι
x h : (i : ι) → M₁ i
⊢ ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x) +
      ∑ x_1 ∈ Finset.univ.powerset with ¬2 ≤ #x_1, f (x_1.piecewise h x) =
    f x + (f.linearDeriv x) h + ∑ s ∈ Finset.univ.powerset with 2 ≤ #s, f (s.piecewise h x)

Tactic:
not_le,

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 ι
inst✝ : Fintype ι
x h : (i : ι) → M₁ i
⊢ ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x) +
      ∑ x_1 ∈ Finset.univ.powerset with #x_1 < 2, f (x_1.piecewise h x) =
    f x + (f.linearDeriv x) h + ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x)
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✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
Y : D
⊢ { app := fun Y ↦ F.map (f ≫ g ×ₘ 𝟙 Y), naturality := ⋯ }.app Y =
    ({ app := fun Y ↦ F.map (f ×ₘ 𝟙 Y), naturality := ⋯ } ≫ { app := fun Y ↦ F.map (g ×ₘ 𝟙 Y), naturality := ⋯ }).app Y

Tactic:
simp [← F.map_comp]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type r
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
⊢ Function.Injective fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x

Tactic:
intro (x : E.pt)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type r
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
x : E.pt
⊢ ∀ ⦃a₂ : ToType D.pt⦄,
    (fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x) x = (fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x) a₂ → x = a₂
Module: Mathlib.Algebra.Category.Grp.ForgetCorepresentable

Goal state before:
pp: G : Type u
inst✝ : AddCommGroup G
x y : G
⊢ (uliftZMultiplesHom G) (x + y) = (uliftZMultiplesHom G) x + (uliftZMultiplesHom G) y

Tactic:
by
  ext
  simp_all only [uliftZMultiplesHom_apply_apply, smul_add, AddMonoidHom.add_apply]

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ RingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget RingCat).sections
this✝ : (forget₂ RingCat SemiRingCat).ReflectsIsomorphisms
this : Small.{u, max u v} ↑((F ⋙ forget₂ RingCat SemiRingCat) ⋙ forget SemiRingCat).sections
c : Cone F :=
  { pt := of (Types.Small.limitCone (F ⋙ forget RingCat)).pt,
    π := { app := fun x ↦ ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ RingCat SemiRingCat) x), naturality := ⋯ } }
c' : Cone (F ⋙ forget₂ RingCat SemiRingCat)
t : IsLimit c'
⊢ (forget₂ RingCat SemiRingCat).mapCone c ≅ c'

Tactic:
by apply IsLimit.uniqueUpToIso (SemiRingCat.HasLimits.limitConeIsLimit _) t

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 ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ (G.map (δ F (X ⊗ Y) Z) ≫ δ G (F.obj (X ⊗ Y)) (F.obj Z)) ≫
      (G.map (δ F X Y) ≫ δ G (F.obj X) (F.obj Y)) ▷ G.obj (F.obj Z) ≫
        (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom =
    G.map (F.map (α_ X Y Z).hom) ≫
      (G.map (δ F X (Y ⊗ Z)) ≫ δ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
        G.obj (F.obj X) ◁ (G.map (δ F Y Z) ≫ δ G (F.obj Y) (F.obj Z))

Tactic:
rw [comp_whiskerRight, assoc, assoc, assoc, δ_natural_left_assoc, associativity,
      ← G.map_comp_assoc, ← G.map_comp_assoc, assoc, associativity, map_comp, map_comp,
      assoc, assoc, MonoidalCategory.whiskerLeft_comp, δ_natural_right_assoc]

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✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ ε (F.prod G) ≫ η (F.prod G) = 𝟙 (𝟙_ (D × C'))

Tactic:
ext <;> apply Monoidal.ε_η

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 G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (λ_ (G.obj X)).hom =
    (εIso F ≪≫ i.app (𝟙_ C)).hom ▷ G.obj X ≫
      ((i.symm.app (𝟙_ C) ⊗ᵢ i.symm.app X) ≪≫ μIso F (𝟙_ C) X ≪≫ i.app (𝟙_ C ⊗ X)).hom ≫ G.map (λ_ X).hom

Tactic:
simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← tensorHom_id, tensorIso_hom, Iso.symm_hom,
      μIso_hom, Category.assoc, tensorHom_comp_tensorHom_assoc, Iso.hom_inv_id_app,
      Category.comp_id, Category.id_comp]

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 G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (λ_ (G.obj X)).hom =
    (LaxMonoidal.ε F ⊗ₘ i.inv.app X) ≫ LaxMonoidal.μ F (𝟙_ C) X ≫ i.hom.app (𝟙_ C ⊗ X) ≫ G.map (λ_ X).hom
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
eq : (Hom.hom m).comp ↑(AddEquiv.ofBijective (Quot.desc F c) h) = Quot.desc F s
⊢ (Hom.hom m) ((AddEquiv.ofBijective (Quot.desc F c) h) x) = (Quot.desc F s) x

Tactic:
rw [← eq]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
eq : (Hom.hom m).comp ↑(AddEquiv.ofBijective (Quot.desc F c) h) = Quot.desc F s
⊢ (Hom.hom m) ((AddEquiv.ofBijective (Quot.desc F c) h) x) =
    ((Hom.hom m).comp ↑(AddEquiv.ofBijective (Quot.desc F c) h)) x
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
⊢ (Hom.hom m).comp ↑(AddEquiv.ofBijective (Quot.desc F c) h) = Quot.desc F s

Tactic:
exact Quot.addMonoidHom_ext F (by simp [← hm])

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
β : R₂ ⟶ R₁
αβ : α ≫ β = 𝟙 R₁
⊢ (conjugateEquiv adj₁ adj₁).symm (𝟙 R₁) = 𝟙 L₁

Tactic:
conjugateEquiv_symm_id

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
β : R₂ ⟶ R₁
αβ : α ≫ β = 𝟙 R₁
⊢ 𝟙 L₁ = 𝟙 L₁
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
β : R₂ ⟶ R₁
αβ : α ≫ β = 𝟙 R₁
⊢ (conjugateEquiv adj₂ adj₁).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = 𝟙 L₁

Tactic:
rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_id]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Bialgebra R A
inst✝¹ : Semiring B
inst✝ : Bialgebra R B
a✝ : A
b✝ : B
a b : A
⊢ ∑ x ∈ (ℛ R a).index,
      (_root_.TensorProduct.map (LinearMap.mul' R A) (LinearMap.mul' R A))
        ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A A A)
          ((ℛ R a).left x ⊗ₜ[R] (ℛ R a).right x ⊗ₜ[R] ∑ i ∈ (ℛ R b).index, (ℛ R b).left i ⊗ₜ[R] (ℛ R b).right i)) =
    (∑ i ∈ (ℛ R a).index, (ℛ R a).left i ⊗ₜ[R] (ℛ R a).right i) *
      ∑ i ∈ (ℛ R b).index, (ℛ R b).left i ⊗ₜ[R] (ℛ R b).right i

Tactic:
simp [TensorProduct.tmul_sum, Finset.sum_mul_sum]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
P : Type u_5
M' : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
g : P →ₗ[R] M
⊢ ε ⊗ₘ f ∘ₗ δ ∘ₗ g = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹ ∘ₗ g

Tactic:
by
  simp_rw [← LinearMap.comp_assoc, map_counit_comp_comul_left]

Goal state after: