-- 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
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 ∧ star v ⬝ᵥ B *ᵥ v = 0

Tactic:
refine ⟨le_antisymm ?_ (hA.2 v), le_antisymm ?_ (hB.2 v)⟩

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 ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v = 0
⊢ star v ⬝ᵥ A *ᵥ v ≤ 0

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

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 : 0 = ↑t * (star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v)
⊢ False

Tactic:
replace h_sum : star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v = 0 := by
  rw [eq_comm, ← mul_zero (t : 𝕜)] at h_sum
  exact mul_left_cancel₀ (RCLike.ofReal_ne_zero.mpr ht) h_sum

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
⊢ 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
⊢ t • star v ⬝ᵥ A *ᵥ v + star (t • v) ⬝ᵥ B *ᵥ v = t • star v ⬝ᵥ A *ᵥ v + t • star v ⬝ᵥ B *ᵥ v

Tactic:
congr 2 with i

Result:
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

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 : star v ⬝ᵥ (A - B) *ᵥ v = 0
⊢ False

Tactic:
rw [hv', dotProduct_smul, RCLike.real_smul_eq_coe_mul, ← mul_zero ↑t] at aux

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 : ↑t * star v ⬝ᵥ v = ↑t * 0
⊢ 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 : 0 = ↑t * (star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v)
⊢ star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v = 0

Tactic:
rw [eq_comm, ← mul_zero (t : 𝕜)] at h_sum

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 : ↑t * (star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v) = ↑t * 0
⊢ star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ 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 ^ 2 - B ^ 2) *ᵥ v = star v ⬝ᵥ A *ᵥ (A - B) *ᵥ v + star v ⬝ᵥ (A - B) *ᵥ B *ᵥ v

Tactic:
rw [mulVec_mulVec, mulVec_mulVec, ← dotProduct_add, ← add_mulVec, mul_sub, sub_mul,
  add_sub, sub_add_cancel, pow_two, pow_two]

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 : ↑t * (star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v) = ↑t * 0
⊢ star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v = 0

Tactic:
exact mul_left_cancel₀ (RCLike.ofReal_ne_zero.mpr ht) h_sum

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 ⬝ᵥ B *ᵥ v = -(star v ⬝ᵥ A *ᵥ v)
⊢ star v ⬝ᵥ A *ᵥ v ≤ 0

Tactic:
simpa only [h_sum, neg_nonneg] using hB.2 v

Result:
no goals