awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
n : Type u_2
inst : DecidableEq n
R : Type u_3
inst_1 : NonAssocSemiring R
inst_2 : StarRing R
i j : n
⊢ (swap R i j)ᴴ = swap R i j

Tactic:
simp [swap]

Premises used: Matrix.swap
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
S : Type u_4
inst_2 : NonAssocSemiring S
f : R →+* S
i j : n
⊢ (swap R i j).map (⇑f : (a : R) → S) = swap S i j

Tactic:
simp [swap]

Premises used: Matrix.swap
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
a : n → R
⊢ swap R i j *ᵥ a = a ∘ (⇑(Equiv.swap i j) : (a : n) → n)

Tactic:
simp [swap, PEquiv.toMatrix_toPEquiv_mulVec]

Premises used: PEquiv.toMatrix_toPEquiv_mulVec, Matrix.swap
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
a : n → R
⊢ a ᵥ* swap R i j = a ∘ (⇑(Equiv.swap i j) : (a : n) → n)

Tactic:
simp [swap, PEquiv.vecMul_toMatrix_toPEquiv]

Premises used: PEquiv.vecMul_toMatrix_toPEquiv, Matrix.swap
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
a : n → R
⊢ (swap R i j *ᵥ a) i = a j

Tactic:
simp [swap, PEquiv.toMatrix_toPEquiv_mulVec]

Premises used: PEquiv.toMatrix_toPEquiv_mulVec, Matrix.swap
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
a : n → R
⊢ (a ᵥ* swap R i j) i = a j

Tactic:
simp [swap, PEquiv.vecMul_toMatrix_toPEquiv]

Premises used: PEquiv.vecMul_toMatrix_toPEquiv, Matrix.swap
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
m : Type u_3
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
a : m
g : Matrix n m R
⊢ (swap R i j * g) i a = g j a

Tactic:
simp [swap, PEquiv.toMatrix_toPEquiv_mul]

Premises used: PEquiv.toMatrix_toPEquiv_mul, Matrix.swap
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
m : Type u_3
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
a : m
g : Matrix n m R
rw : (swap R j i * g) j a = g i a
rw₁ rw₂ : g i a = g i a
⊢ (swap R i j * g) j a = g i a

Tactic:
rw [swap_comm, swap_mul_apply_left]

Premises used: Matrix.swap_mul_apply_left, Matrix.swap_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
m : Type u_3
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j a : n
b : m
hai : a ≠ i
haj : a ≠ j
g : Matrix n m R
⊢ (swap R i j * g) a b = g a b

Tactic:
simp [swap, PEquiv.toMatrix_toPEquiv_mul, Equiv.swap_apply_of_ne_of_ne hai haj]

Premises used: PEquiv.toMatrix_toPEquiv_mul, Equiv.swap_apply_of_ne_of_ne, Matrix.swap
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
m : Type u_3
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
a : m
g : Matrix m n R
⊢ (g * swap R i j) a i = g a j

Tactic:
simp [swap, PEquiv.mul_toMatrix_toPEquiv]

Premises used: Matrix.swap, PEquiv.mul_toMatrix_toPEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
m : Type u_3
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
a : m
g : Matrix m n R
rw : (g * swap R j i) a j = g a i
rw₁ rw₂ : g a i = g a i
⊢ (g * swap R i j) a j = g a i

Tactic:
rw [swap_comm, mul_swap_apply_left]

Premises used: Matrix.mul_swap_apply_left, Matrix.swap_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
m : Type u_3
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j b : n
a : m
hbi : b ≠ i
hbj : b ≠ j
g : Matrix m n R
⊢ (g * swap R i j) a b = g a b

Tactic:
simp [swap, PEquiv.mul_toMatrix_toPEquiv, Equiv.swap_apply_of_ne_of_ne hbi hbj]

Premises used: Equiv.swap_apply_of_ne_of_ne, Matrix.swap, PEquiv.mul_toMatrix_toPEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
simp : Equiv.Perm.permMatrix R (Equiv.swap i j) * Equiv.Perm.permMatrix R (Equiv.swap i j) = 1
⊢ swap R i j * swap R i j = 1

