awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : MulZeroOneClass α
M : Matrix n n α
⊢ M ⊙ 1 = diagonal M.diag

Tactic:
mul_one M.diag ▸ hadamard_diagonal M 1

Premises used: Matrix.diag, Eq.rec, mul_one, Matrix.hadamard_diagonal, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : MulZeroOneClass α
M : Matrix n n α
⊢ 1 ⊙ M = diagonal M.diag

Tactic:
one_mul M.diag ▸ diagonal_hadamard M 1

Premises used: Matrix.diag, Eq.rec, Matrix.diagonal_hadamard, OfNat.ofNat, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : MulZeroOneClass α
A : Matrix n n α
d : n → α
⊢ 1 ⊙ A = diagonal d ↔ A.diag = d

Tactic:
simpa using diagonal_hadamard_eq_diagonal_iff (A := A) (d := 1)

Premises used: Matrix.diagonal_hadamard_eq_diagonal_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : MulZeroOneClass α
A : Matrix n n α
d : n → α
⊢ A ⊙ 1 = diagonal d ↔ A.diag = d

Tactic:
simpa using hadamard_diagonal_eq_diagonal_iff (A := A) (d := 1)

Premises used: Matrix.hadamard_diagonal_eq_diagonal_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : MulZeroOneClass α
A : Matrix n n α
⊢ 1 ⊙ A = 0 ↔ A.diag = 0

Tactic:
simpa using one_hadamard_eq_diagonal_iff (A := A) (d := 0)

Premises used: Matrix.one_hadamard_eq_diagonal_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : MulZeroOneClass α
A : Matrix n n α
⊢ A ⊙ 1 = 0 ↔ A.diag = 0

Tactic:
simpa using hadamard_one_eq_diagonal_iff (A := A) (d := 0)

Premises used: Matrix.hadamard_one_eq_diagonal_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : MulZeroOneClass α
A : Matrix n n α
⊢ 1 ⊙ A = 1 ↔ A.diag = 1

Tactic:
one_hadamard_eq_diagonal_iff

Premises used: Matrix.one_hadamard_eq_diagonal_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : MulZeroOneClass α
A : Matrix n n α
⊢ A ⊙ 1 = 1 ↔ A.diag = 1

Tactic:
hadamard_one_eq_diagonal_iff

Premises used: Matrix.hadamard_one_eq_diagonal_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : MulOneClass α
A : Matrix m n α
a : ∀ (i : m) (j : n), (A ⊙ (of : (a : m → n → α) → Matrix m n α) 1) i j = A i j
⊢ A ⊙ (of : (a : m → n → α) → Matrix m n α) 1 = A

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : MulOneClass α
A : Matrix m n α
i : m
j : n
⊢ (A ⊙ (of : (a : m → n → α) → Matrix m n α) 1) i j = A i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : MulOneClass α
A : Matrix m n α
a : ∀ (i : m) (j : n), ((of : (a : m → n → α) → Matrix m n α) 1 ⊙ A) i j = A i j
⊢ (of : (a : m → n → α) → Matrix m n α) 1 ⊙ A = A

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : MulOneClass α
A : Matrix m n α
i : m
j : n
⊢ ((of : (a : m → n → α) → Matrix m n α) 1 ⊙ A) i j = A i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : Mul α
A : Matrix m n α
⊢ A ⊙ A = A ↔ ∀ (i : m) (j : n), IsIdempotentElem (A i j)

Tactic:
ext_iff.symm

Premises used: Matrix.hadamard, IsIdempotentElem, Matrix.ext_iff, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
l : Type u_5
o : Type u_6
inst : Mul α
A B : Matrix m n α
e : l → m
f : o → n
⊢ (A ⊙ B).submatrix e f = A.submatrix e f ⊙ B.submatrix e f

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.hadamard, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : Mul α
A B : Matrix m n α
⊢ (A ⊙ B)ᵀ = Aᵀ ⊙ Bᵀ

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : Mul α
inst_1 : StarMul α
A B : Matrix m n α
⊢ (A ⊙ B)ᴴ = Bᴴ ⊙ Aᴴ

Tactic:
ext fun _ _ => StarMul.star_mul _ _

Premises used: StarMul.star_mul, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : MulZeroClass α
i : m
j : n
a b : α
⊢ single i j a ⊙ single i j b = single i j (a * b)

