mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Perm α
⊢ (∀ c ∈ g.cycleFactorsFinset, Commute z c) ↔
    ∀ c ∈ g.cycleFactorsFinset,
      ∃ (hc : ∀ (x : α), z x ∈ c.support ↔ x ∈ c.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers c

Tactic:
apply forall_congr'

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Perm α
⊢ ∀ (a : Perm α),
    a ∈ g.cycleFactorsFinset → Commute z a ↔
      a ∈ g.cycleFactorsFinset →
        ∃ (hc : ∀ (x : α), z x ∈ a.support ↔ x ∈ a.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers a
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : ↑(colimitCocone F).pt
⊢ (Hom.hom m) x = (Hom.hom (descMorphism F s)) x

Tactic:
refine Quot.inductionOn x ?_
    intro x
    induction x with
    | zero => simp
    | one => simp
    | neg x ih => simp [ih]
    | of j x =>
      exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x
    | add x y ih_x ih_y => simp [ih_x, ih_y]
    | mul x y ih_x ih_y => simp [ih_x, ih_y]

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
A B : Matrix n n R
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
h : ∀ {s t : ℤˣ}, detp s A * detp t B = ∑ σ ∈ ofSign s, ∑ τ ∈ ofSign (t * s), ∏ k, A k (σ k) * B (σ k) (τ k)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
s : ℤˣ
⊢ ∑ σ ∈ ofSign s, ∏ k, (A * B) k (σ k) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) +
      (∑ x ∈ ofSign 1, ∑ x_1 ∈ ofSign s, ∏ k, A k (x k) * B (x k) (x_1 k) +
        ∑ x ∈ ofSign (-1), ∑ x_1 ∈ ofSign s, ∏ k, A k (x k) * B (x k) (x_1 k))

Tactic:
mul_apply,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
h : ∀ {s t : ℤˣ}, detp s A * detp t B = ∑ σ ∈ ofSign s, ∑ τ ∈ ofSign (t * s), ∏ k, A k (σ k) * B (σ k) (τ k)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
s : ℤˣ
⊢ ∑ σ ∈ ofSign s, ∏ k, ∑ j, A k j * B j (σ k) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) +
      (∑ x ∈ ofSign 1, ∑ x_1 ∈ ofSign s, ∏ k, A k (x k) * B (x k) (x_1 k) +
        ∑ x ∈ ofSign (-1), ∑ x_1 ∈ ofSign s, ∏ k, A k (x k) * B (x k) (x_1 k))
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : ↑(colimitCocone F).pt
⊢ (Hom.hom m) x = (Hom.hom (descMorphism F s)) x

Tactic:
refine Quot.inductionOn x ?_
    intro x
    induction x with
    | zero => simp
    | one => simp
    | neg x ih => simp [ih]
    | of j x =>
      exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x
    | add x y ih_x ih_y => simp [ih_x, ih_y]
    | mul x y ih_x ih_y => simp [ih_x, ih_y]

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
inst✝ : IsEmpty n
x✝ : Matrix n n R
⊢ x✝.det = const (Matrix n n R) 1 x✝

Tactic:
exact det_isEmpty

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
M N : Matrix n n R
p : n → n
H : ¬Bijective p
i j : n
hpij : p i = p j
hij : i ≠ j
σ : Perm n
x✝ : σ ∈ univ
⊢ ∀ (x : n), M (σ x) (p x) = M ((σ * Equiv.swap i j) ((Equiv.swap i j) x)) (p ((Equiv.swap i j) x))

Tactic:
by simp [apply_swap_eq_self hpij]

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
i : n
key : ∑ j, ∑ i ∈ ofSign s with i i = j, ∏ k, A k (i k) = ∑ i ∈ ofSign s, ∏ k, A k (i k)
⊢ (A * adjp s A) i i = detp s A

Tactic:
mul_apply,

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)
⊢ ∑ j, A i j * adjp s A j i = detp s A
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
⊢ ∀ ⦃X Y : J⦄ (f_1 : X ⟶ Y), F.map f_1 ≫ f ⋯ = f ⋯ ≫ ((Functor.const J).obj Z).map f_1

Tactic:
intro j j' g

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ F.map g ≫ f ⋯ = f ⋯ ≫ ((Functor.const J).obj Z).map g
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 (Option n) (Option n) R
⊢ (A * adjp s A) none none =
    A none none * detp s (A.submatrix some some) +
      ∑ k, A none (some k) * detp (-s) (A.submatrix some (Function.update some k none))

Tactic:
mul_apply,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix (Option n) (Option n) R
⊢ ∑ j, A none j * adjp s A j none =
    A none none * detp s (A.submatrix some some) +
      ∑ k, A none (some k) * detp (-s) (A.submatrix some (Function.update some k none))
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
M : Matrix n n R
j : n
u v : n → R
⊢ (Mᵀ.updateRow j (u + v)).det = (M.updateCol j u).det + (M.updateCol j v).det

Tactic:
det_updateRow_add

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
u v : n → R
⊢ (Mᵀ.updateRow j u).det + (Mᵀ.updateRow j v).det = (M.updateCol j u).det + (M.updateCol j v).det
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
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
i j : n
⊢ IsAddUnit (detp s A * (B * adjp t B) i j)

Tactic:
mul_apply,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
i j : n
⊢ IsAddUnit (detp s A * ∑ j_1, B i j_1 * adjp t B j_1 j)
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
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
i j : n
⊢ IsAddUnit ((detp s A • (B * adjp t B)) i j)

Tactic:
simp_rw [smul_apply, smul_eq_mul, mul_apply, detp, adjp_apply, mul_sum, sum_mul,
    IsAddUnit.sum_iff]

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
i j : n
⊢ ∀ a ∈ univ,
    ∀ a_2 ∈ {x ∈ ofSign t | x j = a},
      ∀ a_4 ∈ ofSign s, IsAddUnit ((∏ k, A k (a_4 k)) * (B i a * ∏ k ∈ {j}ᶜ, B k (a_2 k)))
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
A B : Matrix n n R
hAB : A * B = 1
⊢ detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B

Tactic:
by
  have key := congr(A * $(mul_adjp_add_detp B))
  simp_rw [mul_add, ← mul_assoc, hAB, one_mul, Matrix.mul_smul, mul_one] at key
  rwa [add_comm, eq_comm, add_comm]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
⊢ ∀ ⦃X Y : J⦄ (f_1 : X ⟶ Y), ((Functor.const J).obj Z).map f_1 ≫ f ⋯ = f ⋯ ≫ F.map f_1

