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
hij : j ≠ i
right✝ : j ∈ s
⊢ g j • 0 = 0

Tactic:
smul_zero

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
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case inl.inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp 1 A + b * detp (-1) A = b * detp 1 A + a * detp (-1) A

pp: case inr.inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp (-1) A + b * detp 1 A = b * detp (-1) A + a * detp 1 A

pp: case inr.inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp (-1) A + b * detp (-1) A = b * detp (-1) A + a * detp (-1) A

Tactic:
· rw [h]

Goal state after:
case inr.inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp (-1) A + b * detp 1 A = b * detp (-1) A + a * detp 1 A

case inr.inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp (-1) A + b * detp (-1) A = b * detp (-1) A + a * detp (-1) A
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case neg
n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
le : Fintype.card n ≤ Fintype.card m
f g : m → n
hf : Function.Injective f
hg : ¬Function.Injective g
⊢ (A.submatrix f g).IsDetpBalanced a b

pp: case pos
n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
le : Fintype.card n ≤ Fintype.card m
f g : m → n
hf : Function.Injective f
hg : Function.Injective g
⊢ (A.submatrix f g).IsDetpBalanced a b

Tactic:
· obtain ⟨p, q, eq, ne⟩ := Function.not_injective_iff.mp hg
    exact .of_eq (detp_eq_of_col_eq ne <| by ext; simp [eq])

Goal state after:
case pos
n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
le : Fintype.card n ≤ Fintype.card m
f g : m → n
hf : Function.Injective f
hg : Function.Injective g
⊢ (A.submatrix f g).IsDetpBalanced a b
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered 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 → (X ⟶ S')
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
⊢ ∀ (mX_1 : X' ∈ O) (mY_1 : Y' ∈ O) {f_1 : X' ⟶ Y'},
    ⟨X', ⟨Y', ⟨mX_1, ⟨mY_1, f_1⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' →
      f_1 ≫ (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mY_1 =
        (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX_1

Tactic:
mX'

Goal state after:
case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered 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 → (X ⟶ S')
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
mX' : X' ∈ O
⊢ ∀ (mY_1 : Y' ∈ O) {f_1 : X' ⟶ Y'},
    ⟨X', ⟨Y', ⟨mX', ⟨mY_1, f_1⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' →
      f_1 ≫ (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mY_1 =
        (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered 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 → (X ⟶ S')
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' : ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H'
⊢ f' ≫ (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mY' =
    (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'

Tactic:
← Category.assoc

Goal state after:
case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered 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 → (X ⟶ S')
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' : ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H'
⊢ (f' ≫ T' mY') ≫ coeqHom (f ≫ T' mY) (T' mX) = (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case insert
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
X' Y' : C
⊢ ∀ (mX_1 : X' ∈ O) (mY_1 : Y' ∈ O) {f_1 : X' ⟶ Y'},
    ⟨X', ⟨Y', ⟨mX_1, ⟨mY_1, f_1⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' →
      (fun {X_1} mZ ↦ eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mX_1 ≫ f_1 =
        (fun {X_1} mZ ↦ eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY_1

Tactic:
mX'

Goal state after:
case insert
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
X' Y' : C
mX' : X' ∈ O
⊢ ∀ (mY_1 : Y' ∈ O) {f_1 : X' ⟶ Y'},
    ⟨X', ⟨Y', ⟨mX', ⟨mY_1, f_1⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' →
      (fun {X_1} mZ ↦ eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mX' ≫ f_1 =
        (fun {X_1} mZ ↦ eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY_1
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.IsColimit
c' : F.CoconeTypes
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
⊢ Function.Bijective f

Tactic:
← Function.Bijective.of_comp_iff _ hc.bijective

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimit
c' : F.CoconeTypes
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
⊢ Function.Bijective (f ∘ F.descColimitType c)
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' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
inst✝ : DecidableEq ι₂
v : ι₂ → M₂
i : ι₂
a : R
b : M₂
⊢ (m fun i_1 ↦ update v i (a • b) (σ i_1)) = a • m fun i_1 ↦ update v i b (σ i_1)

Tactic:
by
    let := σ.injective.decidableEq
    simp_rw [Function.update_apply_equiv_apply v]
    rw [m.map_update_smul]

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
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
σ : (a : o) → a ∈ univ → Perm n
ha₁✝ : σ ∈ univ
σ' : (a : o) → a ∈ univ → Perm n
ha₂✝ : σ' ∈ univ
eq : (prodCongrLeft fun k ↦ σ k ⋯) = prodCongrLeft fun k ↦ σ' k ⋯
x✝ : o
hx : x✝ ∈ univ
k✝ k : n
x : o
⊢ (prodCongrLeft fun k ↦ σ k ⋯) (k, x) = (prodCongrLeft fun k ↦ σ' k ⋯) (k, x)

Tactic:
rw [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
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range).toFinset
h1 : ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)
a : m
ha : ¬∃ y, Sum.inl y = σ (Sum.inl a)
⊢ ↑↑(sign σ) * ∏ i, fromBlocks A B 0 D (σ i) i = 0

Tactic:
rcases hx : σ (Sum.inl a) with a2 | b

Goal state after:
case convert_2.inl
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
h1 : ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)
a : m
ha : ¬∃ y, Sum.inl y = σ (Sum.inl a)
a2 : m
hx : σ (Sum.inl a) = Sum.inl a2
⊢ ↑↑(sign σ) * ∏ i, fromBlocks A B 0 D (σ i) i = 0

case convert_2.inr
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
h1 : ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)
a : m
ha : ¬∃ y, Sum.inl y = σ (Sum.inl a)
b : n
hx : σ (Sum.inl a) = Sum.inr b
⊢ ↑↑(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✝⁵ : CommSemiring 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 ι
c : ι → R
m : (i : ι) → M₁ i
s : Finset ι
⊢ f (s.piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ s, c i) • f m

Tactic:
by
  refine s.induction_on (by simp) ?_
  intro j s j_notMem_s Hrec
  have A :
    Function.update (s.piecewise (fun i => c i • m i) m) j (m j) =
      s.piecewise (fun i => c i • m i) m := by
    ext i
    by_cases h : i = j
    · rw [h]
      simp [j_notMem_s]
    · simp [h]
  rw [s.piecewise_insert, f.map_update_smul, A, Hrec]
  simp [j_notMem_s, mul_smul]

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 ι
m : (i : ι) → M₁ i
i : ι
x : M₁ i
⊢ f (update m i (-x)) + f (update m i x) = 0

Tactic:
by
    rw [← MultilinearMap.map_update_add, neg_add_cancel, f.map_coord_zero i (update_self i 0 m)]

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝¹ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
σ : Perm (Fin n)
x✝ : σ ∈ univ
⊢ (-1 * ↑(sign σ)) • (A i.succ 0 * ∏ i', A (i.succ.succAbove (i.cycleRange (σ i'))) i'.succ) =
    -1 * (A i.succ 0 * ↑(sign σ) • ∏ i', A (i.succ.succAbove (i.cycleRange (σ i'))) i'.succ)

Tactic:
by
      simp [_root_.neg_mul, one_mul, zsmul_eq_mul, neg_smul,
        Fin.succAbove_cycleRange, mul_left_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))
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((limitCone F).π.app (Opposite.op 0)))

Tactic:
intro a
  refine ⟨⟨fun ⟨n⟩ ↦ preimage hF a n, ?_⟩, rfl⟩
  intro ⟨n⟩ ⟨m⟩ ⟨⟨⟨(h : m ≤ n)⟩⟩⟩
  induction h with
  | refl =>
    erw [CategoryTheory.Functor.map_id, id_apply]
  | @step p h ih =>
    rw [← ih]
    have h' : m ≤ p := h
    erw [CategoryTheory.Functor.map_comp (f := (homOfLE (Nat.le_succ p)).op) (g := (homOfLE h').op),
      comp_apply, (hF p _).choose_spec]
    rfl

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

Goal state before:
pp: case pos.h
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✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
h₁ : i = k ∨ i ∈ s → i < k
⊢ i ≠ k

Tactic:
· exact fun h ↦ (h₁ <| .inl h).ne h

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : Matrix (Fin 2) (Fin 2) R
⊢ (-1) ^ 0 * A 0 0 * A 1 1 + (-1) ^ (0 + 1) * A 0 1 * A 1 0 = A 0 0 * A 1 1 - A 0 1 * A 1 0

Tactic:
ring

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : Matrix (Fin 3) (Fin 3) R
⊢ (-1) ^ 0 * A 0 0 * ((-1) ^ 0 * A 1 1 * A 2 2 + (-1) ^ (0 + 1) * A 1 2 * A 2 1) +
      ((-1) ^ (0 + 1) * A 0 1 * ((-1) ^ 0 * A 1 0 * A 2 2 + (-1) ^ (0 + 1) * A 1 2 * A 2 0) +
        (-1) ^ (0 + 1 + 1) * A 0 2 * ((-1) ^ 0 * A 1 0 * A 2 1 + (-1) ^ (0 + 1) * A 1 1 * A 2 0)) =
    A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 +
        A 0 2 * A 1 0 * A 2 1 -
      A 0 2 * A 1 1 * A 2 0

Tactic:
ring

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 : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
h₁ : ¬(i = k ∨ i ∈ s → i < k)
h₂ : k = i
⊢ update (s.piecewise b a) k (s.piecewise b a k - b k) i = a i - b i

Tactic:
cases h₂
      rw [update_self, s.piecewise_eq_of_notMem _ _ (lt_irrefl _ <| hk k ·)]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ (liftedLimitMapsToOriginal t).inv.hom ≫ F.map ((liftLimit t).π.app j) = c.π.app j

Tactic:
show F.map ((liftLimit t).π.app j) = (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app j
    from (by simp),

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ (liftedLimitMapsToOriginal t).inv.hom ≫ (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app j = c.π.app j
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ Cᵒᵖ
c : Cone F
hc : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
j : J
eq :
  (hom ((hc (unop s.pt)).lift ((yoneda.obj (unop s.pt)).mapCone s) ≫ ((yoneda.obj (unop s.pt)).mapCone c).π.app j))
      (𝟙 (unop s.pt)) =
    (hom (((yoneda.obj (unop s.pt)).mapCone s).π.app j)) (𝟙 (unop s.pt))
⊢ (c.π.app j).unop ≫ m.unop =
    (c.π.app j).unop ≫ (hom ((hc (unop s.pt)).lift ((yoneda.obj (unop s.pt)).mapCone s))) (𝟙 (unop s.pt))

Tactic:
simp_all [← hm]

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j : J
s : Cocone F
this : Algebra R ↑c.pt := algebraOfIsFiltered hc j
r : R
⊢ (↑↑(RingCat.Hom.hom (hc.desc ((forget₂ (AlgCat R) RingCat).mapCocone s)))).toFun ((algebraMap R ↑c.pt) r) =
    (algebraMap R ↑s.1) r

Tactic:
simp [RingHom.algebraMap_toAlgebra', ← ConcreteCategory.comp_apply]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
j : J
this : Small.{w, max v w}
  ↑((F ⋙ forget₂ (AlgCat R) RingCat ⋙ forget₂ RingCat SemiRingCat) ⋙ forget SemiRingCat).sections :=
  limitπAlgHom._proof_1 F
x : R
⊢ (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (AlgCat R))).π.app j))
      ((algebraMap R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt) x) =
    (algebraMap R ((F ⋙ forget (AlgCat R)).obj j)) x

Tactic:
simp only [Functor.comp_obj, Types.Small.limitCone_pt, Functor.const_obj_obj,
        Types.Small.limitCone_π_app, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk,
        ← Shrink.algEquiv_apply R, AlgEquiv.commutes]

Goal state after:
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
j : J
this : Small.{w, max v w}
  ↑((F ⋙ forget₂ (AlgCat R) RingCat ⋙ forget₂ RingCat SemiRingCat) ⋙ forget SemiRingCat).sections :=
  limitπAlgHom._proof_1 F
x : R
⊢ ↑((algebraMap R ↑(F ⋙ forget (AlgCat R)).sections) x) j = (algebraMap R (ToType (F.obj j))) x
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Full
inst✝ : L.Faithful
⊢ IsIso (L.whiskerLeft h.counit)

Tactic:
by
  have := ((Functor.associator ..).inv ≫ whiskerRight (inv h.unit) L) ≫= h.left_triangle
  simp only [assoc, ← whiskerRight_comp_assoc, IsIso.inv_hom_id, whiskerRight_id', id_comp,
    Iso.inv_hom_id_assoc] at this
  rw [this]
  infer_instance

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.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (F ⋙ G).obj x✝¹ ◁ (F ⋙ G).map x✝ ≫ μ G (F.obj x✝¹) (F.obj Y✝) ≫ G.map (μ F x✝¹ Y✝) =
    (μ G (F.obj x✝¹) (F.obj X✝) ≫ G.map (μ F x✝¹ X✝)) ≫ (F ⋙ G).map (x✝¹ ◁ x✝)

Tactic:
simp_rw [comp_obj, F.comp_map, μ_natural_right_assoc, assoc, ← G.map_comp, μ_natural_right]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
⊢ (associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom = tensorHom (rightUnitor M).hom (𝟙 N)

Tactic:
by
  ext : 1
  apply TensorProduct.ext_threefold
  intro x y
  exact TensorProduct.tmul_smul _ _

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h h' i i' : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
β : f' ≅ g'
θ : g' ⟶ h'
θs : h' ⟶ i'
ηθ : g ⊗ g' ⟶ h ⊗ h'
ηθs : h ⊗ h' ⟶ i ⊗ i'
ηθ₁ : g ⊗ g' ⟶ i ⊗ i'
ηθ₂ : f ⊗ f' ⟶ i ⊗ i'
e_ηθ : η ⊗ₘ θ = ηθ
e_ηθs : ηs ⊗ₘ θs = ηθs
e_ηθ₁ : ηθ ≫ ηθs = ηθ₁
e_ηθ₂ : (α ⊗ᵢ β).hom ≫ ηθ₁ = ηθ₂
⊢ α.hom ≫ η ≫ ηs ⊗ₘ β.hom ≫ θ ≫ θs = ηθ₂

Tactic:
by
  simp [← e_ηθ, ← e_ηθs, ← e_ηθ₁, ← e_ηθ₂]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ HasWidePushouts Cᵒᵖ ↔ HasWidePullbacks C

Tactic:
refine ⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩
  rw [← hasColimitsOfShape_opposite_opposite_iff]
  exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm

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:
by
        rintro (_ | _ | _) <;> dsimp <;>
          simp only [Category.comp_id, Category.id_comp, ← G.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case comp_of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
g✝ : Y✝ ⟶ Z✝
x✝ y✝ z✝ : C
f' : x✝ ⟶ y✝
g : y✝ ⟶ z✝
hf' : W.multiplicativeClosure f'
hg : W g
h_rec : ∀ (f : X✝ ⟶ x✝), W.multiplicativeClosure f → W.multiplicativeClosure (f ≫ f')
f : X✝ ⟶ x✝
hf : W.multiplicativeClosure f
⊢ W.multiplicativeClosure (f ≫ f' ≫ g)

Tactic:
← Category.assoc

Goal state after:
case comp_of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
g✝ : Y✝ ⟶ Z✝
x✝ y✝ z✝ : C
f' : x✝ ⟶ y✝
g : y✝ ⟶ z✝
hf' : W.multiplicativeClosure f'
hg : W g
h_rec : ∀ (f : X✝ ⟶ x✝), W.multiplicativeClosure f → W.multiplicativeClosure (f ≫ f')
f : X✝ ⟶ x✝
hf : W.multiplicativeClosure f
⊢ W.multiplicativeClosure ((f ≫ f') ≫ g)