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

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (n' → R) →ₗ[R] n → R
⊢ (toMatrix₂' R) (B.compl₁₂ f id) = (toMatrix' f)ᵀ * (toMatrix₂' R) B

Tactic:
]

Goal state after:
n : Type u_11
m : Type u_12
n' : Type u_13
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (n' → R) →ₗ[R] n → R
⊢ (toMatrix₂' R) (B.compl₁₂ f id) = (toMatrix' f)ᵀ * (toMatrix₂' R) B
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
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 m'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (m' → R) →ₗ[R] m → R
⊢ (toMatrix₂' R) (B.compl₁₂ id f) = (toMatrix₂' R) (B ∘ₗ id) * toMatrix' f

Tactic:
]

Goal state after:
n : Type u_11
m : Type u_12
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 m'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (m' → R) →ₗ[R] m → R
⊢ (toMatrix₂' R) (B.compl₁₂ id f) = (toMatrix₂' R) (B ∘ₗ id) * toMatrix' f
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
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 m'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
M : Matrix m m' R
⊢ (toMatrix₂' R) B * M = (toMatrix₂' R) (B.compl₂ (toLin' M))

Tactic:
by
  simp only [B.toMatrix₂'_compl₂, toMatrix'_toLin']

Goal state after:
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
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A (0 + i)) (GradedMonoid.GMul.mul GradedMonoid.GOne.one xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A (0 + i)) (GradedMonoid.GMul.mul GradedMonoid.GOne.one xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
σ₁ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
⊢ σ₁ ((Finsupp.single i 1) i) •> (Finsupp.single j 1) j •> M i j = M i j

Tactic:
]

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
σ₁ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
⊢ σ₁ ((Finsupp.single i 1) i) •> (Finsupp.single j 1) j •> M i j = M i 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
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A (i + 0)) (GradedMonoid.GMul.mul xi GradedMonoid.GOne.one) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A (i + 0)) (GradedMonoid.GMul.mul xi GradedMonoid.GOne.one) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
s : R
x y : GradedMonoid A
⊢ x * (GradedMonoid.mk 0 (GAlgebra.toFun s) * y) = x * (GradedMonoid.mk 0 (GAlgebra.toFun s) * y)

Tactic:
]

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

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
s : R
x y : GradedMonoid A
⊢ GradedMonoid.mk 0 (GAlgebra.toFun s) * x * y = GradedMonoid.mk 0 (GAlgebra.toFun s) * x * y

Tactic:
]

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

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
a b : R
⊢ (of A 0) (GAlgebra.toFun (a * b)) = (of A (0 + 0)) (GradedMonoid.GMul.mul (GAlgebra.toFun a) (GAlgebra.toFun b))

Tactic:
]

Goal state after:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
a b : R
⊢ (of A 0) (GAlgebra.toFun (a * b)) = (of A (0 + 0)) (GradedMonoid.GMul.mul (GAlgebra.toFun a) (GAlgebra.toFun b))
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
σ₁ σ₂ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : n → R
y : m → R
⊢ ∑ y_1, ∑ x_1, σ₁ (x x_1) * (σ₂ (y y_1) * (B (b₁ x_1)) (b₂ y_1)) =
    ∑ x_1, ∑ i, σ₂ (y x_1) * (σ₁ (x i) * (B (b₁ i)) (b₂ x_1))

Tactic:
]

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
σ₁ σ₂ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : n → R
y : m → R
⊢ ∑ y_1, ∑ x_1, σ₁ (x x_1) * (σ₂ (y y_1) * (B (b₁ x_1)) (b₂ y_1)) =
    ∑ x_1, ∑ i, σ₂ (y x_1) * (σ₁ (x i) * (B (b₁ i)) (b₂ x_1))
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
n : ℕ
⊢ (of A 0) (GSemiring.natCast n) + (of A 0) GradedMonoid.GOne.one = (of A 0) (GSemiring.natCast n) + 1

Tactic:
]

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
n : ℕ
⊢ (of A 0) (GSemiring.natCast n) + (of A 0) GradedMonoid.GOne.one = (of A 0) (GSemiring.natCast n) + 1
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A (0 + i)) (GradedMonoid.GMul.mul (GAlgebra.toFun r) xi) =
    (of A (i + 0)) (GradedMonoid.GMul.mul xi (GAlgebra.toFun r))

Tactic:
]

Goal state after:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A (0 + i)) (GradedMonoid.GMul.mul (GAlgebra.toFun r) xi) =
    (of A (i + 0)) (GradedMonoid.GMul.mul xi (GAlgebra.toFun r))
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
σ₁ σ₂ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : M₁
y : M₂
⊢ (B (∑ i, (b₁.repr x) i •> b₁ i)) (∑ i, (b₂.repr y) i •> b₂ i) =
    ⇑σ₁ ∘ ⇑(b₁.repr x) ⬝ᵥ (toMatrix₂ b₁ b₂) B *ᵥ ⇑σ₂ ∘ ⇑(b₂.repr y)

Tactic:
]

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
σ₁ σ₂ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : M₁
y : M₂
⊢ (B (∑ i, (b₁.repr x) i •> b₁ i)) (∑ i, (b₂.repr y) i •> b₂ i) =
    ⇑σ₁ ∘ ⇑(b₁.repr x) ⬝ᵥ (toMatrix₂ b₁ b₂) B *ᵥ ⇑σ₂ ∘ ⇑(b₂.repr y)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : (of A i) a ^ n = (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ (of A (n • i + i)) (GradedMonoid.GMul.mul (GradedMonoid.GMonoid.gnpow n a) a) =
    (of A ((n + 1) • i)) (GradedMonoid.GMonoid.gnpow (n + 1) a)

Tactic:
]

Goal state after:
case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : (of A i) a ^ n = (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ (of A (n • i + i)) (GradedMonoid.GMul.mul (GradedMonoid.GMonoid.gnpow n a) a) =
    (of A ((n + 1) • i)) (GradedMonoid.GMonoid.gnpow (n + 1) a)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih : (of A (tail.dProdIndex fι)) (tail.dProd fι fA) = (List.map (fun a ↦ (of A (fι a)) (fA a)) tail).prod
⊢ (of A ((head :: tail).dProdIndex fι)) (GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA)) =
    (of A (fι head + tail.dProdIndex fι)) (GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA))

Tactic:
]

Goal state after:
case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih : (of A (tail.dProdIndex fι)) (tail.dProd fι fA) = (List.map (fun a ↦ (of A (fι a)) (fA a)) tail).prod
⊢ (of A ((head :: tail).dProdIndex fι)) (GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA)) =
    (of A (fι head + tail.dProdIndex fι)) (GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA))
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A i) (r • xi) = (of A (0 + i)) (GradedMonoid.GMul.mul (GAlgebra.toFun r) xi)

Tactic:
]

Goal state after:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A i) (r • xi) = (of A (0 + i)) (GradedMonoid.GMul.mul (GAlgebra.toFun r) xi)
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
n : ℕ
fι : Fin n → ι
fA : (a : Fin n) → A (fι a)
⊢ (List.map (fun a ↦ (of A (fι a)) (fA a)) (List.finRange n)).prod =
    (List.map (fun a ↦ (of A (fι a)) (fA a)) (List.finRange n)).prod

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
σ₁ σ₂ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂
i : n
j : m
⊢ (B (b₁ i)) (b₂ j) = (B (b₁ i)) (b₂ j)

Tactic:
]

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ f (x + y) = f x + f y + (f (x + y) - f x - f y)

Tactic:
]

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ f (x + y) = f x + f y + (f (x + y) - f x - f y)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ f (y + x) - (f y + f x) = f (y + x) - (f y + f x)

Tactic:
]

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

Tactic:
]

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: M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x x' y : M
⊢ f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y) ↔
    f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
B : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂
i✝ : n
j✝ : m
⊢ (B (Pi.single i✝ 1)) (Pi.single j✝ 1) = (B (Pi.single i✝ 1)) (Pi.single j✝ 1)

Tactic:
]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (x + z)

Tactic:
]

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (x + z)
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.sum a fun a b ↦ ((toAddMonoid fun x ↦ ((compHom (of A (a + x))).comp (gMulHom A)).flip).flip b) 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:
]

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.sum a fun a b ↦ ((toAddMonoid fun x ↦ ((compHom (of A (a + x))).comp (gMulHom A)).flip).flip b) 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✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ (2 * 2) • Q x = ↑4 • Q x

Tactic:
]

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ (2 * 2) • Q x = ↑4 • Q x
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
f : (i : ι) → A i →ₗ[R] B
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
r : R
⊢ r • 1 = r • 1

Tactic:
]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
⊢ 0 = 0

Tactic:
]

Goal state after:
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✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
Q : QuadraticMap R M N
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : SMul S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
a : S
x : M
⊢ (a * a) • Q x = (a * a) • Q x

Tactic:
]

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'
⊢ (B (l (b₁' i))) (r (b₂' j)) = ∑ y, ∑ x, (b₁.repr (l (b₁' i))) y * (B (b₁ y)) (b₂ x) * (b₂.repr (r (b₂' j))) x

Tactic:
]

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'
⊢ (B (l (b₁' i))) (r (b₂' j)) = ∑ y, ∑ x, (b₁.repr (l (b₁' i))) y * (B (b₁ y)) (b₂ x) * (b₂.repr (r (b₂' j))) x
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 : M
⊢ Q x = Q x

Tactic:
]

Goal state after:
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 : M
⊢ Q (y - x) = Q (y - x)

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
this : mulHom A = (mulHom A).flip
⊢ b * a = b * a

Tactic:
]

Goal state after:
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 : M
⊢ -polar (⇑Q) x y = -polar (⇑Q) x y

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
⊢ (of A (ai + bi)) (GradedMonoid.GMul.mul ax bx) = (of A (bi + ai)) (GradedMonoid.GMul.mul bx ax)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
⊢ (of A (ai + bi)) (GradedMonoid.GMul.mul ax bx) = (of A (bi + ai)) (GradedMonoid.GMul.mul bx ax)
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 x' y : M
⊢ polar (⇑Q) x y + -polar (⇑Q) x' y = polar (⇑Q) x y + -polar (⇑Q) x' y

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
i : ι
x : ↥(ℳ i)
⊢ (of (fun i ↦ ↥(ℳ i)) i) x = (of (fun i ↦ ↥(ℳ i)) i) x

Tactic:
]

Goal state after: