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

Goal state before:
pp: ⊢ S⁻¹ = -S

Tactic:
by

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

Goal state before:
pp: ⊢ ↑T⁻¹ = !![1, -1; 0, 1]

Tactic:
by

Goal state after:
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
⊢ (toMatrix₂' R) (B.compl₁₂ l r) = (toMatrix' l)ᵀ * (toMatrix₂' R) B * toMatrix' r

Tactic:
by

Goal state after:
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 ∘ₗ f) = (toMatrix' f)ᵀ * (toMatrix₂' R) B

Tactic:
by

Goal state after:
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₂ f) = (toMatrix₂' R) B * toMatrix' f

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ ↑(T ^ n) = !![1, n; 0, 1]

Tactic:
by

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

Goal state before:
pp: n : ℤ
g : SL(2, ℤ)
⊢ ↑(T ^ n * g) 1 = ↑g 1

Tactic:
by

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

Goal state before:
pp: g : SL(2, ℤ)
⊢ ↑(T * g) 1 = ↑g 1

Tactic:
by

Goal state after:
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
M : Matrix n' n R
N : Matrix m m' R
⊢ M * (toMatrix₂' R) B * N = (toMatrix₂' R) (B.compl₁₂ (toLin' Mᵀ) (toLin' N))

Tactic:
by

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

Goal state before:
pp: g : SL(2, ℤ)
⊢ ↑(T⁻¹ * g) 1 = ↑g 1

Tactic:
by

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

Goal state before:
pp: ⊢ ↑S * ↑S = -1

Tactic:
by

Goal state after:
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
M : Matrix n' n R
⊢ M * (toMatrix₂' R) B = (toMatrix₂' R) (B ∘ₗ toLin' Mᵀ)

Tactic:
by

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

Goal state after:
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'
M : Matrix n m R
P : Matrix n n' R
Q : Matrix m m' R
⊢ (toMatrix₂' R) (((toLinearMap₂' R) M).compl₁₂ (toLin' P) (toLin' Q)) = (toMatrix₂' R) ((toLinearMap₂' R) (Pᵀ * M * Q))

Tactic:
by

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
⊢ (toMatrix₂ b₁ b₂) B i j = (B (b₁ i)) (b₂ j)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
x✝² x✝¹ x✝ : ⨁ (i : ι), A i
⊢ x✝² * (x✝¹ + x✝) = x✝² * x✝¹ + x✝² * x✝

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
x✝² x✝¹ x✝ : ⨁ (i : ι), A i
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
x✝ : ⨁ (i : ι), A i
⊢ 0 * x✝ = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
x✝ : ⨁ (i : ι), A i
⊢ x✝ * 0 = 0

Tactic:
by

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₂
M : Matrix n m N₂
i : n
j : m
⊢ i ∈ univ

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ ((mulHom A) ((of A i) a)) ((of A j) b) = (of A (i + j)) (GradedMonoid.GMul.mul a b)

Tactic:
by

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

Goal state before:
pp: ⊢ S • S • S • T • S • T • S = T⁻¹

Tactic:
by

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₂
M : Matrix n m N₂
i : n
j : m
k : n
x✝ : k ∈ univ
hk : k ≠ i
⊢ ∑ x, σ₁ ((Finsupp.single i 1) k) •> (Finsupp.single j 1) x •> M k x = 0

Tactic:
by

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

Goal state before:
pp: ⊢ S • S • S • T • S • T • S = T⁻¹

Tactic:
by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

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₂
M : Matrix n m N₂
i : n
j : m
⊢ j ∈ univ

Tactic:
by

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₂
M : Matrix n m N₂
i : n
j k : m
x✝ : k ∈ univ
hk : k ≠ j
⊢ σ₁ ((Finsupp.single i 1) i) •> (Finsupp.single j 1) k •> M i k = 0

Tactic:
by

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
⊢ 1 * x = x

Tactic:
by

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₂
M : Matrix n m N₂
i : n
j : m
⊢ (((toLinearMapₛₗ₂ σ₁ b₁ b₂) M) (b₁ i)) (b₂ j) = M i j

Tactic:
by

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
⊢ s • (x * y) = x * s • y

Tactic:
GAlgebra.smul_def,

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
s : R
x y : GradedMonoid A
⊢ GradedMonoid.mk 0 (GAlgebra.toFun s) * (x * y) = x * s • y
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) = x * s • y

Tactic:
GAlgebra.smul_def,

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
s : R
x y : GradedMonoid A
⊢ GradedMonoid.mk 0 (GAlgebra.toFun s) * (x * y) = x * (GradedMonoid.mk 0 (GAlgebra.toFun s) * y)
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
⊢ s • x • y = x • s • y

Tactic:
by

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
⊢ s • x * y = s • (x * y)

Tactic:
GAlgebra.smul_def,

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
s : R
x y : GradedMonoid A
⊢ GradedMonoid.mk 0 (GAlgebra.toFun s) * x * y = s • (x * y)
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 = s • (x * y)

