mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : ↥(𝒜 0)
⊢ (projZeroRingHom' 𝒜) ↑a = a

Tactic:
by

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
N' : Type u_8
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
Q : QuadraticMap R M N
⊢ (f.compQuadraticMap' Q).polarBilin = compr₂ Q.polarBilin f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a b : A
n i : ι
a_mem : a ∈ 𝒜 i
h : ¬i ≤ n
⊢ ↑(((decompose 𝒜) (a * b)) n) = 0

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✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Invertible 2
⊢ ⟨⅟2, ⋯⟩ • 1 * 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a b : A
n i : ι
b_mem : b ∈ 𝒜 i
h : ¬i ≤ n
⊢ ↑(((decompose 𝒜) (a * b)) n) = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
z : ℤ
⊢ ↑z ∈ A 0

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✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Invertible 2
⊢ 2 * ⟨⅟2, ⋯⟩ • 1 = 1

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✝⁹ : 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
x✝³ x✝² : QuadraticMap R M N
x✝¹ x✝ : M
⊢ ((⅟2 • (x✝³ + x✝²).polarBilin) x✝¹) x✝ = ((⅟2 • x✝³.polarBilin + ⅟2 • x✝².polarBilin) x✝¹) x✝

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹⁰ : Semiring A
inst✝⁹ : DecidableEq ι
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : PartialOrder ι
inst✝⁶ : CanonicallyOrderedAdd ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
a b : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
a_mem : a ∈ 𝒜 i
h : i ≤ n
⊢ ↑(((decompose 𝒜) (a * b)) n) = a * ↑(((decompose 𝒜) b) (n - i))

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✝⁹ : 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
x✝³ : S
x✝² : QuadraticMap R M N
x✝¹ x✝ : M
⊢ ((⅟2 • (x✝³ • x✝²).polarBilin) x✝¹) x✝ = (((RingHom.id S) x✝³ • ⅟2 • x✝².polarBilin) x✝¹) x✝

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹⁰ : Semiring A
inst✝⁹ : DecidableEq ι
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : PartialOrder ι
inst✝⁶ : CanonicallyOrderedAdd ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
a b : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
b_mem : b ∈ 𝒜 i
h : i ≤ n
⊢ ↑(((decompose 𝒜) (a * b)) n) = ↑(((decompose 𝒜) a) (n - i)) * b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹¹ : Semiring A
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommMonoid ι
inst✝⁸ : PartialOrder ι
inst✝⁷ : CanonicallyOrderedAdd ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a b : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
a_mem : a ∈ 𝒜 i
⊢ ↑(((decompose 𝒜) (a * b)) n) = if i ≤ n then a * ↑(((decompose 𝒜) b) (n - i)) else 0

Tactic:
by

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✝⁹ : 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
⊢ 2 • (associatedHom S) Q = Q.polarBilin

Tactic:
by

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✝⁹ : 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 y : M
⊢ (((associatedHom S) Q) x) y = (((associatedHom S) Q) y) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹¹ : Semiring A
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommMonoid ι
inst✝⁸ : PartialOrder ι
inst✝⁷ : CanonicallyOrderedAdd ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a b : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
b_mem : b ∈ 𝒜 i
⊢ ↑(((decompose 𝒜) (a * b)) n) = if i ≤ n then ↑(((decompose 𝒜) a) (n - i)) * b else 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι✝ : Type u_1
R✝ : Type u_2
A✝ : Type u_3
σ : Type u_4
R : Type u_5
inst✝⁵ : CommSemiring R
A : Type u_6
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
ι : Type u_7
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
M : ι → Submodule R A
inst✝ : SetLike.GradedMonoid M
hM : IsInternal M
r : R
⊢ (RingEquiv.ofBijective (coeAlgHom M) hM).toFun ((algebraMap R (⨁ (i : ι), ↥(M i))) r) = (algebraMap R A) r

Tactic:
by

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✝⁹ : 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
⊢ LinearMap.flip ((associatedHom S) Q) = (associatedHom S) Q

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ↑((r * r') n) = ∑ ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with ij.1 + ij.2 = n, ↑(r ij.1) * ↑(r' ij.2)

Tactic:
by

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✝¹¹ : 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
N' : Type u_8
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N' →ₗ[R] M
⊢ (associatedHom S) (Q.comp f) = LinearMap.compl₁₂ ((associatedHom S) Q) f f

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
n' : Type u_13
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
⊢ ∀ (B B' : M₁ →ₗ[R] M₂ →ₗ[R] R), B = B' ↔ (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁ b₂) B'

Tactic:
by

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✝⁹ : 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
x y : M
⊢ (((associatedHom S) B.toQuadraticMap) x) y = ⅟2 • ((B x) y + (B y) x)

Tactic:
by

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✝⁹ : 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
⊢ (((associatedHom S) B₁.toQuadraticMap) x) y = (B₁ x) y

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
n' : Type u_13
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
⊢ ((toLinearMap₂ b₁ b₁) J).IsAdjointPair ((toLinearMap₂ b₂ b₂) J') ⇑((toLin b₁ b₂) A) ⇑((toLin b₂ b₁) A') ↔
    J.IsAdjointPair J' A A'

Tactic:
by

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✝⁹ : 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
hB₁ : LinearMap.flip B₁ = B₁
⊢ (associatedHom S) B₁.toQuadraticMap = B₁

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ↑((r * r') n) = DFinsupp.sum r fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : HasAntidiagonal ι
inst✝ : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
n : ι
x✝ : ι × ι
⊢ x✝ ∈ {ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' | ij.1 + ij.2 = n} → x✝ ∈ antidiagonal n

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : HasAntidiagonal ι
inst✝ : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ↑((r * r') n) = ∑ ij ∈ antidiagonal n, ↑(r ij.1) * ↑(r' ij.2)

Tactic:
by

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✝⁹ : 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
⊢ (((associatedHom S) Q) x) x = Q x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ (Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
⊢ (Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ A₁ ∈ pairSelfAdjointMatricesSubmodule J J₂ ↔ J.IsAdjointPair J₂ A₁ A₁

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ A₁ ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A₁

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ A₁ ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A₁

Tactic:
by

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✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
hB₁ : associated' Q ≠ 0
⊢ ∃ x, Q x ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_11
m : Type u_12
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix m n R
h : M.SeparatingLeft
⊢ ((Matrix.toLinearMap₂' R) M).SeparatingLeft

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_11
m : Type u_12
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix m n R
h : M.SeparatingRight
⊢ ((Matrix.toLinearMap₂' R) M).SeparatingRight

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_11
m : Type u_12
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix m n R
⊢ ((toLinearMap₂' R) M).SeparatingLeft ↔ M.SeparatingLeft

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_11
m : Type u_12
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix m n R
⊢ ((toLinearMap₂' R) M).SeparatingRight ↔ M.SeparatingRight

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ ↑(((of (fun i ↦ ↥(A i)) i) r * r') n) = ↑r * ↑(r' j)

Tactic:
by

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
f g : M →ₗ[R] R
⊢ associated (linMulLin f g) = ⅟2 • ((mul R R).compl₁₂ f g + (mul R R).compl₁₂ g f)

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✝⁸ : CommRing R
inst✝⁷ : DecidableEq m
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
M : Matrix m n R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ ((toLinearMap₂ b₁ b₂) M).SeparatingLeft ↔ M.SeparatingLeft

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ ↑((r * (of (fun i ↦ ↥(A i)) i) r') n) = ↑(r j) * ↑r'

Tactic:
coe_mul_apply_eq_dfinsuppSum,

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i_1 ri ↦
      DFinsupp.sum ((of (fun i ↦ ↥(A i)) i) r') fun j rj ↦ if i_1 + j = n then ↑ri * ↑rj else 0) =
    ↑(r j) * ↑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✝⁸ : CommRing R
inst✝⁷ : DecidableEq m
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
M : Matrix m n R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ ((toLinearMap₂ b₁ b₂) M).SeparatingRight ↔ M.SeparatingRight

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ associated sq = mul R R

Tactic:
by

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 : M
⊢ Q.IsOrtho 0 x

Tactic:
by

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 : M
⊢ Q.IsOrtho x 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✝⁸ : CommRing R
inst✝⁷ : DecidableEq m
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
M : Matrix m n R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ ((toLinearMap₂ b₁ b₂) M).Nondegenerate ↔ M.Nondegenerate

Tactic:
by

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 : M
⊢ Q.IsOrtho x y ↔ Q.IsOrtho y x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : IsDomain R
M : Matrix n n R
⊢ ((toLinearMap₂' R) M).Nondegenerate ↔ M.det ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : IsDomain R
M : Matrix n n R
⊢ ((toLinearMap₂' R) M).SeparatingLeft ↔ M.det ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : IsDomain R
M : Matrix n n R
⊢ ((toLinearMap₂' R) M).SeparatingRight ↔ M.det ≠ 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_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:
by

Goal state after:
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.SeparatingRight ↔ ((toMatrix₂ b b) B).det ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsCancelAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
⊢ B.toQuadraticMap.IsOrtho x y ↔ (B x) y = 0

Tactic:
by

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✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
Q : QuadraticMap R M N
x y : M
⊢ (Q.polarBilin x) y = 0 ↔ Q.IsOrtho x y

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_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.Nondegenerate ↔ ((toMatrix₂ b b) B).det ≠ 0

Tactic:
by

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✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
Q : QuadraticMap R M N
inst✝ : Invertible 2
x y : M
⊢ ((associated Q) x) y = 0 ↔ Q.IsOrtho x y

Tactic:
by

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✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
⊢ ¬Q.Anisotropic ↔ ∃ x, x ≠ 0 ∧ Q x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticMap R M R
hB : Q.Anisotropic
x : M
hx : ∀ (y : M), ((associated' Q) x) y = 0
⊢ Q x = 0

Tactic:
by

Goal state after: