-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
lemma eq_of_sq_eq_sq {B : Matrix n n 𝕜} (hB : PosSemidef B) (hAB : A ^ 2 = B ^ 2) : A = B

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
⊢ False

Tactic:
let ⟨v, t, ht, hv, hv'⟩ := (hA.1.sub hB.1).exists_eigenvector_of_ne_zero (sub_ne_zero.mpr h_ne)

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
v : n → 𝕜
t : ℝ
ht : t ≠ 0
hv : v ≠ 0
hv' : (A - B) *ᵥ v = t • v
⊢ False

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
v : n → 𝕜
t : ℝ
ht : t ≠ 0
hv : v ≠ 0
hv' : (A - B) *ᵥ v = t • v
⊢ 0 = star v ⬝ᵥ (A ^ 2 - B ^ 2) *ᵥ v

Tactic:
rw [hAB, sub_self, zero_mulVec, dotProduct_zero]

Result:
no goals

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
v : n → 𝕜
t : ℝ
ht : t ≠ 0
hv : v ≠ 0
hv' : (A - B) *ᵥ v = t • v
h_sum : star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v = 0
h_van : star v ⬝ᵥ A *ᵥ v = 0 ∧ star v ⬝ᵥ B *ᵥ v = 0
⊢ False

Tactic:
have aux : star v ⬝ᵥ (A - B) *ᵥ v = 0 := by
  rw [sub_mulVec, dotProduct_sub, h_van.1, h_van.2, sub_zero]

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
v : n → 𝕜
t : ℝ
ht : t ≠ 0
hv : v ≠ 0
hv' : (A - B) *ᵥ v = t • v
h_sum : star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v = 0
h_van : star v ⬝ᵥ A *ᵥ v = 0 ∧ star v ⬝ᵥ B *ᵥ v = 0
aux : star v ⬝ᵥ (A - B) *ᵥ v = 0
⊢ False

Proof state:
case e_a.e_v.h
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
v : n → 𝕜
t : ℝ
ht : t ≠ 0
hv : v ≠ 0
hv' : (A - B) *ᵥ v = t • v
i : n
⊢ star (t • v) i = (t • star v) i

Tactic:
simp only [Pi.star_apply, Pi.smul_apply, RCLike.real_smul_eq_coe_mul, star_mul',
  RCLike.star_def, RCLike.conj_ofReal]

Result:
no goals

Proof state:
case refine_1
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
v : n → 𝕜
t : ℝ
ht : t ≠ 0
hv : v ≠ 0
hv' : (A - B) *ᵥ v = t • v
h_sum : star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v = 0
⊢ star v ⬝ᵥ A *ᵥ v ≤ 0

Tactic:
rw [add_comm, add_eq_zero_iff_eq_neg] at h_sum

Result:
case refine_1
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
v : n → 𝕜
t : ℝ
ht : t ≠ 0
hv : v ≠ 0
hv' : (A - B) *ᵥ v = t • v
h_sum : star v ⬝ᵥ B *ᵥ v = -(star v ⬝ᵥ A *ᵥ v)
⊢ star v ⬝ᵥ A *ᵥ v ≤ 0

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
v : n → 𝕜
t : ℝ
ht : t ≠ 0
hv : v ≠ 0
hv' : (A - B) *ᵥ v = t • v
⊢ star v ⬝ᵥ A *ᵥ (A - B) *ᵥ v + star v ⬝ᵥ (A - B) *ᵥ B *ᵥ v = ↑t * star v ⬝ᵥ A *ᵥ v + star v ᵥ* (A - B)ᴴ ⬝ᵥ B *ᵥ v

Tactic:
rw [hv', mulVec_smul, dotProduct_smul, RCLike.real_smul_eq_coe_mul,
  dotProduct_mulVec _ (A - B), hA.1.sub hB.1]

Result:
no goals

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
v : n → 𝕜
t : ℝ
ht : t ≠ 0
hv : v ≠ 0
hv' : (A - B) *ᵥ v = t • v
h_sum : star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v = 0
h_van : star v ⬝ᵥ A *ᵥ v = 0 ∧ star v ⬝ᵥ B *ᵥ v = 0
aux : ↑t * star v ⬝ᵥ v = ↑t * 0
⊢ False

Tactic:
exact hv <| dotProduct_star_self_eq_zero.mp <| mul_left_cancel₀
  (RCLike.ofReal_ne_zero.mpr ht) aux

Result:
no goals

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
⊢ A = B

Tactic:
by_contra h_ne

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
⊢ False

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
v : n → 𝕜
t : ℝ
ht : t ≠ 0
hv : v ≠ 0
hv' : (A - B) *ᵥ v = t • v
h_sum : star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v = 0
h_van : star v ⬝ᵥ A *ᵥ v = 0 ∧ star v ⬝ᵥ B *ᵥ v = 0
⊢ star v ⬝ᵥ (A - B) *ᵥ v = 0

Tactic:
rw [sub_mulVec, dotProduct_sub, h_van.1, h_van.2, sub_zero]

Result:
no goals

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
v : n → 𝕜
t : ℝ
ht : t ≠ 0
hv : v ≠ 0
hv' : (A - B) *ᵥ v = t • v
⊢ False

Tactic:
have h_sum : 0 = t * (star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v) := calc
  0 = star v ⬝ᵥ (A ^ 2 - B ^ 2) *ᵥ v := by rw [hAB, sub_self, zero_mulVec, dotProduct_zero]
  _ = star v ⬝ᵥ A *ᵥ (A - B) *ᵥ v + star v ⬝ᵥ (A - B) *ᵥ B *ᵥ v := by
    rw [mulVec_mulVec, mulVec_mulVec, ← dotProduct_add, ← add_mulVec, mul_sub, sub_mul,
      add_sub, sub_add_cancel, pow_two, pow_two]
  _ = t * (star v ⬝ᵥ A *ᵥ v) + (star v) ᵥ* (A - B)ᴴ ⬝ᵥ B *ᵥ v := by
    rw [hv', mulVec_smul, dotProduct_smul, RCLike.real_smul_eq_coe_mul,
      dotProduct_mulVec _ (A - B), hA.1.sub hB.1]
  _ = t * (star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v) := by
    simp_rw [← star_mulVec, hv', mul_add, ← RCLike.real_smul_eq_coe_mul, ← smul_dotProduct]
    congr 2 with i
    simp only [Pi.star_apply, Pi.smul_apply, RCLike.real_smul_eq_coe_mul, star_mul',
      RCLike.star_def, RCLike.conj_ofReal]

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
v : n → 𝕜
t : ℝ
ht : t ≠ 0
hv : v ≠ 0
hv' : (A - B) *ᵥ v = t • v
h_sum : 0 = ↑t * (star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v)
⊢ False

Proof state:
case refine_2
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
v : n → 𝕜
t : ℝ
ht : t ≠ 0
hv : v ≠ 0
hv' : (A - B) *ᵥ v = t • v
h_sum : star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v = 0
⊢ star v ⬝ᵥ B *ᵥ v ≤ 0

Tactic:
simpa only [add_eq_zero_iff_eq_neg.mp h_sum, neg_nonneg] using hA.2 v

Result:
no goals

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
v : n → 𝕜
t : ℝ
ht : t ≠ 0
hv : v ≠ 0
hv' : (A - B) *ᵥ v = t • v
⊢ ↑t * star v ⬝ᵥ A *ᵥ v + star v ᵥ* (A - B)ᴴ ⬝ᵥ B *ᵥ v = ↑t * (star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v)

Tactic:
simp_rw [← star_mulVec, hv', mul_add, ← RCLike.real_smul_eq_coe_mul, ← smul_dotProduct]

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B ^ 2
h_ne : ¬A = B
v : n → 𝕜
t : ℝ
ht : t ≠ 0
hv : v ≠ 0
hv' : (A - B) *ᵥ v = t • v
⊢ t • star v ⬝ᵥ A *ᵥ v + star (t • v) ⬝ᵥ B *ᵥ v = t • star v ⬝ᵥ A *ᵥ v + t • star v ⬝ᵥ B *ᵥ v