Tactic:
simp only [swap]

Premises used: Matrix.swap
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
rw : Equiv.Perm.permMatrix R (Equiv.symm (Equiv.swap i j)) * Equiv.Perm.permMatrix R (Equiv.symm (Equiv.swap i j)) = 1
⊢ Equiv.Perm.permMatrix R (Equiv.swap i j) * Equiv.Perm.permMatrix R (Equiv.swap i j) = 1

Tactic:
rw [← Equiv.swap_inv, Equiv.Perm.inv_def]

Premises used: Equiv.swap_inv, Equiv.Perm.inv_def
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
⊢ Equiv.Perm.permMatrix R (Equiv.symm (Equiv.swap i j)) * Equiv.Perm.permMatrix R (Equiv.symm (Equiv.swap i j)) = 1

Tactic:
simp [← PEquiv.toMatrix_trans, ← Equiv.toPEquiv_trans]

Premises used: Equiv.toPEquiv_trans, PEquiv.toMatrix_trans
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
S : Type u_3
inst_3 : CommRing S
f : R →+* S
i j : n
huv : (↑((map f : (a : GL n R) → GL n S) (swap R i j)) : Matrix n n S) = (↑(swap S i j) : Matrix n n S)
⊢ Eq (α := GL n S) ((map f : (a : GL n R) → GL n S) (swap R i j) : GL n S) (swap S i j : GL n S)

Tactic:
ext : 1
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
S : Type u_3
inst_3 : CommRing S
f : R →+* S
i j : n
⊢ (↑((map f : (a : GL n R) → GL n S) (swap R i j)) : Matrix n n S) = (↑(swap S i j) : Matrix n n S)

Tactic:
simp [swap]

Premises used: Matrix.GeneralLinearGroup.swap
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
A : Matrix n n α
h : A.IsSymm
⊢ Aᵀ = A

Tactic:
h

Premises used: Matrix.IsSymm
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
A : Matrix n n α
⊢ A.IsSymm ↔ ∀ (i j : n), A j i = A i j

Tactic:
Matrix.ext_iff.symm

Premises used: Matrix.transpose, Matrix.IsSymm, Matrix.ext_iff, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
A : Matrix n n α
⊢ (∀ (i j : n), A j i = A i j) → A.IsSymm

Tactic:
Matrix.ext

Premises used: Matrix.transpose, Matrix.IsSymm, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
A : Matrix n n α
h : A.IsSymm
i j : n
⊢ A j i = A i j

Tactic:
IsSymm.ext_iff.1 h i j

Premises used: Iff.mp, Matrix.IsSymm.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : Fintype n
inst_1 : NonUnitalCommSemiring α
A : Matrix n n α
⊢ (A * Aᵀ).IsSymm

Tactic:
transpose_mul _ _

Premises used: Matrix.transpose_mul, Matrix.transpose, Matrix.IsSymm
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : Fintype n
inst_1 : NonUnitalCommSemiring α
A : Matrix n n α
⊢ (Aᵀ * A).IsSymm

Tactic:
transpose_mul _ _

Premises used: Matrix.transpose_mul, Matrix.transpose, Matrix.IsSymm
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : AddCommSemigroup α
A : Matrix n n α
⊢ (A + Aᵀ).IsSymm

Tactic:
add_comm _ _

Premises used: add_comm, Matrix.transpose, Matrix.IsSymm
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : AddCommSemigroup α
A : Matrix n n α
⊢ (Aᵀ + A).IsSymm

Tactic:
add_comm _ _

Premises used: add_comm, Matrix.transpose, Matrix.IsSymm
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : Zero α
⊢ IsSymm.{u_1, u_3} (α := α) (n := n) 0

Tactic:
transpose_zero

Premises used: Matrix.transpose_zero, Matrix.IsSymm
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
⊢ IsSymm.{u_1, u_3} (α := α) (n := n) 1

Tactic:
transpose_one

Premises used: Matrix.transpose_one, Matrix.IsSymm
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : CommSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n α
h : A.IsSymm
k : ℕ
rw : (A ^ k)ᵀ = A ^ k
rw₁ : Aᵀ ^ k = A ^ k
rw₂ rw₃ : A ^ k = A ^ k
⊢ (A ^ k).IsSymm

Tactic:
rw [IsSymm, transpose_pow, h]

Premises used: Matrix.transpose_pow, Matrix.IsSymm
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
h : A.IsSymm
f : α → β
rw : (A.map f)ᵀ = A.map f
rw₁ : Aᵀ.map f = A.map f
rw₂ rw₃ : A.map f = A.map f
⊢ (A.map f).IsSymm

Tactic:
rw [IsSymm, ← transpose_map, h.eq]

Premises used: Matrix.transpose_map, Matrix.IsSymm.eq, Matrix.IsSymm
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
f : α → β
hf : Function.Injective f
rw : (A.map f)ᵀ = A.map f ↔ A.IsSymm
rw₁ : (A.map f)ᵀ = A.map f ↔ Aᵀ = A
rw₂ : Aᵀ.map f = A.map f ↔ Aᵀ = A
rw₃ rw₄ : Aᵀ = A ↔ Aᵀ = A
⊢ (A.map f).IsSymm ↔ A.IsSymm

Tactic:
rw [IsSymm, IsSymm, ← transpose_map, map_injective hf |>.eq_iff]

Premises used: Function.Injective.eq_iff, Matrix.map_injective, Matrix.transpose_map, Matrix.IsSymm
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
A : Matrix n n α
h : A.IsSymm
⊢ Aᵀ.IsSymm

Tactic:
congr_arg _ h

Premises used: congr_arg, Matrix.IsSymm
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
A : Matrix n n α
⊢ Aᵀ.IsSymm ↔ A.IsSymm

Tactic:
⟨fun h ↦ ?_, (·.transpose)⟩

Premises used: Matrix.IsSymm.transpose, Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
A : Matrix n n α
refine : ∀ (h : Aᵀ.IsSymm), A.IsSymm
⊢ Aᵀ.IsSymm ↔ A.IsSymm

Tactic:
refine ⟨fun h ↦ ?_, (·.transpose)⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
A : Matrix n n α
h : Aᵀ.IsSymm
rw : Aᵀᵀ.IsSymm
⊢ A.IsSymm

Tactic:
rw [← A.transpose_transpose]

Premises used: Matrix.transpose_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
A : Matrix n n α
h : Aᵀ.IsSymm
⊢ Aᵀᵀ.IsSymm

Tactic:
h.transpose

Premises used: Matrix.IsSymm.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
A : Matrix n n α
h : Aᵀ.IsSymm
⊢ Aᵀᵀ.IsSymm

Tactic:
exact h.transpose

Premises used: Matrix.IsSymm.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : Star α
A : Matrix n n α
h : A.IsSymm
⊢ Aᴴ.IsSymm

Tactic:
h.transpose.map _

Premises used: Matrix.IsSymm.map, Matrix.IsSymm.transpose, Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : InvolutiveStar α
A : Matrix n n α
⊢ Aᴴ.IsSymm ↔ A.IsSymm

Tactic:
⟨fun h ↦ ?_, (·.conjTranspose)⟩

Premises used: Matrix.IsSymm.conjTranspose, Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : InvolutiveStar α
A : Matrix n n α
refine : ∀ (h : Aᴴ.IsSymm), A.IsSymm
⊢ Aᴴ.IsSymm ↔ A.IsSymm

Tactic:
refine ⟨fun h ↦ ?_, (·.conjTranspose)⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : InvolutiveStar α
A : Matrix n n α
h : Aᴴ.IsSymm
rw : Aᴴᴴ.IsSymm
⊢ A.IsSymm

Tactic:
rw [← A.conjTranspose_conjTranspose]

Premises used: Matrix.conjTranspose_conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : InvolutiveStar α
A : Matrix n n α
h : Aᴴ.IsSymm
⊢ Aᴴᴴ.IsSymm

Tactic:
h.conjTranspose

Premises used: Matrix.IsSymm.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : InvolutiveStar α
A : Matrix n n α
h : Aᴴ.IsSymm
⊢ Aᴴᴴ.IsSymm

Tactic:
exact h.conjTranspose

Premises used: Matrix.IsSymm.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : Neg α
A : Matrix n n α
h : A.IsSymm
⊢ (-A).IsSymm

Tactic:
(transpose_neg _).trans (congr_arg _ h)

Premises used: Matrix.transpose_neg, congr_arg, Matrix.IsSymm, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : InvolutiveNeg α
A : Matrix n n α
⊢ (-A).IsSymm ↔ A.IsSymm

Tactic:
⟨fun h ↦ ?_, (·.neg)⟩

Premises used: Iff.intro, Matrix.IsSymm.neg
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : InvolutiveNeg α
A : Matrix n n α
refine : ∀ (h : (-A).IsSymm), A.IsSymm
⊢ (-A).IsSymm ↔ A.IsSymm

Tactic:
refine ⟨fun h ↦ ?_, (·.neg)⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : InvolutiveNeg α
A : Matrix n n α
h : (-A).IsSymm
rw : (- -A).IsSymm
⊢ A.IsSymm

Tactic:
rw [← neg_neg A]

Premises used: neg_neg
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : InvolutiveNeg α
A : Matrix n n α
h : (-A).IsSymm
⊢ (- -A).IsSymm

Tactic:
h.neg

Premises used: Matrix.IsSymm.neg
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : InvolutiveNeg α
A : Matrix n n α
h : (-A).IsSymm
⊢ (- -A).IsSymm

Tactic:
exact h.neg

Premises used: Matrix.IsSymm.neg
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
A B : Matrix n n α
inst : Add α
hA : A.IsSymm
hB : B.IsSymm
⊢ (A + B).IsSymm

Tactic:
(transpose_add _ _).trans (hA.symm ▸ hB.symm ▸ rfl)

Premises used: Matrix.transpose_add, Eq.rec, Matrix.IsSymm, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
A B : Matrix n n α
inst : Sub α
hA : A.IsSymm
hB : B.IsSymm
⊢ (A - B).IsSymm

Tactic:
(transpose_sub _ _).trans (hA.symm ▸ hB.symm ▸ rfl)

Premises used: Eq.rec, Matrix.transpose_sub, Matrix.IsSymm, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
R : Type u_5
inst : SMul R α
A : Matrix n n α
h : A.IsSymm
k : R
⊢ (k • A).IsSymm

Tactic:
(transpose_smul _ _).trans (congr_arg _ h)

Premises used: congr_arg, Matrix.transpose_smul, Matrix.IsSymm, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
R : Type u_5
inst : Monoid R
inst_1 : MulAction R α
A : Matrix n n α
k : R
inst_2 : Invertible k
⊢ (k • A).IsSymm ↔ A.IsSymm

Tactic:
⟨fun h ↦ ?_, (·.smul k)⟩

Premises used: Matrix.IsSymm.smul, Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
R : Type u_5
inst : Monoid R
inst_1 : MulAction R α
A : Matrix n n α
k : R
inst_2 : Invertible k
refine : ∀ (h : (k • A).IsSymm), A.IsSymm
⊢ (k • A).IsSymm ↔ A.IsSymm

Tactic:
refine ⟨fun h ↦ ?_, (·.smul k)⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
R : Type u_5
inst : Monoid R
inst_1 : MulAction R α
A : Matrix n n α
k : R
inst_2 : Invertible k
h : (k • A).IsSymm
rw : (@Invertible.invOf _ MulOne.toMul MulOne.toOne k _ • k • A).IsSymm
⊢ A.IsSymm

Tactic:
rw [← invOf_smul_smul k A]

Premises used: invOf_smul_smul
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
R : Type u_5
inst : Monoid R
inst_1 : MulAction R α
A : Matrix n n α
k : R
inst_2 : Invertible k
h : (k • A).IsSymm
⊢ (@Invertible.invOf _ MulOne.toMul MulOne.toOne k _ • k • A).IsSymm

Tactic:
h.smul ⅟k

Premises used: Invertible.invOf, Matrix.IsSymm.smul
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
R : Type u_5
inst : Monoid R
inst_1 : MulAction R α
A : Matrix n n α
k : R
inst_2 : Invertible k
h : (k • A).IsSymm
⊢ (@Invertible.invOf _ MulOne.toMul MulOne.toOne k _ • k • A).IsSymm

Tactic:
exact h.smul ⅟k

Premises used: Invertible.invOf, Matrix.IsSymm.smul
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix n n α
h : A.IsSymm
f : m → n
⊢ (A.submatrix f f).IsSymm

Tactic:
(transpose_submatrix _ _ _).trans (h.symm ▸ rfl)

Premises used: Matrix.transpose_submatrix, Eq.rec, Matrix.IsSymm, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix n n α
h : A.IsSymm
f : n ≃ m
rw : IsSymm.{u_1, u_4} (n := m) (A.submatrix (⇑f.symm : (a : m) → n) (⇑f.symm : (a : m) → n))
⊢ IsSymm.{u_1, u_4} (α := α) (n := m) ((Matrix.reindex f f : (a : Matrix n n α) → Matrix m m α) A)

Tactic:
rw [reindex_apply]

Premises used: Matrix.reindex_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix n n α
h : A.IsSymm
f : n ≃ m
⊢ IsSymm.{u_1, u_4} (n := m) (A.submatrix (⇑f.symm : (a : m) → n) (⇑f.symm : (a : m) → n))

Tactic:
apply submatrix h

Premises used: Matrix.IsSymm.submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix n n α
f : n ≃ m
⊢ IsSymm.{u_1, u_4} (α := α) (n := m) ((reindex f f : (a : Matrix n n α) → Matrix m m α) A) ↔ A.IsSymm

Tactic:
⟨fun h ↦ ?_, (·.reindex f)⟩

Premises used: Matrix.IsSymm.reindex, Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix n n α
f : n ≃ m
refine : ∀ (h : IsSymm.{u_1, u_4} (α := α) (n := m) ((reindex f f : (a : Matrix n n α) → Matrix m m α) A)), A.IsSymm
⊢ IsSymm.{u_1, u_4} (α := α) (n := m) ((reindex f f : (a : Matrix n n α) → Matrix m m α) A) ↔ A.IsSymm

Tactic:
refine ⟨fun h ↦ ?_, (·.reindex f)⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix n n α
f : n ≃ m
h : IsSymm.{u_1, u_4} (α := α) (n := m) ((reindex f f : (a : Matrix n n α) → Matrix m m α) A)
⊢ A.IsSymm

Tactic:
simpa using h.reindex f.symm

Premises used: Matrix.IsSymm.reindex, Equiv.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : Zero α
v : n → α
⊢ (diagonal v).IsSymm

Tactic:
diagonal_transpose _

Premises used: Matrix.diagonal_transpose, Matrix.IsSymm
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
rw : Bᵀᵀ = B
⊢ Cᵀ = B

Tactic:
rw [← hBC]
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
⊢ Bᵀᵀ = B

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
⊢ Cᵀ = B