Tactic:
ext fun _ _ => (apply_ite₂ _ _ _ _ _ _).trans (congr_arg _ <| zero_mul 0)

Premises used: apply_ite₂, MulZeroClass.toMul, MulZeroClass.zero_mul, congr_arg, And, Mul.mul, OfNat.ofNat, Eq, Matrix.ext, Eq.trans, ite
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
h : ¬(ia = ib ∧ ja = jb)
a b : α
rw : ∀ (h : ¬ia = ib ∨ ¬ja = jb) (a b : α), single ia ja a ⊙ single ib jb b = 0
⊢ single ia ja a ⊙ single ib jb b = 0

Tactic:
rw [not_and_or] at h

Premises used: not_and_or
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
h : ¬ia = ib ∨ ¬ja = jb
a b : α
inl : ¬ia = ib → single ia ja a ⊙ single ib jb b = 0
inr : ¬ja = jb → single ia ja a ⊙ single ib jb b = 0
⊢ single ia ja a ⊙ single ib jb b = 0

Tactic:
cases h
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
a b : α
h : ¬ia = ib
⊢ Eq (α := Matrix m n α)
    (((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if ia = i' ∧ ja = j' then a else 0) ⊙
      (of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if ib = i' ∧ jb = j' then b else 0)
    0

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
a b : α
h : ¬ja = jb
⊢ Eq (α := Matrix m n α)
    (((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if ia = i' ∧ ja = j' then a else 0) ⊙
      (of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if ib = i' ∧ jb = j' then b else 0)
    0

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
A B : Matrix m n α
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalSemiring α
⊢ ∑ i : m, ∑ j : n, (A ⊙ B) i j = (A * Bᵀ).trace

Tactic:
rfl

Premises used: Multiset.sum, Matrix.diag, Multiset.foldr, dotProduct, Matrix.trace, Matrix.hadamard, Matrix.transpose, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
A B : Matrix m n α
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalSemiring α
inst_3 : DecidableEq m
inst_4 : DecidableEq n
v : m → α
w : n → α
rw : v ᵥ* A ⊙ B ⬝ᵥ w = ∑ y : n, ∑ x : m, ((diagonal v * A) ⊙ (B * diagonal w)) x y
⊢ v ᵥ* A ⊙ B ⬝ᵥ w = (diagonal v * A * (B * diagonal w)ᵀ).trace

Tactic:
rw [← sum_hadamard_eq, Finset.sum_comm]

Premises used: Matrix.sum_hadamard_eq, Finset.sum_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
A B : Matrix m n α
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalSemiring α
inst_3 : DecidableEq m
inst_4 : DecidableEq n
v : m → α
w : n → α
⊢ v ᵥ* A ⊙ B ⬝ᵥ w = ∑ y : n, ∑ x : m, ((diagonal v * A) ⊙ (B * diagonal w)) x y

Tactic:
simp [dotProduct, vecMul, Finset.sum_mul, mul_assoc]

Premises used: dotProduct, mul_assoc, Matrix.vecMul, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
h : A.IsHermitian
⊢ Aᴴ = A

Tactic:
h

Premises used: Matrix.IsHermitian
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
⊢ A.IsHermitian ↔ IsSelfAdjoint A

Tactic:
Iff.rfl

Premises used: IsSelfAdjoint, Iff.rfl, Matrix.IsHermitian
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
a : ∀ (i j : n), Aᴴ i j = A i j
⊢ A.IsHermitian

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
i j : n
⊢ Aᴴ i j = A i j

Tactic:
h i j

Premises used: Matrix.transpose, Matrix.map, Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
i j : n
⊢ Aᴴ i j = A i j

Tactic:
exact h i j
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
h : A.IsHermitian
i j : n
⊢ star (A j i) = A i j

Tactic:
congr_fun (congr_fun h _) _

Premises used: Matrix.transpose, Matrix.map, congr_fun, Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
⊢ A.IsHermitian ↔ ∀ (i j : n), star (A j i) = A i j

Tactic:
⟨IsHermitian.apply, IsHermitian.ext⟩

Premises used: Matrix.IsHermitian.apply, Matrix.IsHermitian.ext, Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
β : Type u_2
n : Type u_4
inst : Star α
inst_1 : Star β
A : Matrix n n α
h : A.IsHermitian
f : α → β
hf : Function.Semiconj f star star
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).IsHermitian

Tactic:
rw [IsHermitian, ← conjTranspose_map f hf, h.eq]

Premises used: Matrix.IsHermitian.eq, Matrix.IsHermitian, Matrix.conjTranspose_map
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
β : Type u_2
n : Type u_4
inst : Star α
inst_1 : Star β
A : Matrix n n α
f : α → β
hf : Function.Semiconj f star star
hinj : Function.Injective f
rw : (A.map f)ᴴ = A.map f ↔ A.IsHermitian
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).IsHermitian ↔ A.IsHermitian

Tactic:
rw [IsHermitian, IsHermitian, ← conjTranspose_map f hf, map_injective hinj |>.eq_iff]

Premises used: Function.Injective.eq_iff, Matrix.map_injective, Matrix.IsHermitian, Matrix.conjTranspose_map
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
inst_1 : Subsingleton α
⊢ A.IsHermitian

Tactic:
.ext fun _ _ ↦ Subsingleton.elim ..

Premises used: Matrix.IsHermitian.ext, Subsingleton.elim, Star.star
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
h : A.IsHermitian
rw : (Aᵀ.map star)ᵀ = Aᵀ
⊢ Aᵀ.IsHermitian

Tactic:
rw [IsHermitian, conjTranspose, transpose_map]

Premises used: Matrix.transpose_map, Matrix.IsHermitian, Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
h : A.IsHermitian
⊢ (Aᵀ.map star)ᵀ = Aᵀ

Tactic:
congr_arg Matrix.transpose h

Premises used: congr_arg, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
h : A.IsHermitian
⊢ (Aᵀ.map star)ᵀ = Aᵀ

Tactic:
exact congr_arg Matrix.transpose h

Premises used: congr_arg, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
h : Aᵀ.IsHermitian
rw : Aᵀᵀ.IsHermitian
⊢ A.IsHermitian

Tactic:
rw [← transpose_transpose A]

Premises used: Matrix.transpose_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
h : Aᵀ.IsHermitian
⊢ Aᵀᵀ.IsHermitian

Tactic:
IsHermitian.transpose h

Premises used: Matrix.IsHermitian.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
h : Aᵀ.IsHermitian
⊢ Aᵀᵀ.IsHermitian

Tactic:
exact IsHermitian.transpose h

Premises used: Matrix.IsHermitian.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : Star α
A : Matrix n n α
h : A.IsHermitian
⊢ Aᴴ.IsHermitian

Tactic:
h.transpose.map _ fun _ => rfl

Premises used: Matrix.IsHermitian.transpose, Matrix.IsHermitian.map, Matrix.conjTranspose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : Star α
A : Matrix n n α
h : A.IsHermitian
f : m → n
⊢ (A.submatrix f f).IsHermitian

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

Premises used: Eq.rec, Matrix.conjTranspose_submatrix, Matrix.IsHermitian, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : Star α
A : Matrix n n α
e : m ≃ n
h : IsHermitian.{u_1, u_3} (n := m) (A.submatrix (⇑e : (a : m) → n) (⇑e : (a : m) → n))
⊢ A.IsHermitian

Tactic:
simpa using h.submatrix e.symm

Premises used: Matrix.IsHermitian.submatrix, Equiv.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : Star α
A : Matrix n n α
h : A.IsHermitian
f : n ≃ m
rw : IsHermitian.{u_1, u_3} (n := m) (A.submatrix (⇑f.symm : (a : m) → n) (⇑f.symm : (a : m) → n))
⊢ IsHermitian.{u_1, u_3} (α := α) (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.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : Star α
A : Matrix n n α
h : A.IsHermitian
f : n ≃ m
⊢ IsHermitian.{u_1, u_3} (n := m) (A.submatrix (⇑f.symm : (a : m) → n) (⇑f.symm : (a : m) → n))

Tactic:
apply submatrix h

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

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

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

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

Tactic:
simpa using h.reindex f.symm

Premises used: Matrix.IsHermitian.reindex, Equiv.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
inst : Star α
I : Type u_5
J : Type u_6
K : Type u_7
L : Type u_8
M : Matrix I J (Matrix K L α)
⊢ Eq (α := Matrix (J × L) (I × K) α) ((comp I J K L α : (a : Matrix I J (Matrix K L α)) → Matrix (I × K) (J × L) α) M)ᴴ
    ((comp J I L K α : (a : Matrix J I (Matrix L K α)) → Matrix (J × L) (I × K) α) (Mᵀ.map fun (x : Matrix K L α) ↦ xᴴ))

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.map, Matrix.conjTranspose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
inst : Star α
I : Type u_5
J : Type u_6
K : Type u_7
M : Matrix I J (Matrix K K α)
⊢ Eq (α := Matrix (J × K) (I × K) α) ((comp I J K K α : (a : Matrix I J (Matrix K K α)) → Matrix (I × K) (J × K) α) M)ᴴ
    ((comp J I K K α : (a : Matrix J I (Matrix K K α)) → Matrix (J × K) (I × K) α) Mᴴ)

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.map, Matrix.conjTranspose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : Star α
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.IsHermitian
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
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ᴴ : 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
rw₃ rw₄ : Aᴴ = A ↔ Aᴴ = A
⊢ IsHermitian (α := α) (n := m × n) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    A.IsHermitian

Tactic:
rw [IsHermitian, IsHermitian, conjTranspose_comp', comp .. |>.injective.eq_iff]

Premises used: Matrix.comp, Function.Injective.eq_iff, Matrix.conjTranspose_comp', Matrix.IsHermitian, Equiv.injective
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : Star α
A : Matrix m m (Matrix n n α)
simp :
  (∀ (a : m) (b : n) (a_1 : m) (b_1 : n), star (A a_1 a b_1 b) = A a a_1 b b_1) ↔
    ∀ (i j : m) (i' j' : n), star (A j i j' i') = A i j i' j'
⊢ IsHermitian (α := α) (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), star (A j i j' i') = A i j i' j'

Tactic:
simp [IsHermitian.ext_iff]

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

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : InvolutiveStar α
A : Matrix n n α
⊢ Aᴴ.IsHermitian ↔ A.IsHermitian

Tactic:
IsSelfAdjoint.star_iff

Premises used: IsSelfAdjoint, IsSelfAdjoint.star_iff, Matrix.IsHermitian
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
rw : Bᴴᴴ = B
rw₁ rw₂ : B = B
⊢ Cᴴ = B

Tactic:
rw [← hBC, conjTranspose_conjTranspose]

Premises used: Matrix.conjTranspose_conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
⊢ Cᴴ = B

Tactic:
have hCB : Cᴴ = B := by rw [← hBC, conjTranspose_conjTranspose]
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
hCB : Cᴴ = B
rw : Matrix.fromBlocks Aᴴ Cᴴ Bᴴ Dᴴ = Matrix.fromBlocks A B C D
rw₁ : Matrix.fromBlocks Aᴴ Cᴴ C Dᴴ = Matrix.fromBlocks A B C D
rw₂ : Matrix.fromBlocks Aᴴ B C 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_conjTranspose, hBC, hCB, hA, hD]

Premises used: Matrix.fromBlocks_conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ (fromBlocks A B C D).IsHermitian ↔ A.IsHermitian ∧ Bᴴ = C ∧ Cᴴ = B ∧ D.IsHermitian

Tactic:
⟨fun h =>
    ⟨congr_arg toBlocks₁₁ h, congr_arg toBlocks₂₁ h, congr_arg toBlocks₁₂ h,
      congr_arg toBlocks₂₂ h⟩,
    fun ⟨hA, hBC, _hCB, hD⟩ => IsHermitian.fromBlocks hA hBC hD⟩

Premises used: Matrix.fromBlocks, Matrix.toBlocks₁₂, Matrix.toBlocks₂₁, congr_arg, Matrix.toBlocks₁₁, _private.0.Matrix.isHermitian_fromBlocks_iff.match_1, And.intro, Iff.intro, Matrix.toBlocks₂₂, Matrix.IsHermitian, Matrix.IsHermitian.fromBlocks
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : CommMonoid α
inst_1 : StarMul α
A B : Matrix n n α
hA : A.IsHermitian
hB : B.IsHermitian
rw : (A ⊙ B)ᴴ = A ⊙ B
rw₁ : Bᴴ ⊙ Aᴴ = A ⊙ B
rw₂ : B ⊙ Aᴴ = A ⊙ B
rw₃ : B ⊙ A = A ⊙ B
rw₄ rw₅ : A ⊙ B = A ⊙ B
⊢ (A ⊙ B).IsHermitian

Tactic:
rw [IsHermitian, conjTranspose_hadamard, hB.eq, hA.eq, hadamard_comm]

Premises used: Matrix.IsHermitian.eq, Matrix.hadamard_comm, Matrix.IsHermitian, Matrix.conjTranspose_hadamard
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : AddMonoid α
inst_1 : StarAddMonoid α
inst_2 : DecidableEq n
v : n → α
h : IsSelfAdjoint v
⊢ (diagonal v).IsHermitian

Tactic:
(-- TODO: add a `pi.has_trivial_star` instance and remove the `funext`
        diagonal_conjTranspose v).trans <| congr_arg _ h

Premises used: Matrix.diagonal_conjTranspose, congr_arg, Matrix.IsHermitian, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : AddMonoid α
inst_1 : StarAddMonoid α
inst_2 : DecidableEq n
d : n → α
⊢ (diagonal d).IsHermitian ↔ ∀ (i : n), IsSelfAdjoint (d i)

Tactic:
simp [isSelfAdjoint_iff, IsHermitian, conjTranspose, diagonal_transpose, diagonal_map]

Premises used: Matrix.diagonal_transpose, Matrix.IsHermitian, isSelfAdjoint_iff, Matrix.diagonal_map, Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : AddMonoid α
inst_1 : StarAddMonoid α
inst_2 : DecidableEq n
p : n → Type u_5
M : (i : n) → Matrix.{u_5, u_5, u_1} (p i) (p i) α
⊢ (blockDiagonal' (m' := p) (n' := p) M).IsHermitian ↔ ∀ (i : n), (M i).IsHermitian

Tactic:
grind [IsHermitian, blockDiagonal'_conjTranspose, blockDiagonal'_inj]

Premises used: Matrix.blockDiagonal'_inj, Matrix.IsHermitian, Matrix.blockDiagonal'_conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : AddMonoid α
inst_1 : StarAddMonoid α
inst_2 : DecidableEq n
M : n → Matrix m m α
⊢ (blockDiagonal M).IsHermitian ↔ ∀ (i : n), (M i).IsHermitian

Tactic:
simpa [IsHermitian] using isHermitian_blockDiagonal'_iff

Premises used: Matrix.isHermitian_blockDiagonal'_iff, Matrix.IsHermitian
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : AddMonoid α
inst_1 : StarAddMonoid α
inst_2 : TrivialStar α
inst_3 : DecidableEq n
v : n → α
⊢ (diagonal v).IsHermitian

Tactic:
isHermitian_diagonal_of_self_adjoint _ (IsSelfAdjoint.all _)

Premises used: Matrix.isHermitian_diagonal_of_self_adjoint, IsSelfAdjoint.all
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : AddMonoid α
inst_1 : StarAddMonoid α
⊢ IsHermitian.{u_1, u_4} (α := α) (n := n) 0

Tactic:
IsSelfAdjoint.zero _

Premises used: IsSelfAdjoint, IsSelfAdjoint.zero, Matrix.IsHermitian
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : AddMonoid α
inst_1 : StarAddMonoid α
A B : Matrix n n α
hA : A.IsHermitian
hB : B.IsHermitian
⊢ (A + B).IsHermitian

Tactic:
IsSelfAdjoint.add hA hB

Premises used: IsSelfAdjoint, IsSelfAdjoint.add, Matrix.IsHermitian
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : AddCommMonoid α
inst_1 : StarAddMonoid α
A : Matrix n n α
⊢ (A + Aᴴ).IsHermitian

Tactic:
IsSelfAdjoint.add_star_self A

Premises used: IsSelfAdjoint, IsSelfAdjoint.add_star_self, Matrix.IsHermitian
-- Module: Mathlib.LinearAlgebra.Matrix.Hermitian
Goal:
α : Type u_1
n : Type u_4
inst : AddCommMonoid α
inst_1 : StarAddMonoid α
A : Matrix n n α
⊢ (Aᴴ + A).IsHermitian

Tactic:
IsSelfAdjoint.star_add_self A

Premises used: IsSelfAdjoint, IsSelfAdjoint.star_add_self, Matrix.IsHermitian