Tactic:
intro j j' g

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ ((Functor.const J).obj Z).map g ≫ f ⋯ = f ⋯ ≫ F.map g
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
c' : F.CoconeTypes
j : J
⊢ (Equiv.ulift.toFun ∘ hc.desc (c'.postcomp ⇑Equiv.ulift.symm)) ∘ c.ι j = c'.ι j

Tactic:
rw [Function.comp_assoc, hc.fac]

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
c' : F.CoconeTypes
j : J
⊢ Equiv.ulift.toFun ∘ (c'.postcomp ⇑Equiv.ulift.symm).ι j = c'.ι j
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
x y : (j : J) × F.obj j
x✝ : F.ColimitTypeRel x y
f : x.fst ⟶ y.fst
h : y.snd = (hom (F.map f)) x.snd
⊢ (hom (F.map f)) x.snd = (hom (F.map (𝟙 y.fst))) y.snd

Tactic:
by rw [← h, Functor.map_id, id_apply]

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i j : J) (xi : (fun X ↦ X) (F.obj i)) (xj : (fun X ↦ X) (F.obj j)),
    (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj → ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
α : t.pt → J := fun x ↦ ⋯.choose
f : (x : t.pt) → F.obj (α x) := fun x ↦ ⋯.choose
hf : ∀ (x : t.pt), x = (hom (t.ι.app (α x))) (f x)
s : Cocone F
j : J
y : F.obj j
⊢ (hom (t.ι.app j ≫ ↾fun x ↦ (hom (s.ι.app (α x))) (f x))).toFun y = (hom (s.ι.app j)).toFun y

Tactic:
obtain ⟨k, l, g, eq⟩ := hinj _ _ _ _ (hf (t.ι.app j y))

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i j : J) (xi : (fun X ↦ X) (F.obj i)) (xj : (fun X ↦ X) (F.obj j)),
    (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj → ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
α : t.pt → J := fun x ↦ ⋯.choose
f : (x : t.pt) → F.obj (α x) := fun x ↦ ⋯.choose
hf : ∀ (x : t.pt), x = (hom (t.ι.app (α x))) (f x)
s : Cocone F
j : J
y : F.obj j
k : J
l : j ⟶ k
g : α ((hom (t.ι.app j)) y) ⟶ k
eq : (hom (F.map l)) y = (hom (F.map g)) (f ((hom (t.ι.app j)) y))
⊢ (hom (t.ι.app j ≫ ↾fun x ↦ (hom (s.ι.app (α x))) (f x))).toFun y = (hom (s.ι.app j)).toFun y
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)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
z : (i : { a // a ∉ s }) → M₁ ↑i
⊢ ∀ [inst : DecidableEq α] (m : α → (i : ι) → M₁ i) (i : α) (x y : (i : ι) → M₁ i),
    (((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i (x + y) (e.symm i_1) ↑i_1) =
      (((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i x (e.symm i_1) ↑i_1) +
        ((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i y (e.symm i_1) ↑i_1

Tactic:
simp [iteratedFDeriv_aux]

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)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
z : (i : { a // a ∉ s }) → M₁ ↑i
⊢ ∀ [inst : DecidableEq α] (m : α → (i : ι) → M₁ i) (i : α) (c : R) (x : (i : ι) → M₁ i),
    (((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i (c • x) (e.symm i_1) ↑i_1) =
      c • ((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i x (e.symm i_1) ↑i_1

Tactic:
simp [iteratedFDeriv_aux]

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

Goal state before:
pp: case e'_3.refine_4
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
σ₂ : Perm n
⊢ (↑↑(sign σ₁) * ∏ x, A (σ₁ x) x) * (↑↑(sign σ₂) * ∏ x, D (σ₂ x) x) =
    ↑↑(sign (σ₁.sumCongr σ₂)) *
      ((∏ x, fromBlocks A B 0 D (Sum.map (⇑σ₁) (⇑σ₂) (Sum.inl x)) (Sum.inl x)) *
        ∏ x, fromBlocks A B 0 D (Sum.map (⇑σ₁) (⇑σ₂) (Sum.inr x)) (Sum.inr x))

Tactic:
Sum.map_inr,

Goal state after:
case e'_3.refine_4
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
σ₂ : Perm n
⊢ (↑↑(sign σ₁) * ∏ x, A (σ₁ x) x) * (↑↑(sign σ₂) * ∏ x, D (σ₂ x) x) =
    ↑↑(sign (σ₁.sumCongr σ₂)) *
      ((∏ x, fromBlocks A B 0 D (Sum.map (⇑σ₁) (⇑σ₂) (Sum.inl x)) (Sum.inl x)) *
        ∏ x, fromBlocks A B 0 D (Sum.inr (σ₂ x)) (Sum.inr x))
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)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), (directLimitCocone G f).ι.app j ≫ m = s.ι.app j
⊢ m = ↟(Module.DirectLimit.lift R ι G f (fun i ↦ Hom.hom (s.ι.app i)) ⋯)

Tactic:
have :
      s.ι.app = fun i =>
        (ofHom (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)) ≫ m := by
      funext i
      rw [← h]
      rfl

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)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), (directLimitCocone G f).ι.app j ≫ m = s.ι.app j
this : s.ι.app = fun i ↦ ↟(DirectLimit.of R ι (fun i ↦ G i) (fun i j H ↦ f i j H) i) ≫ m
⊢ m = ↟(Module.DirectLimit.lift R ι G f (fun i ↦ Hom.hom (s.ι.app i)) ⋯)
Module: Mathlib.CategoryTheory.Monoidal.Category

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

Tactic:
injections h
    replace h := congr_fun h (𝟙_ C)
    simpa using h

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

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

Tactic:
injections h
    replace h := congr_fun h (𝟙_ C)
    simpa using h

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

Tactic:
by
  rw [← MonoidalCategory.whiskerLeft_comp, μ_δ, MonoidalCategory.whiskerLeft_id]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ (f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ₘ f)

Tactic:
by
  ext : 1
  apply TensorProduct.ext'
  intro x y
  rfl

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cone F.unop
hc : IsLimit c
s : Cocone F
m : (coconeOfConeUnop c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeOfConeUnop c).ι.app j ≫ m = s.ι.app j
j : J
⊢ (m.unop ≫ c.π.app j).op = ((hc.lift (coneUnopOfCocone s)).op.unop ≫ c.π.app j).op

Tactic:
simpa only [Quiver.Hom.unop_op, IsLimit.fac] using! w (op j)

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : C ⥤ D
⊢ snd ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)) =
    (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt).hom ≫ (c.map G).snd

Tactic:
dsimp only [snd]

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : C ⥤ D
⊢ ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).π.app WalkingCospan.right =
    (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt).hom ≫
      (c.map G).π.app WalkingCospan.right
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalCategory D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
inst✝⁷ : MonoidalCategory E
C' : Type u₁'
inst✝⁶ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁵ : F.OplaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : adj.IsMonoidal
F' : D ⥤ E
G' : E ⥤ D
adj' : F' ⊣ G'
inst✝² : F'.OplaxMonoidal
inst✝¹ : G'.LaxMonoidal
inst✝ : adj'.IsMonoidal
X Y : E
⊢ μ (G' ⋙ G) X Y =
    (adj.comp adj').unit.app ((G' ⋙ G).obj X ⊗ (G' ⋙ G).obj Y) ≫
      (G' ⋙ G).map
        (δ (F ⋙ F') ((G' ⋙ G).obj X) ((G' ⋙ G).obj Y) ≫ ((adj.comp adj').counit.app X ⊗ₘ (adj.comp adj').counit.app Y))

Tactic:
simp only [comp_obj, comp_μ, IsMonoidal.leftAdjoint_μ (adj := adj), id_obj,
      IsMonoidal.leftAdjoint_μ (adj := adj'), assoc, ← map_comp, comp_unit_app, comp_δ,
      comp_counit_app, ← tensorHom_comp_tensorHom, δ_natural_assoc, Functor.comp_map]
    simp

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

Goal state before:
pp: case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
h : IsLimit c.unop
⊢ IsColimit c

Tactic:
exact (IsColimit.equivIsoColimit c.unopOpIso).toFun
      ((IsColimit.precomposeHomEquiv _ _).invFun
      ((IsColimit.whiskerEquivalenceEquiv walkingCospanOpEquiv.symm).toFun h.op))

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'
e : C ≌ D
inst✝ : e.functor.Monoidal
this✝ : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
this : IsIso (LaxMonoidal.ε e.inverse)
X Y : D
⊢ IsIso (LaxMonoidal.μ e.inverse X Y)

Tactic:
simp only [Adjunction.rightAdjointLaxMonoidal_μ, Adjunction.homEquiv_unit]
    infer_instance

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
i j : J
f : i ⟶ j
⊢ F.map f ≫ homMk (colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j) ⋯ =
    homMk (colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) i) ⋯ ≫
      ((Functor.const J).obj (mkOfSMul (coconePointSMul F))).map f

Tactic:
apply (forget₂ _ AddCommGrpCat).map_injective
        simp only [Functor.map_comp, forget₂_map_homMk]
        dsimp
        erw [colimit.w (F ⋙ forget₂ _ AddCommGrpCat), comp_id]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
X✝ : C
⊢ (L₂.map (G.map (adj₁.unit.app X✝)) ≫ α.natTrans.app (R₁.obj (L₁.obj X✝))) ≫ H.map (adj₁.counit.app (L₁.obj X✝)) =
    α.natTrans.app X✝

Tactic:
← Functor.comp_map,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
X✝ : C
⊢ ((G ⋙ L₂).map (adj₁.unit.app X✝) ≫ α.natTrans.app (R₁.obj (L₁.obj X✝))) ≫ H.map (adj₁.counit.app (L₁.obj X✝)) =
    α.natTrans.app X✝