Tactic:
have hCB : Cᵀ = B := by
    rw [← hBC]
    simp
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
rw : Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
rw₁ : Matrix.fromBlocks A Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
rw₂ : Matrix.fromBlocks A B Bᵀ Dᵀ = Matrix.fromBlocks A B C D
rw₃ : Matrix.fromBlocks A B C Dᵀ = Matrix.fromBlocks A B C D
rw₄ rw₅ : Matrix.fromBlocks A B C D = Matrix.fromBlocks A B C D
⊢ (Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D

Tactic:
rw [fromBlocks_transpose, hA, hCB, hBC, hD]

Premises used: Matrix.fromBlocks_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ (fromBlocks A B C D).IsSymm ↔ A.IsSymm ∧ Bᵀ = C ∧ Cᵀ = B ∧ D.IsSymm

Tactic:
⟨fun h =>
    ⟨(congr_arg toBlocks₁₁ h :), (congr_arg toBlocks₂₁ h :), (congr_arg toBlocks₁₂ h :),
      (congr_arg toBlocks₂₂ h :)⟩,
    fun ⟨hA, hBC, _, hD⟩ => IsSymm.fromBlocks hA hBC hD⟩

Premises used: Matrix.fromBlocks, Matrix.toBlocks₁₂, _private.0.Matrix.isSymm_fromBlocks_iff.match_1, Matrix.toBlocks₂₁, congr_arg, Matrix.toBlocks₁₁, And.intro, Iff.intro, Matrix.IsSymm, Matrix.toBlocks₂₂, Matrix.IsSymm.fromBlocks
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
rw :
  Eq (α := Matrix (m × n) (m × n) α) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A)ᵀ
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
rw₁ :
  Eq (α := Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α)
          (Aᵀ.map fun (x : Matrix n n α) ↦ xᵀ) :
        Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A : Matrix (m × n) (m × n) α) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
rw₂ :
  Eq (α := Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α)
          (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ :
        Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A : Matrix (m × n) (m × n) α) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
rw₃ : (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ = A ↔ Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
rw₄ : A = (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ ↔ Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
rw₅ rw₆ : A = (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ ↔ A = (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ
⊢ IsSymm (α := α) (n := m × n) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ

Tactic:
rw [IsSymm, transpose_comp, transpose_map, comp .. |>.injective.eq_iff, eq_comm,
    transpose_involutive _ _ |>.eq_iff]

Premises used: Matrix.comp, Matrix.transpose_involutive, Function.Injective.eq_iff, Matrix.transpose_comp, Matrix.transpose_map, eq_comm, Function.Involutive.eq_iff, Matrix.IsSymm, Equiv.injective
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
simp :
  (∀ (a : m) (b : n) (a_1 : m) (b_1 : n), A a_1 a b_1 b = A a a_1 b b_1) ↔
    ∀ (i j : m) (i' j' : n), A j i j' i' = A i j i' j'
⊢ IsSymm (α := α) (n := m × n) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    ∀ (i j : m) (i' j' : n), A j i j' i' = A i j i' j'

Tactic:
simp [IsSymm.ext_iff]

Premises used: Matrix.IsSymm.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Symmetric
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
⊢ (∀ (a : m) (b : n) (a_1 : m) (b_1 : n), A a_1 a b_1 b = A a a_1 b b_1) ↔
    ∀ (i j : m) (i' j' : n), A j i j' i' = A i j i' j'

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
m : Type u_2
n : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : SMulCommClass S R A
inst_6 : SMulCommClass S A A
inst_7 : IsScalarTower R A A
inst_8 : Fintype m
v : m → A
M : Matrix m n A
⊢ ((((vecMulBilin R S : (m → A) →ₗ[R] Matrix m n A →ₗ[S] n → A) : (a : m → A) → Matrix m n A →ₗ[S] n → A) v :
          Matrix m n A →ₗ[S] n → A) :
        (a : Matrix m n A) → n → A)
      M =
    v ᵥ* M

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.vecMul, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
m : Type u_2
n : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : SMulCommClass S R A
inst_6 : SMulCommClass S A A
inst_7 : IsScalarTower R A A
inst_8 : Fintype n
M : Matrix m n A
v : n → A
⊢ ((((mulVecBilin R S : Matrix m n A →ₗ[R] (n → A) →ₗ[S] m → A) : (a : Matrix m n A) → (n → A) →ₗ[S] m → A) M :
          (n → A) →ₗ[S] m → A) :
        (a : n → A) → m → A)
      v =
    M *ᵥ v

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl