-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
theorem isHermitian_iff_isSymmetric [Fintype n] [DecidableEq n] {A : Matrix n n α} :
    IsHermitian A ↔ A.toEuclideanLin.IsSymmetric

Proof state:
case mpr.a
α : Type u_1
n : Type u_4
inst✝² : RCLike α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : ∀ (x₁ x₂ : n → α), star x₁ ᵥ* Aᴴ ⬝ᵥ x₂ = star x₁ ᵥ* A ⬝ᵥ x₂
i j : n
⊢ Aᴴ i j = A i j

Tactic:
simpa only [(Pi.single_star i 1).symm, ← star_mulVec, mul_one, dotProduct_single,
  single_one_vecMul, star_one] using h (Pi.single i 1) (Pi.single j 1)

Result:
no goals

Proof state:
case mp
α : Type u_1
n : Type u_4
inst✝² : RCLike α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ A.IsHermitian → ∀ (x₁ x₂ : n → α), star x₁ ᵥ* Aᴴ ⬝ᵥ x₂ = star x₁ ᵥ* A ⬝ᵥ x₂

Tactic:
rintro (h : Aᴴ = A) x y

Result:
case mp
α : Type u_1
n : Type u_4
inst✝² : RCLike α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : Aᴴ = A
x y : n → α
⊢ star x ᵥ* Aᴴ ⬝ᵥ y = star x ᵥ* A ⬝ᵥ y

Proof state:
α : Type u_1
n : Type u_4
inst✝² : RCLike α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ A.IsHermitian ↔ (toEuclideanLin A).IsSymmetric

Tactic:
rw [LinearMap.IsSymmetric, (WithLp.equiv 2 (n → α)).symm.surjective.forall₂]

Result:
α : Type u_1
n : Type u_4
inst✝² : RCLike α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ A.IsHermitian ↔
    ∀ (x₁ x₂ : n → α),
      inner ((toEuclideanLin A) ((WithLp.equiv 2 (n → α)).symm x₁)) ((WithLp.equiv 2 (n → α)).symm x₂) =
        inner ((WithLp.equiv 2 (n → α)).symm x₁) ((toEuclideanLin A) ((WithLp.equiv 2 (n → α)).symm x₂))

Proof state:
case mp
α : Type u_1
n : Type u_4
inst✝² : RCLike α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : Aᴴ = A
x y : n → α
⊢ star x ᵥ* Aᴴ ⬝ᵥ y = star x ᵥ* A ⬝ᵥ y

Tactic:
rw [h]

Result:
no goals

Proof state:
case mpr
α : Type u_1
n : Type u_4
inst✝² : RCLike α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : ∀ (x₁ x₂ : n → α), star x₁ ᵥ* Aᴴ ⬝ᵥ x₂ = star x₁ ᵥ* A ⬝ᵥ x₂
⊢ A.IsHermitian

Tactic:
ext i j

Result:
case mpr.a
α : Type u_1
n : Type u_4
inst✝² : RCLike α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : ∀ (x₁ x₂ : n → α), star x₁ ᵥ* Aᴴ ⬝ᵥ x₂ = star x₁ ᵥ* A ⬝ᵥ x₂
i j : n
⊢ Aᴴ i j = A i j

Proof state:
α : Type u_1
n : Type u_4
inst✝² : RCLike α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ A.IsHermitian ↔
    ∀ (x₁ x₂ : n → α),
      inner ((toEuclideanLin A) ((WithLp.equiv 2 (n → α)).symm x₁)) ((WithLp.equiv 2 (n → α)).symm x₂) =
        inner ((WithLp.equiv 2 (n → α)).symm x₁) ((toEuclideanLin A) ((WithLp.equiv 2 (n → α)).symm x₂))

Tactic:
simp only [toEuclideanLin_piLp_equiv_symm, EuclideanSpace.inner_piLp_equiv_symm, toLin'_apply,
  star_mulVec, dotProduct_mulVec]

Result:
α : Type u_1
n : Type u_4
inst✝² : RCLike α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ A.IsHermitian ↔ ∀ (x₁ x₂ : n → α), star x₁ ᵥ* Aᴴ ⬝ᵥ x₂ = star x₁ ᵥ* A ⬝ᵥ x₂

Proof state:
case mpr
α : Type u_1
n : Type u_4
inst✝² : RCLike α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ (∀ (x₁ x₂ : n → α), star x₁ ᵥ* Aᴴ ⬝ᵥ x₂ = star x₁ ᵥ* A ⬝ᵥ x₂) → A.IsHermitian

Tactic:
intro h

Result:
case mpr
α : Type u_1
n : Type u_4
inst✝² : RCLike α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : ∀ (x₁ x₂ : n → α), star x₁ ᵥ* Aᴴ ⬝ᵥ x₂ = star x₁ ᵥ* A ⬝ᵥ x₂
⊢ A.IsHermitian

Proof state:
α : Type u_1
n : Type u_4
inst✝² : RCLike α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ A.IsHermitian ↔ ∀ (x₁ x₂ : n → α), star x₁ ᵥ* Aᴴ ⬝ᵥ x₂ = star x₁ ᵥ* A ⬝ᵥ x₂

Tactic:
constructor

Result:
case mp
α : Type u_1
n : Type u_4
inst✝² : RCLike α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ A.IsHermitian → ∀ (x₁ x₂ : n → α), star x₁ ᵥ* Aᴴ ⬝ᵥ x₂ = star x₁ ᵥ* A ⬝ᵥ x₂

case mpr
α : Type u_1
n : Type u_4
inst✝² : RCLike α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ (∀ (x₁ x₂ : n → α), star x₁ ᵥ* Aᴴ ⬝ᵥ x₂ = star x₁ ᵥ* A ⬝ᵥ x₂) → A.IsHermitian