Tactic:
GAlgebra.smul_def,

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
s : R
x y : GradedMonoid A
⊢ GradedMonoid.mk 0 (GAlgebra.toFun s) * x * y = GradedMonoid.mk 0 (GAlgebra.toFun s) * (x * y)
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
⊢ (s • x) • y = s • x • y

Tactic:
by

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
⊢ x * 1 = x

Tactic:
by

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).comp GAlgebra.toFun) (a * b) = ((of A 0).comp GAlgebra.toFun) a * ((of A 0).comp GAlgebra.toFun) b

Tactic:
by

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
a b c : ⨁ (i : ι), A i
this : AddMonoidHom.mulLeft₃ = AddMonoidHom.mulRight₃
⊢ a * b * c = a * (b * c)

Tactic:
by

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
a b c : ⨁ (i : ι), A i
⊢ a * b * c = a * (b * c)

Tactic:
by

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
⊢ ↑0 = 0

Tactic:
by

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_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
⊢ ⇑σ₁ ∘ x ⬝ᵥ (toMatrix₂ b₁ b₂) B *ᵥ ⇑σ₂ ∘ y = (B (b₁.equivFun.symm x)) (b₂.equivFun.symm y)

Tactic:
by

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
n : ℕ
⊢ ↑(n + 1) = ↑n + 1

Tactic:
by

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 ι
r : R
x : ⨁ (i : ι), A i
⊢ { toFun := ⇑((of A 0).comp GAlgebra.toFun), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x =
    x * { toFun := ⇑((of A 0).comp GAlgebra.toFun), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r

Tactic:
by

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
i : ι
a : A i
n : ℕ
⊢ (of A i) a ^ n = (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)

Tactic:
by

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_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₂
this :
  ∑ j, ∑ i, σ₂ ((b₂.repr y) j) * σ₁ ((b₁.repr x) i) * (B (b₁ i)) (b₂ j) =
    ∑ i, ∑ j, σ₁ ((b₁.repr x) i) * σ₂ ((b₂.repr y) j) * (B (b₁ i)) (b₂ j)
⊢ (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:
by

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
α : Type u_3
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ (of A (l.dProdIndex fι)) (l.dProd fι fA) = (List.map (fun a ↦ (of A (fι a)) (fA a)) l).prod

Tactic:
induction l with
  | nil => simp only [List.map_nil, List.prod_nil, List.dProd_nil]; rfl
  | cons head tail =>
    rename_i ih
    simp only [List.map_cons, List.prod_cons, List.dProd_cons, ← ih]
    rw [DirectSum.of_mul_of (fA head)]
    rfl

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
α : Type u_3
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ (of A (l.dProdIndex fι)) (l.dProd fι fA) = (List.map (fun a ↦ (of A (fι a)) (fA a)) l).prod

Tactic:
by

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_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 x) y = ⇑σ₁ ∘ ⇑(b₁.repr x) ⬝ᵥ (toMatrix₂ b₁ b₂) B *ᵥ ⇑σ₂ ∘ ⇑(b₂.repr y)

Tactic:
by

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
n : ℕ
fι : Fin n → ι
fA : (a : Fin n) → A (fι a)
⊢ (List.ofFn fun a ↦ (of A (fι a)) (fA a)).prod =
    (of A ((List.finRange n).dProdIndex fι)) ((List.finRange n).dProd fι fA)

Tactic:
by

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
⊢ (toMatrix₂Aux R ⇑b₁ ⇑b₂) B i j = (toMatrix₂ b₁ b₂) B i j

Tactic:
by

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 ι
r : R
x : ⨁ (i : ι), A i
⊢ r • x =
    { toFun := ⇑((of A 0).comp GAlgebra.toFun), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x

Tactic:
by

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 + polar f x y

Tactic:
by

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 g : M → N
x y : M
⊢ polar (f + g) x y = polar f x y + polar g x y

Tactic:
by

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
⊢ polar (-f) x y = -polar f x y

Tactic:
by

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

Goal state before:
pp: S : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Monoid S
inst✝ : DistribMulAction S N
f : M → N
s : S
x y : M
⊢ polar (s • f) x y = s • polar f x y

Tactic:
by

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
⊢ toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) = toLinearMap₂' R

Tactic:
by

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
⊢ polar f x y = polar f y x

Tactic:
by

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 x' y : M
⊢ polar f (x + x') y = polar f x y + polar f x' y ↔
    f (x + x' + y) + (f x + f x' + f y) = f (x + x') + f (x' + y) + f (y + x)

Tactic:
by

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

Goal state before:
pp: S : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
F : Type u_8
inst✝² : AddCommGroup S
inst✝¹ : FunLike F N S
inst✝ : AddMonoidHomClass F N S
f : M → N
g : F
x y : M
⊢ polar (⇑g ∘ f) x y = g (polar f x y)

Tactic:
by

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

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q Q' x y : QuadraticMap R M N
h : x.toFun = y.toFun
⊢ x = y

Tactic:
by

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
⊢ toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) = toMatrix₂' R

Tactic:
by

Goal state after: