mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x✝¹ : n
x✝ : x✝¹ ∈ univ
⊢ ∑ j, v x✝¹ •> w j •> M x✝¹ j = ∑ i, v x✝¹ * (M x✝¹ i * w i)

Tactic:
refine Finset.sum_congr rfl fun _ _ => ?_

Goal state after:
n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ v x✝³ •> w x✝¹ •> M x✝³ x✝¹ = v x✝³ * (M x✝³ x✝¹ * w x✝¹)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ (∑ i_1,
      ((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj ↦
        ((Pi.basisFun R n).repr (l (Pi.single i 1))) i_1 •> yj •> (B ((Pi.basisFun R n) i_1)) ((Pi.basisFun R m) j)) =
    ∑ y,
      ∑ x,
        of (fun i j ↦ l (Pi.single j 1) i) y i * (B (Pi.single y 1)) (Pi.single x 1) *
          of (fun i j ↦ r (Pi.single j 1) i) x j

Tactic:
apply sum_congr rfl

Goal state after:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ ∀ x ∈ univ,
    (((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj ↦
        ((Pi.basisFun R n).repr (l (Pi.single i 1))) x •> yj •> (B ((Pi.basisFun R n) x)) ((Pi.basisFun R m) j)) =
      ∑ x_1,
        of (fun i j ↦ l (Pi.single j 1) i) x i * (B (Pi.single x 1)) (Pi.single x_1 1) *
          of (fun i j ↦ r (Pi.single j 1) i) x_1 j
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∑ i_1,
      ((Pi.basisFun R n).repr (l (Pi.single i 1))) i' •>
        ((Pi.basisFun R m).repr (r (Pi.single j 1))) i_1 •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) i_1) =
    ∑ x,
      of (fun i j ↦ l (Pi.single j 1) i) i' i * (B (Pi.single i' 1)) (Pi.single x 1) *
        of (fun i j ↦ r (Pi.single j 1) i) x j

Tactic:
apply sum_congr rfl

Goal state after:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∀ x ∈ univ,
    ((Pi.basisFun R n).repr (l (Pi.single i 1))) i' •>
        ((Pi.basisFun R m).repr (r (Pi.single j 1))) x •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) x) =
      of (fun i j ↦ l (Pi.single j 1) i) i' i * (B (Pi.single i' 1)) (Pi.single x 1) *
        of (fun i j ↦ r (Pi.single j 1) i) x j
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ ((DFinsupp.liftAddHom fun x ↦ (toAddMonoid fun x_1 ↦ ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip) a) a' =
    DFinsupp.sum a fun x ai ↦ DFinsupp.sum a' fun x_1 aj ↦ (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Tactic:
DFinsupp.liftAddHom_apply

Goal state after:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ ((DFinsupp.sumAddHom fun x ↦ (toAddMonoid fun x_1 ↦ ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip) a) a' =
    DFinsupp.sum a fun x ai ↦ DFinsupp.sum a' fun x_1 aj ↦ (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x y y' : M
⊢ polar (⇑Q) x (y + y') = polar (⇑Q) x y + polar (⇑Q) x y'

Tactic:
by
  rw [polar_comm Q x, polar_comm Q x, polar_comm Q x, polar_add_left]

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ (∑ i_1, (b₂.repr (r (b₂' j))).sum fun j yj ↦ (b₁.repr (l (b₁' i))) i_1 •> yj •> (B (b₁ i_1)) (b₂ j)) =
    ∑ y, ∑ x, (b₁.repr (l (b₁' i))) y * (B (b₁ y)) (b₂ x) * (b₂.repr (r (b₂' j))) x

Tactic:
apply sum_congr rfl

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ ∀ x ∈ univ,
    ((b₂.repr (r (b₂' j))).sum fun j yj ↦ (b₁.repr (l (b₁' i))) x •> yj •> (B (b₁ x)) (b₂ j)) =
      ∑ x_1, (b₁.repr (l (b₁' i))) x * (B (b₁ x)) (b₂ x_1) * (b₂.repr (r (b₂' j))) x_1
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∑ i_1, (b₁.repr (l (b₁' i))) i' •> (b₂.repr (r (b₂' j))) i_1 •> (B (b₁ i')) (b₂ i_1) =
    ∑ x, (b₁.repr (l (b₁' i))) i' * (B (b₁ i')) (b₂ x) * (b₂.repr (r (b₂' j))) x

Tactic:
apply sum_congr rfl

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∀ x ∈ univ,
    (b₁.repr (l (b₁' i))) i' •> (b₂.repr (r (b₂' j))) x •> (B (b₁ i')) (b₂ x) =
      (b₁.repr (l (b₁' i))) i' * (B (b₁ i')) (b₂ x) * (b₂.repr (r (b₂' j))) x
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
B₁ : BilinMap R M N
h : ∀ (x y : M), (B₁ x) y = (B₁ y) x
x y : M
⊢ 2 • (B₁ x) y = 2 • (B₁ x) y

Tactic:
two_smul,

Goal state after:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
B₁ : BilinMap R M N
h : ∀ (x y : M), (B₁ x) y = (B₁ y) x
x y : M
⊢ (B₁ x) y + (B₁ x) y = 2 • (B₁ x) y
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x : M
⊢ ⅟2 • 2 • Q x = Q x

Tactic:
two_smul,

Goal state after:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x : M
⊢ ⅟2 • (Q x + Q x) = Q x
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x : M
⊢ 2 • Q x = 2 • Q x

Tactic:
two_smul,

Goal state after:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x : M
⊢ Q x + Q x = 2 • Q x
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
m : Type u_12
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : IsDomain R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
b : Basis m R M₁
B : M₁ →ₗ[R] M₁ →ₗ[R] R
⊢ B.SeparatingLeft ↔ ((toMatrix₂ b b) B).det ≠ 0

Tactic:
← Matrix.separatingLeft_iff_det_ne_zero,

Goal state after:
R : Type u_1
M₁ : Type u_6
m : Type u_12
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : IsDomain R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
b : Basis m R M₁
B : M₁ →ₗ[R] M₁ →ₗ[R] R
⊢ B.SeparatingLeft ↔ ((toMatrix₂ b b) B).SeparatingLeft
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
f : (n → R) →ₗ[R] n → R
⊢ discr' (QuadraticMap.comp Q f) = (LinearMap.toMatrix' f).det * (LinearMap.toMatrix' f).det * Q.discr'

Tactic:
by
  simp [mul_left_comm, toMatrix'_comp, mul_comm, discr']

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

Goal state before:
pp: case succ.inl
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hd : finrank K V = d + 1
hB₂ : IsSymm 0
b : Basis (Fin (d + 1)) K V
⊢ ∃ v, IsOrthoᵢ 0 ⇑v

Tactic:
exact ⟨b, fun i j _ => rfl⟩

Goal state after:
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case pos
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
h : i ≤ n
⊢ ↑(((of (fun i ↦ ↥(A i)) i) r * r') n) = ↑r * ↑(r' (n - i))

pp: case neg
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
h : ¬i ≤ n
⊢ ↑(((of (fun i ↦ ↥(A i)) i) r * r') n) = 0

Tactic:
exacts [coe_of_mul_apply_of_le _ _ _ n h, coe_of_mul_apply_of_not_le _ _ _ n h]

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

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
p : Fin (n + 1)
f : M p →ₗ[R] MultilinearMap R (fun i ↦ M (p.succAbove i)) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
x y : M i
⊢ (f (update m i (x + y) p)) (p.removeNth (update m i (x + y))) =
    (f (update m i x p)) (p.removeNth (update m i x)) + (f (update m i y p)) (p.removeNth (update m i y))

Tactic:
by cases i using Fin.succAboveCases p <;> simp

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

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
p : Fin (n + 1)
f : M p →ₗ[R] MultilinearMap R (fun i ↦ M (p.succAbove i)) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
x : R
y : M i
⊢ (f (update m i (x • y) p)) (p.removeNth (update m i (x • y))) = x • (f (update m i y p)) (p.removeNth (update m i y))

Tactic:
by cases i using Fin.succAboveCases p <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.mem_mul.mem_mul_mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
m₁ : M
hm : (ι Q) m₁ ∈ (ι Q).range
m₂ : M
hn : (ι Q) m₂ ∈ (ι Q).range
⊢ motive ((ι Q) m₁ * (ι Q) m₂ * y * b) ⋯

Tactic:
simp_rw [mul_assoc _ y b]

Goal state after:
case mem_mul_mem.mem_mul.mem_mul_mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
m₁ : M
hm : (ι Q) m₁ ∈ (ι Q).range
m₂ : M
hn : (ι Q) m₂ ∈ (ι Q).range
⊢ motive ((ι Q) m₁ * (ι Q) m₂ * (y * b)) ⋯
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.mem_mul.add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝¹ : CliffordAlgebra Q
hx✝ : x✝¹ ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x✝ : CliffordAlgebra Q
n'' : ℕ
y✝ : CliffordAlgebra Q
hy✝ : y✝ ∈ ((ι Q).range ^ 2) ^ n''
ihy✝ : motive (y✝ * b) ⋯
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range * (ι Q).range
y : CliffordAlgebra Q
hy : y ∈ (ι Q).range * (ι Q).range
ihx : motive (x * y✝ * b) ⋯
ihy : motive (y * y✝ * b) ⋯
⊢ motive ((x + y) * y✝ * b) ⋯

Tactic:
| add x hx y hy ihx ihy =>

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

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ExteriorAlgebra R M →ₗ[R] M

Tactic:
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)

Goal state after:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
this : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
⊢ ExteriorAlgebra R M →ₗ[R] M
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
hv : LinearIndependent R v
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
hm : Mono S.f
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ LinearIndependent R u

Tactic:
linearIndependent_sum

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
hv : LinearIndependent R v
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
hm : Mono S.f
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ LinearIndependent R (u ∘ Sum.inl) ∧
    LinearIndependent R (u ∘ Sum.inr) ∧ Disjoint (span R (range (u ∘ Sum.inl))) (span R (range (u ∘ Sum.inr)))
Module: Mathlib.Algebra.Category.ModuleCat.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v', u'} R'
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
⊢ injectiveDimension M = injectiveDimension N

Tactic:
refine eq_of_forall_ge_iff (fun N ↦ ?_)
  induction N with
  | bot => simpa [injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton] using
      e.subsingleton_congr
  | coe n =>
    induction n with
    | top => simp
    | coe n =>
      simp [injectiveDimension_le_iff, hasInjectiveDimensionLE_iff_of_semiLinearEquiv eR e n]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsInitial x
⊢ IsConnected C

Tactic:
let : Nonempty C := ⟨x⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsInitial x
this : Nonempty C := Nonempty.intro x
⊢ IsConnected C
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsTerminal x
⊢ IsConnected C

Tactic:
let : Nonempty C := ⟨x⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsTerminal x
this : Nonempty C := Nonempty.intro x
⊢ IsConnected C
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
⊢ ∀ ⦃X Y : P.FullSubcategory⦄ (f g : X ⟶ Y), ∃ Z h, f ≫ h = g ≫ h

Tactic:
by
          rintro ⟨X, hX⟩ ⟨Y, hY⟩ ⟨f₁ : X ⟶ Y⟩ ⟨f₂ : X ⟶ Y⟩
          obtain ⟨Z, hZ, ⟨g⟩⟩ := hP (coeq f₁ f₂)
          exact ⟨⟨Z, hZ⟩, ObjectProperty.homMk (coeqHom f₁ f₂ ≫ g),
            ObjectProperty.hom_ext _ (coeq_condition_assoc _ _ _) ⟩

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

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
Q : DiagramOfCones (curry.obj G) := DiagramOfCones.mkOfHasLimits (curry.obj G)
x y : J × K
x✝ : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this : (Q.obj x.1).π.app x.2 ≫ ((curry.obj G).obj x.1).map f₂ = (Q.obj x.1).π.app y.2
⊢ ((const (J × K)).obj (limit (curry.obj G ⋙ lim))).map (f₁, f₂) ≫
      limit.π (curry.obj G ⋙ lim) y.1 ≫ (Q.obj y.1).π.app y.2 =
    (limit.π (curry.obj G ⋙ lim) x.1 ≫ (Q.obj x.1).π.app x.2) ≫ G.map (f₁, f₂)

Tactic:
dsimp [Q] at this ⊢

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
Q : DiagramOfCones (curry.obj G) := DiagramOfCones.mkOfHasLimits (curry.obj G)
x y : J × K
x✝ : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this : limit.π ((curry.obj G).obj x.1) x.2 ≫ G.map (Prod.mkHom (𝟙 x.1) f₂) = limit.π ((curry.obj G).obj x.1) y.2
⊢ 𝟙 (limit (curry.obj G ⋙ lim)) ≫ limit.π (curry.obj G ⋙ lim) y.1 ≫ limit.π ((curry.obj G).obj y.1) y.2 =
    (limit.π (curry.obj G ⋙ lim) x.1 ≫ limit.π ((curry.obj G).obj x.1) x.2) ≫ G.map (f₁, f₂)